awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (a : E) → F) ((hf.leftInverse : (a : F) → E) ((f : (a : E) → F) x : F) : E) : F)
    ((f : (a : E) → F) x : F)
⊢ 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)

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

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_coe, ContinuousLinearMap.coe_codRestrict_apply, Function.comp_apply
-- 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 h₁ : Eq.{u_10 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) x : F)
⊢ 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:
rw [hf.leftInverse_leftInverse]

Premises used: ContinuousLinearMap.HasLeftInverse.leftInverse_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
inst_7 : T1Space F
hf : f.HasLeftInverse
inst_8 : IsTopologicalAddGroup F
rw : IsClosed (↑((↑f : E →ₗ[R] F) ∘ₗ (↑hf.leftInverse : F →ₗ[R] E) - LinearMap.id).ker : Set F)
⊢ IsClosed.{u_10} (X := F) (range.{u_10, u_8 + 1} (ι := E) (⇑f : (a : E) → F))

Tactic:
rw [← f.range_toLinearMap, ← f.coe_range,
    f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)]

Premises used: ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse, ContinuousLinearMap.range_toLinearMap, ContinuousLinearMap.toLinearMap, LinearMap.coe_range, LinearMap.range_eq_ker_of_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
inst_7 : T1Space F
hf : f.HasLeftInverse
inst_8 : IsTopologicalAddGroup F
⊢ IsClosed (↑((↑f : E →ₗ[R] F) ∘ₗ (↑hf.leftInverse : F →ₗ[R] E) - LinearMap.id).ker : Set F)

Tactic:
((f.comp hf.leftInverse) - (ContinuousLinearMap.id R F)).isClosed_ker

Premises used: ContinuousLinearMap.comp, HSub.hSub, ContinuousLinearMap.isClosed_ker, ContinuousLinearMap.id, 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
inst_7 : T1Space F
hf : f.HasLeftInverse
inst_8 : IsTopologicalAddGroup F
⊢ IsClosed (↑((↑f : E →ₗ[R] F) ∘ₗ (↑hf.leftInverse : F →ₗ[R] E) - LinearMap.id).ker : Set F)

Tactic:
exact ((f.comp hf.leftInverse) - (ContinuousLinearMap.id R F)).isClosed_ker

Premises used: ContinuousLinearMap.comp, HSub.hSub, ContinuousLinearMap.isClosed_ker, ContinuousLinearMap.id, 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
inst_7 : T1Space F
h : f.HasLeftInverse
⊢ IsClosed (↑h.complement : Set F)

Tactic:
h.closedComplemented_range.isClosed_complement

Premises used: Submodule.ClosedComplemented.isClosed_complement, ContinuousLinearMap.HasLeftInverse.closedComplemented_range
-- 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
h : f.HasLeftInverse
⊢ IsCompl (↑f : E →ₗ[R] F).range h.complement

Tactic:
h.closedComplemented_range.isCompl_complement

Premises used: Submodule.ClosedComplemented.isCompl_complement, ContinuousLinearMap.HasLeftInverse.closedComplemented_range, ContinuousLinearMap.HasLeftInverse.complement
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
rw : (↑f : E →ₗ[R] F).ker = ⊥
⊢ LinearMap.ker (M₂ := ↥(↑f : E →ₗ[R] F).range) (↑f.rangeRestrict : E →ₗ[R] ↥(↑f : E →ₗ[R] F).range) = ⊥

Tactic:
rw [ker_codRestrict]

Premises used: ContinuousLinearMap.ker_codRestrict
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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 : E →ₗ[R] F).ker = ⊥

Tactic:
LinearMap.ker_eq_bot.mpr hf

Premises used: Iff.mpr, LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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 : E →ₗ[R] F).ker = ⊥

Tactic:
exact LinearMap.ker_eq_bot.mpr hf

Premises used: Iff.mpr, LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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) = ⊥

Tactic:
have : (f.rangeRestrict).ker = ⊥ := by
    rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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) = ⊥
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
⊢ f.HasLeftInverse

Tactic:
obtain ⟨p, hp⟩ := hf''
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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

Tactic:
⟨(f.leftInverse_of_injective_of_isClosed_range hf hf').comp p, fun x ↦ ?_⟩

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

Tactic:
refine ⟨(f.leftInverse_of_injective_of_isClosed_range hf hf').comp p, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : E
⊢ Membership.mem (α := F) (↑f : E →ₗ[R] F).range ((f : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.ContinuousInverse
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
x : E
⊢ (f.leftInverse_of_injective_of_isClosed_range hf hf' ∘SL p : (a : F) → E) ((f : (a : E) → F) x : F) = x

Tactic:
simpa [hp ⟨f x, by simp⟩] using f.rangeRestrict.leftInverse_apply_of_inj this x

Premises used: Subtype.mk, LinearMap.leftInverse_apply_of_inj, 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
h : f.HasRightInverse
⊢ RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑h.rightInverse : (a : F) → E) (⇑f : (a : E) → F)

Tactic:
Classical.choose_spec h

Premises used: Classical.choose_spec
-- 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 : f.HasRightInverse
⊢ Surjective.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
h.rightInverse_rightInverse.surjective

Premises used: ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse, Function.RightInverse.surjective
-- 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.HasRightInverse
hfg : g = f
⊢ g.HasRightInverse

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 : E →L[R] F) ∘SL (↑f.symm : F →L[R] E) = ContinuousLinearMap.id R F

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) ((⋯.rightInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)
⊢ ⋯.rightInverse = (↑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_4 + 1} (α := F) ((f : (a : E) → F) ((⋯.rightInverse : (a : F) → E) y : E) : F)
    ((f : (a : E) → F) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E) : F)

Tactic:
simpa using f.hasRightInverse.rightInverse_rightInverse y

Premises used: ContinuousLinearEquiv.hasRightInverse, ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse
-- 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) ((⋯.rightInverse : (a : F) → E) y : E) (((↑f.symm : F →L[R] E) : (a : F) → E) y : E)

Tactic:
exact f.injective <| by simpa using f.hasRightInverse.rightInverse_rightInverse y

Premises used: ContinuousLinearEquiv.injective
-- 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).HasRightInverse
⊢ f.HasRightInverse

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).HasRightInverse

Tactic:
e.hasRightInverse

Premises used: ContinuousLinearEquiv.hasRightInverse
-- 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).HasRightInverse

Tactic:
exact e.hasRightInverse

Premises used: ContinuousLinearEquiv.hasRightInverse
-- 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.HasRightInverse
hg : g.HasRightInverse
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
⊢ (f.prodMap g).HasRightInverse

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.HasRightInverse
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
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
⊢ (f.prodMap g).HasRightInverse

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 : 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')
h :
  RightInverse (α := E × E') (β := F × F') (⇑(finv.prodMap ginv) : (a : F × F') → E × E')
    (⇑(f.prodMap g) : (a : E × E') → F × F')
⊢ (f.prodMap g).HasRightInverse

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 : 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')
⊢ RightInverse (α := 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.HasRightInverse
hf : f.HasRightInverse
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
⊢ (g ∘SL f).HasRightInverse

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.HasRightInverse
finv : F →L[R] E
hfinv : RightInverse.{u_2 + 1, u_4 + 1} (α := E) (β := F) (⇑finv : (a : F) → E) (⇑f : (a : E) → F)
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
⊢ (g ∘SL f).HasRightInverse

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 : 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

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

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

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 : 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
simp : (g : (a : F) → G) ((f : (a : E) → F) ((finv : (a : F) → E) ((ginv : (a : G) → F) x : F) : E) : F) = x
⊢ (g ∘SL f : (a : E) → G) ((finv ∘SL ginv : (a : G) → E) x : E) = x

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

Premises used: ContinuousLinearMap.coe_comp', Function.comp_apply