awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue T S
x : R
⊢ (algebraMap R (WithAbs v) : (a : R) → WithAbs v) x = toAbs v ((algebraMap R T : (a : R) → T) x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue T S
h : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := WithAbs v) (⇑(algebraMap R (WithAbs v)) : (a : R) → WithAbs v)

Tactic:
(toAbs_injective v).comp h

Premises used: WithAbs.toAbs_injective, Function.Injective.comp
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue R S
w : AbsoluteValue T S
x : WithAbs v
⊢ Eq.{u_4 + 1} (α := T)
    (ofAbs.{u_4, u_2} (S := S) (v := w) ((algebraMap (WithAbs v) (WithAbs w) : (a : WithAbs v) → WithAbs w) x) : T)
    ((algebraMap R T : (a : R) → T) x.ofAbs : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue T S
x : WithAbs v
⊢ (algEquiv R v : (a : WithAbs v) → T) x = x.ofAbs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Ring.WithAbs
Goal:
S : Type u_2
inst : Semiring S
inst_1 : PartialOrder S
R : Type u_3
T : Type u_4
inst_2 : CommSemiring R
inst_3 : Semiring T
inst_4 : Algebra R T
v : AbsoluteValue T S
x : T
⊢ (AlgEquiv.symm (algEquiv R v) : (a : T) → WithAbs v) x = toAbs v x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 f f' : AlgebraNorm R S
h : Eq (α := (a : S) → ℝ) (⇑f.toRingSeminorm : (a : S) → ℝ) (⇑f'.toRingSeminorm : (a : S) → ℝ)
mk :
  ∀ (toRingNorm : RingNorm S) (smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x)
    (h :
      Eq (α := (a : S) → ℝ)
        (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
        (⇑f'.toRingSeminorm : (a : S) → ℝ)),
    { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = f'
⊢ f = f'

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f f' : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
h :
  Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
    (⇑f'.toRingSeminorm : (a : S) → ℝ)
mk :
  ∀ (toRingNorm_1 : RingNorm S) (smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x)
    (h :
      Eq (α := (a : S) → ℝ)
        (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
        (⇑{ toRingNorm := toRingNorm_1, smul' := smul'_1 : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)),
    { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = { toRingNorm := toRingNorm_1, smul' := smul'_1 }
⊢ { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = f'

Tactic:
cases f'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h :
  Eq (α := (a : S) → ℝ) (⇑{ toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
    (⇑{ toRingNorm := toRingNorm_1, smul' := smul'_1 : AlgebraNorm R S }.toRingSeminorm : (a : S) → ℝ)
mk : toRingNorm = toRingNorm_1
⊢ { toRingNorm := toRingNorm, smul' := smul' : AlgebraNorm R S } = { toRingNorm := toRingNorm_1, smul' := smul'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h : Eq (α := (a : S) → ℝ) (⇑toRingNorm.toRingSeminorm : (a : S) → ℝ) (⇑toRingNorm_1.toRingSeminorm : (a : S) → ℝ)
mk : ∀ (s : S), Eq (α := ℝ) ((toRingNorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)
⊢ toRingNorm = toRingNorm_1

Tactic:
ext s
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h : Eq (α := (a : S) → ℝ) (⇑toRingNorm.toRingSeminorm : (a : S) → ℝ) (⇑toRingNorm_1.toRingSeminorm : (a : S) → ℝ)
s : S
mk : Eq (α := ℝ) ((toRingNorm_1.toRingSeminorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)
⊢ Eq (α := ℝ) ((toRingNorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)

Tactic:
erw [h]
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toRingNorm : RingNorm S
smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x
toRingNorm_1 : RingNorm S
smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x
h : Eq (α := (a : S) → ℝ) (⇑toRingNorm.toRingSeminorm : (a : S) → ℝ) (⇑toRingNorm_1.toRingSeminorm : (a : S) → ℝ)
s : S
⊢ Eq (α := ℝ) ((toRingNorm_1.toRingSeminorm : (a : S) → ℝ) s : ℝ) ((toRingNorm_1 : (a : S) → ℝ) s : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
p : AlgebraNorm R S
⊢ p.toFun = (⇑p : (a : S) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
p q : AlgebraNorm R S
⊢ (∀ (x : S), Eq (α := ℝ) ((p : (a : S) → ℝ) x : ℝ) ((q : (a : S) → ℝ) x : ℝ)) → p = q

Tactic:
DFunLike.ext p q

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = HMul.hMul (β := ℝ) ‖a‖ ((f : (a : S) → ℝ) 1 : ℝ)
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← hf1]

Premises used: Norm.norm, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = HMul.hMul (β := ℝ) ‖a‖ ((f : (a : S) → ℝ) 1 : ℝ)

Tactic:
f.smul' _ _

Premises used: AlgebraNorm.smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = HMul.hMul (β := ℝ) ‖a‖ ((f : (a : S) → ℝ) 1 : ℝ)

Tactic:
exact f.smul' _ _

Premises used: AlgebraNorm.smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
⊢ (f : (a : S) → ℝ) ((algebraMap R S : (a : R) → S) a : S) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
extends_norm' hf1 _

Premises used: AlgebraNorm.extends_norm'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
hf1 : Eq (α := ℝ) ((f : (a : S) → ℝ) 1 : ℝ) (1 : ℝ)
a : R
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
exact extends_norm' hf1 _

Premises used: AlgebraNorm.extends_norm'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) (↑x : S) : ℝ) (0 : ℝ)
rw : (↑x : S) = 0
⊢ x = 0

Tactic:
rw [← ZeroMemClass.coe_eq_zero]

Premises used: ZeroMemClass.coe_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) (↑x : S) : ℝ) (0 : ℝ)
⊢ (↑x : S) = 0

Tactic:
eq_zero_of_map_eq_zero f hx

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) (↑x : S) : ℝ) (0 : ℝ)
⊢ (↑x : S) = 0

Tactic:
exact eq_zero_of_map_eq_zero f hx

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
⊢ Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) 0 : S) : ℝ) (0 : ℝ)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x y : A
⊢ (f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) (x + y) : S) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)
      ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) y : S) : ℝ)

Tactic:
simp only [map_add, map_add_le_add]

Premises used: map_add, SubadditiveHomClass.map_add_le_add
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x : A
⊢ Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) (-x) : S) : ℝ)
    ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)

Tactic:
simp only [map_neg, map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map, map_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x y : A
⊢ (f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) (x * y) : S) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)
      ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) y : S) : ℝ)

