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
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (1 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
have rw₁ : HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 1
Tactic: rw [one_mul, hpm _ hn, div_self (pow_ne_zero n hc)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
rw₁ : HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 1
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (1 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [one_mul, hpm _ hn, div_self (pow_ne_zero n hc)]
-- 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
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
    HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
have nth_rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (m + (n - m))) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
  HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)
Tactic: nth_rw 1 [← Nat.add_sub_of_le hmn]
-- 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
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ (m + (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 rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m * 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)
Tactic: rw [pow_add, ← mul_assoc]
-- 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
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m * 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 hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
Tactic: have hc_pos : 0 < f c := lt_of_le_of_ne (apply_nonneg f _) hc.symm
-- 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 : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m * 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 apply : 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)
Tactic: apply le_trans ((div_le_div_iff_of_pos_right (pow_pos hc_pos _)).mpr (map_mul_le_mul 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 : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
⊢ n - m = 0
have rw : n - n = 0
Tactic: rw [heq, Nat.sub_self 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
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
rw : n - n = 0
⊢ n - m = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [heq, Nat.sub_self 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 n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
⊢ 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 hnm : n - m = 0
Tactic: have hnm : n - m = 0 := by rw [heq, Nat.sub_self 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
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
hnm : n - m = 0
⊢ 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 inl : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
  (f : (a : R) → ℝ) (x * c ^ n)
Tactic: rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
-- 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 : ℝ)
heq : m = n
hnm : n - m = 0
| (f : (a : R) → ℝ) (x * c ^ n)
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)
Tactic: rw [← mul_one (f (x * 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) → ℝ)
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
hnm : n - m = 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    (f : (a : R) → ℝ) (x * c ^ n)
have inl : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)
Tactic: conv_rhs => rw [← mul_one (f (x * 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) → ℝ)
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
heq : m = n
hnm : n - m = 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) ((f : (a : R) → ℝ) 1 : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) (x * c ^ n) : ℝ) (1 : ℝ)
have inl : LE.le (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) (x * 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 n : ℕ
hmn : m ≤ n
hc_pos : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : R) → ℝ) c : ℝ)
hlt : m < n
⊢ 1 ≤ n - m
have rw : n - m ≠ 0
Tactic: rw [Nat.one_le_iff_ne_zero]
-- 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 : ℝ)
hlt : m < n
⊢ 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 h1 : 1 ≤ n - m
Tactic: have h1 : 1 ≤ n - m := by
      rw [Nat.one_le_iff_ne_zero]
      exact Nat.sub_ne_zero_of_lt hlt
-- 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
⊢ 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 - m)) /
    HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n ≤
  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 (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)
⊢ 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 - m) / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) ≤
  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 (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)
⊢ 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 - m) * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹) ≤
  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 (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)
⊢ 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 : ℝ) m)⁻¹ *
      (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹) ≤
  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 (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)
⊢ 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 : ℝ) m)⁻¹ * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n)⁻¹)) ≤
  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 (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)
⊢ 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]