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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ DifferentiableAt ℂ (fun t ↦ ↑π * t) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ DifferentiableAt ℂ (HMul.hMul ↑π) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (↑k) (fun x ↦ x + ↑d) ℂ_ℤ

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ -1 < ψ

Tactic:
neg_lt,

Goal state after:
⊢ -ψ < 1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℤ
⊢ ↑(Int.fib n) = (φ ^ n - ψ ^ n) / √5

Tactic:
by
  obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
  · exact coe_fib_eq n
  · simp only [Int.fib_neg, Int.even_coe_nat, Int.fib_natCast, Int.cast_ite, Int.cast_neg,
      Int.cast_natCast, zpow_neg, zpow_natCast, ← inv_pow, inv_goldenRatio, inv_goldenConj,
      ← neg_one_mul ψ, ← neg_one_mul φ, mul_pow, neg_one_pow_eq_ite]
    grind [coe_fib_eq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℂ
ha : a ∈ K
⊢ ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ a‖ ≤ cotTermUpperBound k A B hB n

Tactic:
rcases hKAB ha with ⟨a, haAB, rfl⟩
  simp only [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n a.im_pos, Complex.norm_mul,
    norm_pow, norm_neg, norm_one, one_pow, Complex.norm_natCast, one_mul, cotTermUpperBound,
    Int.reduceNeg, norm_zpow, Real.norm_eq_abs, two_mul, add_mul]
  gcongr
  have h1 := summand_bound_of_mem_verticalStrip (k := k + 1) (by positivity) ![1, n + 1] hB haAB
  have h2 := abs_norm_eq_max_natAbs_neg n ▸ summand_bound_of_mem_verticalStrip (k := k + 1)
    (by positivity) ![1, -(n + 1)] hB haAB
  apply norm_add_le_of_le
  · simpa (disch := positivity) [sub_eq_add_neg, ← Real.rpow_intCast, abs_norm_eq_max_natAbs,
      abs_of_nonneg] using h1
  · simpa (disch := positivity) [sub_eq_add_neg, ← Real.rpow_intCast, abs_norm_eq_max_natAbs,
      abs_of_nonneg] using h2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ y + (↑n + 1)) ℍₒ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: n l : ℕ
⊢ DifferentiableOn ℂ (fun y ↦ y - (↑n + 1)) ℍₒ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L

Tactic:
refine lt_of_le_of_lt ?_ hk

Goal state after:
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x ↦ (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) ≤ ((fun x ↦ (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ ↑π) ℍₒ z

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun i ↦ i) ℍₒ z

Tactic:
fun_prop

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 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n

Tactic:
rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩

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)
⊢ ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
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 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩

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
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)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

pp: case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
· exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A

Goal state after:
case refine_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall (CostructuredArrow yoneda A)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_2
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₂
⊢ ∃ W h, h ≫ u = h ≫ v

Tactic:
have := IsCofiltered.eq_condition u.right v.right

Goal state after:
case refine_2
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
⊢ ∃ W h, h ≫ u = h ≫ v
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
⊢ IsIndObject (colimit F)

Tactic:
by
  have : IsFiltered (CostructuredArrow yoneda (colimit F)) :=
    IndizationClosedUnderFilteredColimitsAux.isFiltered F hF
  refine (isIndObject_iff _).mpr ⟨this, ?_⟩
  -- It remains to show that `CostructuredArrow yoneda (colimit F)` is finally small. Because we
  -- have already shown it is filtered, it suffices to exhibit a small weakly terminal set. For this
  -- we use that all the `CostructuredArrow yoneda (F.obj i)` have small weakly terminal sets.
  have : ∀ i, ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v} s),
      ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
    fun i => (hF i).finallySmall.exists_small_weakly_terminal_set
  choose s hs j hjs hj using this
  refine finallySmall_of_small_weakly_terminal_set
    (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)
  obtain ⟨i, y, hy⟩ := FunctorToTypes.jointly_surjective'.{v, v} F _ (yonedaEquiv A.hom)
  let y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
  obtain ⟨x⟩ := hj _ y'
  refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩
  · simp only [Set.mem_iUnion, Set.mem_image]
    exact ⟨i, j i y', hjs _ _, rfl⟩
  · refine ?_ ≫ (map (colimit.ι F i)).map x
    refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)
    simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']

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

Goal state before:
pp: case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = y
⊢ y = y'

Tactic:
obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'

Goal state after:
case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = y
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = y'
⊢ y = y'
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

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

