mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ log b r = 0

Tactic:
by
  rcases le_total 1 r with h | h
  · rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]
  · rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b ^ (log b r + 1)

Tactic:
rw [log_of_right_le_zero _ hr, zero_add, zpow_one]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ∫⁻ (x : X), ↑‖f‖₊ ∂μ

Tactic:
gcongr; apply nnnorm_coe_le_nnnorm

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

Goal state before:
pp: L : PeriodPair
x : ℂ
⊢ x ∈ L.lattice ↔ ∃ m n, ↑m * L.ω₁ + ↑n * L.ω₂ = x

Tactic:
simp only [lattice, Submodule.mem_span_pair, zsmul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ go n a (fuel + 1) guess ^ (n + 2) ≤ a

Tactic:
go

Goal state after:
case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, guess ≤ fuel → go n a fuel guess ^ (n + 2) ≤ a
guess : ℕ
hle : guess ≤ fuel + 1
⊢ (if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
        go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
      else guess) ^
      (n + 2) ≤
    a
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a < (go n a (fuel + 1) guess + 1) ^ (n + 2)

Tactic:
go

Goal state after:
case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a <
    ((if (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess then
          go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2))
        else guess) +
        1) ^
      (n + 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
by
      gcongr (4 * ?_ * ?_) / ‖l‖ ^ 4
      refine (norm_sub_le _ _).trans ?_
      simp only [Complex.norm_mul, Complex.norm_ofNat]
      linarith

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

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * -(I * I) = sinh ((↑n + 1) * θ)

Tactic:
I_mul_I,

Goal state after:
θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * - -1 = sinh ((↑n + 1) * θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1

Tactic:
by
  refine ⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
  rintro h rfl
  have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
    filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'
  have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)
  simpa using (uniqueDiffOn_Ici _ _ self_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)

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

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in Set.Ioc (-1) 1, NNReal.mk √(1 - x ^ 2)⁻¹ ⋯ • f x ∂volume =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume

Tactic:
congr! 2 with x hx

Goal state after:
f : ℝ → ℝ
x : ℝ
⊢ NNReal.mk √(1 - x ^ 2)⁻¹ ⋯ • f x = f x * √(1 - x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ (∫ (x : ℝ), eval x (T ℝ (↑n + ↑m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑m)) ∂measureT) / 2 = 0

Tactic:
integral_eval_T_real_measureT_of_ne_zero (by grind),

Goal state after:
n m : ℕ
h : n ≠ m
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑m)) ∂measureT) / 2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (∫ (x : ℝ), eval x (T ℝ (↑n + ↑n)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑n)) ∂measureT) / 2 = π / 2

Tactic:
integral_eval_T_real_measureT_of_ne_zero (by grind),

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑n)) ∂measureT) / 2 = π / 2
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ 2 * cos (↑r * π) = 2 * ↑hcos.choose

Tactic:
linarith [hcos.choose_spec]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)

Tactic:
integral_eval_T_real_measureT_of_ne_zero (by grind),

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ 0 = sumZeroes n (T ℝ ↑i)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ r1 z = 1 / ((z.re ^ 2 + z.im ^ 2) / z.im ^ 2)

Tactic:
one_div_div,

Goal state after:
z : ℍ
⊢ r1 z = z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h✝ : ¬(1 ≤ i ∧ i ≤ n - k)
⊢ (Finset.Icc 1 (n - k)).card = n - k

Tactic:
grind [Nat.card_Icc]

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
h✝ : 1 ≤ i ∧ i ≤ n - k
⊢ ((Finset.Icc 1 (n - k + 1)).erase i).card = n - k

Tactic:
grind [Nat.card_Icc]

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

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)

Tactic:
by
  simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
  exact L.weierstrassPExceptSeries_hasSum _ z x fun l hl ↦ hx l

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

Goal state before:
pp: case inr
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
this :
  ∀ (n : ℤ) (k : ℕ) {x : ℝ}, |x| ≤ 1 → 0 ≤ n → |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
hn : ¬0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))

pp: n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))

Tactic:
· convert! this (-n) k hx (by grind) using 1 <;> rw [T_neg]

Goal state after:
n : ℤ
k : ℕ
x : ℝ
hx : |x| ≤ 1
hn : 0 ≤ n
⊢ |eval x ((⇑derivative)^[k] (T ℝ n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ n))
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ 2 ∣ n.minFac

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
⊢ n.minFac % 2 = 0
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ⁻¹ = -ψ

Tactic:
by
  grind

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

Goal state before:
pp: ⊢ φ * ψ = -1

Tactic:
by
  grind

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

Goal state before:
pp: a : ℕ
h : a % 2 = 0
⊢ 2 ∣ a

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
a : ℕ
h : a % 2 = 0
⊢ a % 2 = 0
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n

Tactic:
by
  grind

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

Goal state before:
pp: ⊢ φ ^ 2 = φ + 1

Tactic:
by
  grind

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

Goal state before:
pp: ⊢ ψ ^ 2 = ψ + 1

Tactic:
by
  grind

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
ε : ℝ
ε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)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
⊢ u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n

Tactic:
have IcN : (c N : ℝ) ≤ (1 + ε) * c (N - 1) := by
      have A : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
      have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
      have := (ha _ A).1
      rwa [B] at this

Goal state after:
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)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inl ≫ 0

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0

Tactic:
· rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero,
      ← assoc, cokernel.condition]

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
⊢ biprod.inr ≫
      biprod.desc (f ≫ biprod.inl) (biprod.lift (-𝟙 Y) g) ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) =
    biprod.inr ≫ 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (F.whiskerLeft (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
simp only [← comp_evaluation, comp_obj, evaluation_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
    whiskerLeft_app, uliftFunctor_map, Functor.comp_map, evaluation_obj_map, yoneda_map_app]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (largeCurriedYonedaLemma.hom.app (op X)).app (F.obj j) ≫
      (↾fun x ↦ { down := (ConcreteCategory.hom (colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)) j)) x.down }) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    ↾fun g ↦ g ≫ colimit.ι F j
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
n : ℕ
⊢ IntegrableOn f (Ioc (↑N) (↑n + ↑N)) volume

Tactic:
← intervalIntegrable_iff_integrableOn_Ioc_of_le (by grind)

Goal state after:
case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
n : ℕ
⊢ IntervalIntegrable f volume (↑N) (↑n + ↑N)
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)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
let hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
    isColimitOfPreserves (Over.map _) (Over.isColimitToOver P.coconeIsColimit)

Goal state after:
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)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))
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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.rightOp ⋙ coyoneda) i).op ≫
          ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app (op i)))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }

Tactic:
simp only [coyonedaLemma, comp_apply]

Goal state after:
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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        (((D ⋙ Prod.sectL C F).isoWhiskerLeft
                (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯)).hom.app
          (op i)))
      ((ConcreteCategory.hom ((yoneda.obj F).map (colimit.ι (D.rightOp ⋙ coyoneda) i).op)) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Full
⊢ (F C ⋙ G C ⋙ H C).Full

Tactic:
have : (G C).Full := by rw [G]; infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝ : (F C).Full
this : (G C).Full
⊢ (F C ⋙ G C ⋙ H C).Full
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

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

Tactic:
by
  rw [functor]
  have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance
  have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp
  have : PreservesFiniteColimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding _
  infer_instance

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 : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x)).hom =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
change SmallShiftedHom.equiv _ _ ((CohomologyClass.mk x).toSmallShiftedHom.comp _ _) = _

Goal state after:
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
⊢ (SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q)
      ((CohomologyClass.mk x).toSmallShiftedHom.comp (SmallShiftedHom.mk₀Inv 0 ⋯ R.ι' ⋯) ⋯) =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯
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
⊢ pseudoApply f 0 = 0

Tactic:
by
  rw [pseudoZero_def, pseudoApply_mk']
  simp

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 := ⋯
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ p' ≫ a'.hom ≫ g = 0

Tactic:
simpa using comm'

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv

Tactic:
← cancel_mono (J.isoRightDerivedObj F n).hom,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ ((I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f) ≫ (J.isoRightDerivedObj F n).hom =
    ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
        (J.isoRightDerivedObj F n).inv) ≫
      (J.isoRightDerivedObj F n).hom
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (NatTrans.rightDerived α n).app X =
    (P.isoRightDerivedObj F n).hom ≫
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Tactic:
dsimp [NatTrans.rightDerived, isoRightDerivedObj]
  rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, Functor.map_comp, assoc]
  erw [← (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality_assoc
    ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)]
  simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

Tactic:
refine ⟨?_, fun hf ↦ ?_⟩
  · rintro ⟨X', s, hs, eq⟩
    have := P.epiModSerre.comp_mem s (Abelian.factorThruImage f) hs
      (epiModSerre_of_epi _ _)
    rwa [show s ≫ Abelian.factorThruImage f = 0 by cat_disch,
      epiModSerre_zero_iff] at this
  · exact ⟨_, kernel.ι f, P.prop_of_iso (Abelian.coimageIsoImage f).symm hf, by simp⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)

Tactic:
intro X Y Z i hi f ⟨hY, hZ⟩
    rw [isomorphisms.iff] at hi
    exact ⟨(P.prop_iff_of_isIso i).mpr hY, hZ⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderSubobjects
⊢ (MorphismProperty.ofObjectProperty P P).kernels ≤ P

Tactic:
by
    intro _ ⟨_, k, hk, hf⟩
    let := Fork.IsLimit.mono hk
    exact P.prop_of_mono k.ι hf.1

Goal state after: