-- Mathlib/Analysis/Normed/Ring/IsPowMulFaithful.lean
theorem eq_seminorms {F : Type*} {α : outParam (Type*)} [Ring α] [FunLike F α ℝ]
    [RingSeminormClass F α ℝ] {f g : F} (hfpm : IsPowMul f) (hgpm : IsPowMul g)
    (hfg : ∃ (r : ℝ) (_ : 0 < r), ∀ a : α, f a ≤ r * g a)
    (hgf : ∃ (r : ℝ) (_ : 0 < r), ∀ a : α, g a ≤ r * f a) : f = g

Proof state:
case intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
hgf : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
⊢ f = g

Tactic:
obtain ⟨s, hs0, hs⟩ := hgf

Result:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
⊢ f = g

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
⊢ f = g

Tactic:
have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩

Result:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
⊢ f = g

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
⊢ f = g

Tactic:
have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩

Result:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
⊢ f = g

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
⊢ ⇑f = ⇑g

Tactic:
ext x

Result:
case intro.intro.intro.intro.h
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
x : α
⊢ f x = g x

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
⊢ f = g

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

Result:
case intro.intro.intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
⊢ ⇑f = ⇑g

Proof state:
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
hfg : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a
hgf : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a
⊢ f = g

Tactic:
obtain ⟨r, hr0, hr⟩ := hfg

Result:
case intro.intro
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
hgf : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
⊢ f = g

Proof state:
case intro.intro.intro.intro.h
F : Type u_1
α : outParam (Type u_2)
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
r : ℝ
hr0 : 0 < r
hr : ∀ (a : α), f a ≤ r * g a
s : ℝ
hs0 : 0 < s
hs : ∀ (a : α), g a ≤ s * f a
hle : RingHom.IsBoundedWrt (⇑f) (⇑g) (RingHom.id α)
hge : RingHom.IsBoundedWrt (⇑g) (⇑f) (RingHom.id α)
x : α
⊢ f x = g x

Tactic:
exact le_antisymm (contraction_of_isPowMul_of_boundedWrt g hfpm hge x)
  (contraction_of_isPowMul_of_boundedWrt f hgpm hle x)

Result:
no goals