awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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) : ℝ)
g : 0 ≤ 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)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
apply : ∀ (b : ℕ), ∃ (a : ℕ), b ≤ m * a
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))

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) _)

Premises used: mul_le_mul_right, Filter.tendsto_atTop_atTop_of_monotone, HPow.hPow, Filter.Tendsto.comp, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℕ
h : n ≤ m * n
⊢ ∃ (a : ℕ), n ≤ m * a

Tactic:
use n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℕ
⊢ n ≤ m * n

Tactic:
le_mul_of_one_le_left' hm

Premises used: le_mul_of_one_le_left'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℕ
⊢ n ≤ m * n

Tactic:
exact le_mul_of_one_le_left' hm

Premises used: le_mul_of_one_le_left'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)))

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
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)))
apply :
  Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (iInf (seminormFromConst_seq c f x) ^ m))
⊢ iInf (seminormFromConst_seq c f (x ^ m)) = iInf (seminormFromConst_seq c f x) ^ m

Tactic:
apply tendsto_nhds_unique hlim

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 (x_1 : ℕ) ↦ seminormFromConst_seq c f x x_1 ^ m) atTop (𝓝 (seminormFromConst' c f x ^ m))

Tactic:
(tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).pow m

Premises used: Filter.Tendsto.pow, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)))
h :
  Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) fun (x_1 : ℕ) ↦
    seminormFromConst_seq c f x x_1 ^ m
⊢ Tendsto (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (iInf (seminormFromConst_seq c f x) ^ m))

Tactic:
convert! (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).pow m using 1

Premises used: Filter.Tendsto.pow, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)))
h : ∀ (n : ℕ), seminormFromConst_seq c f (x ^ m) (m * n) = seminormFromConst_seq c f x n ^ m
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ seminormFromConst_seq c f (x ^ m) (m * n)) fun (x_1 : ℕ) ↦
    seminormFromConst_seq c f x x_1 ^ m

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)))
n : ℕ
⊢ seminormFromConst_seq c f (x ^ m) (m * n) = seminormFromConst_seq c f x n ^ m

Tactic:
simp only [seminormFromConst_seq, div_pow, ← hpm _ hm, ← pow_mul, mul_pow, mul_comm m n]

Premises used: pow_mul, div_pow, mul_comm, mul_pow, seminormFromConst_seq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
apply : ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ (f : (a : R) → ℝ) x
⊢ seminormFromConst' c f x ≤ (f : (a : R) → ℝ) x

Tactic:
apply le_of_tendsto (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x)

Premises used: le_of_tendsto, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x
⊢ ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ (f : (a : R) → ℝ) x

Tactic:
simp only [eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
h : ∀ (b : ℕ), 1 ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ (f : (a : R) → ℝ) x

Tactic:
use 1
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
⊢ 0 < HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
h :
  (f : (a : R) → ℝ) (x * c ^ n) ≤ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ)
⊢ seminormFromConst_seq c f x n ≤ (f : (a : R) → ℝ) x

Tactic:
rw [seminormFromConst_seq, div_le_iff₀ (by positivity), ← hpm c hn]

Premises used: div_le_iff₀, seminormFromConst_seq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
⊢ (f : (a : R) → ℝ) (x * c ^ n) ≤ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ)

Tactic:
map_mul_le_mul ..

Premises used: SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
⊢ (f : (a : R) → ℝ) (x * c ^ n) ≤ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : R) → ℝ) x : ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ)

Tactic:
exact map_mul_le_mul ..

Premises used: SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℝ)
h : ∀ (n : ℕ), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
⊢ seminormFromConst_seq c f x = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) x

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
neg : ∀ (hn : ¬n = 0), seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x
⊢ seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℕ
hn : n = 0
⊢ seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x

Tactic:
simp only [seminormFromConst_seq, hn, pow_zero, mul_one, div_one]

Premises used: pow_zero, mul_one, seminormFromConst_seq, div_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 : ℕ
hn : ¬n = 0
⊢ seminormFromConst_seq c f x n = (f : (a : R) → ℝ) x

Tactic:
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]

Premises used: Iff.mpr, mul_div_assoc, pow_ne_zero, HPow.hPow, Nat.one_le_iff_ne_zero, mul_one, seminormFromConst_seq, div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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

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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
rw : Tendsto (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) x : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) x) : Filter ℝ)
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 ((f : (a : R) → ℝ) x))

Tactic:
rw [hseq]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) x : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) x) : Filter ℝ)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) x : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) x) : Filter ℝ)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
rw :
  Tendsto (seminormFromConst_seq c f (x * y)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst' c f y)))
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop (𝓝 (seminormFromConst' c f x * seminormFromConst' c f y))

Tactic:
rw [seminormFromConst_apply_of_isMul hf1 hc hpm hx]

Premises used: seminormFromConst_apply_of_isMul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
h :
  ∀ (n : ℕ),
    seminormFromConst_seq c f (x * y) n = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)
⊢ seminormFromConst_seq c f (x * y) = fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
n : ℕ
⊢ seminormFromConst_seq c f (x * y) n = HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)

Tactic:
simp only [seminormFromConst_seq, mul_assoc, hx, mul_div_assoc]

Premises used: mul_assoc, mul_div_assoc, seminormFromConst_seq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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)

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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
hseq :
  seminormFromConst_seq c f (x * y) = fun (n : ℕ) ↦
    HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst_seq c f y n)
⊢ Tendsto (seminormFromConst_seq c f (x * y)) atTop
    (𝓝 (HMul.hMul (α := ℝ) ((f : (a : R) → ℝ) x : ℝ) (seminormFromConst' c f y)))

Tactic:
simpa [hseq] using (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y).const_mul _

Premises used: Filter.Tendsto.const_mul, tendsto_seminormFromConst_seq_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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) → ℝ)
h : ∀ (n : ℕ), seminormFromConst_seq c f c n = (f : (a : R) → ℝ) c
⊢ seminormFromConst_seq c f c = fun (_n : ℕ) ↦ (f : (a : R) → ℝ) c

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
h₇ h₈ : Eq (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) ((f : (a : R) → ℝ) c : ℝ)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c * 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]

Premises used: pow_succ, mul_div_assoc, pow_ne_zero, mul_comm, mul_one, le_add_self, div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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

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]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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
rw : Tendsto (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) c : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) c) : Filter ℝ)
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 ((f : (a : R) → ℝ) c))

Tactic:
rw [hseq]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) c : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) c) : Filter ℝ)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
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 (β := ℝ) (fun (_n : ℕ) ↦ ((f : (a : R) → ℝ) c : ℝ)) atTop (𝓝 ((f : (a : R) → ℝ) c) : Filter ℝ)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds