awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ x ≠ 0 → Ne (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0

Tactic:
fun hx ↦ ne_of_gt (lt_of_lt_of_le (map_pos_of_ne_zero _ hx)
      (Finite.le_ciSup (fun σ ↦ (algNormOfAlgEquiv σ) x) AlgEquiv.refl))

Premises used: IsUltrametricDist.algNormOfAlgEquiv, ne_of_gt, Finite.le_ciSup, map_pos_of_ne_zero, AlgEquiv.refl, DFunLike.coe, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ x ≠ 0 → Ne (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x) 0

Tactic:
exact fun hx ↦ ne_of_gt (lt_of_lt_of_le (map_pos_of_ne_zero _ hx)
      (Finite.le_ciSup (fun σ ↦ (algNormOfAlgEquiv σ) x) AlgEquiv.refl))

Premises used: IsUltrametricDist.algNormOfAlgEquiv, ne_of_gt, Finite.le_ciSup, map_pos_of_ne_zero, AlgEquiv.refl, DFunLike.coe, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
r : K
x : L
⊢ ⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) (r • x) =
    ‖r‖ * ⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x

Tactic:
simp only [AlgebraNormClass.map_smul_eq_mul,
      Real.mul_iSup_of_nonneg (norm_nonneg _)]

Premises used: AlgebraNormClass.map_smul_eq_mul, norm_nonneg, Real.mul_iSup_of_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
⊢ Eq (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ)
    (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: iSup, dite, rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
rw :
  Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n))
    (⨆ (i : L ≃ₐ[K] L), HPow.hPow (α := ℝ) ((algNormOfAlgEquiv i : (a : L) → ℝ) x : ℝ) n)
⊢ (invariantExtension K L : (a : L) → ℝ) (x ^ n) = HPow.hPow (α := ℝ) ((invariantExtension K L : (a : L) → ℝ) x : ℝ) n

Tactic:
rw [invariantExtension_apply, invariantExtension_apply, Real.iSup_pow
    (fun σ ↦ apply_nonneg (algNormOfAlgEquiv σ) x)]

Premises used: IsUltrametricDist.invariantExtension_apply, IsUltrametricDist.algNormOfAlgEquiv, Real.iSup_pow, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
⊢ Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n))
    (⨆ (i : L ≃ₐ[K] L), HPow.hPow (α := ℝ) ((algNormOfAlgEquiv i : (a : L) → ℝ) x : ℝ) n)

Tactic:
iSup_congr fun σ ↦ isPowMul_algNormOfAlgEquiv σ _ hn

Premises used: IsUltrametricDist.isPowMul_algNormOfAlgEquiv, iSup_congr
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : L
n : ℕ
hn : 1 ≤ n
⊢ Eq (α := ℝ) (⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ : (a : L) → ℝ) (x ^ n))
    (⨆ (i : L ≃ₐ[K] L), HPow.hPow (α := ℝ) ((algNormOfAlgEquiv i : (a : L) → ℝ) x : ℝ) n)

Tactic:
exact iSup_congr fun σ ↦ isPowMul_algNormOfAlgEquiv σ _ hn

Premises used: IsUltrametricDist.isPowMul_algNormOfAlgEquiv, iSup_congr
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
⊢ IsNonarchimedean (R := ℝ) (α := L) (⇑(invariantExtension K L) : (a : L) → ℝ)

Tactic:
fun x y ↦
  ciSup_le fun σ ↦ le_trans (isNonarchimedean_algNormOfAlgEquiv σ x y)
    (max_le_max (Finite.le_ciSup_of_le σ le_rfl) (Finite.le_ciSup_of_le σ le_rfl))

Premises used: le_rfl, iSup, dite, max_le_max, Finite.le_ciSup_of_le, IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv, IsNonarchimedean, ciSup_le, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension
Goal:
K : Type u_1
inst : NormedField K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
x : K
⊢ (invariantExtension K L : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖

Tactic:
simp [algNormOfAlgEquiv_extends _ x, ciSup_const]

Premises used: IsUltrametricDist.algNormOfAlgEquiv_extends, ciSup_const
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
hf : RingHom.IsBoundedWrt (⇑nα : (a : α) → ℝ) nβ f
x : α
obtain :
  ∀ (C : ℝ) (hC0 : 0 < C) (hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)),
    nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x
⊢ nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x

Tactic:
obtain ⟨C, hC0, hC⟩ := hf
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
nth_rewrite :
  Tendsto (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)) atTop
    (𝓝 (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((nα : (a : α) → ℝ) x : ℝ)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)

Tactic:
nth_rewrite 2 [← one_mul (nα x)]

Premises used: DFunLike.coe, one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)) atTop
    (𝓝 (HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((nα : (a : α) → ℝ) x : ℝ)))

Tactic:
exact ((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
      (tendsto_const_div_atTop_nhds_zero_nat 1)).mul tendsto_const_nhds
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)

Tactic:
have hlim : Tendsto (fun n : ℕ => C ^ (1 / (n : ℝ)) * nα x) atTop (𝓝 (nα x)) := by
    nth_rewrite 2 [← one_mul (nα x)]
    exact ((rpow_zero C ▸ ContinuousAt.tendsto (continuousAt_const_rpow (ne_of_gt hC0))).comp
      (tendsto_const_div_atTop_nhds_zero_nat 1)).mul tendsto_const_nhds
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
apply :
  ∀ᶠ (c : ℕ) in atTop,
    nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑c : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
