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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ reflect n (C u * X ^ k + C v * X ^ m + C w * X ^ n) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
reflect_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (reflect n (C u * X ^ k + C v * X ^ m) + reflect n (C w * X ^ n)) * X ^ k = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (reflect n (C u * X ^ k + C v * X ^ m) + reflect n (C w * X ^ n)) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
reflect_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ (reflect n (C u * X ^ k) + reflect n (C v * X ^ m) + reflect n (C w * X ^ n)) * X ^ k =
    trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
⊢ ⊥ < (∏ i ∈ s, g i).degree

Tactic:
rw [bot_lt_iff_ne_bot, degree_ne_bot]
        exact hpm.ne_zero_of_polynomial_ne fun h : r₂ i - r₁ i = g i => lt_irrefl _ (h ▸ hdr)

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
simp only [sub_mul, Finset.sum_sub_distrib] at hp0

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : q₁ - q₂ = 0
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ x ∈ s, r₁ x * ∏ k ∈ s.erase x, g k - ∑ x ∈ s, r₂ x * ∏ k ∈ s.erase x, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * x✝).re

Tactic:
simp [mul_add]

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝².re * x✝¹.re + x✝².re * x✝.re + (a * x✝².im * x✝¹.im + a * x✝².im * x✝.im) =
    x✝².re * x✝¹.re + a * x✝².im * x✝¹.im + (x✝².re * x✝.re + a * x✝².im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * (x✝¹ + x✝)).im = (x✝² * x✝¹ + x✝² * x✝).im

Tactic:
simp [mul_add]

Goal state after:
case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝².re * x✝¹.im + x✝².re * x✝.im + (x✝².im * x✝¹.re + x✝².im * x✝.re) + (b * x✝².im * x✝¹.im + b * x✝².im * x✝.im) =
    x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im + (x✝².re * x✝.im + x✝².im * x✝.re + b * x✝².im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : CommRing R
inst✝ : CharZero R
m n : ℕ
⊢ ↑m = ↑n → m = n

Tactic:
by
    simp [QuadraticAlgebra.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x : Rᵐᵒᵖ
⊢ ∀ {y z : Rᵐᵒᵖ},
    op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
y

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : Rᵐᵒᵖ
⊢ ∀ {z : Rᵐᵒᵖ},
    op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x

Tactic:
← left_cancel x

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x : Conj G
⊢ ∀ {y z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)

Tactic:
y

Goal state after:
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ ∀ {z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x : Dihedral n
⊢ ∀ {y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
y

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y : Dihedral n
⊢ ∀ {z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x : R
⊢ ∀ {y : R}, act' (x ◃ y) = act' x ◃ act' y

Tactic:
y

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x ◃ act' y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
mul✝¹ add✝¹ : 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
mul✝ add✝ : 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
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { mul := mul✝¹, add := add✝¹, left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹ } =
    { mul := mul✝, add := add✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: 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✝¹, mul := mul✝¹, left_distrib := left_distrib✝¹,
      right_distrib := right_distrib✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹ } =
    { toAddCommMonoid := toAddCommMonoid✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ }

Tactic:
congr

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: 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:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
toAddMonoid✝¹ : AddMonoid R
toOne✝¹ : One R
natCast✝¹ : ℕ → R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
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 =
    { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddMonoid
h_zero' :
  { natCast := natCast✝¹, toAddMonoid := toAddMonoid✝¹, toOne := toOne✝¹, natCast_zero := natCast_zero✝¹,
        natCast_succ := natCast_succ✝¹ }.toZero =
    { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toZero
h_one' :
  { natCast := natCast✝¹, toAddMonoid := toAddMonoid✝¹, toOne := toOne✝¹, natCast_zero := natCast_zero✝¹,
        natCast_succ := natCast_succ✝¹ }.toOne =
    { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toOne
h_natCast : NatCast.natCast = NatCast.natCast
⊢ { natCast := natCast✝¹, toAddMonoid := toAddMonoid✝¹, toOne := toOne✝¹, natCast_zero := natCast_zero✝¹,
      natCast_succ := natCast_succ✝¹ } =
    { natCast := natCast✝, toAddMonoid := toAddMonoid✝, toOne := toOne✝, natCast_zero := natCast_zero✝,
      natCast_succ := natCast_succ✝ }

Tactic:
congr

Goal state after:
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:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x✝¹ x✝ : R
⊢ x✝¹ + x✝ = x✝¹ + x✝

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: 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✝¹, mul := mul✝¹, left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹,
      zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹ } =
    { toAddCommGroup := toAddCommGroup✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ }

Tactic:
congr

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.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ F
      { re := x✝.re + 0 + 0 + 0, imI := 0 + x✝.imI • 1 + 0 + 0, imJ := 0 + 0 + x✝.imJ • 1 + 0,
        imK := 0 + 0 + 0 + x✝.imK • 1 } =
    F x✝

Tactic:
congr

Goal state after:
case e_6.e_re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝.re + 0 + 0 + 0 = x✝.re

case e_6.e_imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + x✝.imI • 1 + 0 + 0 = x✝.imI

case e_6.e_imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + 0 + x✝.imJ • 1 + 0 = x✝.imJ

case e_6.e_imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + 0 + 0 + x✝.imK • 1 = x✝.imK
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
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 =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_assoc := mul_assoc✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ + x✝ = x✝¹ + x✝

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝

Tactic:
congr

Goal state after:
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:
congr

Goal state after:
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:
congr

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toOne
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonAssocSemiring =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroupWithOne =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne
⊢ toOne✝¹ = toOne✝

Tactic:
injection h₂

Goal state after: