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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
refine :
  ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
refine₁ :
  ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
refine₂ :
  ((↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)) →
    ∀ (hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤) (c : ℝ≥0)
      (hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)),
      Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)

Tactic:
refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤

Tactic:
simpa [SetLike.ext'_iff] using h.2.denseRange.closure_eq

Premises used: Function.Surjective.denseRange, Dense.closure_eq, And.right, SetLike.ext'_iff
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤

Tactic:
case eq_top => simpa [SetLike.ext'_iff] using h.2.denseRange.closure_eq

Premises used: Function.Surjective.denseRange, Dense.closure_eq, And.right, SetLike.ext'_iff
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)

Tactic:
⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearEquiv.ofBijective, Exists.intro
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
refine_1 : (↑f : E →ₛₗ[σ] F).ker = ⊥
refine_2 : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)

Tactic:
refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ (↑f : E →ₛₗ[σ] F).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
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ (↑f : E →ₛₗ[σ] F).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
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)

Tactic:
case anti =>
    refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩ <;>
    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
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
rwa : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
rwa₁ : (↑f : E →ₛₗ[σ] F).range = ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.range_eq_top, ContinuousLinearMap.closed_range_of_antilipschitz
-- 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
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
case : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
case₁ : (↑f : E →ₛₗ[σ] F).range = ⊤
case₂ case₃ case₄ case₅ : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
case surj => rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]

Premises used: ContinuousLinearMap.coe_coe, LinearMap.range_eq_top, ContinuousLinearMap.closed_range_of_antilipschitz
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
rw : UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
⊢ ∃ (C' : ℝ), ∀ (i : ι), ‖g i‖ ≤ C'

Tactic:
rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]

Premises used: NormedSpace.equicontinuous_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)

Tactic:
(norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Premises used: WithSeminorms.banach_steinhaus, norm_withSeminorms
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
refine :
  ∀ (x : Fin 1) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)

Tactic:
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Premises used: WithSeminorms.banach_steinhaus, norm_withSeminorms
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
x_1 : Fin 1
x : E
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))

Tactic:
simpa [bddAbove_def, forall_mem_range] using h x

Premises used: Set.forall_mem_range, bddAbove_def
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
rw : UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
⊢ LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑‖g i‖₊ : ℝ≥0∞)) ∞

Tactic:
rw [show ((⨆ i, ↑‖g i‖₊) < ∞) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 8 2]

Premises used: NormedSpace.equicontinuous_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)

Tactic:
(norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Premises used: WithSeminorms.banach_steinhaus, norm_withSeminorms
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
refine :
  ∀ (x : Fin 1) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)

Tactic:
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)

Premises used: WithSeminorms.banach_steinhaus, norm_withSeminorms
-- Module: Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
x_1 : Fin 1
x : E
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))

Tactic:
simpa [← NNReal.bddAbove_coe, ← Set.range_comp] using ENNReal.iSup_coe_lt_top.1 (h x)

Premises used: Set.range_comp, ENNReal.iSup_coe_lt_top, Iff.mp, NNReal.bddAbove_coe
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
r : ℝ
hr : 0 < r
⊢ norm.{u_5} (E := F) 0 < r

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
refine :
  ∀ (h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)),
    Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F) ↔
    Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)
rw :
  Subset.{u_5} (α := Set F) (ball 0 r)
    (Set.range.{u_5, u_4 + 1} (ι := E)
      (⇑(↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F) : (a : E) → F))
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe]

Premises used: LinearMap.coe_coe, ball_zero_subset_range_iff_surjective
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)
simp_rw :
  ∀ (x : F),
    Membership.mem (γ := Set F) (ball 0 r) x →
      Membership.mem (γ := Submodule 𝕜₂ F)
        (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x
⊢ Subset.{u_5} (α := Set F) (ball 0 r)
    (Set.range.{u_5, u_4 + 1} (ι := E)
      (⇑(↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F) : (a : E) → F))

Tactic:
simp_rw [← LinearMap.coe_range, Set.subset_def, SetLike.mem_coe] at h ⊢

Premises used: Set.subset_def, LinearMap.coe_range, SetLike.mem_coe
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
_ :
  Membership.mem (γ := Set F) (ball 0 r) x_1 →
    Membership.mem (γ := Submodule 𝕜₂ F)
      (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x_1
⊢ Membership.mem (γ := Set F) (ball 0 r) x_1 →
    Membership.mem (γ := Submodule 𝕜₂ F)
      (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x_1

Tactic:
_
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
h_1 : Membership.mem (γ := Set F) (ball 0 r) x_1
rw :
  Membership.mem (γ := Submodule 𝕜₂ F)
    (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) (x_1 + x)
⊢ Membership.mem (γ := Submodule 𝕜₂ F)
    (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x_1

Tactic:
rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self hr)]

Premises used: LinearMap.range, Metric.mem_ball_self, SemilinearMapClass.semilinearMap, Submodule.add_mem_iff_left
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
h_1 : Membership.mem (γ := Set F) (ball 0 r) x_1
a : x_1 + x ∈ ball x r
⊢ Membership.mem (γ := Submodule 𝕜₂ F)
    (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) (x_1 + x)

Tactic:
apply h
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
h_1 : Membership.mem (γ := Set F) (ball 0 r) x_1
⊢ x_1 + x ∈ ball x r

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    closedBall x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)

Tactic:
simp_all