awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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 g : E →L[R] F
hf : f.HasLeftInverse
hfg : g = f
⊢ g.HasLeftInverse

Tactic:
hfg ▸ hf

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
⊢ (↑f.symm : F →L[R] E) ∘SL (↑f : E →L[R] F) = ContinuousLinearMap.id R E

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h : ∀ (y : F), Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)
⊢ ⋯.leftInverse = (↑f.symm : F →L[R] E)

Tactic:
ext y
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
y : F
⊢ Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) y : E)
    ((⋯.leftInverse : (a : F) → E) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) : E)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
y : F
⊢ Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) : E)
    ((f.symm : (a : F) → E) y : E)

Tactic:
f.hasLeftInverse.leftInverse_leftInverse (f.symm y)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse, ContinuousLinearEquiv.hasLeftInverse, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
y : F
calc :
  Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) y : E)
    ((⋯.leftInverse : (a : F) → E) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) : E)
⊢ Eq.{u_2 + 1} (α := E) ((⋯.leftInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)

Tactic:
calc f.hasLeftInverse.leftInverse y
    _ = f.hasLeftInverse.leftInverse (f (f.symm y)) := by simp
    _ = f.symm y := f.hasLeftInverse.leftInverse_leftInverse (f.symm y)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse, ContinuousLinearEquiv.hasLeftInverse, ContinuousLinearMap.HasLeftInverse.leftInverse, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
obtain : ∀ (e : E ≃L[R] F), (↑e : E →L[R] F).HasLeftInverse
⊢ f.HasLeftInverse

Tactic:
obtain ⟨e, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
e : E ≃L[R] F
⊢ (↑e : E →L[R] F).HasLeftInverse

Tactic:
e.hasLeftInverse

Premises used: ContinuousLinearEquiv.hasLeftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
e : E ≃L[R] F
⊢ (↑e : E →L[R] F).HasLeftInverse

Tactic:
exact e.hasLeftInverse

Premises used: ContinuousLinearEquiv.hasLeftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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.HasLeftInverse
hg : g.HasLeftInverse
obtain :
  ∀ (finv : F →L[R] E)
    (hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)),
    (f.prodMap g).HasLeftInverse
⊢ (f.prodMap g).HasLeftInverse

