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

Goal state before:
pp: case pos
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
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : (↑f).toFun z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨↑z, ⋯⟩ = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))

Tactic:
LinearPMap.toFun_eq_coe

Goal state after:
case pos
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
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨↑z, ⋯⟩ = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) (p * q) =
    p • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) q +
      q • (PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm) p

Tactic:
dsimp

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p * q)) =
    p • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm p)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

Tactic:
ext n m

Goal state after:
case h₁.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

case h₁.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₂
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

Tactic:
ext n m

Goal state after:
case h₂.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

case h₂.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m
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
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : ∃ y, f.toFun y = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
⊢ ∃ y, (sSupFun hc).toFun y = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))

Tactic:
LinearPMap.toFun_eq_coe

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
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c✝
hf' : ↑f' = f
h : ∃ y, ↑f y = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
⊢ ∃ y, ↑(sSupFun hc) y = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))
Module: Mathlib.Data.List.Destutter

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

Tactic:
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.Homogenize

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)) = p.sum fun x c ↦ f c

Tactic:
sum_def p

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ∑ m ∈ (p.homogenize p.natDegree).support, f (MvPolynomial.coeff m (p.homogenize p.natDegree)) =
    ∑ n ∈ p.support, f (p.coeff n)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 1 x = 1 • x ^ 0

Tactic:
rw [← C_1, smeval_C]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ 1 • x ^ 0 = 1 • x ^ 0
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
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff n = w

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m).coeff n + (C w * X ^ n).coeff n = w
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
⊢ (C u * X ^ k + C v * X ^ m).coeff n + (C w * X ^ n).coeff n = w

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k).coeff n + (C v * X ^ m).coeff n + (C w * X ^ n).coeff n = w
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
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff m = v

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m).coeff m + (C w * X ^ n).coeff m = v
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
⊢ (C u * X ^ k + C v * X ^ m).coeff m + (C w * X ^ n).coeff m = v

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k).coeff m + (C v * X ^ m).coeff m + (C w * X ^ n).coeff m = v
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
⊢ (C u * X ^ k + C v * X ^ m + C w * X ^ n).coeff k = u

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (C u * X ^ k + C v * X ^ m).coeff k + (C w * X ^ n).coeff k = 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
⊢ (C u * X ^ k + C v * X ^ m).coeff k + (C w * X ^ n).coeff k = u

Tactic:
coeff_add,

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ∑ i_1 ∈ s, r i_1 * b i_1 %ₘ g i * ∏ x ∈ s, g x +
      (∑ i_1 ∈ s, (r i_1 * b i_1 /ₘ g i + r i_1 * a i_1 /ₘ g i_1) * (g i * ∏ x ∈ s, g x) +
        ∑ x ∈ s,
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)

Tactic:
← Finset.sum_add_distrib,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ∑ i_1 ∈ s, r i_1 * b i_1 %ₘ g i * ∏ x ∈ s, g x +
      ∑ x ∈ s,
        ((r x * b x /ₘ g i + r x * a x /ₘ g x) * (g i * ∏ x ∈ s, g x) +
          Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) x *
            ∏ k ∈ (Finset.cons i s hi).erase x, g k)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
hy : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff m)
hz : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff n)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
coeff_add,

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k).coeff k + (C y * X ^ m).coeff k + (C z * X ^ n).coeff k)
hy : IsUnit ((C x * X ^ k).coeff m + (C y * X ^ m).coeff m + (C z * X ^ n).coeff m)
hz : IsUnit ((C x * X ^ k).coeff n + (C y * X ^ m).coeff n + (C z * X ^ n).coeff n)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
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 : eval 1 (trinomial k m n ↑u ↑v ↑w) ^ 2 = eval 1 (trinomial k m' n ↑x ↑v ↑z) ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
simp only [eval_add, eval_C_mul, eval_X_pow, one_pow, mul_one, trinomial_def] at hadd

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 : (↑u + ↑v + ↑w) ^ 2 = (↑x + ↑v + ↑z) ^ 2
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
generalize hs_nC : SignType.sign P.nextCoeff = s_nC

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Quandle

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

Tactic:
← right_inv x y,

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toDistrib R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonAssocRing R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) 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 α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (z₁.prop.left_assoc z₂ a).symm

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 α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
x✝¹ x✝ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
x✝¹ x✝ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ ((f * g) a✝ - (g * f) a✝) * r * ((f * g) a✝ - (g * f) a✝) = 0

Tactic:
rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A G
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
by simp [← equivMapDomain_trans]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A H
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

Tactic:
by simp [← equivMapDomain_trans]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝ } ^ 0 = 1

Tactic:
simp only [pow_quot, ← one_quot, pow_zero]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Semiring T
r : R → R → Prop
F : RingQuot r →+* T
⊢ (fun f ↦ preLift ⋯) ((fun F ↦ ⟨F.comp (mkRingHom r), ⋯⟩) F) = F

Tactic:
by
      simp only [preLift_def]
      ext
      simp only [mkRingHom_def, RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        Function.comp_apply]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂

Tactic:
apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg coeff _

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ ∀ (a : G →₀ k), { coeff := _s₁ • a } = { coeff := _s₂ • a }
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
⊢ (x * single g r).coeff g' = 0

Tactic:
simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ rfl)

Goal state after:
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).map u ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso (⋯.pullbackIso.app ((Sheaf.forget A Y).obj Y✝)) ≪≫
          (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology ↑X) A).preimageIso
            (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).symm).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso (⋯.pullbackIso.app ((Sheaf.forget A Y).obj X✝)) ≪≫
          (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology ↑X) A).preimageIso
            (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).symm).hom ≫
      (sheafPullback A hf).map u

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map ((Presheaf.pullback A f).map ((Sheaf.forget A Y).map u)) ≫
      (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj Y✝)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        ObjectProperty.homMk (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).inv) ≫
      (sheafPullback A hf).map u