awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
toRingSeminorm : RingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0
toRingSeminorm_1 : RingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
x : R
⊢ Eq (α := ℝ) ((toRingSeminorm : (a : R) → ℝ) x : ℝ) ((toRingSeminorm_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
toRingSeminorm : RingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0
toRingSeminorm_1 : RingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : RingNorm R) ↦ f.toFun)
      { toRingSeminorm := toRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
x : R
⊢ Eq (α := ℝ) ((toRingSeminorm : (a : R) → ℝ) x : ℝ) ((toRingSeminorm_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 : RingNorm R
⊢ p.toFun = (⇑p : (a : R) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonUnitalRing R
p q : RingNorm 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 : NonAssocRing R
f g : MulRingSeminorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : MulRingSeminorm R) ↦ f.toFun) f)
    ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)
mk :
  ∀ (toAddGroupSeminorm : AddGroupSeminorm R) (map_one' : toAddGroupSeminorm.toFun 1 = 1)
    (map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : MulRingSeminorm R) ↦ f.toFun)
          { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)),
    { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
g : MulRingSeminorm R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun) g)
mk :
  ∀ (toAddGroupSeminorm_1 : AddGroupSeminorm R) (map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1)
    (map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
          { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
        ((fun (f : MulRingSeminorm R) ↦ f.toFun)
          { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
    { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })
mk : toAddGroupSeminorm = toAddGroupSeminorm_1
⊢ { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' : MulRingSeminorm R } =
    { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
toAddGroupSeminorm : AddGroupSeminorm R
map_one' : toAddGroupSeminorm.toFun 1 = 1
map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y
toAddGroupSeminorm_1 : AddGroupSeminorm R
map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1
map_mul'_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 : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : MulRingSeminorm R) ↦ f.toFun)
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_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 : NonAssocRing R
p : MulRingSeminorm 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 : NonAssocRing R
p q : MulRingSeminorm 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 : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
inl : AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun.{u_1} (G := R) 1 0 * AddGroupSeminorm.toFun 1 y
inr : ∀ (hx : x ≠ 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:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
y : R
⊢ AddGroupSeminorm.toFun 1 (0 * y) = AddGroupSeminorm.toFun.{u_1} (G := R) 1 0 * AddGroupSeminorm.toFun 1 y

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
hx : x ≠ 0
inr : AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun.{u_1} (G := R) 1 0
inr₁ : ∀ (hy : 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:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x : R
hx : x ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * 0) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun.{u_1} (G := R) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ AddGroupSeminorm.toFun 1 (x * y) = AddGroupSeminorm.toFun 1 x * AddGroupSeminorm.toFun 1 y

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : DecidableEq R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
x : R
⊢ Eq (α := ℝ) ((1 : (a : R) → ℝ) x : ℝ) (if x = 0 then 0 else 1 : ℝ)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
f g : MulRingNorm R
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ) ((fun (f : MulRingNorm R) ↦ f.toFun) f)
    ((fun (f : MulRingNorm R) ↦ f.toFun) g)
mk :
  ∀ (toMulRingSeminorm : MulRingSeminorm R) (eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : MulRingNorm R) ↦ f.toFun)
          { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : MulRingNorm R) ↦ f.toFun) g)),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
g : MulRingNorm R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun) g)
mk :
  ∀ (toMulRingSeminorm_1 : MulRingSeminorm R)
    (eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0)
    (h :
      Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
        ((fun (f : MulRingNorm R) ↦ f.toFun)
          { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : MulRingNorm R) ↦ f.toFun)
          { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })),
    { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
mk : toMulRingSeminorm = toMulRingSeminorm_1
⊢ { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : MulRingNorm R } =
    { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
mk : ∀ (x : R), Eq (α := ℝ) ((toMulRingSeminorm : (a : R) → ℝ) x : ℝ) ((toMulRingSeminorm_1 : (a : R) → ℝ) x : ℝ)
⊢ toMulRingSeminorm = toMulRingSeminorm_1

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
x : R
⊢ Eq (α := ℝ) ((toMulRingSeminorm : (a : R) → ℝ) x : ℝ) ((toMulRingSeminorm_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 : NonAssocRing R
toMulRingSeminorm : MulRingSeminorm R
eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0
toMulRingSeminorm_1 : MulRingSeminorm R
eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0
h :
  Eq.{max (u_1 + 1) 1} (α := (a : R) → ℝ)
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : MulRingNorm R) ↦ f.toFun)
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
x : R
⊢ Eq (α := ℝ) ((toMulRingSeminorm : (a : R) → ℝ) x : ℝ) ((toMulRingSeminorm_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 : NonAssocRing R
p : MulRingNorm R
⊢ p.toFun = (⇑p : (a : R) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
inst : NonAssocRing R
p q : MulRingNorm 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_1 : Type u_1
inst : NonAssocRing R_1
inst_1 : DecidableEq R_1
inst_2 : NoZeroDivisors R_1
inst_3 : Nontrivial R_1
R : Type u_2
inst_4 : Ring R
inst_5 : Nontrivial R
N : MulRingNorm R
⊢ (fun (v : AbsoluteValue R ℝ) ↦
        { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
          eq_zero_of_map_eq_zero' := ⋯ : MulRingNorm R })
      ((fun (N : MulRingNorm R) ↦
          { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ : AbsoluteValue R ℝ })
        N) =
    N

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
inst : NonAssocRing R_1
inst_1 : DecidableEq R_1
inst_2 : NoZeroDivisors R_1
inst_3 : Nontrivial R_1
R : Type u_2
inst_4 : Ring R
inst_5 : Nontrivial R
v : AbsoluteValue R ℝ
a :
  ∀ (x : R),
    Eq (α := ℝ)
      (((fun (N : MulRingNorm R) ↦
                { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ : AbsoluteValue R ℝ })
              ((fun (v : AbsoluteValue R ℝ) ↦
                  { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
                    eq_zero_of_map_eq_zero' := ⋯ : MulRingNorm R })
                v) :
            (a : R) → ℝ)
          x :
        ℝ)
      ((v : (a : R) → ℝ) x : ℝ)
⊢ (fun (N : MulRingNorm R) ↦
        { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ : AbsoluteValue R ℝ })
      ((fun (v : AbsoluteValue R ℝ) ↦
          { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
            eq_zero_of_map_eq_zero' := ⋯ : MulRingNorm R })
        v) =
    v

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
inst : NonAssocRing R_1
inst_1 : DecidableEq R_1
inst_2 : NoZeroDivisors R_1
inst_3 : Nontrivial R_1
R : Type u_2
inst_4 : Ring R
inst_5 : Nontrivial R
v : AbsoluteValue R ℝ
x : R
⊢ Eq (α := ℝ)
    (((fun (N : MulRingNorm R) ↦
              { toFun := N.toFun, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ : AbsoluteValue R ℝ })
            ((fun (v : AbsoluteValue R ℝ) ↦
                { toFun := v.toFun, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯,
                  eq_zero_of_map_eq_zero' := ⋯ : MulRingNorm R })
              v) :
          (a : R) → ℝ)
        x :
      ℝ)
    ((v : (a : R) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_2
inst : Ring R
inst_1 : Nontrivial R
N : MulRingNorm R
x : R
⊢ Eq (α := ℝ)
    ((((mulRingNormEquivAbsoluteValue : (a : MulRingNorm R) → AbsoluteValue R ℝ) N : AbsoluteValue R ℝ) : (a : R) → ℝ)
        x :
      ℝ)
    ((N : (a : R) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_2
inst : Ring R
inst_1 : Nontrivial R
v : AbsoluteValue R ℝ
x : R
⊢ Eq (α := ℝ)
    ((((Equiv.symm mulRingNormEquivAbsoluteValue : (a : AbsoluteValue R ℝ) → MulRingNorm R) v : MulRingNorm R) :
          (a : R) → ℝ)
        x :
      ℝ)
    ((v : (a : R) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
obtain : ∀ (c : K) (hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)), x = 0
⊢ x = 0

Tactic:
obtain ⟨c, hc⟩ := RingSeminorm.ne_zero_iff.mp hnt

Premises used: RingSeminorm.ne_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
by_contra : ∀ (hn0 : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra hn0
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
rw : Eq (α := ℝ) ((f : (a : K) → ℝ) (x * (c * x⁻¹)) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)

Tactic:
rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]

Premises used: mul_inv_cancel₀, mul_assoc, mul_comm, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((f.toAddGroupSeminorm : (a : K) → ℝ) x : ℝ)
      ((f.toAddGroupSeminorm : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤
    0
rw₁ : f.toFun x * f.toFun (c * x⁻¹) ≤ 0
rw₂ : 0 * f.toFun (c * x⁻¹) ≤ 0
rw₃ rw₄ : LE.le (α := ℝ) 0 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : K) → ℝ) x : ℝ) ((f : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤ 0

Tactic:
rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]

Premises used: MulZeroClass.zero_mul, AddGroupSeminorm.toFun_eq_coe, RingSeminorm.toFun_eq_coe
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
⊢ Eq (α := ℝ) ((f : (a : K) → ℝ) (x * (c * x⁻¹)) : ℝ) (0 : ℝ)

Tactic:
exact
          le_antisymm
            (le_trans (map_mul_le_mul f _ _)
              (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]))
            (apply_nonneg f _)

Premises used: le_antisymm, NonnegHomClass.apply_nonneg, le_trans, SubmultiplicativeHomClass.map_mul_le_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
⊢ Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)

Tactic:
have hc0 : f c = 0 := by
        rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]
        exact
          le_antisymm
            (le_trans (map_mul_le_mul f _ _)
              (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]))
            (apply_nonneg f _)
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
hc0 : Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
⊢ False

Tactic:
hc hc0
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
hc0 : Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
⊢ False

Tactic:
exact hc hc0