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 n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
hlt : m < n
h1 : 1 ≤ n - m
inr :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n - m)) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
inr₁ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n - m) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
inr₂ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (n - m) * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
inr₃ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)⁻¹ *
        (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
inr₄ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n *
        ((HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)⁻¹ * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹)) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
inr₅ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n *
        ((HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹ * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)⁻¹)) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) ((f : (a : R) → ℝ) (c ^ (n - m)) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
have inr₆ : HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ)
    (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹ *
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)⁻¹) ≤
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
Tactic: rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]
-- 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
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) ((f : (a : R) → ℝ) (c ^ (n - m)) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
have x₁ : m = n ∨ m < n
Tactic: cases hmn.eq_or_lt with
  | inl heq =>
    have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
    rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
    conv_rhs => rw [← mul_one (f (x * c ^ n))]
    gcongr
  | inr hlt =>
    have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt
    rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹,
      ← mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]
-- 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' c f 1 = 1
have apply : seminormFromConst_seq c f 1 =ᶠ[atTop] fun (x : ℕ) ↦ 1
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_seminormFromConst_seq_atTop hf1 hc hpm 1)
    tendsto_const_nhds
-- 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 1 =ᶠ[atTop] fun (x : ℕ) ↦ 1
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1
Tactic: simp only [EventuallyEq, 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 y : R
⊢ seminormFromConst' c f (x + y) ≤ seminormFromConst' c f x + seminormFromConst' c f y
have apply : ∀ (x_1 : ℕ), seminormFromConst_seq c f (x + y) x_1 ≤ seminormFromConst_seq c f x x_1 + seminormFromConst_seq c f y x_1
Tactic: apply le_of_tendsto_of_tendsto' (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x + y)) <|
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).add
        (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)
-- 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 y : R
n : ℕ
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n + seminormFromConst_seq c f y n
have h_add : (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
Tactic: have h_add : f ((x + y) * c ^ n) ≤ f (x * c ^ n) + f (y * c ^ n) := by
      simp only [add_mul, map_add_le_add f _ _]
-- 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 y : R
n : ℕ
h_add :
  (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
⊢ seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n + seminormFromConst_seq c f y n
have simp : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) /
    HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
Tactic: simp only [seminormFromConst_seq, ← add_div]
-- 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 y : R
n : ℕ
h_add :
  (f : (a : R) → ℝ) ((x + y) * c ^ n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) /
      HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
have hc₁ : 0 ≤ HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
Tactic: gcongr
-- 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) = seminormFromConst' c f x
have apply : seminormFromConst_seq c f (-x) =ᶠ[atTop] seminormFromConst_seq c f x
Tactic: apply tendsto_nhds_unique_of_eventuallyEq (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (-x))
      (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
⊢ seminormFromConst_seq c f (-x) =ᶠ[atTop] seminormFromConst_seq c f x
have simp : ∃ (a : ℕ), ∀ b ≥ a, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
Tactic: simp only [EventuallyEq, eventually_atTop]
-- 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, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
have h : ∀ b ≥ 0, seminormFromConst_seq c f (-x) b = seminormFromConst_seq c f x b
Tactic: use 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 y : R
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
have apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ 2 * a
Tactic: apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
        (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by
          simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)
-- 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 y : R
n : ℕ
⊢ ∃ (a : ℕ), n ≤ 2 * a
have h : n ≤ 2 * n
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 y : R
⊢ seminormFromConst' c f (x * y) ≤ seminormFromConst' c f x * seminormFromConst' c f y
have hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
Tactic: have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop
        (𝓝 (seminormFromConst' c f (x * y))) := by
      apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
        (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by
          simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)
      · 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 y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
⊢ seminormFromConst' c f (x * y) ≤ seminormFromConst' c f x * seminormFromConst' c f y
have refine : ∀ (n : ℕ), seminormFromConst_seq c f (x * y) (2 * n) ≤ seminormFromConst_seq c f x n * seminormFromConst_seq c f y n
Tactic: refine le_of_tendsto_of_tendsto' hlim ((tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).mul
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)) (fun 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 y : R
hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' c f (x * y)))
n : ℕ
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * y * c ^ (2 * n)) : ℝ)
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (2 * n)) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) *
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
have rw : (f : (a : R) → ℝ) (x * c ^ n * (y * c ^ n)) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
Tactic: rw [div_mul_div_comm, ← pow_add, two_mul,
      div_le_div_iff_of_pos_right (pow_pos (lt_of_le_of_ne (apply_nonneg f _) hc.symm) _), pow_add,
      ← mul_assoc, mul_comm (x * y), ← mul_assoc, mul_assoc, mul_comm (c ^ 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
⊢ seminormFromConst' c f (x + y) ≤ max (seminormFromConst' c f x) (seminormFromConst' c f y)
have apply : ∀ (x_1 : ℕ),
  seminormFromConst_seq c f (x + y) x_1 ≤ max (seminormFromConst_seq c f x x_1) (seminormFromConst_seq c f y x_1)
Tactic: apply le_of_tendsto_of_tendsto' (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x + y)) <|
    (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).max
      (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
⊢ seminormFromConst_seq c f (x + y) n ≤ max (seminormFromConst_seq c f x n) (seminormFromConst_seq c f y n)
have hmax : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ)
  (max ((f : (a : R) → ℝ) (x * c ^ n)) ((f : (a : R) → ℝ) (y * c ^ n)) : ℝ)
Tactic: have hmax : f ((x + y) * c ^ n) ≤ max (f (x * c ^ n)) (f (y * c ^ n)) := by
    simp only [add_mul, hna _ _]
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ)
    (max ((f : (a : R) → ℝ) (x * c ^ n)) ((f : (a : R) → ℝ) (y * c ^ n)) : ℝ)
⊢ seminormFromConst_seq c f (x + y) n ≤ max (seminormFromConst_seq c f x n) (seminormFromConst_seq c f y n)
have rw : ∀
  (hmax :
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
      LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)),
  seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f x n ∨
    seminormFromConst_seq c f (x + y) n ≤ seminormFromConst_seq c f y n
Tactic: rw [le_max_iff] at hmax ⊢
Cleared hypotheses: hmax
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ∨
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
have f₁ : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) →
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
Tactic: apply hmax.imp
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
f₁ :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) →
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ∨
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
have g : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) →
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
Tactic: apply hmax.imp
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
h : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
have f₁ : 0 ≤ HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
Tactic: gcongr
-- 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) → ℝ)
hna : IsNonarchimedean (R := ℝ) (α := R) (⇑f : (a : R) → ℝ)
x y : R
n : ℕ
hmax :
  LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ∨
    LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
h : LE.le (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) ((x + y) * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (y * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)
have g : 0 ≤ HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n
Tactic: gcongr
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
have apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ m * a
Tactic: apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x ^ m)).comp
      (tendsto_atTop_atTop_of_monotone (fun _ _ hnk ↦ mul_le_mul_right hnk m) _)
-- 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
n : ℕ
⊢ ∃ (a : ℕ), n ≤ m * a
have h : n ≤ m * n
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
m : ℕ
hm : 1 ≤ m
⊢ iInf (seminormFromConst_seq c f (x ^ m)) = iInf (seminormFromConst_seq c f x) ^ m
have hlim : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
Tactic: have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop
      (𝓝 (seminormFromConst' c f (x ^ m))) := by
    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x ^ m)).comp
      (tendsto_atTop_atTop_of_monotone (fun _ _ hnk ↦ mul_le_mul_right hnk m) _)
    rintro n; use n; exact le_mul_of_one_le_left' hm
-- 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)))
⊢ iInf (seminormFromConst_seq c f (x ^ m)) = iInf (seminormFromConst_seq c f x) ^ m
have apply : Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (iInf (seminormFromConst_seq c f x) ^ m))
Tactic: apply tendsto_nhds_unique hlim