awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
choose :
  ∀ (C : ℝ) (hC : C > 0) (fsymm : (y : F) → E) (h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖),
    ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
⊢ ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm

Tactic:
choose C hC fsymm h using
    exists_preimage_norm_le _ (LinearMap.range_eq_top.1 hsurj)

Premises used: ContinuousLinearMap.exists_preimage_norm_le, LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
C : ℝ
hC : C > 0
fsymm : (y : F) → E
h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
h₁ :
  0 <
    NonlinearRightInverse.nnnorm.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) (f := f)
      { toFun := fsymm, nnnorm := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯, bound' := ⋯, right_inv' := ⋯ :
        f.NonlinearRightInverse }
⊢ ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm

Tactic:
use {
      toFun := fsymm
      nnnorm := ⟨C, hC.lt.le⟩
      bound' := fun y => (h y).2
      right_inv' := fun y => (h y).1 }
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
C : ℝ
hC : C > 0
fsymm : (y : F) → E
h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ 0 <
    NonlinearRightInverse.nnnorm.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) (f := f)
      { toFun := fsymm, nnnorm := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯, bound' := ⋯, right_inv' := ⋯ :
        f.NonlinearRightInverse }

Tactic:
hC
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
C : ℝ
hC : C > 0
fsymm : (y : F) → E
h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ 0 <
    NonlinearRightInverse.nnnorm.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) (f := f)
      { toFun := fsymm, nnnorm := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C ⋯, bound' := ⋯, right_inv' := ⋯ :
        f.NonlinearRightInverse }

Tactic:
exact hC
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
rw : 0 < (Classical.choose (p := fun (x : f.NonlinearRightInverse) ↦ 0 < x.nnnorm) ⋯).nnnorm
⊢ 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm

Tactic:
rw [nonlinearRightInverseOfSurjective]

Premises used: ContinuousLinearMap.nonlinearRightInverseOfSurjective
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ 0 < (Classical.choose (p := fun (x : f.NonlinearRightInverse) ↦ 0 < x.nnnorm) ⋯).nnnorm

Tactic:
Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

Premises used: ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, Classical.choose_spec
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ 0 < (Classical.choose (p := fun (x : f.NonlinearRightInverse) ↦ 0 < x.nnnorm) ⋯).nnnorm

Tactic:
exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

Premises used: ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective, Classical.choose_spec
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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)
rw :
  ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e.symm : (a : F) → E) ⁻¹' s)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e.symm : (a : F) → E)

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e : (a : E) → F) '' s)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e.symm : (a : F) → E) ⁻¹' s)

Tactic:
rw [← e.image_eq_preimage_symm]

Premises used: LinearEquiv.image_eq_preimage_symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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
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)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e : (a : E) → F) '' s)

Tactic:
rw [← e.coe_coe] at h ⊢

Premises used: LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
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 : 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:
ContinuousLinearMap.isOpenMap (σ := σ) ⟨_, h⟩ e.surjective s hs

Premises used: ContinuousLinearMap.mk, LinearEquiv.surjective, ContinuousLinearMap.isOpenMap
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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 : 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:
exact ContinuousLinearMap.isOpenMap (σ := σ) ⟨_, h⟩ e.surjective s hs

Premises used: ContinuousLinearMap.mk, LinearEquiv.surjective, ContinuousLinearMap.isOpenMap
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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)
⊢ Eq (α := (a : E) → F) (⇑(e.toContinuousLinearEquivOfContinuous h) : (a : E) → F) (⇑e : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
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)
⊢ Eq (α := (a : F) → E) (⇑(e.toContinuousLinearEquivOfContinuous h).symm : (a : F) → E) (⇑e.symm : (a : F) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
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 : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hclo :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_4, u_3 + 1} (ι := E) (⇑f : (a : E) → F))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_2, u_3, u_4} σ E ↥(↑f : E →ₛₗ[σ] F).range)
    ((↑(equivRange hinj hclo) : ContinuousLinearMap.{u_1, u_2, u_3, u_4} σ E ↥(↑f : E →ₛₗ[σ] F).range) :
      ContinuousLinearMap.{u_1, u_2, u_3, u_4} σ E ↥(↑f : E →ₛₗ[σ] F).range)
    (f.rangeRestrict : ContinuousLinearMap.{u_1, u_2, u_3, u_4} σ E ↥(↑f : E →ₛₗ[σ] F).range)

Tactic:
rfl

Premises used: ContinuousLinearMap.codRestrict, LinearMap.codRestrict, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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 : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hclo :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_4, u_3 + 1} (ι := E) (⇑f : (a : E) → F))
⊢ Eq (α := (a : E) → ↥(↑f : E →ₛₗ[σ] F).range) (⇑(equivRange hinj hclo) : (a : E) → ↥(↑f : E →ₛₗ[σ] F).range)
    (⇑f.rangeRestrict : (a : E) → ↥(↑f : E →ₛₗ[σ] F).range)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
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 : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hclo :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_4, u_3 + 1} (ι := E) (⇑f : (a : E) → F))
⊢ Eq (α := LinearEquiv.{u_2, u_1, u_4, u_3} σ' (↥(↑f : E →ₛₗ[σ] F).range) E)
    (LinearEquiv.symm (↑(equivRange hinj hclo) : E ≃ₛₗ[σ] ↥(↑f : E →ₛₗ[σ] F).range))
    (LinearEquiv.symm (LinearEquiv.ofInjective (↑f : E →ₛₗ[σ] F) hinj))

Tactic:
rfl

Premises used: LinearEquiv.ofLeftInverse, LinearEquiv.ofInjective, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f_1 : E →SL[σ] 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 : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hclo :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_4, u_3 + 1} (ι := E) (⇑f : (a : E) → F))
x : E
⊢ Membership.mem (α := F) (↑f : E →ₛₗ[σ] F).range ((f : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : 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 : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hclo :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_4, u_3 + 1} (ι := E) (⇑f : (a : E) → F))
x : E
⊢ (ContinuousLinearEquiv.symm (equivRange hinj hclo) : (a : ↥(↑f : E →ₛₗ[σ] F).range) → E)
      (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₛₗ[σ] F).range) ((f : (a : E) → F) x) ⋯ : ↥(↑f : E →ₛₗ[σ] F).range) =
    x

Tactic:
simp [ContinuousLinearEquiv.symm_apply_eq, Subtype.ext_iff]

Premises used: Subtype.ext_iff, ContinuousLinearEquiv.symm_apply_eq
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
hf' :
  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)

Tactic:
⟨_, .comp (.subtype_coe (Set.range f)) (f.equivRange hf hf').antilipschitz⟩

Premises used: ContinuousLinearEquiv.antilipschitz, AntilipschitzWith.subtype_coe, AntilipschitzWith.comp, Exists.intro, Set.range, DFunLike.coe, ContinuousLinearMap.equivRange
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
⊢ AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
    (⇑f : (a : E) → F)

Tactic:
Classical.choose_spec (f.antilipschitz_of_injective_of_isClosed_range hf hf')

Premises used: Classical.choose_spec, ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range, ContinuousLinearMap.antilipschitzConstant_of_injective_of_isClosed_range
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)

Tactic:
⟨fun h ↦ f.antilipschitz_of_injective_of_isClosed_range hf h, fun h ↦ ?_⟩

Premises used: ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range, Iff.intro
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
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))
⊢ 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)

Tactic:
refine ⟨fun h ↦ f.antilipschitz_of_injective_of_isClosed_range hf h, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
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))
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))

Tactic:
choose K hf' using h
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
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:
hf'.isClosed_range f.uniformContinuous

Premises used: AntilipschitzWith.isClosed_range, ContinuousLinearMap.uniformContinuous
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
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:
exact hf'.isClosed_range f.uniformContinuous

Premises used: AntilipschitzWith.isClosed_range, ContinuousLinearMap.uniformContinuous