awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (iInf (seminormFromConst_seq c f x) ^ m))
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) fun (x_1 : ℕ) ↦
  seminormFromConst_seq c f x x_1 ^ m
Tactic: convert! (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).pow m using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) fun (x_1 : ℕ) ↦
    seminormFromConst_seq c f x x_1 ^ m
have h : ∀ (n : ℕ), seminormFromConst_seq c f (x ^ m) (m * n) = seminormFromConst_seq c f x n ^ m
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ seminormFromConst' c f x ≤ (f : (a : R) → ℝ) x
have apply : ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ (f : (a : R) → ℝ) x
Tactic: apply le_of_tendsto (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ (f : (a : R) → ℝ) x
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x
Tactic: simp only [eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x
have h : ∀ (b : ℕ), 1 ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
n : ℕ
hn : 1 ≤ n
⊢ seminormFromConst_seq c f x n ≤ (f : (a : R) → ℝ) x
have h : (f : (a : R) → ℝ) (x * c ^ n) ≤ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ)
Tactic: rw [seminormFromConst_seq, div_le_iff₀ (by positivity), ← hpm c hn]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
⊢ seminormFromConst_seq c f x = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) x
have h : ∀ (n : ℕ), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
n : ℕ
⊢ seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
have pos : ∀ (hn : n = 0), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
n : ℕ
pos : ∀ (hn : n = 0), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
⊢ seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
have neg : ∀ (hn : ¬n = 0), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 ((f : (a : R) → ℝ) x))
have hseq : seminormFromConst_seq c f x = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) x
Tactic: have hseq : seminormFromConst_seq c f x = fun _n ↦ f x := by
      ext n
      by_cases hn : n = 0
      · simp only [seminormFromConst_seq, hn, pow_zero, mul_one, div_one]
      · simp only [seminormFromConst_seq, hx (c ^ n), hpm _ (Nat.one_le_iff_ne_zero.mpr hn),
          mul_div_assoc, div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
hseq : seminormFromConst_seq c f x = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) x
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 ((f : (a : R) → ℝ) x))
have rw : Tendsto (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) x : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) x) : Filter ℝ)
Tactic: rw [hseq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (seminormFromConst' c f x * seminormFromConst' c f y))
have rw : Tendsto (seminormFromConst_seq c f (x * y)) atTop
  (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst' c f y)))
Tactic: rw [seminormFromConst_apply_of_isMul hf1 hc hpm hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
y : R
⊢ seminormFromConst_seq c f (x * y) = fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)
have h : ∀ (n : ℕ),
  seminormFromConst_seq c f (x * y) n = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hx :
  ∀ (y : R), (f : (a : R) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) y : ℝ)
y : R
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst' c f y)))
have hseq : seminormFromConst_seq c f (x * y) = fun (n : ℕ) ↦
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)
Tactic: have hseq : seminormFromConst_seq c f (x * y) =
        fun n ↦ f x * seminormFromConst_seq c f y n := by
      ext n
      simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ seminormFromConst_seq c f c = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) c
have h : ∀ (n : ℕ), seminormFromConst_seq c f c n = (f : (a : R) → ℝ) c
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₁ : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₂ : HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₂ :
  HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₃ : HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ((f : (a : R) → ℝ) c : ℝ) /
    HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₂ :
  HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ((f : (a : R) → ℝ) c : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₄ : HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) /
    HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₂ :
  HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ((f : (a : R) → ℝ) c : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₄ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₅ : HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
    (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
  (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₂ :
  HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ((f : (a : R) → ℝ) c : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₄ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₅ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₆ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) c : ℝ) (1 : ℝ) = (f : (a : R) → ℝ) c
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
h :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n * c) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₁ :
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ (n + 1)) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₂ :
  HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n + 1) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ((f : (a : R) → ℝ) c : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₄ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n =
    (f : (a : R) → ℝ) c
h₅ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
h₆ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) c : ℝ) (1 : ℝ) = (f : (a : R) → ℝ) c
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) =
    (f : (a : R) → ℝ) c
have h₇ : Eq (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) ((f : (a : R) → ℝ) c : ℝ)
Tactic: rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 ((f : (a : R) → ℝ) c))
have hseq : seminormFromConst_seq c f c = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) c
Tactic: have hseq : seminormFromConst_seq c f c = fun _n ↦ f c := by
      ext n
      simp only [seminormFromConst_seq]
      rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
hseq : seminormFromConst_seq c f c = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) c
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 ((f : (a : R) → ℝ) c))
have rw : Tendsto (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) c : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) c) : Filter ℝ)
Tactic: rw [hseq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
have apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ a + 1
Tactic: apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
n : ℕ
⊢ ∃ (a : ℕ), n ≤ a + 1
have h : n ≤ n + 1
Tactic: use n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x
have hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
Tactic: have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
      (𝓝 (seminormFromConst' c f x)) := by
    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)
    rintro n; use n; lia
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x
have rw : seminormFromConst' c f (c * x) = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)
Tactic: rw [seminormFromConst_apply_c hf1 hc hpm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf1 : LE.le (α := ℝ) ((f : (a : R) → ℝ) 1 : ℝ) (1 : ℝ)
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
x : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
⊢ seminormFromConst' c f (c * x) = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)
have apply : Tendsto (seminormFromConst_seq c f (c * x)) atTop
  (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (seminormFromConst' c f x)))
Tactic: apply tendsto_nhds_unique (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (c * x))