mathlib-initiative/mathlib-tactics huggingface dataset:
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 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial ((X - C η) * P).natDegree) P.leadingCoeff -
      (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    ((X - C η) * P.eraseLead).eraseLead

Tactic:
← self_sub_monomial_natDegree_leadingCoeff,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial ((X - C η) * P).natDegree) P.leadingCoeff -
      (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial ((X - C η) * P.eraseLead).natDegree) ((X - C η) * P.eraseLead).leadingCoeff
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 : (↑v + (↑w + ↑u)) ^ 2 = (↑v + (↑z + ↑x)) ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
simp only [add_sq', add_assoc, add_right_inj, ← Units.val_pow_eq_pow_val, Int.units_sq] 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 : 2 * ↑w * ↑u + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : ¬decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

pp: case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
· rfl

Goal state after:
case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue.isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : ¬1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

pp: case isTrue.isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (1 ::
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
· rfl

Goal state after:
case isTrue.isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (1 ::
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
x : ι
hx : x ∈ s
⊢ (gi x * (algebraMap R[X] K) (g x)) ^ n x = 1

Tactic:
hgi x hx,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
x : ι
hx : x ∈ s
⊢ 1 ^ n x = 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (algebraMap R[X] K) (r i (Fin.revPerm j) * g i ^ ↑(Fin.revPerm j) * ∏ k ∈ s.erase i, g k ^ n k) *
      ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
Fin.revPerm_apply,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (algebraMap R[X] K) (r i j.rev * g i ^ ↑j.rev * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
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
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (algebraMap R[X] K) (r i (Fin.revPerm j)) * gi i ^ (↑(Fin.revPerm j) + 1) * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (r i j.rev) * (algebraMap R[X] K) (g i) ^ ↑j * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x) ^ n x

Tactic:
Fin.revPerm_apply,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
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
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ (algebraMap R[X] K) (r i j.rev) * gi i ^ (↑j.rev + 1) * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (r i j.rev) * (algebraMap R[X] K) (g i) ^ ↑j * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x) ^ n x
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case negSucc
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = IntCast.intCast (Int.negSucc n)

Tactic:
rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr

Goal state after:
Module: Mathlib.Algebra.Ring.Semireal.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : ↑n = 0
⊢ n = 0

Tactic:
cases n with
    | zero => rfl
    | succ n =>
      rw [add_comm] at hn
      push_cast at hn
      simpa using IsSemireal.one_add_ne_zero (by simp) hn

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
⊢ 0 * (b + c) = 0 * b + 0 * c

pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
a✝ : α
⊢ ↑a✝ * (b + c) = ↑a✝ * b + ↑a✝ * c

Tactic:
· rfl

Goal state after:
case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
a✝ : α
⊢ ↑a✝ * (b + c) = ↑a✝ * b + ↑a✝ * c
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

Tactic:
by
  simp only [Function.comp_apply]
  rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ SkewMonoidAlgebra k G →ₐ[k] A

Tactic:
apply liftNCAlgHom (Algebra.ofId k A) F

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ ∀ {x : k} {y : G}, (Algebra.ofId k A) (y • x) * F y = F y * (Algebra.ofId k A) x
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.symm
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
a_ih✝ : RingConGen.Rel r x✝ y✝
⊢ RingConGen.Rel r y✝ x✝

Tactic:
| symm =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.symm
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : RingConGen.Rel r x✝ y✝
a_ih✝ : Relation.EqvGen (Rel r) x✝ y✝
⊢ Relation.EqvGen (Rel r) y✝ x✝

Tactic:
| symm =>

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
⊢ ∀ (n : ℕ) (x : RingQuot r), (n + 1) • x = n • x + x

Tactic:
rintro n ⟨⟨⟩⟩

Goal state after:
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
n : ℕ
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ (n + 1) • { toQuot := Quot.mk (Rel r) a✝ } = n • { toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) a✝ }
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
⊢ ∀ (n : ℕ) (x : RingQuot r), x ^ (n + 1) = x ^ n * x

Tactic:
rintro n ⟨⟨⟩⟩

Goal state after:
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
n : ℕ
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝ } ^ (n + 1) = { toQuot := Quot.mk (Rel r) a✝ } ^ n * { toQuot := Quot.mk (Rel r) a✝ }
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
⊢ ∀ (n : ℕ), ↑(n + 1) = ↑n + 1

Tactic:
simp +instances [instNatCast, natCast, ← one_quot, add_quot]

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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (n : ℕ) (a : RingQuot r), ↑n.succ • a = ↑n • a + a

Tactic:
rintro n ⟨⟨⟩⟩

Goal state after:
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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
n : ℕ
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ↑n.succ • { toQuot := Quot.mk (Rel r) a✝ } = ↑n • { toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) a✝ }
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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (n : ℕ) (a : RingQuot r), Int.negSucc n • a = -(↑n.succ • a)

Tactic:
rintro n ⟨⟨⟩⟩

Goal state after:
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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
n : ℕ
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ Int.negSucc n • { toQuot := Quot.mk (Rel r) a✝ } = -(↑n.succ • { toQuot := Quot.mk (Rel r) a✝ })
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case of
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b x✝ y✝ : R
h : r x✝ y✝
⊢ Rel r (Star.star x✝) (Star.star y✝)

Tactic:
| of h          =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun a b ↦ (g a b).sum h

Tactic:
rw [sum_def, coeff_sum' f g, Finsupp.sum_sum_index h_zero h_add]; simp [sum_def]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
x✝¹ : x ∈ b.coeff.support
y : G
x✝ : y ∈ a.coeff.support
⊢ single (y * x) (a.coeff y * b.coeff x) = single (x * y) (b.coeff x * a.coeff y)

Tactic:
by rw [mul_comm, mul_comm (a.coeff y) _]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
⊢ x + y ≤ x + z

pp: case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z

Tactic:
· rw [add_eq_left hx, add_eq_left (hx.trans h)]

Goal state after:
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map β.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
subst h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)
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 (X.restrict ⋯).presheaf

Tactic:
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
          tauto

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

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑(X.restrict ⋯)
⊢ (ConcreteCategory.hom (X.ofRestrict ⋯ ≫ X.toRestrictTop).base) x✝ = (ConcreteCategory.hom (𝟙 (X.restrict ⋯)).base) x✝

pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
· rfl

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f

Tactic:
exact inf_le_right

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
erw [comp_c, toRestrictTop_c, whiskerRight_id',
        comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (𝟙 (X.restrict ⋯).presheaf).app (op U✝) = (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : X.basicOpen f = unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) ≤
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
exact inf_le_right

Goal state after: