awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have rw₁ : C ^ (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑n : ℝ)) = C
Tactic: rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have rw₂ : C ^ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = C
Tactic: rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have rw₃ : HPow.hPow (β := ℝ) C 1 = C
Tactic: rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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
⊢ (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ n = C
have rw₄ : C = C
Tactic: rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
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
⊢ nβ ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
have h : (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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β ((f : (a : α) → β) x) ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ)
have h₁ : nβ ((f : (a : α) → β) x) ^ n ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ) ^ n
Tactic: apply le_of_pow_le_pow_left₀ (ne_of_gt hn) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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β ((f : (a : α) → β) x) ^ n ≤ HMul.hMul (β := ℝ) (C ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ((nα : (a : α) → ℝ) x : ℝ) ^ n
have h₁ : nβ ((f : (a : α) → β) (x ^ n)) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
Tactic: rw [mul_pow, h, ← hβ _ hn, ← map_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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β ((f : (a : α) → β) (x ^ n)) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
have h₁ : HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) (x ^ n) : ℝ) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
Tactic: apply le_trans (hC (x ^ n))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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
⊢ HMul.hMul (β := ℝ) C ((nα : (a : α) → ℝ) (x ^ n) : ℝ) ≤ C * HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
have h₁ : (nα : (a : α) → ℝ) (x ^ n) ≤ HPow.hPow (α := ℝ) ((nα : (a : α) → ℝ) x : ℝ) n
Tactic: rw [mul_le_mul_iff_right₀ hC0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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 : ℝ)
⊢ f = g
have obtain : ∀ (r : ℝ) (hr0 : 0 < r) (hr : ∀ (a : α), (f : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) r ((g : (a : α) → ℝ) a : ℝ)), f = g
Tactic: obtain ⟨r, hr0, hr⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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 : ℝ)
⊢ f = g
have obtain : ∀ (s : ℝ) (hs0 : 0 < s) (hs : ∀ (a : α), (g : (a : α) → ℝ) a ≤ HMul.hMul (β := ℝ) s ((f : (a : α) → ℝ) a : ℝ)), f = g
Tactic: obtain ⟨s, hs0, hs⟩ := hgf
Cleared hypotheses: hgf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
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 : ℝ)
⊢ f = g
have hle : RingHom.IsBoundedWrt (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ) (RingHom.id α)
Tactic: have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
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 α)
⊢ f = g
have hge : RingHom.IsBoundedWrt (⇑g : (a : α) → ℝ) (⇑f : (a : α) → ℝ) (RingHom.id α)
Tactic: have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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 α)
⊢ f = g
have rw : Eq.{max (u_2 + 1) 1} (α := (a : α) → ℝ) (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ)
Tactic: rw [← Function.Injective.eq_iff DFunLike.coe_injective']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
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 α)
⊢ Eq.{max (u_2 + 1) 1} (α := (a : α) → ℝ) (⇑f : (a : α) → ℝ) (⇑g : (a : α) → ℝ)
have h : ∀ (x : α), Eq (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
⊢ f₁ = f₂
have a : ∀ (x : S), Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
Tactic: have hg₁_pm : IsPowMul g₁ := IsPowMul.restriction _ hf₁_pm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
Tactic: have hg₂_pm : IsPowMul g₂ := IsPowMul.restriction _ hf₂_pm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have hy : x = (↑y : S)
Tactic: have hy : x = y.val := rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
Tactic: have h1 : f₁ y.val = g₁ y := rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
Tactic: have h2 : f₂ y.val = g₂ y := rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have a : ∀ (C₁ C₂ : ℝ) (hC₁_pos : 0 < C₁) (hC₂_pos : 0 < C₂)
  (hC :
    ∀ (x_1 : ↥R[x]),
      (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
        (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)),
  Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
Tactic: obtain ⟨C₁, C₂, hC₁_pos, hC₂_pos, hC⟩ := h_eq x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
Tactic: obtain ⟨hC₁, hC₂⟩ := forall_and.mp hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : NormedCommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul (R := S) (⇑f₁ : (a : S) → ℝ)
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul (R := S) (⇑f₂ : (a : S) → ℝ)
h_eq :
  ∀ (y : S),
    ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x : ↥R[y]),
        (f₁ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x : S) : ℝ) ∧
          (f₂ : (a : S) → ℝ) (↑x : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x : S) : ℝ)
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
g₂ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₂
hg₁_pm : IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)
hg₂_pm : IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)
y : ↥R[x] := Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯
hy : x = (↑y : S)
h1 : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)
h2 : Eq (α := ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC :
  ∀ (x_1 : ↥R[x]),
    (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ) ∧
      (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
hC₁ : ∀ (x_1 : ↥R[x]), (f₁ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₁ ((f₂ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
have hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
Tactic: obtain ⟨hC₁, hC₂⟩ := forall_and.mp hC