Tactic:
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✝ n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f + g) ≫ R.cocomplex.d n m = 0

Tactic:
simp [hf, hg]

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✝ n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f - g) ≫ R.cocomplex.d n m = 0

Tactic:
simp [hf, hg]

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 R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ (fun g_1 ↦ app (f ≫ g) g_1) x ≈ (fun g_1 ↦ app g g_1) ((fun g ↦ app f g) x)

Tactic:
simp only [app]
      rw [← Category.assoc, Over.coe_hom]

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
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ f = 0

Tactic:
← Category.id_comp f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.complex.d m n ≫ (f + g) = 0

Tactic:
simp [hf, hg]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.complex.d m n ≫ (f - g) = 0

Tactic:
simp [hf, hg]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f - (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯
          (-↑m) ⋯ ⋯))

Tactic:
rw [Cocycle.toSingleMk_sub _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ -
          Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ g) ⋯ (-↑m) ⋯ ⋯))
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯ ∈
      coboundaries R.cochainComplex ((singleFunctor C 0).obj Y) ↑n ↔
    ∃ g, R.complex.d n p ≫ g = f

Tactic:
rw [Cocycle.toSingleMk_mem_coboundaries_iff _ _ _ _ _ (-p) (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫ g =
        (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ↔
    ∃ g, R.complex.d n p ≫ g = f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

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
inst✝ : Epi f
⊢ P.isoModSerre f ↔ P.monoModSerre f

Tactic:
have := P.epiModSerre_of_epi f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Epi f
this : P.epiModSerre f
⊢ P.isoModSerre f ↔ P.monoModSerre f
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 : C
inst✝ : Injective X
⊢ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex).ExactAt (n + 1)

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : P.isoModSerre t), f₁ ≫ t = f₂ ≫ t

Tactic:
refine ⟨_, cokernel.π (f₁ - f₂), ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ P.isoModSerre (cokernel.π (f₁ - f₂))

case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ ≫ cokernel.π (f₁ - f₂) = f₂ ≫ cokernel.π (f₁ - f₂)
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 : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.toRightDerivedZero.app X =
    I.toRightDerivedZero' F ≫
      (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom ≫
        (I.isoRightDerivedObj F 0).inv

Tactic:
by
  dsimp [Functor.toRightDerivedZero, isoRightDerivedObj]
  have h₁ := InjectiveResolution.toRightDerivedZero'_naturality
    (𝟙 X) (injectiveResolution X) I (desc (𝟙 X) _ _) (by simp) F
  simp only [Functor.map_id, id_comp] at h₁
  have h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (desc (𝟙 X) _ _) :=
    comp_id _
  rw [← cancel_mono ((HomotopyCategory.homologyFunctor _ _ 0).map
      (I.isoRightDerivedToHomotopyCategoryObj F).hom),
    assoc, assoc, assoc, assoc, assoc, ← Functor.map_comp,
    Iso.inv_hom_id, Functor.map_id, comp_id,
    reassoc_of% h₁, h₂, ← HomologicalComplex.homologyπ_naturality_assoc]
  erw [← NatTrans.naturality]
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : Fintype (G ⧸ H)
h : N ≤ H
g : G
⊢ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯) =
    FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ H))).ρ g

Tactic:
ext (x : G ⧸ N)
    induction x using Quotient.inductionOn
    rfl

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

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
⊢ Continuous v

Tactic:
fun_prop

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

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this✝ : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
this : Continuous u
⊢ Continuous (u ∘ v)

Tactic:
fun_prop

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝² : G.Full
inst✝¹ : G.Faithful
inst✝ : H.PreservesEpimorphisms
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (t.adj₂.counit.app X ≫ t.adj₁.unit.app X)

Tactic:
have _ := t.adj₂.isLeftAdjoint
  refine ⟨fun h ↦ by rw [← map_rightToLeft_app]; exact G.map_epi _, fun h ↦ ?_⟩
  rw [epi_rightToLeft_app_iff_epi_map_adj₁_unit_app]
  simpa using epi_comp (t.adj₂.unit.app (H.obj X)) (H.map (t.adj₂.counit.app X ≫ t.adj₁.unit.app X))

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝ = (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ (f₂✝ ≫ g₂✝)

Tactic:
Bicategory.whiskerLeft_comp,

Goal state after:
C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝ = (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ f₂✝ ≫ Z₁✝ ◁ g₂✝
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
by ext; exact whisker_exchange _ _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵖ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
by ext; exact whisker_exchange _ _

Goal state after: