awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ Tendsto.{u_7, 0} (α := E) norm (𝓝 0) (𝓝 0)
have a : Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
Tactic: suffices Continuous p from this.tendsto' 0 _ (map_zero p)
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
have a : ∀ (r : ℝ) (hr : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)),
  Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
Tactic: rcases h₁ with ⟨r, hr⟩
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
have a : ∀ (i' : ι), p' i' → ∃ (i : ℝ), 0 < i ∧ {y : E | ‖y‖ < i} ⊆ s i'
Tactic: rw [(@NormedAddGroup.nhds_zero_basis_norm_lt E
      p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}
have rw : 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}
Tactic: rw [uniformSpace_eq_of_hasBasis p hb h₁ h₂]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}
have simp : 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (-x.1 + x.2) < r}
Tactic: simp only [sub_eq_add_neg, ← map_neg_add p]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
Tactic: have xεpos : 0 < (p x) / ε := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (n : ℤ) (hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))),
  ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
Tactic: rcases exists_mem_Ico_zpow xεpos hc with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have cpos : 0 < ‖c‖
Tactic: have cpos : 0 < ‖c‖ := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ 0 < ‖c ^ (n + 1)‖
have rw : 0 < ‖c‖ ^ (n + 1)
Tactic: rw [norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have cnpos : 0 < ‖c ^ (n + 1)‖
Tactic: have cnpos : 0 < ‖c ^ (n + 1)‖ := by rw [norm_zpow]; exact xεpos.trans hn.2
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have refine_1 : c ^ (-(n + 1)) ≠ 0
Tactic: refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_1 : c ^ (-(n + 1)) ≠ 0
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have refine_2 : (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε
Tactic: refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_1 : c ^ (-(n + 1)) ≠ 0
refine_2 : (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have refine_3 : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x)
Tactic: refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
refine_1 : c ^ (-(n + 1)) ≠ 0
refine_2 : (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε
refine_3 : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x)
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have refine_4 : ‖c ^ (-(n + 1))‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
Tactic: refine ⟨-(n + 1), ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x) < ε
have refine_2 : (p : (a : E) → ℝ) x < ‖c‖ ^ (n + 1) * ε
Tactic: rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff₀ cnpos, mul_comm,
        norm_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ (-(n + 1)) • x)
have refine_3 : ‖c‖ ^ n * ε ≤ (p : (a : E) → ℝ) x
Tactic: rw [zpow_neg, div_le_iff₀ cpos, map_smul_eq_mul, norm_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos),
        zpow_one, mul_inv_rev, mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel₀ (ne_of_gt cpos),
        one_mul, ← div_eq_inv_mul, le_div_iff₀ (zpow_pos cpos _), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c ^ (-(n + 1))‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
Tactic: have : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
⊢ ‖c ^ (-(n + 1))‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
have refine_4 : ‖c‖ ^ n * ‖c‖ ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε * ‖c‖
Tactic: rw [zpow_neg, norm_inv, inv_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one, this,
        ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ) = HMul.hMul (β := ℝ) ε⁻¹ ((p : (a : E) → ℝ) x : ℝ) * ‖c‖
⊢ ‖c‖ ^ n * ‖c‖ ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε * ‖c‖
have refine_4 : ‖c‖ ^ n ≤ HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p q : Seminorm 𝕜 E
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    ε / ‖c‖ ≤ (p : (a : E) → ℝ) x →
      (p : (a : E) → ℝ) x < ε → (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (δ : 𝕜) (hδ : δ ≠ 0) (δxle : (p : (a : E) → ℝ) (δ • x) < ε) (leδx : ε / ‖c‖ ≤ (p : (a : E) → ℝ) (δ • x)),
  (q : (a : E) → ℝ) x ≤ HMul.hMul (β := ℝ) C ((p : (a : E) → ℝ) x : ℝ)
Tactic: rcases p.rescale_to_shell hc ε_pos hx with ⟨δ, hδ, δxle, leδx, -⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
hx : ∃ j ∈ s, Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
have rcases : ∀ (j : ι) (hj : j ∈ s) (hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)),
  LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
Tactic: rcases hx with ⟨j, hj, hjx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (hypothesis)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
have this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: have : (s.sup p) x ≠ 0 :=
    ne_of_gt ((hjx.symm.lt_of_le <| apply_nonneg _ _).trans_le (le_finset_sup_apply hj))
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • s.sup p : (a : E) → ℝ) x : ℝ)
have refine : ∀ (y : E) (hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y) (hlt : (s.sup p : (a : E) → ℝ) y < ε),
  LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
Tactic: refine (s.sup p).bound_of_shell_smul q ε_pos hc (fun y hle hlt ↦ ?_) this
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
have rcases : ∀ (i : ι) (hi : i ∈ s) (hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)),
  LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
Tactic: rcases exists_apply_eq_finset_sup p ⟨j, hj⟩ y with ⟨i, hi, hiy⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (x : E),
    (∀ i ∈ s, (p i : (a : E) → ℝ) x < ε) →
      ∀ j ∈ s,
        ε / ‖c‖ ≤ (p j : (a : E) → ℝ) x → LE.le (α := ℝ) ((q : (a : E) → ℝ) x : ℝ) ((C • p j : (a : E) → ℝ) x : ℝ)
x : E
j : ι
hj : j ∈ s
hjx : Ne (α := ℝ) ((p j : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : Ne (α := ℝ) ((s.sup p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
y : E
hle : ε / ‖c‖ ≤ (s.sup p : (a : E) → ℝ) y
hlt : (s.sup p : (a : E) → ℝ) y < ε
i : ι
hi : i ∈ s
hiy : Eq (α := ℝ) ((s.sup p : (a : E) → ℝ) y : ℝ) ((p i : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((q : (a : E) → ℝ) y : ℝ) ((C • s.sup p : (a : E) → ℝ) y : ℝ)
have rw : (q : (a : E) → ℝ) y ≤ HSMul.hSMul (β := ℝ) C ((p i : (a : E) → ℝ) y : ℝ)
Tactic: rw [smul_apply, hiy]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
⊢ BddAbove (range p)
have rw : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
Tactic: rw [Seminorm.bddAbove_range_iff]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
have obtain : ∀ (c : 𝕜) (hc₀ : c ≠ 0) (hc : c • x ∈ s), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
Tactic: obtain ⟨c, hc₀, hc⟩ : ∃ c ≠ 0, (c : 𝕜) • x ∈ s :=
    (eventually_mem_nhdsWithin.and (hs.eventually_nhdsNE_zero x)).exists
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
have rcases : ∀ (M : ℝ) (hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M),
  BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
Tactic: rcases h _ hc with ⟨M, hM⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
have refine : ∀ (i : ι), HMul.hMul (β := ℝ) ‖c‖ ((p i : (a : E) → ℝ) x : ℝ) ≤ M
Tactic: refine ⟨M / ‖c‖, forall_mem_range.mpr fun i ↦ (le_div_iff₀' (norm_pos_iff.2 hc₀)).2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Seminorm.ball (normSeminorm 𝕜 E) = Metric.ball
have h : ∀ (x : E) (r : ℝ) (y : E), y ∈ Seminorm.ball (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.ball x r
Tactic: ext x r y
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Seminorm.closedBall (normSeminorm 𝕜 E) = Metric.closedBall
have h : ∀ (x : E) (r : ℝ) (y : E), y ∈ Seminorm.closedBall (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.closedBall x r
Tactic: ext x r y
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent.{u_3, u_7} 𝕜 (α := E) (Metric.ball 0 r)
have rw : Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
Tactic: rw [← ball_normSeminorm 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Metric.ball x r)
have rw : Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)
Tactic: rw [← ball_normSeminorm 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced.{u_3, u_7} 𝕜 (E := E) (Metric.ball 0 r)
have rw : Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
Tactic: rw [← ball_normSeminorm 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced.{u_3, u_7} 𝕜 (E := E) (Metric.closedBall 0 r)
have rw : Balanced 𝕜 (Seminorm.closedBall (normSeminorm 𝕜 E) 0 r)
Tactic: rw [← closedBall_normSeminorm 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ rexp (arcosh x) = x + √(HPow.hPow (β := ℕ) x 2 - 1)
have hx₁ : 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: apply exp_log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1))⁻¹ = x - √(HPow.hPow (β := ℕ) x 2 - 1)
have a : (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1
Tactic: apply inv_eq_of_mul_eq_one_right