awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this_1 : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (HVAdd.hVAdd (β := E) x 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
have h : ∀ (this : (sr.1.sup p).ball (x + 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2),
  (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Tactic: rwa [vadd_eq_add, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this_1 : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (HVAdd.hVAdd (β := E) x 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
h :
  ∀ (this : (sr.1.sup p).ball (x + 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2),
    (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
have h₁ : ∀ (this : (sr.1.sup p).ball x sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2),
  (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Tactic: rwa [vadd_eq_add, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
U : Set E
⊢ U ∈ 𝓝 x ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
have rw : (∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball x i.2 ⊆ U) ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
Tactic: rw [hp.hasBasis_ball.mem_iff, Prod.exists]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
U : Set E
rw : (∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball x i.2 ⊆ U) ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
⊢ U ∈ 𝓝 x ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
have rw₁ : (∃ (a : Finset ι) (b : ℝ), 0 < (a, b).2 ∧ ((a, b).1.sup p).ball x (a, b).2 ⊆ U) ↔
  ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
Tactic: rw [hp.hasBasis_ball.mem_iff, Prod.exists]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
⊢ IsOpen[inst_3] U ↔ ∀ x ∈ U, ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
have simp_rw : IsOpen[inst_3] U ↔ ∀ x ∈ U, U ∈ 𝓝 x
Tactic: simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ T1Space E
have this : IsTopologicalAddGroup E
Tactic: have := hp.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
⊢ T1Space E
have refine : IsClosed[inst_3] {0}
Tactic: refine IsTopologicalAddGroup.t1Space _ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
⊢ IsClosed[inst_3] {0}
have rw : ∀ (x : E), Membership.mem (γ := Set E) {0}ᶜ x → ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
Tactic: rw [← isOpen_compl_iff, hp.isOpen_iff_mem_balls]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
⊢ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
have obtain : ∀ (i : ι) (pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)),
  ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
Tactic: obtain ⟨i, pi_nonzero⟩ := h x hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
have refine : 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
Tactic: refine ⟨{i}, p i x, by positivity, subset_compl_singleton_iff.mpr ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
have rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
Tactic: rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
have rw₁ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (0 - x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
rw₁ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (0 - x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
have rw₂ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (-x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
rw₁ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (0 - x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₂ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (-x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
have rw₃ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
rw₁ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (0 - x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₂ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (-x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₃ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
have rw₄ : LE.le (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
Tactic: rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
⊢ ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
Tactic: have := ((t1Space_TFAE E).out 0 9).mp (inferInstance : T1Space E)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
⊢ ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have by_contra! : ∀ (h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ False
have refine : x ⤳ 0
Tactic: refine hx (this ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ x ⤳ 0
have rw : ∀ (i : Finset ι × ℝ), 0 < i.2 → x ∈ (i.1.sup p).ball 0 i.2
Tactic: rw [hp.hasBasis_zero_ball.specializes_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)) ↔ T1Space E
have refine : T1Space E → ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨WithSeminorms.T1_of_separating hp, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε
have rw : (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p : (a : E) → ℝ) (u x - y₀) < ε) ↔
  ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε
Tactic: rw [hp.tendsto_nhds' u y₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : SemilatticeSup F
inst_5 : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ Tendsto u atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε
have rw : (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i : (a : E) → ℝ) (u x - y₀) < ε) ↔
  ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε
Tactic: rw [hp.tendsto_nhds u y₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ WithSeminorms p
have inferInstance : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: refine
    ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
have rw : WithSeminorms p ↔
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
Tactic: rw [← p.filter_eq_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
have refine : ∀ (h : WithSeminorms p),
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
Tactic: refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
have rw : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
Tactic: rw [h.topology_eq_withSeminorms]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ t = ⨅ (i : ι), UniformSpace.toTopologicalSpace
have rw : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
Tactic: rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsTopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
    nhds_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
have a : ∀ (i : ι), Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)
Tactic: congrm _ = ⨅ i, ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
⊢ Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
have this : IsTopologicalAddGroup E
Tactic: have := hp.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
have rw : Continuous[⨅ (i : ι), PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑(p i) : (a : E) → ℝ)
Tactic: rw [p.withSeminorms_iff_topologicalSpace_eq_iInf.mp hp]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ WithSeminorms.{u_2, u_6, u_6} (𝕜 := 𝕜) (E := E) (ι := { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) })
    fun (p : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }) ↦ (↑p : Seminorm 𝕜 E)
have this : IsTopologicalAddGroup E
Tactic: have := hp.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ WithSeminorms.{u_2, u_6, u_6} (𝕜 := 𝕜) (E := E) (ι := { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) })
    fun (p : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }) ↦ (↑p : Seminorm 𝕜 E)
have hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
Tactic: have hp' (i : ι) : Continuous (p i) := hp.continuous_seminorm i
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
⊢ WithSeminorms.{u_2, u_6, u_6} (𝕜 := 𝕜) (E := E) (ι := { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) })
    fun (p : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }) ↦ (↑p : Seminorm 𝕜 E)
have rw : ∀ (hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)))
  (this : IsTopologicalAddGroup E) (hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)),
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at ⊢ hp
Cleared hypotheses: hp, this, hp'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
have refine_1 : LE.le.{u_6} (α := Filter E) (𝓝 0)
  (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
    comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
refine_1 :
  LE.le.{u_6} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
have refine_2 : LE.le.{u_6} (α := Filter E)
  (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
    comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
  (𝓝 0)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
⊢ LE.le.{u_6} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
have refine_1 : ∀ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
  Tendsto (α := E) (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0) (𝓝 0)
Tactic: simp_rw [le_iInf_iff, ← tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
⊢ LE.le.{u_6} (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (𝓝 0)
have refine_2 : ∀ (i : ι),
  LE.le (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
Tactic: simp_rw [hp, le_iInf_iff]