awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α)
x : α
⊢ Eq (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)

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

Premises used: contraction_of_isPowMul_of_boundedWrt, le_antisymm
-- 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 α)
x : α
⊢ Eq (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)

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

Premises used: contraction_of_isPowMul_of_boundedWrt, le_antisymm
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) : ℝ)
a : ∀ (x : S), Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)
⊢ f₁ = f₂

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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₂
⊢ IsPowMul (R := ↥R[x]) (⇑g₁ : (a : ↥R[x]) → ℝ)

Tactic:
have hg₁_pm : IsPowMul g₁ := IsPowMul.restriction _ hf₁_pm
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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]) → ℝ)
⊢ IsPowMul (R := ↥R[x]) (⇑g₂ : (a : ↥R[x]) → ℝ)

Tactic:
have hg₂_pm : IsPowMul g₂ := IsPowMul.restriction _ hf₂_pm
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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 ⋯
⊢ x = (↑y : S)

Tactic:
have hy : x = y.val := rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) → ℝ) (↑y : S) : ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ)

Tactic:
have h1 : f₁ y.val = g₁ y := rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) → ℝ) (↑y : S) : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)

Tactic:
have h2 : f₂ y.val = g₂ y := rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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 : ℝ)
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 : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)

Tactic:
obtain ⟨C₁, C₂, hC₁_pos, hC₂_pos, hC⟩ := h_eq x
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) : ℝ)
⊢ ∀ (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

Premises used: Iff.mp, forall_and
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) : ℝ)
⊢ ∀ (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

Premises used: Iff.mp, forall_and
-- Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
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) : ℝ)
hC₂ : ∀ (x_1 : ↥R[x]), (f₂ : (a : S) → ℝ) (↑x_1 : S) ≤ HMul.hMul (β := ℝ) C₂ ((f₁ : (a : S) → ℝ) (↑x_1 : S) : ℝ)
a : Eq (α := ℝ) ((f₁ : (a : S) → ℝ) (↑y : S) : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
a₁ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((f₂ : (a : S) → ℝ) (↑y : S) : ℝ)
a₂ : Eq (α := ℝ) ((g₁ : (a : ↥R[x]) → ℝ) y : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
a₃ a₄ : Eq (α := ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ) ((g₂ : (a : ↥R[x]) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((f₁ : (a : S) → ℝ) x : ℝ) ((f₂ : (a : S) → ℝ) x : ℝ)

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

Premises used: eq_seminorms, Exists.intro
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
f g : RingSeminorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : RingSeminorm R) ↦ f.toFun) f)
    ((fun (f : RingSeminorm R) ↦ f.toFun) g)
mk :
  ∀ (toAddGroupSeminorm : AddGroupSeminorm R)
    (mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
        ((fun (f : RingSeminorm R) ↦ f.toFun) g)),
    { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
g : RingSeminorm R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) g)
mk :
  ∀ (toAddGroupSeminorm_1 : AddGroupSeminorm R)
    (mul_le'_1 :
      ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
        ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })),
    { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
mk : toAddGroupSeminorm = toAddGroupSeminorm_1
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' : RingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
mk : ∀ (x : R), Eq (α := ℝ) ((toAddGroupSeminorm : (a : R) → ℝ) x : ℝ) ((toAddGroupSeminorm_1 : (a : R) → ℝ) x : ℝ)
⊢ toAddGroupSeminorm = toAddGroupSeminorm_1

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
x : R
⊢ Eq (α := ℝ) ((toAddGroupSeminorm : (a : R) → ℝ) x : ℝ) ((toAddGroupSeminorm_1 : (a : R) → ℝ) x : ℝ)

Tactic:
congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toAddGroupSeminorm : AddGroupSeminorm R
mul_le' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
mul_le'_1 :
  ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) ≤ toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm, mul_le' := mul_le' })
    ((fun (f : RingSeminorm R) ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm_1, mul_le' := mul_le'_1 })
x : R
⊢ Eq (α := ℝ) ((toAddGroupSeminorm : (a : R) → ℝ) x : ℝ) ((toAddGroupSeminorm_1 : (a : R) → ℝ) x : ℝ)

Tactic:
exact congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
p : RingSeminorm R
⊢ Eq (α := (a : R) → ℝ) (⇑p.toAddGroupSeminorm : (a : R) → ℝ) (⇑p : (a : R) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
p q : RingSeminorm R
⊢ (∀ (x : R), Eq (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) ((q : (a : R) → ℝ) x : ℝ)) → p = q

Tactic:
DFunLike.ext p q

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
p : RingSeminorm R
⊢ p = 0 ↔ ∀ (x : R), Eq (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
DFunLike.ext_iff

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
p : RingSeminorm R
⊢ p ≠ 0 ↔ ∃ (x : R), Ne (α := ℝ) ((p : (a : R) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp [eq_zero_iff]

Premises used: RingSeminorm.eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
pos : ∀ (h : x * y = 0), AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
neg : ∀ (h : ¬x * y = 0), AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
by_cases h : x * y = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
(if_pos h).trans_le (mul_nonneg ?_ ?_)

Premises used: mul_nonneg, Eq.trans_le, if_pos, ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : 0 ≤ AddGroupSeminorm.toFun 1 x
pos₁ : 0 ≤ AddGroupSeminorm.toFun 1 y
⊢ AddGroupSeminorm.toFun 1 (x * y) ≤ AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
refine (if_pos h).trans_le (mul_nonneg ?_ ?_)

Premises used: mul_nonneg, Eq.trans_le, if_pos
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : LE.le (α := ℝ) 0 (if x = 0 then 0 else 1)
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x

Tactic:
change _ ≤ ite _ _ _

Premises used: ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : x = 0 → LE.le (α := ℝ) 0 0
neg : ¬x = 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if x = 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : x = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : ¬x = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : x = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)
⊢ 0 ≤ AddGroupSeminorm.toFun 1 y

Tactic:
change _ ≤ ite _ _ _

Premises used: ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
pos : y = 0 → LE.le (α := ℝ) 0 0
neg : ¬y = 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if y = 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : y = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : ¬y = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : DecidableEq R
x y : R
h : x * y = 0
h_1 : y = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one