awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E
F : Type u_5
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
inst_14 : CompleteSpace.{u_5} ↥G
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
rw : (↑f : E →ₗ[𝕜] F).ker.prod (↑G.subtypeL : ↥G →ₗ[𝕜] F).ker = ⊥
rw₁ : Disjoint (↑f : E →ₗ[𝕜] F).range (↑G.subtypeL : ↥G →ₗ[𝕜] F).range
⊢ (↑(f.coprod G.subtypeL) : E × ↥G →ₗ[𝕜] F).ker = ⊥

Tactic:
rw [ker_coprod_of_disjoint_range]

Premises used: ContinuousLinearMap.ker_coprod_of_disjoint_range
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E
F : Type u_5
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
inst_14 : CompleteSpace.{u_5} ↥G
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
⊢ (↑f : E →ₗ[𝕜] F).ker.prod (↑G.subtypeL : ↥G →ₗ[𝕜] F).ker = ⊥

Tactic:
simp [hker]
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E
F : Type u_5
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
inst_14 : CompleteSpace.{u_5} ↥G
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
⊢ Disjoint (↑f : E →ₗ[𝕜] F).range (↑G.subtypeL : ↥G →ₗ[𝕜] F).range

Tactic:
simp [h.disjoint]

Premises used: IsCompl.disjoint
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E
F : Type u_5
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
inst_14 : CompleteSpace.{u_5} ↥G
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
⊢ (↑(f.coprod G.subtypeL) : E × ↥G →ₗ[𝕜] F).range = ⊤

Tactic:
simp [LinearMap.range_coprod, h.sup_eq_top]

Premises used: IsCompl.sup_eq_top, LinearMap.range_coprod
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑G : Set F)
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
⊢ CompleteSpace.{u_5} ↥G

Tactic:
haveI : CompleteSpace G := hG.completeSpace_coe
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑G : Set F)
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
this : CompleteSpace.{u_5} ↥G
g : Prod.{u_3, u_5} E ↥G ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
rw :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (↑(Submodule.map (↑(↑(f.coprodSubtypeLEquivOfIsCompl h hker) : (E × ↥G) ≃ₗ[𝕜] F) : E × ↥G →ₗ[𝕜] F)
          (Submodule.prod ⊤ ⊥)) :
      Set F)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(↑f : E →ₗ[𝕜] F).range : Set F)

Tactic:
rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]

Premises used: ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑G : Set F)
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
this : CompleteSpace.{u_5} ↥G
g : Prod.{u_3, u_5} E ↥G ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
apply : IsClosed[instTopologicalSpaceProd] (↑(Submodule.prod ⊤ ⊥) : Set (E × ↥G))
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (↑(Submodule.map (↑(↑(f.coprodSubtypeLEquivOfIsCompl h hker) : (E × ↥G) ≃ₗ[𝕜] F) : E × ↥G →ₗ[𝕜] F)
          (Submodule.prod ⊤ ⊥)) :
      Set F)

Tactic:
apply g.toHomeomorph.isClosed_image.2

Premises used: Iff.mpr, Homeomorph.isClosed_image, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑G : Set F)
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
this : CompleteSpace.{u_5} ↥G
g : Prod.{u_3, u_5} E ↥G ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[instTopologicalSpaceProd] (↑(Submodule.prod ⊤ ⊥) : Set (E × ↥G))

Tactic:
isClosed_univ.prod isClosed_singleton

Premises used: isClosed_univ, Set.Mem, Set.univ, setOf, Set.prod, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f : E →ₗ[𝕜] F).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑G : Set F)
hker : (↑f : E →ₗ[𝕜] F).ker = ⊥
this : CompleteSpace.{u_5} ↥G
g : Prod.{u_3, u_5} E ↥G ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[instTopologicalSpaceProd] (↑(Submodule.prod ⊤ ⊥) : Set (E × ↥G))

Tactic:
exact isClosed_univ.prod isClosed_singleton

Premises used: isClosed_univ, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
this : CompleteSpace ↥g.graph := ⋯
φ₀ : E →ₗ[𝕜] E × F := prod id g
⊢ LeftInverse (α := E) (β := E × F) Prod.fst (⇑φ₀ : (a : E) → E × F)

Tactic:
have : Function.LeftInverse Prod.fst φ₀ := fun x => rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
this_1 : CompleteSpace ↥g.graph := ⋯
φ₀ : E →ₗ[𝕜] E × F := prod id g
this : LeftInverse (α := E) (β := E × F) Prod.fst (⇑φ₀ : (a : E) → E × F)
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq φ₀.range g.graph ⋯
ψ : ↥g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous ⋯
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑g : (a : E) → F)

Tactic:
(continuous_subtype_val.comp ψ.symm.continuous).snd

Premises used: ContinuousLinearEquiv.symm, continuous_subtype_val, Continuous.snd, Continuous.comp, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
this_1 : CompleteSpace ↥g.graph := ⋯
φ₀ : E →ₗ[𝕜] E × F := prod id g
this : LeftInverse (α := E) (β := E × F) Prod.fst (⇑φ₀ : (a : E) → E × F)
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq φ₀.range g.graph ⋯
ψ : ↥g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous ⋯
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑g : (a : E) → F)

Tactic:
exact (continuous_subtype_val.comp ψ.symm.continuous).snd

Premises used: ContinuousLinearEquiv.symm, continuous_subtype_val, Continuous.snd, Continuous.comp, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑g : (a : E) → F)

Tactic:
g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)

Premises used: IsSeqClosed.isClosed, LinearMap.continuous_of_isClosed_graph
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
refine : IsSeqClosed (↑g.graph : Set (E × F))
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑g : (a : E) → F)

Tactic:
refine g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)

Premises used: IsSeqClosed.isClosed, LinearMap.continuous_of_isClosed_graph
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ (x, y) ∈ (↑g.graph : Set (E × F))

Tactic:
hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_

Premises used: Set.Mem, setOf, Function.comp, continuous_fst, Prod.fst, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
refine : Tendsto ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) atTop (𝓝 y)
⊢ (x, y) ∈ (↑g.graph : Set (E × F))

Tactic:
refine hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_

Premises used: Function.comp, continuous_fst, Prod.fst, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
h : ∀ (n : ℕ), ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n
⊢ (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
n : ℕ
⊢ ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n

Tactic:
(hφg n).symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
n : ℕ
⊢ ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n

Tactic:
exact (hφg n).symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ

Tactic:
have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
    ext n
    exact (hφg n).symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
this : (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
rw : Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
⊢ Tendsto ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) atTop (𝓝 y)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
this : (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)

Tactic:
(continuous_snd.tendsto _).comp hφ

Premises used: continuous_snd, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ (↑g.graph : Set (E × F))
hφ : Tendsto φ atTop (𝓝 (x, y))
this : (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)

Tactic:
exact (continuous_snd.tendsto _).comp hφ

Premises used: continuous_snd, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
⊢ Eq (α := (a : E) → F) (⇑(ofIsClosedGraph hg) : (a : E) → F) (⇑g : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
h :
  ∀ (x : E), Eq.{u_5 + 1} (α := F) (((↑(ofIsClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
⊢ (↑(ofIsClosedGraph hg) : E →ₗ[𝕜] F) = g

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed[instTopologicalSpaceProd] (↑g.graph : Set (E × F))
x : E
⊢ Eq.{u_5 + 1} (α := F) (((↑(ofIsClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
⊢ Eq (α := (a : E) → F) (⇑(ofSeqClosedGraph hg) : (a : E) → F) (⇑g : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
h :
  ∀ (x : E),
    Eq.{u_5 + 1} (α := F) (((↑(ofSeqClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
⊢ (↑(ofSeqClosedGraph hg) : E →ₗ[𝕜] F) = g

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
x : E
⊢ Eq.{u_5 + 1} (α := F) (((↑(ofSeqClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
f : E →SL[σ] F
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
⊢ (↑f : E →ₛₗ[σ] F).range.topologicalClosure = (↑f : E →ₛₗ[σ] F).range

Tactic:
SetLike.ext'_iff.mpr <| (hf.isClosed_range f.uniformContinuous).closure_eq

Premises used: Iff.mpr, AntilipschitzWith.isClosed_range, ContinuousLinearMap.uniformContinuous, IsClosed.closure_eq, SetLike.ext'_iff
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
f : E →SL[σ] F
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
⊢ CompleteSpace.{u_4} ↥(↑f : E →ₛₗ[σ] F).range

Tactic:
IsClosed.completeSpace_coe (hs := hf.isClosed_range f.uniformContinuous)

Premises used: IsClosed.completeSpace_coe
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)

Tactic:
⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩

Premises used: _private.0.ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz.match_1, AntilipschitzWith.injective, And.intro, Iff.intro, Function.Bijective, DFunLike.coe