⊢ nβ ((f : (a : α) → β) x) ≤ (nα : (a : α) → ℝ) x

Tactic:
apply ge_of_tendsto hlim

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
simp :
  ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
⊢ ∀ᶠ (c : ℕ) in atTop,
    nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑c : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)

Tactic:
simp only [eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
h :
  ∀ (b : ℕ),
    1 ≤ b → nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
⊢ ∃ (a : ℕ),
    ∀ (b : ℕ),
      a ≤ b →
        nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)

Tactic:
use 1
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
hn0 : Ne (α := ℝ) (↑n : ℝ) 0
rw : HPow.hPow (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑n : ℝ) = C
rw₁ : C ^ (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑n : ℝ)) = C
rw₂ : C ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = C
rw₃ : HPow.hPow (β := ℝ) C 1 = C
rw₄ rw₅ : C = C
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C

Tactic:
rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]

Premises used: LT.lt.le, Real.rpow_one, one_div, Real.rpow_mul, inv_mul_cancel₀, Real.rpow_natCast
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C

Tactic:
have h : (C ^ (1 / n : ℝ)) ^ n = C := by
    have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
    rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
⊢ 0 ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
h₁ :
  nβ ((f : (a : α) → β) x) ^ n ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ) ^ n
⊢ nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)

Tactic:
apply le_of_pow_le_pow_left₀ (ne_of_gt hn) (by positivity)

Premises used: ne_of_gt, le_of_pow_le_pow_left₀
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
h₁ : nβ ((f : (a : α) → β) (x ^ n)) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
⊢ nβ ((f : (a : α) → β) x) ^ n ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ) ^ n

Tactic:
rw [mul_pow, h, ← hβ _ hn, ← map_pow]

Premises used: map_pow, mul_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
h₁ : HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) (x ^ n) : ℝ) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
⊢ nβ ((f : (a : α) → β) (x ^ n)) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n

Tactic:
apply le_trans (hC (x ^ n))

Premises used: HPow.hPow, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
h₁ : (nα : (a : α) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
⊢ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) (x ^ n) : ℝ) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n

Tactic:
rw [mul_le_mul_iff_right₀ hC0]

Premises used: mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
⊢ (nα : (a : α) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n

Tactic:
map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)

Premises used: map_pow_le_pow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
β : Type u_3
inst_3 : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) x : ℝ)
hlim :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ))
    atTop (𝓝 ((nα : (a : α) → ℝ) x) : Filter ℝ)
n : ℕ
hn : 1 ≤ n
h : (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
⊢ (nα : (a : α) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n

Tactic:
exact map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)

Premises used: map_pow_le_pow, Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedRing β
hβ : IsPowMul.{u_2} (R := β) Norm.norm
f : α →+* β
hf : f.IsBounded
x : α
⊢ Norm.norm.{u_2} (E := β) ((f : (a : α) → β) x : β) ≤ ‖x‖

Tactic:
contraction_of_isPowMul_of_boundedWrt (SeminormedRing.toRingSeminorm α) hβ hf x

Premises used: contraction_of_isPowMul_of_boundedWrt, SeminormedRing.toRingSeminorm
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
hfg : ∃ (r : ℝ) (_ : 0 < r), ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
hgf : ∃ (r : ℝ) (_ : 0 < r), ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((f : (a : α) → ℝ) a : ℝ)
obtain :
  ∀ (r : ℝ) (hr0 : 0 < r) (hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)), f = g
⊢ f = g

Tactic:
obtain ⟨r, hr0, hr⟩ := hfg
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
hgf : ∃ (r : ℝ) (_ : 0 < r), ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((f : (a : α) → ℝ) a : ℝ)
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
obtain :
  ∀ (s : ℝ) (hs0 : 0 < s) (hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)), f = g
⊢ f = g

Tactic:
obtain ⟨s, hs0, hs⟩ := hgf
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)
⊢ RingHom.IsBoundedWrt (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ) (RingHom.id α)

Tactic:
have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)
hle : RingHom.IsBoundedWrt (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ) (RingHom.id α)
⊢ RingHom.IsBoundedWrt (⇑g : (a : α) → ℝ) (⇑f : (a : α) → ℝ) (RingHom.id α)

Tactic:
have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)
hle : RingHom.IsBoundedWrt (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g : (a : α) → ℝ) (⇑f : (a : α) → ℝ) (RingHom.id α)
rw : Eq.{max (u_2 + 1) 1} (α := (a : α) → ℝ) (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ)
⊢ f = g

Tactic:
rw [← Function.Injective.eq_iff DFunLike.coe_injective']

Premises used: Function.Injective.eq_iff, DFunLike.coe_injective'
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
Goal:
F : Type u_1
α : Type u_2
inst : Ring α
inst_1 : FunLike F α ℝ
inst_2 : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul.{u_2} (R := α) (⇑f : (a : α) → ℝ)
hgpm : IsPowMul.{u_2} (R := α) (⇑g : (a : α) → ℝ)
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)
hle : RingHom.IsBoundedWrt (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g : (a : α) → ℝ) (⇑f : (a : α) → ℝ) (RingHom.id α)
h : ∀ (x : α), Eq (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)
⊢ Eq.{max (u_2 + 1) 1} (α := (a : α) → ℝ) (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ)

Tactic:
ext x