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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (√(2 * ↑(2 * n)) ^ 2 * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))

pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n

Tactic:
sq_sqrt

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))

Tactic:
refine Tendsto.congr' (eventually_atTop.mpr ⟨1, fun n hn =>
    stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩) ?_
  have h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2) := by
    rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
    simp
  rw [h]
  exact ((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2)
    (pow_ne_zero 2 hane)).mul tendsto_self_div_two_mul_self_add_one

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

Goal state before:
pp: case ha
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ 0 ≤ (-1) ^ i * c i

pp: case hbc
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ 1

Tactic:
· exact (hcnonneg i (Finset.mem_Iic.mp hi))

Goal state after:
case hbc
n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ 1
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
hk_values : k ∈ Finset.Icc (-2) 2
⊢ ↑k / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
fin_cases hk_values <;> simp

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ) (x_1 : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i x_1 * (z - x) ^ i

Tactic:
apply Summable.tsum_comm

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
    Finset.card_Icc_prod]
  simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg,
    fst_one, fst_natCast, snd_add, snd_neg, snd_one, snd_natCast]

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

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)

Tactic:
refine tsub_eq_of_eq_add ?_

Goal state after:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ = L.relation w

Tactic:
relation,

Goal state after:
L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃ =
    if w ∈ L.lattice then 0 else ℘'[L] w ^ 2 - 4 * ℘[L] w ^ 3 + L.g₂ * ℘[L] w + L.g₃
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
rw [h1, h2]

Goal state after:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / (cexp (-(z * I)) * (1 - cexp (2 * I * z)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: Z : Set ℂ
hZC : IsCompact Z
⊢ MultipliableUniformlyOn (fun n z ↦ 1 + sineTerm z n) Z

Tactic:
obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC

Goal state after:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ MultipliableUniformlyOn (fun n z ↦ 1 + sineTerm z n) Z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ↑π * (↑π * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))

Tactic:
have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 : ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n)) = ∑' (n : ℕ), (1 / (x - ↑(n + 1)) + 1 / (x + ↑(n + 1)))
⊢ ↑π * (↑π * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))
Module: Mathlib.NumberTheory.Real.GoldenRatio

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

Tactic:
repeat rw [coe_fib_eq]

Goal state after:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
simp only [one_div]

Goal state after:
case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -x⁻¹) ℍₒ z
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : ObjectProperty C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) ≤ ∫ (x : ℝ) in Ioi (↑N - 1), f x

Tactic:
convert! AntitoneOn.tsum_comp_add_le_integral (N - 1) (mod_cast anti) (mod_cast integrable)
      (mod_cast nonneg) using 1

Goal state after:
case e'_3
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∑' (i : ℕ), f ↑(i + N) = ∑' (n : ℕ), f ↑(n + (N - 1) + 1)

case e'_4
f : ℝ → ℝ
N : ℕ
hN : 1 ≤ N
anti : AntitoneOn f (Ici (↑N - 1))
integrable : IntegrableOn f (Ioi (↑N - 1)) volume
nonneg : ∀ t ∈ Ioi (↑N - 1), 0 ≤ f t
⊢ ∫ (x : ℝ) in Ioi (↑N - 1), f x = ∫ (x : ℝ) in Ioi ↑(N - 1), f x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_
      exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

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)
⊢ (fst L R).Initial

Tactic:
Functor.initial_iff_of_isCofiltered

Goal state after:
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)
⊢ (∀ (d : A), ∃ c, Nonempty ((fst L R).obj c ⟶ d)) ∧
    ∀ {d : A} {c : Comma L R} (s s' : (fst L R).obj c ⟶ d), ∃ c' t, (fst L R).map t ≫ s = (fst L R).map t ≫ s'
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✝¹ : IsConnected A
inst✝ : R.Final
⊢ IsConnected (Comma L R)

Tactic:
by
  rwa [isConnected_iff_of_final (fst L R)]

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
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F (op i)).op = limit.π (F.rightOp ⋙ coyoneda) i

Tactic:
by
  rw [← coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Tactic:
simpa using! hf j

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ ((g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom =
    ((h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom

Tactic:
simpa using! hf j

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
⊢ Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

Tactic:
Pi.ι_π_of_ne _ hb₁,

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
⊢ Pi.π f (↑b).as ≫ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
n : ℤ
hn : ¬n ≤ 0
⊢ Projective (R.cochainComplex.X n)

Tactic:
exact IsZero.projective (CochainComplex.isZero_of_isStrictlyLE _ 0 _)

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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (Cocycle.fromSingleMk (-f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
Cocycle.fromSingleMk_neg _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (-Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
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 : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (F.rightDerived n).map f =
    (P.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map g ≫
        (Q.isoRightDerivedObj F n).inv

Tactic:
← cancel_mono (Q.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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (F.rightDerived n).map f ≫ (Q.isoRightDerivedObj F n).hom =
    ((P.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
            g ≫
          (Q.isoRightDerivedObj F n).inv) ≫
      (Q.isoRightDerivedObj F n).hom
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hX : P X✝
hY : Q Y✝
⊢ ofObjectProperty P Q' f✝

Tactic:
exact ⟨hX, h _ hY⟩

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:
by
  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.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasCokernels C
inst✝ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) P.ι

Tactic:
have := P.createsCokernels f
  have := P.hasColimit_parallelPair_comp_ι f
  exact preservesColimit_of_createsColimit_and_hasColimit _ _

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
⊢ X✝ ⟶ Y✝

Tactic:
refine ⟨h.preimage f.hom, fun _ ↦ h.map_injective ?_⟩

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
x✝ : G
⊢ F.map (X✝.ρ x✝ ≫ h.preimage f.hom) = F.map (h.preimage f.hom ≫ Y✝.ρ x✝)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ ≫ 𝟙 (𝟙_ D)

Tactic:
rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (constructLeftAdjointEquiv R F' adj₁ adj₂ h✝ Y' X) (h ≫ g) =
    (constructLeftAdjointEquiv R F' adj₁ adj₂ h✝ Y X) h ≫ R.map g

Tactic:
rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ↑⟨(adj₁.homEquiv (U.obj X) (R.obj Y')).symm
          ((adj₂.homEquiv (U.obj X) Y')
            ↑((Cofork.IsColimit.homIso
                  (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                  Y')
                (h ≫ g))),
        ⋯⟩ =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y'))
        ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩ ≫
          R.map g))
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ eqToHom ⋯ ≫
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.fiber =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).fiber

Tactic:
simp only [Cat.Hom.comp_toFunctor, comp_obj, categoryStruct_comp_base, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, eqToHom_refl, map_comp, ← Cat.Hom.comp_map, assoc,
        NatTrans.naturality_assoc]
      simp [naturality_comp_inv_app, ← Functor.map_comp, ← reassoc_of% Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ (f a).Dom

Tactic:
WellFounded.fixF_eq

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ (f a).Dom
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
WellFounded.fixF_eq

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'