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_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
⊢ dist x 0 ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) 0 : F)

Tactic:
have aux := hfK.le_mul_dist x 0
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  dist x 0 ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) 0 : F)
⊢ ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simp only [dist_zero_right, map_zero] at aux

Premises used: map_zero, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)

Tactic:
aux
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
h :
  ((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
          LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
        (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
      (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
        ↥(↑f : E →ₗ[𝕜] F).range) =
    x
⊢ norm.{u_5} (E := E)
      (((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
              LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
            (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
          (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
            ↥(↑f : E →ₗ[𝕜] F).range) :
        E) ≤
    (↑K : ℝ) *
      norm.{u_6} (E := ↥(↑f : E →ₗ[𝕜] F).range)
        (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
          ↥(↑f : E →ₗ[𝕜] F).range)

Tactic:
convert! aux
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
rw : (↑f : E →ₗ[𝕜] F).ker = ⊥
⊢ LinearMap.ker (M₂ := ↥(↑f : E →ₗ[𝕜] F).range) (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) = ⊥

Tactic:
rw [ker_codRestrict]

Premises used: ContinuousLinearMap.ker_codRestrict
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ (↑f : E →ₗ[𝕜] F).ker = ⊥

Tactic:
LinearMap.ker_eq_bot.mpr hf

Premises used: Iff.mpr, LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ (↑f : E →ₗ[𝕜] F).ker = ⊥

Tactic:
exact LinearMap.ker_eq_bot.mpr hf

Premises used: Iff.mpr, LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜 E_1
F_1 : Type u_4
inst_4 : NormedAddCommGroup F_1
inst_5 : NormedSpace 𝕜' F_1
f_1 : E_1 →SL[σ] F_1
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F_1
inst_10 : CompleteSpace E_1
inst_11 : RingHomInvPair σ' σ
f_2 : E_1 →SL[σ] F_1
E : Type u_5
F : Type u_6
inst_12 : NormedAddCommGroup E
inst_13 : NormedSpace 𝕜 E
inst_14 : NormedAddCommGroup F
inst_15 : NormedSpace 𝕜 F
inst_16 : CompleteSpace E
inst_17 : CompleteSpace F
f : E →L[𝕜] F
hf : Injective.{u_5 + 1, u_6 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
hf' :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range.{u_6, u_5 + 1} (ι := E) (⇑f : (a : E) → F))
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith.{u_5, u_6} (α := E) (β := F) (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf')
  (⇑f : (a : E) → F) :=
  ⋯
x : E
aux :
  ‖x‖ ≤
    (↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') : ℝ) *
      norm.{u_6} (E := F) ((f : (a : E) → F) x : F)
⊢ ((LinearMap.leftInverse (↑f.rangeRestrict : E →ₗ[𝕜] ↥(↑f : E →ₗ[𝕜] F).range) :
          LinearMap.{u_1, u_1, u_6, u_5} (RingHom.id 𝕜) (↥(↑f : E →ₗ[𝕜] F).range) E) :
        (a : ↥(↑f : E →ₗ[𝕜] F).range) → E)
      (Subtype.mk (p := fun (x : F) ↦ x ∈ (↑f : E →ₗ[𝕜] F).range) (((↑f : E →ₗ[𝕜] F) : (a : E) → F) x) ⋯ :
        ↥(↑f : E →ₗ[𝕜] F).range) =
    x

Tactic:
exact f.rangeRestrict.leftInverse_apply_of_inj
      (by rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf) x

Premises used: LinearMap.leftInverse_apply_of_inj
-- 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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(LinearEquiv.ofBijective (↑f : E →ₛₗ[σ] F) ⋯) : (a : E) → F)

Tactic:
f.continuous

Premises used: ContinuousLinearMap.continuous
-- 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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(LinearEquiv.ofBijective (↑f : E →ₛₗ[σ] F) ⋯) : (a : E) → F)

Tactic:
exact f.continuous

Premises used: ContinuousLinearMap.continuous
-- 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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ Eq (α := (a : E) → F) (⇑(ofBijective f hinj hsurj) : (a : E) → F) (⇑f : (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 σ' σ
f : E →SL[σ] F
hinj : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
h :
  ∀ (x : E),
    Eq.{u_4 + 1} (α := F) (((↑(ofBijective f hinj hsurj) : E →SL[σ] F) : (a : E) → F) x : F) ((f : (a : E) → F) x : F)
⊢ (↑(ofBijective f hinj hsurj) : E →SL[σ] F) = f

Tactic:
ext
-- 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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
x : E
⊢ Eq.{u_4 + 1} (α := F) (((↑(ofBijective f hinj hsurj) : E →SL[σ] F) : (a : E) → F) x : F) ((f : (a : E) → F) x : F)

Tactic:
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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
x : E
⊢ (ContinuousLinearEquiv.symm (ofBijective f hinj hsurj) : (a : F) → E) ((f : (a : E) → F) x : F) = x

Tactic:
(ofBijective f hinj hsurj).symm_apply_apply x

Premises used: ContinuousLinearEquiv.ofBijective, ContinuousLinearEquiv.symm_apply_apply
-- 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 : (↑f : E →ₛₗ[σ] F).ker = ⊥
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
y : F
⊢ (f : (a : E) → F) ((ContinuousLinearEquiv.symm (ofBijective f hinj hsurj) : (a : F) → E) y : E) = y

Tactic:
(ofBijective f hinj hsurj).apply_symm_apply y

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.ofBijective
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
mp : IsUnit f → Bijective (α := E) (β := E) (⇑f : (a : E) → E)
mpr : Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f
⊢ IsUnit f ↔ Bijective (α := E) (β := E) (⇑f : (a : E) → E)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : (E →L[𝕜] E)ˣ
⊢ Bijective (α := E) (β := E) (⇑(↑f : E →L[𝕜] E) : (a : E) → E)

Tactic:
ofUnit f |>.bijective

Premises used: ContinuousLinearEquiv.bijective, ContinuousLinearEquiv.ofUnit
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : (E →L[𝕜] E)ˣ
⊢ Bijective (α := E) (β := E) (⇑(↑f : E →L[𝕜] E) : (a : E) → E)

Tactic:
exact ofUnit f |>.bijective

Premises used: ContinuousLinearEquiv.bijective, ContinuousLinearEquiv.ofUnit
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f

Tactic:
fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩

Premises used: IsUnit, ContinuousLinearEquiv.ofBijective, Exists.intro, ContinuousLinearEquiv.toUnit, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
mpr : ∀ (h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)), (↑f : E →ₗ[𝕜] E).ker = ⊥
mpr₁ : ∀ (h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)), (↑f : E →ₗ[𝕜] E).range = ⊤
⊢ Bijective (α := E) (β := E) (⇑f : (a : E) → E) → IsUnit f

Tactic:
refine fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)
⊢ (↑f : E →ₗ[𝕜] E).ker = ⊥

Tactic:
simp only [LinearMap.range_eq_top, LinearMap.ker_eq_bot, f.coe_coe, h.1, h.2]

Premises used: LinearMap.ker_eq_bot, ContinuousLinearMap.coe_coe, LinearMap.range_eq_top, And.right, And.left
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
h : Bijective (α := E) (β := E) (⇑f : (a : E) → E)
⊢ (↑f : E →ₗ[𝕜] E).range = ⊤

Tactic:
simp only [LinearMap.range_eq_top, LinearMap.ker_eq_bot, f.coe_coe, h.1, h.2]

Premises used: LinearMap.ker_eq_bot, ContinuousLinearMap.coe_coe, LinearMap.range_eq_top, And.right, And.left
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f ↔ IsUnit (↑f : E →ₗ[𝕜] E)

Tactic:
f.isUnit_iff_bijective.trans (Module.End.isUnit_iff _).symm

Premises used: Module.End.isUnit_iff, Iff.trans, Iff.symm, ContinuousLinearMap.isUnit_iff_bijective
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
h : ∀ (μ : 𝕜), μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 (↑f : E →ₗ[𝕜] E)
⊢ spectrum 𝕜 f = spectrum 𝕜 (↑f : E →ₗ[𝕜] E)

Tactic:
ext μ
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
h :
  ¬IsUnit
        (↑(HSub.hSub (α := E →L[𝕜] E) ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) μ : E →L[𝕜] E) f) : E →ₗ[𝕜] E) ↔
    ¬IsUnit
        (HSub.hSub (α := E →ₗ[𝕜] E) ((algebraMap 𝕜 (E →ₗ[𝕜] E) : (a : 𝕜) → E →ₗ[𝕜] E) μ : E →ₗ[𝕜] E) (↑f : E →ₗ[𝕜] E))
⊢ μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 (↑f : E →ₗ[𝕜] E)

Tactic:
rw [spectrum.mem_iff, spectrum.mem_iff, ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap]

Premises used: ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap, spectrum.mem_iff
-- Module: Mathlib.Analysis.Normed.Operator.Banach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
⊢ ¬IsUnit
        (↑(HSub.hSub (α := E →L[𝕜] E) ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) μ : E →L[𝕜] E) f) : E →ₗ[𝕜] E) ↔
    ¬IsUnit
        (HSub.hSub (α := E →ₗ[𝕜] E) ((algebraMap 𝕜 (E →ₗ[𝕜] E) : (a : 𝕜) → E →ₗ[𝕜] E) μ : E →ₗ[𝕜] E) (↑f : E →ₗ[𝕜] E))

Tactic:
rfl