awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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 : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e : (a : E) → F) '' s)
have rw : ∀
  (h :
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (⇑(↑e : E →ₛₗ[σ] F) : (a : E) → F))
  (s : Set E) (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(↑e : E →ₛₗ[σ] F) : (a : E) → F) '' s)
Tactic: rw [← e.coe_coe] at h ⊢
Cleared hypotheses: h, s, hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_5
F : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F)) ↔
    ∃ (K : ℝ≥0), AntilipschitzWith.{u_5, u_6} (α := E) (β := F) K (⇑f : (a : E) → F)
have refine : ∀ (h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_5, u_6} (α := E) (β := F) K (⇑f : (a : E) → F)),
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
Tactic: refine ⟨fun h ↦ f.antilipschitz_of_injective_of_isClosed_range hf h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_5
F : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_5, u_6} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
have choose : ∀ (K : ℝ≥0) (hf' : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) K (⇑f : (a : E) → F)),
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
Tactic: choose K hf' using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
⊢ norm.{u_5} (E := E)
      (((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
              LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
            (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
          (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
            ↥(↑f : E →ₗ[𝕜] F).range) :
        E) ≤
    (↑K : ℝ) *
      norm.{u_6} (E := ↥(↑f : E →ₗ[𝕜] F).range)
        (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
          ↥(↑f : E →ₗ[𝕜] F).range)
have aux : dist x 0 ≤
  (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
    dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) 0 : F)
Tactic: have aux := hfK.le_mul_dist x 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  dist x 0 ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) 0 : F)
⊢ norm.{u_5} (E := E)
      (((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
              LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
            (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
          (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
            ↥(↑f : E →ₗ[𝕜] F).range) :
        E) ≤
    (↑K : ℝ) *
      norm.{u_6} (E := ↥(↑f : E →ₗ[𝕜] F).range)
        (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
          ↥(↑f : E →ₗ[𝕜] F).range)
have aux₁ : ‖x‖ ≤
  (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) * norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
Tactic: simp only [dist_zero_right, map_zero] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ norm.{u_5} (E := E)
      (((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
              LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
            (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
          (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
            ↥(↑f : E →ₗ[𝕜] F).range) :
        E) ≤
    (↑K : ℝ) *
      norm.{u_6} (E := ↥(↑f : E →ₗ[𝕜] F).range)
        (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
          ↥(↑f : E →ₗ[𝕜] F).range)
have h : ((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
        LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
      (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
    (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) sorry :
      ↥(↑f : E →ₗ[𝕜] F).range) =
  x
Tactic: convert! aux
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ LinearMap.ker (M₂ := ↥(↑f : E →ₗ[𝕜] F).range) (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) = ⊥
have rw : (↑f : E →ₗ[𝕜] F).ker = ⊥
Tactic: rw [ker_codRestrict]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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 : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ (↑(ofBijective f hinj hsurj) : E →SL[σ] F) = f
have h : ∀ (x : E),
  Eq.{u_4 + 1} (α := F) (((↑(ofBijective f hinj hsurj) : E →SL[σ] F) : (a : E) → F) x : F) ((f : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f ↔ Bijective (α := E) (β := E) (⇑f : (a : E) → E)
have mp : IsUnit f → Bijective (α := E) (β := E) (⇑f : (a : E) → E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
mp : IsUnit f → Bijective (α := E) (β := E) (⇑f : (a : E) → E)
⊢ IsUnit f ↔ Bijective (α := E) (β := E) (⇑f : (a : E) → E)
have mpr : Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f
have mpr : ∀ (h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)), (↑f : E →ₗ[𝕜] E).ker = ⊥
Tactic: refine fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
mpr : ∀ (h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)), (↑f : E →ₗ[𝕜] E).ker = ⊥
⊢ Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f
have mpr₁ : ∀ (h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)), (↑f : E →ₗ[𝕜] E).range = ⊤
Tactic: refine fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
⊢ spectrum 𝕜 f = spectrum 𝕜 (↑f : E →ₗ[𝕜] E)
have h : ∀ (μ : 𝕜), μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 (↑f : E →ₗ[𝕜] E)
Tactic: ext μ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
⊢ μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 (↑f : E →ₗ[𝕜] E)
have h : ¬IsUnit (↑(HSub.hSub (α := E →L[𝕜] E) ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) μ : E →L[𝕜] E) f) : E →ₗ[𝕜] E) ↔
  ¬IsUnit (HSub.hSub (α := E →ₗ[𝕜] E) ((algebraMap 𝕜 (E →ₗ[𝕜] E) : (a : 𝕜) → E →ₗ[𝕜] E) μ : E →ₗ[𝕜] E) (↑f : E →ₗ[𝕜] E))
Tactic: rw [spectrum.mem_iff, spectrum.mem_iff, ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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).ker = ⊥
have rw : (↑f : E →ₗ[𝕜] F).ker.prod (↑G.subtypeL : ↥G →ₗ[𝕜] F).ker = ⊥
Tactic: rw [ker_coprod_of_disjoint_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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 = ⊥
⊢ (↑(f.coprod G.subtypeL) : E × ↥G →ₗ[𝕜] F).ker = ⊥
have rw₁ : Disjoint (↑f : E →ₗ[𝕜] F).range (↑G.subtypeL : ↥G →ₗ[𝕜] F).range
Tactic: rw [ker_coprod_of_disjoint_range]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
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 = ⊥
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(↑f : E →ₗ[𝕜] F).range : Set F)
have this : CompleteSpace.{u_5} ↥G
Tactic: haveI : CompleteSpace G := hG.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(↑f : E →ₗ[𝕜] F).range : Set F)
have rw : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (↑(Submodule.map (↑(↑(f.coprodSubtypeLEquivOfIsCompl h hker) : (E × ↥G) ≃ₗ[𝕜] F) : E × ↥G →ₗ[𝕜] F)
        (Submodule.prod ⊤ ⊥)) :
    Set F)
Tactic: rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (↑(Submodule.map (↑(↑(f.coprodSubtypeLEquivOfIsCompl h hker) : (E × ↥G) ≃ₗ[𝕜] F) : E × ↥G →ₗ[𝕜] F)
          (Submodule.prod ⊤ ⊥)) :
      Set F)
have apply : IsClosed[instTopologicalSpaceProd] (↑(Submodule.prod ⊤ ⊥) : Set (E × ↥G))
Tactic: apply g.toHomeomorph.isClosed_image.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
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
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑g : (a : E) → F)
have this₁ : LeftInverse (α := E) (β := E × F) Prod.fst (⇑φ₀ : (a : E) → E × F)
Tactic: have : Function.LeftInverse Prod.fst φ₀ := fun x => rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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)
have refine : IsSeqClosed (↑g.graph : Set (E × F))
Tactic: refine g.continuous_of_isClosed_graph (IsSeqClosed.isClosed ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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))
have refine : Tendsto ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) atTop (𝓝 y)
Tactic: refine hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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 ∘ φ
have h : ∀ (n : ℕ), ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
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))
⊢ Tendsto ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) atTop (𝓝 y)
have this : (⇑g : (a : E) → F) ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
Tactic: have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
    ext n
    exact (hφg n).symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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 ((⇑g : (a : E) → F) ∘ Prod.fst ∘ φ) atTop (𝓝 y)
have rw : Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
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))
⊢ (↑(ofIsClosedGraph hg) : E →ₗ[𝕜] F) = g
have h : ∀ (x : E), Eq.{u_5 + 1} (α := F) (((↑(ofIsClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
Tactic: ext