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

Goal state before:
pp: case refine_2
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

Tactic:
have hzy : z < y := by
    change z.val < y.val
    refine (sub_lt_sub_iff_right x).mp <|
      ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg ?_ (sub_nonneg_of_le h.le)
    simpa using! hz (by simpa [sub_eq_zero])

Goal state after:
case refine_2
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
⊢ ↑(A.unitGroupMulEquiv.symm ↑x) ∈ A.principalUnitGroup

Tactic:
rw [A.coe_mem_principalUnitGroup_iff]; simp

Goal state after:
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
⊢ ↑(f.extendFun hx) y < ↑(f.extendFun hx) z

Tactic:
apply lt_of_sub_pos

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
⊢ 0 < ↑(f.extendFun hx) z - ↑(f.extendFun hx) y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
⊢ 0 = sInf {r | x < f r}

Tactic:
have hr {r} := hx.trans_le (mk_map_nonneg_of_archimedean f r)

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
⊢ 0 = sInf {r | x < f r}
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg.inr
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (ofLex (f.eval x)).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d

Tactic:
rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc, eval, ofLex_toLex]

Goal state after:
case neg.inr
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ }.coeff d = 0
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p + q) = evalEval x y p + evalEval x y q

Tactic:
simp only [evalEval, eval_add]

Goal state after:
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
⊢ ↑(sSupFun hc) x < ↑(sSupFun hc) y

Tactic:
apply lt_of_sub_pos

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
⊢ 0 < ↑(sSupFun hc) y - ↑(sSupFun hc) x
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ 1 < ↑(Fintype.card Fq)

Tactic:
exact mod_cast @Fintype.one_lt_card Fq _ _

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
x✝ : IsMonicOfDegree 1 n
H : natDegree 1 = n
monic✝ : Monic 1
⊢ n = 0

Tactic:
rwa [natDegree_one, eq_comm] at H

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
⊢ q.IsMonicOfDegree n

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
    exact hpq.2

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0

Tactic:
have : p.coeff i = (p.homogenize n).coeff fun₀ | 0 => i | 1 => n - i := by
      simp [coeff_homogenize, Nat.add_sub_of_le (H.trans hn)]

Goal state after:
case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
this : p.coeff i = MvPolynomial.coeff (fun₀ | 0 => i | 1 => n - i) (p.homogenize n)
⊢ p.coeff i = 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup

Tactic:
rw [destutter_cons_cons, ← destutter_cons', ← destutter_cons', h.2.destutter_eq_dedup]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_3
inst✝ : Semiring R
r : R
⊢ leval r = smeval.linearMap R r

Tactic:
refine LinearMap.ext ?_
  intro
  rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬q ∣ p

Tactic:
rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - C (-q.coeff 0) ∣ p
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]
  · exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)
  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]
  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑q ! * ↑((q + k).descFactorial k) * (aeval r) p'

Tactic:
← Nat.cast_mul,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑(q ! * (q + k).descFactorial k) * (aeval r) p'
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩

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

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
have hk : k = k' := by
    rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
hk : k = k'
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ QuadraticAlgebra.C (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by
  ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : star z ∈ (QuadraticAlgebra R a b)⁰
⊢ star (star z) ∈ (QuadraticAlgebra R a b)⁰

Tactic:
exact star_mem_nonZeroDivisors h

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = x ◃ y

Tactic:
have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]

Goal state after:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
⊢ (x ◃ y) ◃ x = x ◃ y
Module: Mathlib.Algebra.Quandle

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

Tactic:
by
  rw [← left_cancel x]
  simp

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:
solve | injection h₁ | injection h₂ | injection h₃

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

Goal state before:
pp: case e_toNatCast
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
⊢ toNatCast✝¹ = toNatCast✝

Tactic:
solve | injection h₁ | injection h₂ | injection h₃

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:
solve | injection h₁ | injection h₂ | injection h₃

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h : ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑R, g * T = T * g
a b : α
⊢ (↑T).toFun (a * b) = (↑T).toFun a * b

Tactic:
· exact congr($(h (R b) (.inr ⟨b, rfl⟩)) a).symm

Goal state after: