awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E'
inst_5 : AddCommMonoid E'
inst_6 : Module R E'
inst_7 : TopologicalSpace F
inst_8 : AddCommMonoid F
inst_9 : Module R F
inst_10 : TopologicalSpace F'
inst_11 : AddCommMonoid F'
inst_12 : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : F' →L[R] E'
hginv : LeftInverse.{u_3 + 1, u_5 + 1} (α := E') (β := F') (⇑ginv : (a : F') → E') (⇑g : (a : E') → F')
⊢ (f.prodMap g).HasLeftInverse
have h : LeftInverse (α := E × E') (β := F × F') (⇑(finv.prodMap ginv) : (a : F × F') → E × E')
  (⇑(f.prodMap g) : (a : E × E') → F × F')
Tactic: use finv.prodMap ginv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hg : g.HasLeftInverse
hf : f.HasLeftInverse
⊢ (g ∘SL f).HasLeftInverse
have obtain : ∀ (finv : F →L[R] E)
  (hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)),
  (g ∘SL f).HasLeftInverse
Tactic: obtain ⟨finv, hfinv⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hg : g.HasLeftInverse
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
⊢ (g ∘SL f).HasLeftInverse
have obtain : ∀ (ginv : G →L[R] F)
  (hginv : LeftInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)),
  (g ∘SL f).HasLeftInverse
Tactic: obtain ⟨ginv, hginv⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : LeftInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
⊢ (g ∘SL f).HasLeftInverse
have refine : ∀ (x : E), (finv ∘SL ginv : (a : G) → E) ((g ∘SL f : (a : E) → G) x : G) = x
Tactic: refine ⟨finv.comp ginv, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : LeftInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : E
⊢ (finv ∘SL ginv : (a : G) → E) ((g ∘SL f : (a : E) → G) x : G) = x
have simp : (finv : (a : F) → E) ((ginv : (a : G) → F) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G) : F) = x
Tactic: simp only [coe_comp', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : LeftInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : E
⊢ (finv : (a : F) → E) ((ginv : (a : G) → F) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G) : F) = x
have rw : (finv : (a : F) → E) ((f : (a : E) → F) x : F) = x
Tactic: rw [hginv, hfinv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : LeftInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : E
rw : (finv : (a : F) → E) ((f : (a : E) → F) x : F) = x
⊢ (finv : (a : F) → E) ((ginv : (a : G) → F) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G) : F) = x
have rw₁ : x = x
Tactic: rw [hginv, hfinv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hfg : (g ∘SL f).HasLeftInverse
⊢ f.HasLeftInverse
have obtain : ∀ (fginv : G →L[R] E)
  (hfginv : LeftInverse.{u_2 + 1, u_6 + 1} (α := E) (β := G) (⇑fginv : (a : G) → E) (⇑(g ∘SL f) : (a : E) → G)),
  f.HasLeftInverse
Tactic: obtain ⟨fginv, hfginv⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
fginv : G →L[R] E
hfginv : LeftInverse.{u_2 + 1, u_6 + 1} (α := E) (β := G) (⇑fginv : (a : G) → E) (⇑(g ∘SL f) : (a : E) → G)
⊢ f.HasLeftInverse
have refine : ∀ (y : E), (fginv ∘SL g : (a : F) → E) ((f : (a : E) → F) y : F) = y
Tactic: refine ⟨fginv.comp g, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
fginv : G →L[R] E
hfginv : LeftInverse.{u_2 + 1, u_6 + 1} (α := E) (β := G) (⇑fginv : (a : G) → E) (⇑(g ∘SL f) : (a : E) → G)
y : E
⊢ (fginv ∘SL g : (a : F) → E) ((f : (a : E) → F) y : F) = y
have simp : (fginv : (a : G) → E) ((g : (a : F) → G) ((f : (a : E) → F) y : F) : G) = y
Tactic: simp only [coe_comp', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace F
inst_2 : AddCommMonoid F
inst_3 : Module R F
inst_4 : TopologicalSpace G
inst_5 : AddCommMonoid G
inst_6 : Module R G
⊢ ContinuousLinearMap.HasLeftInverse (inl R F G)
have h : LeftInverse (α := F) (β := F × G) (⇑(fst R F G) : (a : F × G) → F) (⇑(inl R F G) : (a : F) → F × G)
Tactic: use ContinuousLinearMap.fst _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace F
inst_2 : AddCommMonoid F
inst_3 : Module R F
inst_4 : TopologicalSpace G
inst_5 : AddCommMonoid G
inst_6 : Module R G
⊢ ContinuousLinearMap.HasLeftInverse (inr R F G)
have h : LeftInverse (α := G) (β := F × G) (⇑(snd R F G) : (a : F × G) → G) (⇑(inr R F G) : (a : G) → F × G)
Tactic: use ContinuousLinearMap.snd _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
𝕜 : Type u_7
inst : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
f : E →L[𝕜] F
inst_12 : CompleteSpace 𝕜
inst_13 : FiniteDimensional 𝕜 F
hf : Injective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ f.HasLeftInverse
have obtain : ∀ (g : F →ₗ[𝕜] E) (hg : g ∘ₗ (↑f : E →ₗ[𝕜] F) = LinearMap.id), f.HasLeftInverse
Tactic: obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_leftInverse_of_injective (f.ker_eq_bot_of_injective hf)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_10
inst : Ring R
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
⊢ (↑f : E →ₗ[R] F).range.ClosedComplemented
have h : ∀ (x : ↥(↑f : E →ₗ[R] F).range),
  ((f ∘SL hf.leftInverse).codRestrict (↑f : E →ₗ[R] F).range sorry : (a : F) → ↥(↑f : E →ₗ[R] F).range) (↑x : F) = x
Tactic: use (f.comp hf.leftInverse).codRestrict f.range (by intro y; simp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_10
inst : Ring R
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
x : E
⊢ Eq (α := ↥(↑f : E →ₗ[R] F).range)
    (((f ∘SL hf.leftInverse).codRestrict (↑f : E →ₗ[R] F).range ⋯ : (a : F) → ↥(↑f : E →ₗ[R] F).range)
        (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) ⋯) : F) :
      ↥(↑f : E →ₗ[R] F).range)
    (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) ⋯ :
      ↥(↑f : E →ₗ[R] F).range)
have h : Eq.{u_10 + 1} (α := F)
  ((↑(((f ∘SL hf.leftInverse).codRestrict (↑f : E →ₗ[R] F).range sorry : (a : F) → ↥(↑f : E →ₗ[R] F).range)
          (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) sorry) : F)) :
      F) :
    F)
  ((↑(Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) sorry) : F) : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_10