Tactic:
simp only [map_mul, map_mul_le_mul]

Premises used: map_mul, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x : A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ) (0 : ℝ)
rw : Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) (0 : S)
⊢ x = 0

Tactic:
rw [← map_eq_zero_iff (algebraMap A S) hinj]

Premises used: Algebra.algebraMap, map_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x : A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ) (0 : ℝ)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) (0 : S)

Tactic:
eq_zero_of_map_eq_zero f hx

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
x : A
hx : Eq (α := ℝ) ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ) (0 : ℝ)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) (0 : S)

Tactic:
exact eq_zero_of_map_eq_zero f hx

Premises used: AddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
r : R
x : A
simp :
  (f : (a : S) → ℝ)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap A S : (a : A) → S) x : S)) =
    HMul.hMul (β := ℝ) ‖r‖ ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)
⊢ (f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) (r • x) : S) =
    HMul.hMul (β := ℝ) ‖r‖ ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)

Tactic:
simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply]

Premises used: map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
inst : SeminormedCommRing R
S : Type u_2
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
A : Type u_3
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra A S
inst_6 : IsScalarTower R A S
hinj : Function.Injective.{u_3 + 1, u_2 + 1} (α := A) (β := S) (⇑(algebraMap A S) : (a : A) → S)
f : AlgebraNorm R S
r : R
x : A
⊢ (f : (a : S) → ℝ)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap A S : (a : A) → S) x : S)) =
    HMul.hMul (β := ℝ) ‖r‖ ((f : (a : S) → ℝ) ((algebraMap A S : (a : A) → S) x : S) : ℝ)

Tactic:
simp only [← smul_eq_mul, algebraMap_smul, map_smul_eq_mul]

Premises used: algebraMap_smul, SeminormClass.map_smul_eq_mul, smul_eq_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h :
  Eq.{max (u_2 + 1) 1} (α := (a : S) → ℝ) ((fun (f : MulAlgebraNorm R S) ↦ f.toFun) f)
    ((fun (f : MulAlgebraNorm R S) ↦ f.toFun) f')
⊢ f.toMulRingSeminorm = f'.toMulRingSeminorm

Tactic:
simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe, DFunLike.coe_fn_eq] at h

Premises used: AddGroupSeminorm.toFun_eq_coe, DFunLike.coe_fn_eq, MulRingSeminorm.toFun_eq_coe
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f_1 : AlgebraNorm R S
f f' : MulAlgebraNorm R S
h : f.toMulRingSeminorm = f'.toMulRingSeminorm
obtain :
  ∀ (toMulRingSeminorm : MulRingSeminorm S) (eq_zero_of_map_eq_zero' : ∀ (x : S), toMulRingSeminorm.toFun x = 0 → x = 0)
    (smul' :
      ∀ (a : R) (x : S),
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
                MulRingNorm S }.toFun
            (a • x) =
          ‖a‖ *
            { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
                  MulRingNorm S }.toFun
              x)
    (h :
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
            MulAlgebraNorm R S }.toMulRingSeminorm =
        f'.toMulRingSeminorm),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
        MulAlgebraNorm R S } =
      f'
⊢ f = f'

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
f' : MulAlgebraNorm R S
toMulRingSeminorm : MulRingSeminorm S
eq_zero_of_map_eq_zero' : ∀ (x : S), toMulRingSeminorm.toFun x = 0 → x = 0
smul' :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm S }.toFun
        (a • x) =
      ‖a‖ *
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
              MulRingNorm S }.toFun
          x
h :
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
        MulAlgebraNorm R S }.toMulRingSeminorm =
    f'.toMulRingSeminorm
obtain :
  ∀ (toMulRingSeminorm_1 : MulRingSeminorm S)
    (eq_zero_of_map_eq_zero'_1 : ∀ (x : S), toMulRingSeminorm_1.toFun x = 0 → x = 0)
    (smul'_1 :
      ∀ (a : R) (x : S),
        { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
                MulRingNorm S }.toFun
            (a • x) =
          ‖a‖ *
            { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
                  MulRingNorm S }.toFun
              x)
    (h :
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
            MulAlgebraNorm R S }.toMulRingSeminorm =
        { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1,
            smul' := smul'_1 : MulAlgebraNorm R S }.toMulRingSeminorm),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
        MulAlgebraNorm R S } =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1,
        smul' := smul'_1 }
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
      MulAlgebraNorm R S } =
    f'

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : AlgebraNorm R S
toMulRingSeminorm : MulRingSeminorm S
eq_zero_of_map_eq_zero' : ∀ (x : S), toMulRingSeminorm.toFun x = 0 → x = 0
smul' :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm S }.toFun
        (a • x) =
      ‖a‖ *
        { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' :
              MulRingNorm S }.toFun
          x
toMulRingSeminorm_1 : MulRingSeminorm S
eq_zero_of_map_eq_zero'_1 : ∀ (x : S), toMulRingSeminorm_1.toFun x = 0 → x = 0
smul'_1 :
  ∀ (a : R) (x : S),
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
            MulRingNorm S }.toFun
        (a • x) =
      ‖a‖ *
        { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 :
              MulRingNorm S }.toFun
          x
h :
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
        MulAlgebraNorm R S }.toMulRingSeminorm =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1, smul' := smul'_1 :
        MulAlgebraNorm R S }.toMulRingSeminorm
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero', smul' := smul' :
      MulAlgebraNorm R S } =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1, smul' := smul'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p : MulAlgebraNorm R S
⊢ p.toFun = (⇑p : (a : S) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : MulAlgebraNorm R S
⊢ (∀ (x : S), Eq (α := ℝ) ((p : (a : S) → ℝ) x : ℝ) ((q : (a : S) → ℝ) x : ℝ)) → p = q

Tactic:
DFunLike.ext p q

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * 1
rw₁ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖ * f.toFun 1
rw₂ : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = f.toFun (HSMul.hSMul (β := S) a 1)
rw₃ rw₄ :
  Eq (α := ℝ) ((f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) : ℝ) ((f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) : ℝ)
⊢ (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]

Premises used: Norm.norm, MulRingNorm.toMulRingSeminorm, MulAlgebraNorm.toFun_eq_coe, mul_one, MulRingSeminorm.map_one', MulAlgebraNorm.toMulRingNorm, MulAlgebraNorm.smul'
-- Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
Goal:
R : Type u_1
S : Type u_2
inst : SeminormedCommRing R
inst_1 : Ring S
inst_2 : Algebra R S
f : MulAlgebraNorm R S
a : R
rw : (f : (a : S) → ℝ) (HSMul.hSMul (β := S) a 1) = ‖a‖
⊢ (f : (a : S) → ℝ) ((algebraMap R S : (a : R) → S) a : S) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one