mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case mk.mk
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1 + c₂ • i✝¹
j_mul_j✝¹ : j✝¹ * j✝¹ = c₃ • 1
i_mul_j✝¹ : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = c₂ • j✝¹ - k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1 + c₂ • i✝
j_mul_j✝ : j✝ * j✝ = c₃ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = c₂ • j✝ - k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1 + c₂ • i✝¹
j_mul_j✝¹ : j✝¹ * j✝¹ = c₃ • 1
i_mul_j✝¹ : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = c₂ • j✝¹ - k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1 + c₂ • i✝
j_mul_j✝ : j✝ * j✝ = c₃ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = c₂ • j✝ - k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ ↑s ∧ (↑t).Nonempty ∨ 0 ∈ ↑t ∧ (↑s).Nonempty ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ ↑s ∧ (↑t).Nonempty ∨ 0 ∈ ↑t ∧ (↑s).Nonempty ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommMonoid✝¹ = toAddCommMonoid✝

Tactic:
;

Goal state after:
case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommMonoid✝¹ = toAddCommMonoid✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
case e_toAddCommMonoid
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹,
        mul_assoc := mul_assoc✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_assoc := mul_assoc✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }

Tactic:
;

Goal state after:
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹,
        mul_assoc := mul_assoc✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_assoc := mul_assoc✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ HAdd.hAdd = HAdd.hAdd
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
⊢ ↑n = ↑n

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddMonoid =
    inst₂.toAddMonoid
h_zero' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toZero =
    inst₂.toZero
h_one' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toOne =
    inst₂.toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
      natCast_succ := natCast_succ✝ } =
    inst₂

Tactic:
;

Goal state after:
R : Type u
inst₂ : AddMonoidWithOne R
toAddMonoid✝ : AddMonoid R
toOne✝ : One R
natCast✝ : ℕ → R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddMonoid =
    inst₂.toAddMonoid
h_zero' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toZero =
    inst₂.toZero
h_one' :
  { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toOne =
    inst₂.toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
      natCast_succ := natCast_succ✝ } =
    inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
add_comm✝¹ : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne✝ : AddMonoidWithOne R
add_comm✝ : ∀ (a b : R), a + b = b + a
a✝ :
  { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ }.toAddMonoidWithOne =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }.toAddMonoidWithOne
⊢ { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ } =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }

Tactic:
;

Goal state after:
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
add_comm✝¹ : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne✝ : AddMonoidWithOne R
add_comm✝ : ∀ (a b : R), a + b = b + a
a✝ :
  { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ }.toAddMonoidWithOne =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }.toAddMonoidWithOne
⊢ { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ } =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_2.e_2
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁.toMulZeroOneClass.toMulOneClass = inst₂.toMulZeroOneClass.toMulOneClass

Tactic:
;

Goal state after:
case e_2.e_2
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ inst₁.toMulZeroOneClass.toMulOneClass = inst₂.toMulZeroOneClass.toMulOneClass
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_2.e_2
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ Mul.mul = Mul.mul

Tactic:
;

Goal state after:
case e_2.e_2
R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
⊢ Mul.mul = Mul.mul
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { toAddCommGroup := toAddCommGroup✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ } =
    inst₂

Tactic:
;

Goal state after:
R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { toAddCommGroup := toAddCommGroup✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ } =
    inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝

Tactic:
;

Goal state after:
case e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toAddCommGroup✝¹ = toAddCommGroup✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
case e_toAddCommGroup
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
mul✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ HAdd.hAdd = HAdd.hAdd
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ } = inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ } = inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
⊢ HAdd.hAdd = HAdd.hAdd
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
h_group :
  { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, toZSMul := inst₁.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ } =
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, toZSMul := inst₂.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
⊢ inst₁ = inst₂

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
h_group :
  { toAddMonoid := inst₁.toAddMonoid, toNeg := inst₁.toNeg, toSub := inst₁.toSub, toZSMul := inst₁.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ } =
    { toAddMonoid := inst₂.toAddMonoid, toNeg := inst₂.toNeg, toSub := inst₂.toSub, toZSMul := inst₂.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℤ
⊢ IntCast.intCast n = IntCast.intCast n
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ ↑n = ↑n

Tactic:
;

Goal state after:
case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case negSucc
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ -↑(n + 1) = -↑(n + 1)

Tactic:
;

Goal state after:
case negSucc
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ -↑(n + 1) = -↑(n + 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddCommGroup = inst₂.toAddCommGroup
toIntCast_eq✝ : inst₁.toIntCast = inst₂.toIntCast
h_addMonoidWithOne :
  { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ } =
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ inst₁ = inst₂

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddCommGroup = inst₂.toAddCommGroup
toIntCast_eq✝ : inst₁.toIntCast = inst₂.toIntCast
h_addMonoidWithOne :
  { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ } =
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
⊢ HMul.hMul = HMul.hMul

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
⊢ HMul.hMul = HMul.hMul
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
;

Goal state after:
R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toSemiring = inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
⊢ HAdd.hAdd = HAdd.hAdd