inst : Ring R
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
x : E
⊢ Eq.{u_10 + 1} (α := F)
    ((↑(((f ∘SL hf.leftInverse).codRestrict (↑f : E →ₗ[R] F).range ⋯ : (a : F) → ↥(↑f : E →ₗ[R] F).range)
            (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) ⋯) :
              F)) :
        F) :
      F)
    ((↑(Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[R] F).range) (((↑f : E →ₗ[R] F) : (a : E) → F) x) ⋯) : F) : F)
have h : Eq.{u_10 + 1} (α := F) ((f : (a : E) → F) ((hf.leftInverse : (a : F) → E) ((f : (a : E) → F) x : F) : E) : F)
  ((f : (a : E) → F) x : F)
Tactic: simp only [coe_coe, coe_codRestrict_apply, coe_comp', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_10
inst : Ring R
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : Module R F
f : E →L[R] F
hf : f.HasLeftInverse
x : E
⊢ Eq.{u_10 + 1} (α := F) ((f : (a : E) → F) ((hf.leftInverse : (a : F) → E) ((f : (a : E) → F) x : F) : E) : F)
    ((f : (a : E) → F) x : F)
have h : Eq.{u_10 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) x : F)
Tactic: rw [hf.leftInverse_leftInverse]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_10
inst : Ring R
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : Module R F
f : E →L[R] F
inst_7 : T1Space F
hf : f.HasLeftInverse
inst_8 : IsTopologicalAddGroup F
⊢ IsClosed.{u_10} (X := F) (range.{u_10, u_8 + 1} (ι := E) (⇑f : (a : E) → F))
have rw : IsClosed (↑((↑f : E →ₗ[R] F) ∘ₗ (↑hf.leftInverse : F →ₗ[R] E) - LinearMap.id).ker : Set F)
Tactic: rw [← f.range_toLinearMap, ← f.coe_range,
    f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_9
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace R E
inst_3 : CompleteSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace R F
inst_6 : CompleteSpace F
f : E →L[R] F
hf : Injective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' : IsClosed.{u_9} (X := F) (range.{u_9, u_8 + 1} (ι := E) (⇑f : (a : E) → F))
hf'' : (↑f : E →ₗ[R] F).range.ClosedComplemented
⊢ LinearMap.ker (M₂ := ↥(↑f : E →ₗ[R] F).range) (↑f.rangeRestrict : E →ₗ[R] ↥(↑f : E →ₗ[R] F).range) = ⊥
have rw : (↑f : E →ₗ[R] F).ker = ⊥
Tactic: rw [ker_codRestrict]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (hypothesis)
Goal:
R : Type u_7
E : Type u_8
F : Type u_9
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace R E
inst_3 : CompleteSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace R F
inst_6 : CompleteSpace F
f : E →L[R] F
hf : Injective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' : IsClosed.{u_9} (X := F) (range.{u_9, u_8 + 1} (ι := E) (⇑f : (a : E) → F))
hf'' : (↑f : E →ₗ[R] F).range.ClosedComplemented
⊢ f.HasLeftInverse
have this : LinearMap.ker (M₂ := ↥(↑f : E →ₗ[R] F).range) (↑f.rangeRestrict : E →ₗ[R] ↥(↑f : E →ₗ[R] F).range) = ⊥
Tactic: have : (f.rangeRestrict).ker = ⊥ := by
    rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_9
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace R E
inst_3 : CompleteSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace R F
inst_6 : CompleteSpace F
f : E →L[R] F
hf : Injective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' : IsClosed.{u_9} (X := F) (range.{u_9, u_8 + 1} (ι := E) (⇑f : (a : E) → F))
hf'' : (↑f : E →ₗ[R] F).range.ClosedComplemented
this : LinearMap.ker (M₂ := ↥(↑f : E →ₗ[R] F).range) (↑f.rangeRestrict : E →ₗ[R] ↥(↑f : E →ₗ[R] F).range) = ⊥
⊢ f.HasLeftInverse
have obtain : ∀ (p : F →L[R] ↥(↑f : E →ₗ[R] F).range)
  (hp : ∀ (x : ↥(↑f : E →ₗ[R] F).range), (p : (a : F) → ↥(↑f : E →ₗ[R] F).range) (↑x : F) = x), f.HasLeftInverse
Tactic: obtain ⟨p, hp⟩ := hf''
Cleared hypotheses: hf''
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_7
E : Type u_8
F : Type u_9
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace R E
inst_3 : CompleteSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace R F
inst_6 : CompleteSpace F
f : E →L[R] F
hf : Injective.{u_8 + 1, u_9 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' : IsClosed.{u_9} (X := F) (range.{u_9, u_8 + 1} (ι := E) (⇑f : (a : E) → F))
this : LinearMap.ker (M₂ := ↥(↑f : E →ₗ[R] F).range) (↑f.rangeRestrict : E →ₗ[R] ↥(↑f : E →ₗ[R] F).range) = ⊥
p : F →L[R] ↥(↑f : E →ₗ[R] F).range
hp : ∀ (x : ↥(↑f : E →ₗ[R] F).range), (p : (a : F) → ↥(↑f : E →ₗ[R] F).range) (↑x : F) = x
⊢ f.HasLeftInverse
have refine : ∀ (x : E), (f.leftInverse_of_injective_of_isClosed_range hf hf' ∘SL p : (a : F) → E) ((f : (a : E) → F) x : F) = x
Tactic: refine ⟨(f.leftInverse_of_injective_of_isClosed_range hf hf').comp p, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E ≃L[R] F
⊢ ⋯.rightInverse = (↑f.symm : F →L[R] E)
have h : ∀ (y : F), Eq.{u_2 + 1} (α := E) ((sorry.rightInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
hf : f.IsInvertible
⊢ f.HasRightInverse
have obtain : ∀ (e : E ≃L[R] F), (↑e : E →L[R] F).HasRightInverse
Tactic: obtain ⟨e, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E'
inst_5 : AddCommMonoid E'
inst_6 : Module R E'
inst_7 : TopologicalSpace F
inst_8 : AddCommMonoid F
inst_9 : Module R F
inst_10 : TopologicalSpace F'
inst_11 : AddCommMonoid F'
inst_12 : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasRightInverse
hg : g.HasRightInverse
⊢ (f.prodMap g).HasRightInverse
have obtain : ∀ (finv : F →L[R] E)
  (hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)),
  (f.prodMap g).HasRightInverse
Tactic: obtain ⟨finv, hfinv⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E'
inst_5 : AddCommMonoid E'
inst_6 : Module R E'
inst_7 : TopologicalSpace F
inst_8 : AddCommMonoid F
inst_9 : Module R F
inst_10 : TopologicalSpace F'
inst_11 : AddCommMonoid F'
inst_12 : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hg : g.HasRightInverse
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
⊢ (f.prodMap g).HasRightInverse
have obtain : ∀ (ginv : F' →L[R] E')
  (hginv : RightInverse.{u_3 + 1, u_5 + 1} (α := E') (β := F') (⇑ginv : (a : F') → E') (⇑g : (a : E') → F')),
  (f.prodMap g).HasRightInverse
Tactic: obtain ⟨ginv, hginv⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace E'
inst_5 : AddCommMonoid E'
inst_6 : Module R E'
inst_7 : TopologicalSpace F
inst_8 : AddCommMonoid F
inst_9 : Module R F
inst_10 : TopologicalSpace F'
inst_11 : AddCommMonoid F'
inst_12 : Module R F'
f : E →L[R] F
g : E' →L[R] F'
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : F' →L[R] E'
hginv : RightInverse.{u_3 + 1, u_5 + 1} (α := E') (β := F') (⇑ginv : (a : F') → E') (⇑g : (a : E') → F')
⊢ (f.prodMap g).HasRightInverse
have h : RightInverse (α := E × E') (β := F × F') (⇑(finv.prodMap ginv) : (a : F × F') → E × E')
  (⇑(f.prodMap g) : (a : E × E') → F × F')
Tactic: use finv.prodMap ginv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hg : g.HasRightInverse
hf : f.HasRightInverse
⊢ (g ∘SL f).HasRightInverse
have obtain : ∀ (finv : F →L[R] E)
  (hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)),
  (g ∘SL f).HasRightInverse
Tactic: obtain ⟨finv, hfinv⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
hg : g.HasRightInverse
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
⊢ (g ∘SL f).HasRightInverse
have obtain : ∀ (ginv : G →L[R] F)
  (hginv : RightInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)),
  (g ∘SL f).HasRightInverse
Tactic: obtain ⟨ginv, hginv⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : RightInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
⊢ (g ∘SL f).HasRightInverse
have refine : ∀ (x : G), (g ∘SL f : (a : E) → G) ((finv ∘SL ginv : (a : G) → E) x : E) = x
Tactic: refine ⟨finv.comp ginv, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.ContinuousInverse (goal)
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : TopologicalSpace F
inst_5 : AddCommMonoid F
inst_6 : Module R F
f : E →L[R] F
inst_7 : TopologicalSpace G
inst_8 : AddCommMonoid G
inst_9 : Module R G
g : F →L[R] G
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
ginv : G →L[R] F
hginv : RightInverse.{u_4 + 1, u_6 + 1} (α := F) (β := G) (⇑ginv : (a : G) → F) (⇑g : (a : F) → G)
x : G
⊢ (g ∘SL f : (a : E) → G) ((finv ∘SL ginv : (a : G) → E) x : E) = x
have simp : (g : (a : F) → G) ((f : (a : E) → F) ((finv : (a : F) → E) ((ginv : (a : G) → F) x : F) : E) : F) = x
Tactic: simp only [coe_comp', Function.comp_apply]