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

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
⊢ 0 < ↑(sSupFun hc) (y - x)

Tactic:
obtain ⟨f, hmem, hf⟩ :=
    (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hyx

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
⊢ 0 < ↑(sSupFun hc) (y - x)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.IsMonicOfDegree 0 ↔ p = 1

Tactic:
by
  simp only [isMonicOfDegree_iff']
  refine ⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩
  subst H
  simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
← hp.natDegree_eq,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * n)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case ha
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ 1 ≤ spanCoeffs(q)

pp: case hmn
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ deg(r) + 1 ≤ deg(p)

Tactic:
exacts [le_sup_left, deg_r_lt_deg_p]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0

Tactic:
tauto

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

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    (q %ₘ g + g * (q /ₘ g)) * g ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc

Tactic:
modByMonic_add_div q

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i = q * g ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
by
    by_cases hab : R a b
    case pos => simp [destutter', if_pos hab, Nat.le_succ]
    obtain hac | hac : R a c ∨ Rᶜ a c := em _
    · have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
      simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]
    · have hbc : ¬R b c := trans (symm hab) hac
      simp only [destutter', if_neg hbc, if_neg hac, if_neg hab]
      exact (length_destutter'_congr cs hab).ge

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

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Tactic:
refine ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩

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

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
⊢ p.IsUnitTrinomial

Tactic:
have key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1 := fun k hk =>
      Int.sq_eq_one_of_sq_le_three
        ((single_le_sum (fun k _ => sq_nonneg (p.coeff k)) hk).trans hp.le) (mem_support_iff.mp hk)

Goal state after:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
key : ∀ k ∈ p.support, p.coeff k ^ 2 = 1
⊢ p.IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
⊢ ∃ c₀ cs,
    ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧ ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs

Tactic:
have h₆ : P.eraseLead ≠ 0 := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₂ : P.nextCoeff ≠ 0
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
⊢ ∃ c₀ cs,
    ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs ∧ ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝³ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝² : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝¹ : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ((X - C η) * P).nextCoeff = 0
this✝ : ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead
this :
  ((X - C η) * P).coeffList =
    ((X - C η) * P).leadingCoeff ::
      (List.replicate (((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have : ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1 := by grind

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝⁴ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝³ : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝² : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ((X - C η) * P).nextCoeff = 0
this✝¹ : ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead
this✝ :
  ((X - C η) * P).coeffList =
    ((X - C η) * P).leadingCoeff ::
      (List.replicate (((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.coeffList)
this : ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑u + (↑v + ↑w)) ^ 2 = (↑x + (↑v + ↑z)) ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
add_comm (u : ℤ),

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑v + ↑w + ↑u) ^ 2 = (↑x + (↑v + ↑z)) ^ 2
⊢ q = p ∨ q = p.mirror
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✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).re =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).re

Tactic:
simp [Algebra.smul_def]

Goal state after:
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✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).im =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).im

Tactic:
simp [Algebra.smul_def]

Goal state after:
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.i * F q.i = c₁ • 1 + c₂ • F q.i

Tactic:
rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]

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

Goal state before:
pp: case mk.mk.e_toIntCast
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
⊢ toIntCast✝¹ = toIntCast✝

Tactic:
injection h₃

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

Goal state before:
pp: case e_toNeg
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
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₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toNeg✝¹ = toNeg✝

Tactic:
injection h₃

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

Goal state before:
pp: case e_toSub
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
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₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toSub✝¹ = toSub✝

Tactic:
injection h₃

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

Goal state before:
pp: case mk.mk.e_toZSMul
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
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₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toZSMul✝¹ = toZSMul✝

Tactic:
injection h₃

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ⇑f
a b : α
⊢ f' (a * b) = a * f' b

Tactic:
simp_rw [h, map_mul_left]

Goal state after: