mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l ^ 2 - (s - l) ^ 2‖ = ‖s * (2 * l - s)‖

Tactic:
rw [sq_sub_sq]; simp [← sub_add, two_mul, sub_add_eq_add_sub]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn

Goal state after:
case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ IntervalIntegrable (deriv f) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
refine ⟨exp c, exp_pos _, fun n => ?_⟩

Goal state after:
c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ rexp c ≤ stirlingSeq (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x
          else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)).coeff
      i =
    ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else (↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0

Tactic:
cases i with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
⊢ (L.weierstrassPExceptSeries l₀ x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i l

Tactic:
delta weierstrassPExceptSummand weierstrassPExceptSeries
  cases i with
  | zero => simp [weierstrassPExcept, sub_sq_comm x, zpow_ofNat]
  | succ i =>
    split_ifs with hl₀
    · trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
      · rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
        simp [add_assoc, one_add_one_eq_two]
      · rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))
    · have h₁ (l : L.lattice) : l.1 ≠ l₀ := fun e ↦ hl₀ (e ▸ l.2)
      simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]

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

Goal state before:
pp: n m : ℤ
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
suffices ∫ x, (2 * T ℝ n * T ℝ m).eval x ∂measureT =
      (∫ x, (T ℝ (n + m)).eval x ∂measureT) +
      (∫ x, (T ℝ (n - m)).eval x ∂measureT) by
    simp_rw [eval_mul, eval_ofNat, mul_assoc] at this
    rw [MeasureTheory.integral_const_mul] at this
    grind

Goal state after:
n m : ℤ
⊢ ∫ (x : ℝ), eval x (2 * T ℝ n * T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ sumZeroes n (c • P) = c * sumZeroes n P

Tactic:
by
  simp_rw [sumZeroes, eval_smul, ← smul_sum, smul_eq_mul]; ring

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

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i

Tactic:
obtain ⟨i, hi, hix⟩ := Finset.mem_image.mp hx

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hi : i ∈ Finset.range (n + 1)
hix : node n i = x
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ ∃ n_1, ↑n_1 * π = (↑↑n + 1) * ((↑k + 1) * π / (↑n + 1))

Tactic:
use k + 1

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ ↑(↑k + 1) * π = (↑↑n + 1) * ((↑k + 1) * π / (↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : 2 ≤ ↑k
⊢ (fun n ↦ (↑n * z + ↑d)⁻¹ ^ k) =O[cofinite] fun n ↦ |(↑n)⁻¹| ^ k

Tactic:
apply (linear_inv_isBigO_left d hz).abs_right.pow

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ + ψ = 1

Tactic:
rw [goldenRatio, goldenConj]

Goal state after:
⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ fibRec.IsSolution fun x ↦ φ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
  simp

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ fibRec.IsSolution fun x ↦ ψ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
  simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x)) = ↑k ! / c ^ (k + 1)

Tactic:
key,

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ (1 / c) ^ (↑k + 1) * Gamma (↑k + 1) = ↑k ! / c ^ (k + 1)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ ↑k ! / c ^ (k + 1)

Tactic:
have hk : (0 : ℝ) < ↑k + 1 := by positivity
  have key := integral_rpow_mul_exp_neg_mul_Ioi hk hc
  have hint : IntegrableOn (fun x ↦ x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x))) (Ioi 0) :=
    .of_integral_ne_zero (by rw [key]; positivity)
  rw [intervalIntegral.integral_of_le hM]
  calc ∫ x in Ioc (0 : ℝ) M, x ^ k * rexp (-(c * x))
    _ = ∫ x in Ioc (0 : ℝ) M, x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        simp [add_sub_cancel_right, rpow_natCast]
    _ ≤ ∫ x in Ioi (0 : ℝ), x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE
        filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
        exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)
    _ = k ! / c ^ (k + 1) := by
        simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
        norm_cast

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in ↑0..↑M, x ^ k * rexp (-(c * (x - 1))) ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
simp only [mul_sub, mul_one, neg_sub, CharP.cast_eq_zero]

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..↑M, x ^ k * rexp (c - c * x) ≤ ↑k ! / c ^ (k + 1) * rexp c
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
| 2 ^ (-(c * ↑i))

Tactic:
← exp_log zero_lt_two,

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
| rexp (log 2) ^ (-(c * ↑i))
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 = (↑S).centralizer

Tactic:
simp [commutant]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ (preadditiveCoyonedaObj P).PreservesEpimorphisms

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
  refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩
  · exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyonedaObj P)
        (forget _)
  · intro
    exact (inferInstance : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
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 : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + (↑i + 1), f (x₀ + ↑i)

Tactic:
refine integral_mono_on (by simp) this (by simp) fun _ _ ↦ by apply hf <;> grind

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
⊢ IsColimit (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
apply ShortComplex.isColimitOfIsColimitπ

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₁.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₂.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

case h₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit
    (ShortComplex.π₃.mapCocone
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
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 : ∀ ⦃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) * ↑(c n) ≤ ε * ↑(c n)

Tactic:
by
          gcongr
          refine le_trans (neg_le_abs _) ?_
          simpa using hn

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
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
f : φ.obj cm.X₂ ⟶ φ.obj Y
⊢ φ.map ((ConcreteCategory.hom f) (𝟙 G)) = f

Tactic:
cat_disch

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))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right) = L.map va₂ ≫ j₁.hom
ib : A
vb₁ : ib ⟶ Q.left
vb₂ : ib ⟶ j₂.left
heqb : L.map vb₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right) = L.map vb₂ ≫ j₂.hom
i₀ : A
il₀ : i₀ ⟶ ia
ir₀ : i₀ ⟶ ib
heq : il₀ ≫ va₁ = ir₀ ≫ vb₁
⊢ L.map (ir₀ ≫ vb₂) ≫ j₂.hom =
    { left := i₀, right := IsCofiltered.min j₁.right j₂.right, hom := L.map (il₀ ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.minToRight j₁.right j₂.right)

Tactic:
cat_disch

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))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ L.map (β ≫ va₂) ≫ j₁.hom =
    { left := i₀, right := IsCofiltered.eq u.right v.right, hom := L.map (β ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.eqHom u.right v.right)

Tactic:
cat_disch

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))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ u =
    { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ v

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : I ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i))
      ((ConcreteCategory.hom (colimitYonedaHomIsoLimit' D F).hom) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
change ((colimitYonedaHomIsoLimit' D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _
  simp only [colimitYonedaHomIsoLimit', Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
  rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]
  dsimp [yonedaLemma]
  rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Full

Tactic:
by
  rw [functor]
  have : (F C).Full := by rw [F]; infer_instance
  have : (G C).Full := by rw [G]; infer_instance
  have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
  infer_instance

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
⊢ ((HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X).inv ≫
          (((HomologicalComplex.single C (ComplexShape.up ℕ) 0).obj X).extendXIso ComplexShape.embeddingUpNat
              ι'._proof_1).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.up ℕ) 0).obj X).extendXIso ComplexShape.embeddingUpNat ⋯).hom ≫
        R.ι.f 0 ≫ (HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat ⋯).inv =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
cat_disch

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
Z' : C
I' : InjectiveResolution Z'
f : Z ⟶ Z'
φ : I.Hom I' f
⊢ I.ι ≫ φ.hom = (single₀ C).map f ≫ I'.ι

Tactic:
cat_disch

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
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∀ (x y : ↥M), MulOpposite.unop ↑(x + y) = MulOpposite.unop ↑x + MulOpposite.unop ↑y

Tactic:
cat_disch

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
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : ↥M),
    { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id (End G)ᵐᵒᵖ) m • { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯ }.toFun x

Tactic:
cat_disch

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Function.Injective
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }))

Tactic:
cat_disch

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
⊢ ((HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯).hom ≫
        R.π.f 0 ≫
          (HomologicalComplex.extendXIso ((ChainComplex.single₀ C).obj X) ComplexShape.embeddingDownNat ⋯).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.down ℕ) 0).obj X).extendXIso ComplexShape.embeddingDownNat
            π'._proof_1).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X).hom ≫
          (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).inv

Tactic:
cat_disch

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

Goal state before:
pp: case e_g
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ inv (DerivedCategory.Q.map R.ι') = inv (DerivedCategory.Q.map R.ι') ≫ 𝟙 ((DerivedCategory.singleFunctor C 0).obj Y)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
⊢ ⟦Over.mk (a'' ≫ f)⟧ = ⟦Over.mk 0⟧

Tactic:
dsimp at comm
            simp [a'', sub_eq_zero.2 comm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ ((kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0) ≫ t =
    (𝟙 (kernel t) ≫ equalizer.ι t 0) ≫ t

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ ((kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0) ≫ l =
    (𝟙 (kernel t) ≫ equalizer.ι t 0) ≫ l

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯ ≫ kernel.map t b l r ⋯ = 𝟙 (kernel b)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ cokernel.map t b l r ⋯ ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ = 𝟙 (cokernel t)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ r ≫ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    r ≫ coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ b ≫ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    b ≫ coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
cat_disch

Goal state after: