mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
this : eval (cos (0 * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)
⊢ Even 0 ∧ cos (0 * π / ↑n) = cos (↑0 * π / ↑n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ Nat.Coprime 2 (2 * k + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
this : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ 2 * k + 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
rcases n.even_or_odd with (hn | hn)
  · simp [fib, hn, pow_add]
  · simp [fib_of_odd, hn]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: x✝ : ℤ
⊢ fib (↑0 + x✝) = fib (↑0 - 1) * fib x✝ + fib ↑0 * fib (x✝ + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: x✝ : ℤ
⊢ fib (x✝ + ↑0) = fib (x✝ - 1) * fib ↑0 + fib x✝ * fib (↑0 + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: x✝ : ℕ
⊢ fib (-↑x✝ + -↑0) = fib (-↑x✝ - 1) * fib (-↑0) + fib (-↑x✝) * fib (-↑0 + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
rw [← mul_add_one, fib_two_mul]
  grind [fib_add_two]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ 0 ≤ fib ↑m

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ 0 ≤ ↑m

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case refine_2.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2 : k < n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
rcases (succ_le_of_lt h2).eq_or_lt with h2|h2

Goal state after:
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ k + 2 ≤ n.minFac

case refine_2.inr.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ < n.minFac
⊢ k + 2 ≤ n.minFac
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ 1 - 0 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
⊢ ((fun n ↦ u n / ↑n) '' Ici 1).Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑M

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) / ↑(c n) - l ≤ ε

Tactic:
refine (le_abs_self _).trans ?_

Goal state after:
case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ |u (c n) / ↑(c n) - l| ≤ ε
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
⊢ (image (fun i ↦ c i) (range (a + 1))).Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (StarSubalgebra.centralizer ℂ ↑S).carrier.centralizer.centralizer = (StarSubalgebra.centralizer ℂ ↑S).carrier

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ ↑i ≤ ↑(i + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i = ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), f ↑i

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ ↑i ≤ ↑(i + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
i : ℕ
hi : i ∈ Finset.Ico a b
⊢ IntervalIntegrable (fun u ↦ f ↑i) volume ↑i ↑(i + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑S.commutant.commutant = ↑S

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ x₀ + ↑i ≤ x₀ + (↑i + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ IntervalIntegrable (fun x ↦ f (x₀ + ↑i)) volume (x₀ + ↑i) (x₀ + (↑i + 1))

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i) = ∑ i ∈ Finset.range a, f (x₀ + ↑i)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1)) = ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1))

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ IntervalIntegrable (fun x ↦ f (x₀ + (↑i + 1))) volume (x₀ + ↑i) (x₀ + (↑i + 1))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 𝟙 X ≫ f ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫ biprod.snd = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).L₁.g = 𝟙 (snakeInput f g).L₀.X₃ ≫ (snakeInput f g).v₀₁.τ₃

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
⊢ (image (fun i ↦ c i) (range (a + 1))).Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ kernel.ι p ≫ p = 0

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ (ConcreteCategory.hom ((((evaluation K (Type w)).obj k).mapCocone t).ι.app j)) y =
    (ConcreteCategory.hom ((t.ι.app j).app k)) y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f ↦ f)
⊢ Sigma.ι (fun X ↦ ∐ fun x ↦ projectiveSeparator C) X ≫ Sigma.desc (Pi.single X (𝟙 (∐ fun x ↦ projectiveSeparator C))) =
    𝟙 (∐ fun x ↦ projectiveSeparator C)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)

Tactic:
exact Real.log_lt_log hj hi.2

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Tactic:
congr 1
      field

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'),
    (ConcreteCategory.hom
          ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))).map f))
        (Over.mkIdTerminal.from (Opposite.unop ((CostructuredArrow.toOver yoneda (colimit F)).op.obj (G.op.obj j)))) =
      Over.mkIdTerminal.from (Opposite.unop ((CostructuredArrow.toOver yoneda (colimit F)).op.obj (G.op.obj j')))

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
A' : Comma L R
s s' : (fst L R).obj A' ⟶ a
⊢ L.map (IsCofiltered.eqHom s s') ≫ A'.hom =
    { left := IsCofiltered.eq s s', right := A'.right, hom := L.map (IsCofiltered.eqHom s s') ≫ A'.hom }.hom ≫
      R.map (𝟙 A'.right)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ ComplexShape.embeddingUpNat.f 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ ↑0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
⊢ d g ≫ l₂ = d f

Tactic:
simp only [l₂, l₁]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
⊢ d g ≫ Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g)) = d f
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ ((CochainComplex.single₀ C).map f ≫ I.ι).f 0 = f ≫ I.ι.f 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ ComplexShape.embeddingDownNat.f 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Φ.ι ≫ Φ.π = 0 ≫ Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colonπ Ψ).app X = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 0 = I.cocomplex.d 0 1 ≫ descHomotopyZeroZero f comm

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 1 = descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 + I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 2) =
    ⟨g, ⟨g', w⟩⟩.snd.fst ≫ J.cocomplex.d (n + 1) (n + 2) +
      I.cocomplex.d (n + 2) (n + 3) ≫ descHomotopyZeroSucc f n g g' ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ ∀ (x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n),
    R.extEquivCohomologyClass.symm.toFun (x + y) =
      R.extEquivCohomologyClass.symm.toFun x + R.extEquivCohomologyClass.symm.toFun y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ f ≫ d f = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ f ≫ cokernel.π f = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z X₀✝ X₁✝ : C
f : X₀✝ ⟶ X₁✝
⊢ f ≫ d f = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 1 + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ (ofCocomplex Z).d 0 1 = 0

Tactic:
ofCocomplex_d_0_1,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ d (Injective.ι Z) = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n m : ℕ
hm : n + 1 = m
⊢ 0 ≫ R.cocomplex.d n m = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : C
f : Over P
⊢ 𝟙 f.left ≫ f.hom = 𝟙 f.left ≫ f.hom

Tactic:
by simp

Goal state after: