Merge branch 'master' into dagur/RefactorLightProfiniteLimits

Author: dagurtomas

.github/workflows/lean4checker.yml

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.9.0
+          git checkout v4.10.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

Mathlib/Algebra/Group/Units.lean

@@ -134,7 +134,7 @@ theorem eq_iff {a b : αˣ} : (a : α) = b ↔ a = b :=
   ext.eq_iff
 
 @[to_additive]
-theorem ext_iff {a b : αˣ} : a = b ↔ (a : α) = b :=
+protected theorem ext_iff {a b : αˣ} : a = b ↔ (a : α) = b :=
   eq_iff.symm
 
 /-- Units have decidable equality if the base `Monoid` has decidable equality. -/

Mathlib/Algebra/Homology/DerivedCategory/Ext.lean

@@ -129,7 +129,7 @@ lemma comp_hom {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a +
 lemma ext {n : ℕ} {α β : Ext X Y n} (h : α.hom = β.hom) : α = β :=
   homEquiv.injective h
 
-lemma ext_iff {n : ℕ} {α β : Ext X Y n} : α = β ↔ α.hom = β.hom :=
+protected lemma ext_iff {n : ℕ} {α β : Ext X Y n} : α = β ↔ α.hom = β.hom :=
   ⟨fun h ↦ by rw [h], ext⟩
 
 end

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -604,7 +604,7 @@ instance : Coe (Cocycle F G n) (Cochain F G n) where
 lemma ext (z₁ z₂ : Cocycle F G n) (h : (z₁ : Cochain F G n) = z₂) : z₁ = z₂ :=
   Subtype.ext h
 
-lemma ext_iff (z₁ z₂ : Cocycle F G n) : z₁ = z₂ ↔ (z₁ : Cochain F G n) = z₂ :=
+protected lemma ext_iff (z₁ z₂ : Cocycle F G n) : z₁ = z₂ ↔ (z₁ : Cochain F G n) = z₂ :=
   Subtype.ext_iff
 
 instance : SMul R (Cocycle F G n) where

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -208,7 +208,7 @@ variable {M}
 @[ext] lemma ext {χ₁ χ₂ : Weight R L M} (h : ∀ x, χ₁ x = χ₂ x) : χ₁ = χ₂ := by
   cases' χ₁ with f₁ _; cases' χ₂ with f₂ _; aesop
 
-lemma ext_iff {χ₁ χ₂ : Weight R L M} : (χ₁ : L → R) = χ₂ ↔ χ₁ = χ₂ := by aesop
+protected lemma ext_iff {χ₁ χ₂ : Weight R L M} : χ₁ = χ₂ ↔ (χ₁ : L → R) = χ₂ := by aesop
 
 lemma exists_ne_zero (χ : Weight R L M) :
     ∃ x ∈ weightSpace M χ, x ≠ 0 := by
@@ -236,7 +236,7 @@ def IsZero (χ : Weight R L M) := (χ : L → R) = 0
 @[simp] lemma coe_eq_zero_iff (χ : Weight R L M) : (χ : L → R) = 0 ↔ χ.IsZero := Iff.rfl
 
 lemma isZero_iff_eq_zero [Nontrivial (weightSpace M (0 : L → R))] {χ : Weight R L M} :
-    χ.IsZero ↔ χ = 0 := ext_iff (χ₂ := 0)
+    χ.IsZero ↔ χ = 0 := Weight.ext_iff (χ₂ := 0).symm
 
 lemma isZero_zero [Nontrivial (weightSpace M (0 : L → R))] : IsZero (0 : Weight R L M) := rfl
 

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -322,7 +322,7 @@ protected theorem congr_arg {x x' : M} : x = x' → f x = f x' :=
 protected theorem congr_fun (h : f = g) (x : M) : f x = g x :=
   DFunLike.congr_fun h x
 
-theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 @[simp]

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -529,7 +529,7 @@ theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) :
 theorem ext (p q : MvPolynomial σ R) : (∀ m, coeff m p = coeff m q) → p = q :=
   Finsupp.ext
 
-theorem ext_iff (p q : MvPolynomial σ R) : p = q ↔ ∀ m, coeff m p = coeff m q :=
+protected theorem ext_iff (p q : MvPolynomial σ R) : p = q ↔ ∀ m, coeff m p = coeff m q :=
   ⟨fun h m => by rw [h], ext p q⟩
 
 @[simp]

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -155,7 +155,7 @@ variable (f : α →ₙ+* β) {x y : α}
 theorem ext ⦃f g : α →ₙ+* β⦄ : (∀ x, f x = g x) → f = g :=
   DFunLike.ext _ _
 
-theorem ext_iff {f g : α →ₙ+* β} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : α →ₙ+* β} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 @[simp]
@@ -455,7 +455,7 @@ theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
 theorem ext ⦃f g : α →+* β⦄ : (∀ x, f x = g x) → f = g :=
   DFunLike.ext _ _
 
-theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 @[simp]

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -112,7 +112,7 @@ def metricSpaceAux : MetricSpace ℍ where
   dist_comm := UpperHalfPlane.dist_comm
   dist_triangle := UpperHalfPlane.dist_triangle
   eq_of_dist_eq_zero {z w} h := by
-    simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_le, ext_iff] using h
+    simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_le, Set.ext_iff] using h
 
 open Complex
 

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -104,7 +104,7 @@ theorem coe_inj_iff : f = g ↔ (f : V₁ → V₂) = g :=
 theorem ext (H : ∀ x, f x = g x) : f = g :=
   coe_inj <| funext H
 
-theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
   ⟨by rintro rfl x; rfl, ext⟩
 
 variable (f g)

Mathlib/Data/Complex/Basic.lean

@@ -57,7 +57,7 @@ theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
 
 attribute [local ext] Complex.ext
 
-theorem ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im :=
+protected theorem ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im :=
   ⟨fun H => by simp [H], fun h => ext h.1 h.2⟩
 
 theorem re_surjective : Surjective re := fun x => ⟨⟨x, 0⟩, rfl⟩

Mathlib/Data/Finsupp/Defs.lean

@@ -212,7 +212,7 @@ noncomputable def _root_.Equiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →
 theorem unique_ext [Unique α] {f g : α →₀ M} (h : f default = g default) : f = g :=
   ext fun a => by rwa [Unique.eq_default a]
 
-theorem unique_ext_iff [Unique α] {f g : α →₀ M} : f = g ↔ f default = g default :=
+protected theorem unique_ext_iff [Unique α] {f g : α →₀ M} : f = g ↔ f default = g default :=
   ⟨fun h => h ▸ rfl, unique_ext⟩
 
 end Basic

Mathlib/Data/List/AList.lean

@@ -60,7 +60,7 @@ namespace AList
 theorem ext : ∀ {s t : AList β}, s.entries = t.entries → s = t
   | ⟨l₁, h₁⟩, ⟨l₂, _⟩, H => by congr
 
-theorem ext_iff {s t : AList β} : s = t ↔ s.entries = t.entries :=
+protected theorem ext_iff {s t : AList β} : s = t ↔ s.entries = t.entries :=
   ⟨congr_arg _, ext⟩
 
 instance [DecidableEq α] [∀ a, DecidableEq (β a)] : DecidableEq (AList β) := fun xs ys => by

Mathlib/Data/Prod/Basic.lean

@@ -98,7 +98,7 @@ lemma mk_inj_left {a : α} {b₁ b₂ : β} : (a, b₁) = (a, b₂) ↔ b₁ = b
 
 lemma mk_inj_right {a₁ a₂ : α} {b : β} : (a₁, b) = (a₂, b) ↔ a₁ = a₂ := (mk.inj_right _).eq_iff
 
-theorem ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 := by
+protected theorem ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 := by
   rw [mk.inj_iff]
 
 theorem map_def {f : α → γ} {g : β → δ} : Prod.map f g = fun p : α × β ↦ (f p.1, g p.2) :=

Mathlib/Data/Set/Basic.lean

@@ -187,7 +187,7 @@ variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a b : α} {s s
 instance : Inhabited (Set α) :=
   ⟨∅⟩
 
-theorem ext_iff {s t : Set α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
+protected theorem ext_iff {s t : Set α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
   ⟨fun h x => by rw [h], ext⟩
 
 @[trans]

Mathlib/Data/Sigma/Basic.lean

@@ -61,7 +61,7 @@ theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
 theorem eta : ∀ x : Σa, β a, Sigma.mk x.1 x.2 = x
   | ⟨_, _⟩ => rfl
 
-theorem ext_iff {x₀ x₁ : Sigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ HEq x₀.2 x₁.2 := by
+protected theorem ext_iff {x₀ x₁ : Sigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ HEq x₀.2 x₁.2 := by
   cases x₀; cases x₁; exact Sigma.mk.inj_iff
 
 /-- A version of `Iff.mp Sigma.ext_iff` for functions from a nonempty type to a sigma type. -/

Mathlib/Data/Subtype.lean

@@ -59,13 +59,13 @@ protected theorem exists' {q : ∀ x, p x → Prop} : (∃ x h, q x h) ↔ ∃ x
 protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
-theorem ext_iff {a1 a2 : { x // p x }} : a1 = a2 ↔ (a1 : α) = (a2 : α) :=
+protected theorem ext_iff {a1 a2 : { x // p x }} : a1 = a2 ↔ (a1 : α) = (a2 : α) :=
   ⟨congr_arg _, Subtype.ext⟩
 
 theorem heq_iff_coe_eq (h : ∀ x, p x ↔ q x) {a1 : { x // p x }} {a2 : { x // q x }} :
     HEq a1 a2 ↔ (a1 : α) = (a2 : α) :=
   Eq.rec (motive := fun (pp : (α → Prop)) _ ↦ ∀ a2' : {x // pp x}, HEq a1 a2' ↔ (a1 : α) = (a2' : α))
-         (fun _ ↦ heq_iff_eq.trans ext_iff) (funext <| fun x ↦ propext (h x)) a2
+         (fun _ ↦ heq_iff_eq.trans Subtype.ext_iff) (funext <| fun x ↦ propext (h x)) a2
 
 lemma heq_iff_coe_heq {α β : Sort _} {p : α → Prop} {q : β → Prop} {a : {x // p x}}
     {b : {y // q y}} (h : α = β) (h' : HEq p q) : HEq a b ↔ HEq (a : α) (b : β) := by

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -161,7 +161,7 @@ theorem map_one_add (x : ℝ) : f (1 + x) = 1 + f x := by rw [add_comm, map_add_
 theorem ext ⦃f g : CircleDeg1Lift⦄ (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
-theorem ext_iff {f g : CircleDeg1Lift} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : CircleDeg1Lift} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 instance : Monoid CircleDeg1Lift where

Mathlib/FieldTheory/IntermediateField.lean

@@ -603,13 +603,68 @@ end RestrictScalars
 /-- This was formerly an instance called `lift2_alg`, but an instance above already provides it. -/
 example {F : IntermediateField K L} {E : IntermediateField F L} : Algebra K E := by infer_instance
 
+end Tower
+
+end IntermediateField
+
 section ExtendScalars
 
+namespace Subfield
+
+variable {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') {x : L}
+
+/-- If `F ≤ E` are two subfields of `L`, then `E` is also an intermediate field of
+`L / F`. It can be viewed as an inverse to `IntermediateField.toSubfield`. -/
+def extendScalars : IntermediateField F L := E.toIntermediateField fun ⟨_, hf⟩ ↦ h hf
+
+@[simp]
+theorem coe_extendScalars : (extendScalars h : Set L) = (E : Set L) := rfl
+
+@[simp]
+theorem extendScalars_toSubfield : (extendScalars h).toSubfield = E := SetLike.coe_injective rfl
+
+@[simp]
+theorem mem_extendScalars : x ∈ extendScalars h ↔ x ∈ E := Iff.rfl
+
+theorem extendScalars_le_extendScalars_iff : extendScalars h ≤ extendScalars h' ↔ E ≤ E' := Iff.rfl
+
+theorem extendScalars_le_iff (E' : IntermediateField F L) :
+    extendScalars h ≤ E' ↔ E ≤ E'.toSubfield := Iff.rfl
+
+theorem le_extendScalars_iff (E' : IntermediateField F L) :
+    E' ≤ extendScalars h ↔ E'.toSubfield ≤ E := Iff.rfl
+
+variable (F)
+
+/-- `Subfield.extendScalars.orderIso` bundles `Subfield.extendScalars`
+into an order isomorphism from
+`{ E : Subfield L // F ≤ E }` to `IntermediateField F L`. Its inverse is
+`IntermediateField.toSubfield`. -/
+@[simps]
+def extendScalars.orderIso :
+    { E : Subfield L // F ≤ E } ≃o IntermediateField F L where
+  toFun E := extendScalars E.2
+  invFun E := ⟨E.toSubfield, fun x hx ↦ E.algebraMap_mem ⟨x, hx⟩⟩
+  left_inv E := rfl
+  right_inv E := rfl
+  map_rel_iff' {E E'} := by
+    simp only [Equiv.coe_fn_mk]
+    exact extendScalars_le_extendScalars_iff _ _
+
+theorem extendScalars_injective :
+    Function.Injective fun E : { E : Subfield L // F ≤ E } ↦ extendScalars E.2 :=
+  (extendScalars.orderIso F).injective
+
+end Subfield
+
+namespace IntermediateField
+
 variable {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E') {x : L}
 
 /-- If `F ≤ E` are two intermediate fields of `L / K`, then `E` is also an intermediate field of
 `L / F`. It can be viewed as an inverse to `IntermediateField.restrictScalars`. -/
-def extendScalars : IntermediateField F L := E.toSubfield.toIntermediateField fun ⟨_, hf⟩ ↦ h hf
+def extendScalars : IntermediateField F L :=
+  Subfield.extendScalars (show F.toSubfield ≤ E.toSubfield from h)
 
 @[simp]
 theorem coe_extendScalars : (extendScalars h : Set L) = (E : Set L) := rfl
@@ -634,9 +689,11 @@ theorem le_extendScalars_iff (E' : IntermediateField F L) :
 
 variable (F)
 
-/-- `IntermediateField.extendScalars` is an order isomorphism from
+/-- `IntermediateField.extendScalars.orderIso` bundles `IntermediateField.extendScalars`
+into an order isomorphism from
 `{ E : IntermediateField K L // F ≤ E }` to `IntermediateField F L`. Its inverse is
 `IntermediateField.restrictScalars`. -/
+@[simps]
 def extendScalars.orderIso : { E : IntermediateField K L // F ≤ E } ≃o IntermediateField F L where
   toFun E := extendScalars E.2
   invFun E := ⟨E.restrictScalars K, fun x hx ↦ E.algebraMap_mem ⟨x, hx⟩⟩
@@ -650,8 +707,16 @@ theorem extendScalars_injective :
     Function.Injective fun E : { E : IntermediateField K L // F ≤ E } ↦ extendScalars E.2 :=
   (extendScalars.orderIso F).injective
 
+end IntermediateField
+
 end ExtendScalars
 
+namespace IntermediateField
+
+variable {S}
+
+section Tower
+
 section Restrict
 
 variable {F E : IntermediateField K L} (h : F ≤ E)

Mathlib/GroupTheory/GroupAction/Hom.lean

@@ -156,7 +156,7 @@ theorem ext {f g : X →ₑ[φ] Y} :
     (∀ x, f x = g x) → f = g :=
   DFunLike.ext f g
 
-theorem ext_iff  {f g : X →ₑ[φ] Y} :
+protected theorem ext_iff  {f g : X →ₑ[φ] Y} :
     f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -387,7 +387,7 @@ theorem ext {f g : LocalizationMap S N} (h : ∀ x, f.toMap x = g.toMap x) : f =
   exact OneHom.ext h
 
 @[to_additive]
-theorem ext_iff {f g : LocalizationMap S N} : f = g ↔ ∀ x, f.toMap x = g.toMap x :=
+protected theorem ext_iff {f g : LocalizationMap S N} : f = g ↔ ∀ x, f.toMap x = g.toMap x :=
   ⟨fun h _ ↦ h ▸ rfl, ext⟩
 
 @[to_additive]

Mathlib/LinearAlgebra/Alternating/Basic.lean

@@ -125,7 +125,7 @@ theorem coe_inj {f g : M [⋀^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f
 theorem ext {f f' : M [⋀^ι]→ₗ[R] N} (H : ∀ x, f x = f' x) : f = f' :=
   DFunLike.ext _ _ H
 
-theorem ext_iff {f g : M [⋀^ι]→ₗ[R] N} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : M [⋀^ι]→ₗ[R] N} : f = g ↔ ∀ x, f x = g x :=
   ⟨fun h _ => h ▸ rfl, fun h => ext h⟩
 
 attribute [coe] AlternatingMap.toMultilinearMap

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -138,7 +138,7 @@ theorem coe_inj {f g : MultilinearMap R M₁ M₂} : (f : (∀ i, M₁ i) → M
 theorem ext {f f' : MultilinearMap R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
   DFunLike.ext _ _ H
 
-theorem ext_iff {f g : MultilinearMap R M₁ M₂} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : MultilinearMap R M₁ M₂} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 @[simp]

Mathlib/Logic/Equiv/Defs.lean

@@ -134,7 +134,7 @@ protected theorem Perm.congr_arg {f : Equiv.Perm α} {x x' : α} : x = x' → f
 protected theorem Perm.congr_fun {f g : Equiv.Perm α} (h : f = g) (x : α) : f x = g x :=
   Equiv.congr_fun h x
 
-theorem Perm.ext_iff {σ τ : Equiv.Perm α} : σ = τ ↔ ∀ x, σ x = τ x := Equiv.ext_iff
+protected theorem Perm.ext_iff {σ τ : Equiv.Perm α} : σ = τ ↔ ∀ x, σ x = τ x := Equiv.ext_iff
 
 /-- Any type is equivalent to itself. -/
 @[refl] protected def refl (α : Sort*) : α ≃ α := ⟨id, id, fun _ => rfl, fun _ => rfl⟩

Mathlib/Order/Filter/Basic.lean

@@ -120,12 +120,12 @@ theorem filter_eq : ∀ {f g : Filter α}, f.sets = g.sets → f = g
 theorem filter_eq_iff : f = g ↔ f.sets = g.sets :=
   ⟨congr_arg _, filter_eq⟩
 
-protected theorem ext_iff : f = g ↔ ∀ s, s ∈ f ↔ s ∈ g := by
-  simp only [filter_eq_iff, ext_iff, Filter.mem_sets]
-
 @[ext]
-protected theorem ext : (∀ s, s ∈ f ↔ s ∈ g) → f = g :=
-  Filter.ext_iff.2
+protected theorem ext (h : ∀ s, s ∈ f ↔ s ∈ g) : f = g := by
+  simpa [filter_eq_iff, Set.ext_iff, Filter.mem_sets]
+
+protected theorem ext_iff : f = g ↔ ∀ s, s ∈ f ↔ s ∈ g :=
+  ⟨by rintro rfl s; rfl, Filter.ext⟩
 
 /-- An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g.,
 `Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`). -/

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -425,7 +425,7 @@ initialize_simps_projections ContinuousLinearMap (toLinearMap_toFun → apply, t
 theorem ext {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
-theorem ext_iff {f g : M₁ →SL[σ₁₂] M₂} : f = g ↔ ∀ x, f x = g x :=
+protected theorem ext_iff {f g : M₁ →SL[σ₁₂] M₂} : f = g ↔ ∀ x, f x = g x :=
   DFunLike.ext_iff
 
 /-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
@@ -475,7 +475,7 @@ theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁
 theorem ext_ring [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g :=
   coe_inj.1 <| LinearMap.ext_ring h
 
-theorem ext_ring_iff [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} : f = g ↔ f 1 = g 1 :=
+protected theorem ext_ring_iff [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} : f = g ↔ f 1 = g 1 :=
   ⟨fun h => h ▸ rfl, ext_ring⟩
 
 /-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure