-- 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)
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)
inr₇ :
  HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) (x * c ^ m) : ℝ) (1 * (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) m)⁻¹) ≤
    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 : ℝ) 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 : ℝ) m)⁻¹ ≤
  HMul.hMul (α := ℝ) ((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]