mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
⊢ False

Tactic:
rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ (Associates.mk c ⊓ Associates.mk b).out

Tactic:
rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]
        exact ⟨hac, hab⟩

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
div_def,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).leadingCoeff = p.leadingCoeff / q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
⊢ (normalize p).degree = p.degree

Tactic:
by
  simp [normalize_apply]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content)).content * 1 ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content)).content ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd p q).degree ≤ q.degree

Tactic:
gcd_comm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd q p).degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
⊢ False

Tactic:
by
  obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
  by_cases hx : x = 0
  · rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h
  exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
⊢ IsAlgebraic R 1

Tactic:
by
  rw [← map_one (algebraMap R A)]
  exact isAlgebraic_algebraMap 1

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ ((fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
        ⟨k, ⋯⟩)
      (f hk (e x).1) l =
    (piSplitLE
        (fun j ↦ equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨i⁺, hj⟩)
      x ⟨↑l, ⋯⟩

Tactic:
nat le_rfl

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ piLTProj hk ((equiv ⟨i, ⋯⟩) (e x).1) l =
    (piSplitLE
        (fun j ↦ equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨i⁺, hj⟩)
      x ⟨↑l, ⋯⟩
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
j k : ι
hj : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨j, hj⟩) x)

Tactic:
have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
  obtain rfl | hj := le_succ_iff_eq_or_le.mp hj
  · obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
    · simp [InverseSystem.map_self]
    · funext l
      rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]
      simp [piSplitLE_lt (l.2.trans_le hk)]
  · rw [piEquivSucc, piSplitLE_lt (h.trans_lt <| lt_succ hj), nat hj, piSplitLE_lt (lt_succ hj)]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ (fun x ↦ (monomial x) 1) '' 0 ⊆ ↑1

Tactic:
Set.image_subset_iff

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ 0 ⊆ (fun x ↦ (monomial x) 1) ⁻¹' ↑1
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : Finite σ
N : ℕ
this : {f | ∀ (a : σ), f a ≤ N}.Finite
⊢ {s | (s.sum fun x e ↦ e) ≤ N}.Finite

Tactic:
exact this.subset fun n hn i ↦ (eq_or_ne (n i) 0).elim
      (fun h ↦ h.trans_le N.zero_le) fun h ↦
        (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ Submodule.comap (rTensor N' g) (lTensor P g').ker = (lTensor N f').range ⊔ (rTensor N' f).range

Tactic:
← Exact.linearMap_ker_eq (rTensor_exact N' hfg hg)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ Submodule.comap (rTensor N' g) (lTensor P g').ker = (lTensor N f').range ⊔ (rTensor N' g).ker
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
div_def,

Goal state after:
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x / y⟩⟧ =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, a ≤ (F.intervalGapsWithin h a b ↑j).1
hj : ¬j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
· grind [cast_val_eq_self]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ↑q = ↑q

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
  rw [ratCast_def, lift_def, map_ratCast (g i)]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).2 ≤ b
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
· grind [cast_val_eq_self]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + (a * (n / a) + a * 1) = n + a

Tactic:
mul_one,

Goal state after:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + (a * (n / a) + a) = n + a
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ (Multiset.map f s).sum ≡ 0 [MOD n]

Tactic:
by
  simpa using multisetSum_map h

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

Goal state before:
pp: n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 0 [MOD n]
⊢ s.sum ≡ 0 [MOD n]

Tactic:
by
  simpa using multisetSum_map h

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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ (Multiset.map f s).sum ≡ 0 [ZMOD n]

Tactic:
by
  simpa using multisetSum_map h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • (∑ i ∈ range m, g i + g m) +
        -∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • (∑ i ∈ range x, g i + g x)) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • (∑ i ∈ range x, g i + g x)

Tactic:
smul_add

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - (f m • ∑ i ∈ range m, g i + f m • g m) +
        -∑ x ∈ Ico m (n - 1), ((f (x + 1) - f x) • ∑ i ∈ range x, g i + (f (x + 1) - f x) • g x)) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ x ∈ Ico m (n - 1), ((f (x + 1) - f x) • ∑ i ∈ range x, g i + (f (x + 1) - f x) • g x)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
m : Sym α n
h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s
⊢ ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)

Tactic:
exact
      ⟨a, h _ <| Sym.mem_cons_self _ _,
        mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
cases n
  · exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
  · refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
    rintro ⟨_, rfl⟩
    exact sym_empty _

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ ys : List α
h✝ : xs✝ <+ ys
xs : List α
n : ℕ
l₂✝ : List α
a : α
h : xs <+ l₂✝
⊢ List.sym (n + 1) xs <+ List.sym (n + 1) l₂✝

Tactic:
exact h.sym (n + 1)

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case hr
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝

Tactic:
exact h.sym (n + 1)

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁ r₂ : α → α → Prop
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x

Tactic:
simp [eq_swap]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F.toPrefunctor = G.toPrefunctor
⊢ F = G

Tactic:
by
  obtain ⟨obj, map, _, _⟩ := F
  obtain ⟨obj', map', _, _⟩ := G
  obtain rfl : obj = obj' := congr_arg Prefunctor.obj h
  obtain rfl : @map = @map' := by simpa [Functor.toPrefunctor] using h
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
q : Path b c
⊢ (p.comp q).reverse = q.reverse.comp p.reverse

Tactic:
by
  induction q with
  | nil => simp
  | cons _ _ h => simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
by
  rw [Functor.hext hobj fun _ _ => hmap]

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f ≫ τ.app Y) = H.map (τ.app X ≫ Y✝.map f)

Tactic:
← τ.naturality

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f ≫ τ.app Y) = H.map (X✝.map f ≫ τ.app Y)
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext X
    exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ ∀ (f : { as := X } ⟶ { as := Y }), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
⟨⟨p⟩⟩

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : { as := X }.as = { as := Y }.as
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ ⊤.map F f

Tactic:
refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ Arrow.mk (F.map (F.preimage ?refine_1)) ≅ Arrow.mk f
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
by
  rw [iff, iff]
  exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ (P.map (F ⋙ G)).inverseImage G f

Tactic:
exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using coyonedaEquiv_comp _ _

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X : C
⊢ F.obj X = G.obj X

Tactic:
exact congr_arg Comma.left (congr_fun h (Arrow.mk (𝟙 X)))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F✝ : J ⥤ C
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
⊢ (adj.homEquiv s.pt F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j

Tactic:
have eq := NatTrans.congr_app (adj.counit.naturality s.π) j

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F✝ : J ⥤ C
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq :
  ((L ⋙ const J).map s.π ≫ adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt) ≫ (𝟭 (J ⥤ C)).map s.π).app j
⊢ (adj.homEquiv s.pt F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case term.id
J : Type w
j✝ : J
⊢ Hom (some j✝) none

Tactic:
apply Hom.term _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

pp: case none.some.init.init
J : Type w
b : J
⊢ Hom.init b = Hom.init b

pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
repeat rfl

Goal state after: