-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_const_mul (x : R) :
    seminormFromConst' hf1 hc hpm (c * x) =
      seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

Tactic:
rw [seminormFromConst_apply_c hf1 hc hpm]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ seminormFromConst' hf1 hc hpm (c * x) = f c * seminormFromConst' hf1 hc hpm x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

Tactic:
have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
    (𝓝 (seminormFromConst' hf1 hc hpm x)) := by
  apply (seminormFromConst_isLimit hf1 hc hpm x).comp
    (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ add_le_add_right hnm 1) _)
  rintro n; use n; omega

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))

Tactic:
have hterm : seminormFromConst_seq c f (c * x) =
    fun n ↦ f c * seminormFromConst_seq c f x (n + 1) := by
  simp only [seminormFromConst_seq_def]
  ext n
  ring_nf
  rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
hterm : seminormFromConst_seq c f (c * x) = fun n => f c * seminormFromConst_seq c f x (n + 1)
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
n : ℕ
⊢ f (c * c ^ n * x) * (f c)⁻¹ ^ n = f (c * c ^ n * x) * f c * (f c)⁻¹ * (f c)⁻¹ ^ n

Tactic:
rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), ∃ a, b ≤ a + 1

Tactic:
rintro n

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
⊢ ∃ a, n ≤ a + 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
hterm : seminormFromConst_seq c f (c * x) = fun n => f c * seminormFromConst_seq c f x (n + 1)
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))

Tactic:
simpa [hterm] using tendsto_const_nhds.mul hlim

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))

Tactic:
apply (seminormFromConst_isLimit hf1 hc hpm x).comp
  (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ add_le_add_right hnm 1) _)

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), ∃ a, b ≤ a + 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
⊢ n ≤ n + 1

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ seminormFromConst' hf1 hc hpm (c * x) = f c * seminormFromConst' hf1 hc hpm x

Tactic:
apply tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm (c * x))

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
n : ℕ
⊢ f (c * x * c ^ n) / f c ^ n = f c * (f (x * c ^ (n + 1)) / f c ^ (n + 1))

Tactic:
ring_nf

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
n : ℕ
⊢ f (c * c ^ n * x) * (f c)⁻¹ ^ n = f (c * c ^ n * x) * f c * (f c)⁻¹ * (f c)⁻¹ ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
⊢ ∃ a, n ≤ a + 1

Tactic:
use n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
⊢ n ≤ n + 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ seminormFromConst_seq c f (c * x) = fun n => f c * seminormFromConst_seq c f x (n + 1)

Tactic:
simp only [seminormFromConst_seq_def]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ (fun n => f (c * x * c ^ n) / f c ^ n) = fun n => f c * (f (x * c ^ (n + 1)) / f c ^ (n + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
⊢ (fun n => f (c * x * c ^ n) / f c ^ n) = fun n => f c * (f (x * c ^ (n + 1)) / f c ^ (n + 1))

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
n : ℕ
⊢ f (c * x * c ^ n) / f c ^ n = f c * (f (x * c ^ (n + 1)) / f c ^ (n + 1))