-- Mathlib/Analysis/Normed/Ring/IsPowMulFaithful.lean
theorem eq_of_powMul_faithful (f₁ : AlgebraNorm R S) (hf₁_pm : IsPowMul f₁) (f₂ : AlgebraNorm R S)
    (hf₂_pm : IsPowMul f₂)
    (h_eq : ∀ y : S, ∃ (C₁ C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ x : Algebra.adjoin R {y}, f₁ x.val ≤ C₁ * f₂ x.val ∧ f₂ x.val ≤ C₂ * f₁ x.val) :
    f₁ = f₂

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
⊢ f₁ x = f₂ x

Tactic:
set g₂ : AlgebraNorm R (Algebra.adjoin R ({x} : Set S)) := AlgebraNorm.restriction _ f₂

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
⊢ f₁ x = f₂ x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥(Algebra.adjoin R {x}) := ⟨x, ⋯⟩
⊢ f₁ x = f₂ x

Tactic:
have hy : x = y.val := rfl

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥(Algebra.adjoin R {x}) := ⟨x, ⋯⟩
hy : x = ↑y
⊢ f₁ x = f₂ x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
⊢ f₁ x = f₂ x

Tactic:
have hg₁_pm : IsPowMul g₁ := IsPowMul.restriction _ hf₁_pm

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
⊢ f₁ x = f₂ x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
⊢ f₁ x = f₂ x

Tactic:
let y : Algebra.adjoin R ({x} : Set S) := ⟨x, Algebra.self_mem_adjoin_singleton R x⟩

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥(Algebra.adjoin R {x}) := ⟨x, ⋯⟩
⊢ f₁ x = f₂ x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
⊢ f₁ x = f₂ x

Tactic:
have hg₂_pm : IsPowMul g₂ := IsPowMul.restriction _ hf₂_pm

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
⊢ f₁ x = f₂ x

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥(Algebra.adjoin R {x}) := ⟨x, ⋯⟩
hy : x = ↑y
h1 : f₁ ↑y = g₁ y
h2 : f₂ ↑y = g₂ y
⊢ f₁ x = f₂ x

Tactic:
obtain ⟨C₁, C₂, hC₁_pos, hC₂_pos, hC⟩ := h_eq x

Result:
case a.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq :
  ∀ (y : S),
    ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥(Algebra.adjoin R {y})), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₁
g₂ : AlgebraNorm R ↥(Algebra.adjoin R {x}) := AlgebraNorm.restriction (Algebra.adjoin R {x}) f₂
hg₁_pm : IsPowMul ⇑g₁
hg₂_pm : IsPowMul ⇑g₂
y : ↥(Algebra.adjoin R {x}) := ⟨x, ⋯⟩
hy : x = ↑y
h1 : f₁ ↑y = g₁ y
h2 : f₂ ↑y = g₂ y
C₁ C₂ : ℝ
hC₁_pos : 0 < C₁
hC₂_pos : 0 < C₂
hC : ∀ (x_1 : ↥(Algebra.adjoin R {x})), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1 ∧ f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ f₁ x = f₂ x