Tactic:
obtain ⟨finv, hfinv⟩ := hf
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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.HasLeftInverse
finv : F →L[R] E
hfinv : LeftInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
obtain :
  ∀ (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
⊢ (f.prodMap g).HasLeftInverse

Tactic:
obtain ⟨ginv, hginv⟩ := hg
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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')
h :
  LeftInverse (α := E × E') (β := F × F') (⇑(finv.prodMap ginv) : (a : F × F') → E × E')
    (⇑(f.prodMap g) : (a : E × E') → F × F')
⊢ (f.prodMap g).HasLeftInverse

Tactic:
use finv.prodMap ginv

Premises used: ContinuousLinearMap.prodMap
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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')
⊢ LeftInverse (α := E × E') (β := F × F') (⇑(finv.prodMap ginv) : (a : F × F') → E × E')
    (⇑(f.prodMap g) : (a : E × E') → F × F')

Tactic:
simp [hfinv, hginv]
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
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
⊢ (g ∘SL f).HasLeftInverse

Tactic:
obtain ⟨finv, hfinv⟩ := hf
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
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
⊢ (g ∘SL f).HasLeftInverse

Tactic:
obtain ⟨ginv, hginv⟩ := hg
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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

Tactic:
⟨finv.comp ginv, fun x ↦ ?_⟩

Premises used: ContinuousLinearMap.comp, Exists.intro, ContinuousLinearMap.HasLeftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
refine : ∀ (x : E), (finv ∘SL ginv : (a : G) → E) ((g ∘SL f : (a : E) → G) x : G) = x
⊢ (g ∘SL f).HasLeftInverse

Tactic:
refine ⟨finv.comp ginv, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
simp : (finv : (a : F) → E) ((ginv : (a : G) → F) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G) : F) = x
⊢ (finv ∘SL ginv : (a : G) → E) ((g ∘SL f : (a : E) → G) x : G) = x

Tactic:
simp only [coe_comp', Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', Function.comp_apply
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
rw₁ rw₂ : x = x
⊢ (finv : (a : F) → E) ((ginv : (a : G) → F) ((g : (a : F) → G) ((f : (a : E) → F) x : F) : G) : F) = x

Tactic:
rw [hginv, hfinv]
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
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
⊢ f.HasLeftInverse

Tactic:
obtain ⟨fginv, hfginv⟩ := hfg
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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

Tactic:
⟨fginv.comp g, fun y ↦ ?_⟩

Premises used: ContinuousLinearMap.comp, Exists.intro, ContinuousLinearMap.HasLeftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
refine : ∀ (y : E), (fginv ∘SL g : (a : F) → E) ((f : (a : E) → F) y : F) = y
⊢ f.HasLeftInverse

Tactic:
refine ⟨fginv.comp g, fun y ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
simp : (fginv : (a : G) → E) ((g : (a : F) → G) ((f : (a : E) → F) y : F) : G) = y
⊢ (fginv ∘SL g : (a : F) → E) ((f : (a : E) → F) y : F) = y

Tactic:
simp only [coe_comp', Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', Function.comp_apply
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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 : (a : G) → E) ((g : (a : F) → G) ((f : (a : E) → F) y : F) : G) = y

Tactic:
hfginv y
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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 : (a : G) → E) ((g : (a : F) → G) ((f : (a : E) → F) y : F) : G) = y

Tactic:
exact hfginv y
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
F' : Type u_5
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
inst_7 : TopologicalSpace F'
inst_8 : AddCommMonoid F'
inst_9 : Module R F'
f : E →L[R] F
f₀ : F' ≃L[R] E
hf : f.HasLeftInverse
⊢ (f ∘SL (↑f₀ : F' →L[R] E)).HasLeftInverse

Tactic:
hf.comp f₀.hasLeftInverse

Premises used: ContinuousLinearEquiv.hasLeftInverse, ContinuousLinearMap.HasLeftInverse.comp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
Goal:
R : Type u_1
inst : Semiring R
E : Type u_2
F : Type u_4
F' : Type u_5
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
inst_7 : TopologicalSpace F'
inst_8 : AddCommMonoid F'
inst_9 : Module R F'
f : E →L[R] F
g : F ≃L[R] F'
hf : f.HasLeftInverse
⊢ ((↑g : F →L[R] F') ∘SL f).HasLeftInverse

Tactic:
g.hasLeftInverse.comp hf

Premises used: ContinuousLinearEquiv.hasLeftInverse, ContinuousLinearMap.HasLeftInverse.comp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h : LeftInverse (α := F) (β := F × G) (⇑(fst R F G) : (a : F × G) → F) (⇑(inl R F G) : (a : F) → F × G)
⊢ ContinuousLinearMap.HasLeftInverse (inl R F G)

Tactic:
use ContinuousLinearMap.fst _ _ _

Premises used: ContinuousLinearMap.fst
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : F
⊢ (fst R F G : (a : F × G) → F) ((inl R F G : (a : F) → F × G) x : F × G) = x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h : LeftInverse (α := G) (β := F × G) (⇑(snd R F G) : (a : F × G) → G) (⇑(inr R F G) : (a : G) → F × G)
⊢ ContinuousLinearMap.HasLeftInverse (inr R F G)

Tactic:
use ContinuousLinearMap.snd _ _ _

Premises used: ContinuousLinearMap.snd
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : G
⊢ (snd R F G : (a : F × G) → G) ((inr R F G : (a : G) → F × G) x : F × G) = x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
obtain : ∀ (g : F →ₗ[𝕜] E) (hg : g ∘ₗ (↑f : E →ₗ[𝕜] F) = LinearMap.id), f.HasLeftInverse
⊢ f.HasLeftInverse

Tactic:
obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_leftInverse_of_injective (f.ker_eq_bot_of_injective hf)

Premises used: LinearMap.exists_leftInverse_of_injective, ContinuousLinearMap.toLinearMap, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
g : F →ₗ[𝕜] E
hg : g ∘ₗ (↑f : E →ₗ[𝕜] F) = LinearMap.id
⊢ f.HasLeftInverse

Tactic:
⟨⟨g, LinearMap.continuous_of_finiteDimensional _⟩, fun x ↦ congr($hg x)⟩

Premises used: congrArg, ContinuousLinearMap.mk, id, LinearMap.continuous_of_finiteDimensional, Exists.intro, DFunLike.coe, ContinuousLinearMap.HasLeftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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)
g : F →ₗ[𝕜] E
hg : g ∘ₗ (↑f : E →ₗ[𝕜] F) = LinearMap.id
⊢ f.HasLeftInverse

Tactic:
exact ⟨⟨g, LinearMap.continuous_of_finiteDimensional _⟩, fun x ↦ congr($hg x)⟩
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
y : F
⊢ Membership.mem (α := F) (↑f : E →ₗ[R] F).range ((f ∘SL hf.leftInverse : (a : F) → F) y : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h :
  ∀ (x : ↥(↑f : E →ₗ[R] F).range),
    ((f ∘SL hf.leftInverse).codRestrict (↑f : E →ₗ[R] F).range ⋯ : (a : F) → ↥(↑f : E →ₗ[R] F).range) (↑x : F) = x
⊢ (↑f : E →ₗ[R] F).range.ClosedComplemented

Tactic:
use (f.comp hf.leftInverse).codRestrict f.range (by intro y; simp)

Premises used: ContinuousLinearMap.comp, LinearMap.range, ContinuousLinearMap.toLinearMap, ContinuousLinearMap.codRestrict, ContinuousLinearMap.HasLeftInverse.leftInverse
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
h :
  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)
⊢ 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)

Tactic:
ext