-- 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₁
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

Tactic:
have h1 : f₁ y.val = g₁ y := 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
h1 : f₁ ↑y = g₁ 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
⊢ 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₁
⊢ f₁ x = f₂ x

Proof state:
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

Tactic:
obtain ⟨hC₁, hC₂⟩ := forall_and.mp hC

Result:
case a.intro.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
hC₁ : ∀ (x_1 : ↥(Algebra.adjoin R {x})), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥(Algebra.adjoin R {x})), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ 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
⊢ f₁ x = f₂ x

Tactic:
have h2 : f₂ y.val = g₂ y := 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
h1 : f₁ ↑y = g₁ y
h2 : f₂ ↑y = g₂ y
⊢ f₁ x = f₂ x

Proof state:
case a.intro.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
hC₁ : ∀ (x_1 : ↥(Algebra.adjoin R {x})), f₁ ↑x_1 ≤ C₁ * f₂ ↑x_1
hC₂ : ∀ (x_1 : ↥(Algebra.adjoin R {x})), f₂ ↑x_1 ≤ C₂ * f₁ ↑x_1
⊢ f₁ x = f₂ x

Tactic:
rw [hy, h1, h2, eq_seminorms hg₁_pm hg₂_pm ⟨C₁, hC₁_pos, hC₁⟩ ⟨C₂, hC₂_pos, hC₂⟩]

Result:
no goals

Proof state:
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
⊢ f₁ = f₂

Tactic:
ext 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
⊢ f₁ x = f₂ x