awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
have refine : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)))
Tactic: refine Seminorm.continuous' (r := n + n) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 (HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)))
have rw : ∀ (hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x),
  Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}
Tactic: rw [p.closedBall_zero_eq] at hxn ⊢
Cleared hypotheses: hxn
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
⊢ Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}
have hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
Tactic: have hxn' : p x ≤ n := by convert! interior_subset hxn
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn : Membership.mem (γ := Set E) (interior {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) x
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
⊢ Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}
have hxn₁ : Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
  {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
Tactic: rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn
Cleared hypotheses: hxn, hxn'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
⊢ Membership.mem (γ := Filter E) (𝓝 0) {y : E | (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)}
have h : ∀ (y : E)
  (hy :
    Membership.mem (γ := Set E)
      (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)})
      y),
  (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: filter_upwards [hxn] with y hy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) (x + y - x) : ℝ)
have rw : Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) y : ℝ)
Tactic: rw [add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
n : ℕ
x : E
hxn :
  Membership.mem (γ := Filter E) (map (fun (x_1 : E) ↦ x + x_1) (𝓝 0))
    {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}
hxn' : LE.le (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)
y : E
hy :
  Membership.mem (γ := Set E)
    (preimage (β := E) (fun (x_1 : E) ↦ x + x_1) {y : E | LE.le (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((↑n : ℝ) : ℝ)}) y
⊢ (p : (a : E) → ℝ) y ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
have calc : Eq (α := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((p : (a : E) → ℝ) (x + y - x) : ℝ)
Tactic: calc p y = p (x + y - x) := by rw [add_sub_cancel_left]
      _ ≤ p (x + y) + p x := map_sub_le_add _ _ _
      _ ≤ n + n := add_le_add hy hxn'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)
have refine : ∀ (i : κ),
  BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (k : ι) ↦ (q i).comp ((toLinearMap ∘ 𝓕) k)) ∧
    Continuous[inst_7.toTopologicalSpace, _] (⨆ (k : ι), (⇑((q i).comp ((toLinearMap ∘ 𝓕) k)) : (a : E) → ℝ))
Tactic: refine (hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup (toLinearMap ∘ 𝓕)).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))
have rw : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ ((q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F) : (a : E) → ℝ) x)
Tactic: rw [Seminorm.bddAbove_range_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (q k : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
k : κ
⊢ BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (k_1 : ι) ↦ (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous[inst_7.toTopologicalSpace, _] (⨆ (k_1 : ι), (⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)) : (a : E) → ℝ))
have this : BddAbove.{u_6} (α := Seminorm 𝕜₁ E) (range fun (i : ι) ↦ (q k).comp (↑(𝓕 i) : E →ₛₗ[σ₁₂] F))
Tactic: have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) := by
    rw [Seminorm.bddAbove_range_iff]
    exact H k
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)
have hp : WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
  { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
  fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦ (↑p : Seminorm 𝕜₂ F)
Tactic: have hp := PolynormableSpace.withSeminorms 𝕜₂ F
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
⊢ UniformEquicontinuous.{u_2, u_7, u_6} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ 𝓕)
have refine : ∀ (k : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) (x : E),
  BddAbove (α := ℝ) (range fun (i : ι) ↦ ((↑k : Seminorm 𝕜₂ F) : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
Tactic: refine hp.banach_steinhaus ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
H : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ι) ↦ (𝓕 i : (a : E) → F) x)
hp :
  WithSeminorms.{u_5, u_7, u_7} (𝕜 := 𝕜₂) (E := F) (ι :=
    { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) })
    fun (p : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) ↦
    (↑p : Seminorm 𝕜₂ F)
⊢ ∀ (k : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }) (x : E),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ ((↑k : Seminorm 𝕜₂ F) : (a : F) → ℝ) ((𝓕 i : (a : E) → F) x : F))
have H₁ : ∀ (x : E) (i : { p : Seminorm 𝕜₂ F // Continuous[inst_8.toTopologicalSpace, _] (⇑p : (a : F) → ℝ) }),
  BddAbove (α := ℝ)
    (range.{0, u_2 + 1} (ι := ι)
      (Function.comp (β := F) (⇑(↑i : Seminorm 𝕜₂ F) : (a : F) → ℝ) fun (i : ι) ↦ (𝓕 i : (a : E) → F) x))
Tactic: simp_rw [hp.isVonNBounded_iff_seminorm_bddAbove, ← range_comp] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
⊢ Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun
have rcases : ∀ (u : ℕ → α) (hu : Tendsto u atTop l),
  Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun
Tactic: rcases l.exists_seq_tendsto with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ Continuous[inst_7.toTopologicalSpace, inst_8.toTopologicalSpace]
    (linearMapOfTendsto f (fun (a : α) ↦ (↑(g a) : E →ₛₗ[σ₁₂] F)) h).toFun
have refine : ∀ (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)
Tactic: refine (h.comp hu).continuous_of_equicontinuous
      (PolynormableSpace.banach_steinhaus ?_).equicontinuous
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace E
inst_8 : UniformSpace F
inst_9 : IsUniformAddGroup E
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₁ E
inst_12 : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst_13 : PolynormableSpace 𝕜₂ F
inst_14 : ContinuousSMul 𝕜₂ F
inst_15 : T2Space F
l : Filter α
inst_16 : l.IsCountablyGenerated
inst_17 : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun (n : α) (x : E) ↦ (g n : (a : E) → F) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
x : E
⊢ IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)
have rw : ∀ (h : ∀ (x : E), Tendsto (fun (i : α) ↦ (g i : (a : E) → F) x) l (𝓝 (f x))) (u : ℕ → α) (hu : Tendsto u atTop l)
  (x : E), IsVonNBounded.{u_5, u_7} 𝕜₂ (E := F) (range fun (i : ℕ) ↦ (g (u i) : (a : E) → F) x)
Tactic: rw [tendsto_pi_nhds] at h
Cleared hypotheses: u, hu, x
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
A B : Set E
⊢ (∃ (i : ℝ), True ∧ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Ici i) x → B ⊆ x • A) ↔
    ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
have simp : (∃ (i : ℝ), ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) (norm ⁻¹' Ici i) x → B ⊆ x • A) ↔
  ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
Tactic: simp only [true_and]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
x : 𝕜
h : ‖x‖ ≤ 1
⊢ HSMul.hSMul (β := Set E) x ∅ ⊆ ∅
have rw : Subset.{u_3} (α := Set E) ∅ ∅
Tactic: rw [smul_set_empty]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : MulActionHom.{u_1, u_1, u_3, u_4} (M := 𝕜) id E F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
h : x ∈ HSMul.hSMul (β := Set E) a ((⇑f : (a : E) → F) ⁻¹' s)
y : E
hy₁ : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hy₂ : (fun (x : E) ↦ a • x) y = x
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
have rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) y : F) ∈ s
Tactic: rw [mem_preimage, ← hy₂, map_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)
have simp_rw : Balanced 𝕜 (s + -t)
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun (x : E) ↦ c • x) t s
have rw : (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun (x : E) ↦ c⁻¹ • x) t s) ↔
  ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun (x : E) ↦ c • x) t s
Tactic: rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝 0, MapsTo (fun (x : E) ↦ c • x) t s
have rw : MapsTo (fun (x : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x) t s
Tactic: rw [← nhdsNE_sup_pure, Filter.eventually_sup, Filter.eventually_pure,
    ← absorbs_iff_eventually_nhdsNE_zero, and_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
⊢ a • s ⊆ b • s
have inl : ∀ (h : ‖a‖ ≤ norm.{u_1} (E := 𝕜) 0), a • s ⊆ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 s
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
inl : ∀ (h : ‖a‖ ≤ norm.{u_1} (E := 𝕜) 0), a • s ⊆ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 s
⊢ a • s ⊆ b • s
have inr : ∀ (hb : b ≠ 0), a • s ⊆ b • s
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ norm.{u_1} (E := 𝕜) 0
⊢ a • s ⊆ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 s
have h₁ : a = 0
Tactic: rw [norm_zero, norm_le_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s = b • (b⁻¹ • a) • s
have rw : a • s = b • b⁻¹ • a • s
Tactic: rw [smul_assoc, smul_inv_smul₀ hb]