mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf :
  g i * ∑ x ∈ s, (r₁ x * ∏ x ∈ s.erase x, g x - r₂ x * ∏ x ∈ s.erase x, g x) =
    (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
simp only [← sub_mul] at hf

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 : 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
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range q, (aeval r) ((⇑derivative)^[x] p) + ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
this,

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range (q - 1 + 1), (aeval r) ((⇑derivative)^[x] p) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ (r i j).degree + ↑(↑j * (g i).natDegree) < (g i).degree + ↑((n i - 1) * (g i).natDegree)

Tactic:
refine WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
a✝ : Nontrivial R
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₁ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ x ∈ s, (∑ i, r₂ x i * g x ^ ↑i) * ∏ i ∈ s.erase x, g i ^ n i
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
i : ι
hi : i ∈ s
j : Fin (n i)
x✝ : j ∈ Finset.univ
⊢ ↑(↑j * (g i).natDegree) ≤ ↑((n i - 1) * (g i).natDegree)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
⊢ n✝ + 1 ≤ P.signVariations

Tactic:
have hp : P ≠ 0 := by grind [roots_zero, Multiset.countP_zero]

Goal state after:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
⊢ n✝ + 1 ≤ P.signVariations
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a✝ b✝ a'✝ b'✝ : PreEnvelGroup R
ha : PreEnvelGroupRel' R a✝ a'✝
hb : PreEnvelGroupRel' R b✝ b'✝
⊢ mapAux f (a✝.mul b✝) = mapAux f (a'✝.mul b'✝)

Tactic:
by
    simp [toEnvelGroup.mapAux, well_def f ha, well_def f hb]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (g i) ≠ 0

Tactic:
simpa using (hg i hi).ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (g i) ≠ 0

Tactic:
simpa using (hg i hi).ne_zero

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
neg_add

Goal state after:
R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
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✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid.toFun ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]

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
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (a + c) (b + d)

Tactic:
induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.rel
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
h : Rel r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝

Tactic:
induction h with
      | of => exact RingConGen.Rel.of _ _ ‹_›
      | add_left _ h => exact h.add (RingConGen.Rel.refl _)
      | mul_left _ h => exact h.mul (RingConGen.Rel.refl _)
      | mul_right _ h => exact (RingConGen.Rel.refl _).mul h

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 → R → Prop
⊢ ∀ (a b : RingQuot r), a + b = b + a

Tactic:
by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [add_quot, add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
this : 1 = (monomial 0) 1
⊢ coeff 1 n = if 0 = n then 1 else 0

Tactic:
this,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
this : 1 = (monomial 0) 1
⊢ ((monomial 0) 1).coeff n = if 0 = n then 1 else 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X ^ n = (monomial n) 1

Tactic:
exact X_pow_eq_monomial n

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ fst (r, m) = 0

Tactic:
hrm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ (inr (snd (r, m))).fst = 0
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop tl.sum = (map trop tl).prod
⊢ trop (hd :: tl).sum = (map trop (hd :: tl)).prod

Tactic:
| cons hd tl IH =>

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop tl.prod = (map untrop tl).sum
⊢ untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum

Tactic:
| cons hd tl IH =>

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum
⊢ trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a b ↦ (single a b * g).coeff x

Tactic:
← coeff_sum,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = (f.sum fun a b ↦ single a b * g).coeff x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = g.sum fun a b ↦ (f * single a b).coeff x

Tactic:
← coeff_sum,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = (g.sum fun a b ↦ f * single a b).coeff x
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
      (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)

Tactic:
rw [mul_add (unsym a)]

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (unsym a * (unsym b * unsym (a * a)) + unsym a * (unsym (a * a) * unsym b) +
      (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ (TensorProduct.map (star (toConv (single R B i))).ofConv (star (toConv (single R B i))).ofConv)
      (star (comul (star x))) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))

Tactic:
this,

Goal state after:
R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ (TensorProduct.map (star (toConv (single R B i))).ofConv (star (toConv (single R B i))).ofConv)
      ((TensorProduct.comm R (B i) (B i)) (comul x)) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U V : (Opens ↑↑s.pt)ᵒᵖ
i : U ⟶ V
j : Jᵒᵖ
w :
  (Opens.map (colimit.ι (F ⋙ forget C) (unop j))).map
      ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop) =
    eqToHom ⋯ ≫ (Opens.map (((forget C).mapCocone s).ι.app (unop j))).map i.unop ≫ eqToHom ⋯
⊢ (s.pt.presheaf.map i ≫
        limit.lift
            ((pushforwardDiagramToColimit F).leftOp ⋙
              (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V))))
            { pt := s.pt.presheaf.obj V,
              π :=
                { app := fun j ↦ (s.ι.app (unop j)).c.app V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                  naturality := ⋯ } } ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))).inv) ≫
      (limit.π (pushforwardDiagramToColimit F).leftOp j).app
        (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V))) =
    ((limit.lift
            ((pushforwardDiagramToColimit F).leftOp ⋙
              (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
                (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U))))
            { pt := s.pt.presheaf.obj U,
              π :=
                { app := fun j ↦ (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
                  naturality := ⋯ } } ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))).inv) ≫
        (limit (pushforwardDiagramToColimit F).leftOp).map
          ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop).op) ≫
      (limit.π (pushforwardDiagramToColimit F).leftOp j).app
        (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))

Tactic:
simp [congr_arg Quiver.Hom.op w]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf =
    (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj
      ((Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf)

Tactic:
← Presheaf.Pushforward.comp_eq

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = (Presheaf.pushforward C ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.ofRestrict ⋯).c = eqToHom ⋯

Tactic:
by
  /- another approach would be to prove the left-hand side
       is a natural isomorphism, but I encountered a universe
       issue when `apply NatIso.isIso_of_isIso_app`. -/
  ext
  dsimp [ofRestrict]
  erw [eqToHom_map, eqToHom_app]
  simp

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

Goal state before:
pp: case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
⊢ ∀ (y : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) y → y = ⟨gl, ⋯⟩

Tactic:
intro gl'

Goal state after:
case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
⊢ (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) gl' → gl' = ⟨gl, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α = β

Tactic:
by
  ext : 1
  · exact w
  · apply ((TopCat.Sheaf.pushforward _ β.hom.base).obj X.sheaf).hom_ext _
      PrimeSpectrum.isBasis_basic_opens
    intro r
    apply (StructureSheaf.to_basicOpen_epi R r).1
    simpa using! h r

Goal state after: