mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : b ∈ S⁰
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ b * s * a = b * (s * a)

Tactic:
mul_assoc

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : b ∈ S⁰
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ b * (s * a) = b * (s * a)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) ((f x✝².fst j hx) x✝².snd) = (f k i hki) ((f z✝.fst k hz) z✝.snd)

Tactic:
jeq,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
x✝² y✝ z✝ : (i : ι) × F i
x✝¹ : ∃ i, ∃ (hx : x✝².fst ≤ i) (hy : y✝.fst ≤ i), (f x✝².fst i hx) x✝².snd = (f y✝.fst i hy) y✝.snd
x✝ : ∃ i, ∃ (hx : y✝.fst ≤ i) (hy : z✝.fst ≤ i), (f y✝.fst i hx) y✝.snd = (f z✝.fst i hy) z✝.snd
j : ι
hx : x✝².fst ≤ j
w✝¹ : y✝.fst ≤ j
jeq : (f x✝².fst j hx) x✝².snd = (f y✝.fst j w✝¹) y✝.snd
k : ι
w✝ : y✝.fst ≤ k
hz : z✝.fst ≤ k
keq : (f y✝.fst k w✝) y✝.snd = (f z✝.fst k hz) z✝.snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ (f j i hji) ((f y✝.fst j w✝¹) y✝.snd) = (f k i hki) ((f z✝.fst k hz) z✝.snd)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝⁵.fst j hx) x✝⁵.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ x✝².fst i ⋯) x✝².snd)

Tactic:
jeq,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝³.fst j hyj) x✝³.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ x✝².fst i ⋯) x✝².snd)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_2
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
lim : IsSuccPrelimit i
ih : ∀ b < i, ∀ (h : b ∈ s), e₁ ⟨b, h⟩ = e₂ ⟨b, h⟩
hi : i ∈ s
⊢ e₁ ⟨i, hi⟩ = e₂ ⟨i, hi⟩

Tactic:
ext x j
    have ⟨k, hjk, hki⟩ := lim.mid j.2
    have hk : k ∈ s := hs hki.le hi
    rw [piLTProj_intro (f := e₁ _ x) hki.le hjk, piLTProj_intro (f := e₂ _ x) hki.le hjk,
      ← nat₁ _ hk, ← nat₂ _ hk, ih _ hki]

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

Goal state before:
pp: case empty
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ ∅ ⊆ ↑(mapIncl M' N').range

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : 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✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝² * x✝¹ * x✝⟩⟧ = ⟦⟨i, x✝² * (x✝¹ * x✝)⟩⟧

Tactic:
mul_assoc

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case empty
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
hs : (↑∅).PairwiseDisjoint t
⊢ (⋃ i ∈ ∅, t i).mulIndicator f = fun a ↦ ∏ i ∈ ∅, (t i).mulIndicator f a

Tactic:
| empty =>

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
⊢ motive ((↑h.equiv).toFun y)

Tactic:
change motive (TensorProduct.lift f y)

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
⊢ motive ((TensorProduct.lift f) y)
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
wlog hj : j < k + 1 generalizing j
  · convert! this (j : Fin (k + 1)) (by grind) using 3 <;> grind [cast_val_eq_self]
  by_cases hj₁ : j = 0
  · simp only [hj₁]
    by_cases hk : 0 = k
    · simp only [natCast_zero, intervalGapsWithin_zero_fst]
      simp [show 0 = last k by grind, hab]
    · exact hFab (F.intervalGapsWithin_mapsTo h a b (x := 0) (by grind)) |>.left
  have hk : k - 1 + 1 = k := by omega
  by_cases hj₂ : j = k
  · simp only [hj₂, natCast_eq_last, intervalGapsWithin_last_snd, ge_iff_le]
    convert! hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind)) |>.right.right using 1
    simp [hj₂, hk]
  rw [intervalGapsWithin_fst_of_lt_lt (hj₁ := by omega) (hj₂ := by omega),
      intervalGapsWithin_snd_of_lt (hj := by omega)]
  have hj₃ : (⟨j - 1, by omega⟩ : Fin k) ≠ ⟨j, by omega⟩ := by grind
  set G := F.orderEmbOfFin (α := α ×ₗ α) h
  have := hF (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
    (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]) (G.injective.ne (hj₃))
  contrapose! this
  simp only [Set.not_disjoint_iff, Set.mem_Icc]
  use (G ⟨j, by omega⟩).1
  have hG : (G ⟨j - 1, by omega⟩).1 ≤ (G ⟨j, by omega⟩).1 :=
    Prod.Lex.le_iff'.mp (G.monotone (by simp [le_iff_val_le_val])) |>.left
  have hFabi := hFab (z := G ⟨j, by omega⟩) (by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)])
  simp [hFabi, this.le, hG]

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
⊢ ∑ 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

Tactic:
← sum_Ico_sub_bot _ hmn,

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
⊢ ∑ i ∈ Ico m n, f i • ∑ i ∈ range (i + 1), g i - f m • ∑ i ∈ range (m + 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
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
Nat.even_iff,

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s with ¬Even (f x), f x) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
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 + 1), g i +
        ∑ x ∈ Ico m (n - 1), (f x • ∑ i ∈ range (x + 1), g i - f (x + 1) • ∑ i ∈ range (x + 1), g i)) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
simp_rw [this, sum_neg_distrib, sum_range_succ, 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.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ IsBaseChange S f

Tactic:
apply IsTensorProduct.of_equiv (e.restrictScalars R)
  intro x y
  simp [show x ⊗ₜ[R] y = x • (1 ⊗ₜ[R] y) by simp [smul_tmul'], he]

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

Goal state before:
pp: case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧

Tactic:
suffices xs <+~ ys from this.sym2

Goal state after:
case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
      ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩) =
    ⟨i, ⟨m, hm⟩⟩

Tactic:
refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Fin (n + 1) → Type ?u.73

case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → ?refine_1 (id a)

case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g

Tactic:
by
  convert! w (𝟙 Y) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f : α → β
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ ∀ (a_1 b c d : α) (h : Rel α (a_1, b) (c, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = a_1 then b else a_1) ⋯ = fun x ↦ if a = c then d else c

Tactic:
clear h z
    intro b c d e h
    ext hy
    have {f g h} : @Eq.ndrec (Sym2 α) s(b, c)
      (fun x => a ∈ x → α) (fun _ => if a = b then c else b) f g h =
        if a = b then c else b := by subst g; rfl
    aesop

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)

Tactic:
IsIso.inv_comp_eq,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ F.map f = α.app X ≫ G.map f ≫ inv (α.app Y)
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case inl
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match (Sum.inl val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

pp: case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
· simp only
    rfl

Goal state after:
case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
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 }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
· intro ⟨X⟩ ⟨Y⟩ ⟨⟨p⟩⟩; simp only at p; induction p; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type u_3
ι : α → Type u_4
A B : (a : α) → ι a → C
f : (a : α) → (i : ι a) → A a i ⟶ B a i
⊢ ⨆ a, ofHoms (f a) = ofHoms fun j ↦ f j.fst j.snd

Tactic:
ext f
  simp [ofHoms_iff]

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

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Mono (↾f) → Function.Injective f

Tactic:
intro H x x' h

Goal state after:
case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : f x = f x'
⊢ x = x'
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
L : LocallySmall.{w, v, u} C
S : Type w
e : Skeleton C ≃ S
e' : Skeleton (ShrinkHoms.{u} C) ≃ Skeleton C := (ShrinkHoms.equivalence C).skeletonEquiv.symm
⊢ EssentiallySmall.{w, v, u} C

Tactic:
exact ⟨⟨InducedCategory _ (e'.trans e).symm, inferInstance,
      ⟨(ShrinkHoms.equivalence C).trans
      ((skeletonEquivalence (ShrinkHoms C)).symm.trans
      (inducedFunctor _).asEquivalence.symm)⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ (adj.homEquiv A X) u ≫ F.map p = i ≫ (adj.homEquiv B Y) v

Tactic:
by
    simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
    rw [F.map_comp, Adjunction.unit_naturality_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f

Tactic:
by
  constructor
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
⊢ m = Pi.lift fun j ↦ s.π.app { as := j }

Tactic:
dsimp
    ext
    simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
    apply hm

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

Goal state before:
pp: case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
rw [← cancel_epi f]
      simpa using e₁

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryCofan X Y
⊢ inl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)).pt).hom =
    (map F s).inl

Tactic:
by simp [inl]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (prod.map f g) ≫ prodComparison F A' B' = prod.map (F.map f) (F.map g)

Tactic:
IsIso.inv_comp_eq,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)