mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ #(Icc (-1 + -(↑n).1) ((↑n).1 + 1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) -
      #(Icc (-(↑n).1) (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
fst_natCast,

Goal state after:
α : 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 : ℕ
⊢ #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) - #(Icc (-↑n) ↑n) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l = if n = 0 then ℘[L - l] l else ↑(n + 1)! * L.sumInvPow l (n + 2)

Tactic:
rw [← div_mul_cancel₀ (a := iteratedDeriv _ _ _) (b := ↑n !) (by simp),
    ← eq_div_iff_mul_eq (by simp)]
  trans if n = 0 then ℘[L - l] l else (n + 1) * L.sumInvPow l (n + 2)
  · simpa using congr($((L.analyticAt_weierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_weierstrassPExcept l)).coeff n)
  · cases n <;> simp [Nat.factorial_succ]; field

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

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

Tactic:
← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,

Goal state after:
L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
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:
← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L] z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x ↑r

Tactic:
← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,

Goal state after:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x ↑r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → |eval x (T ℝ ↑n)| = 1

Tactic:
rintro ⟨k, hk, rfl⟩

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ |eval (cos (↑k * π / ↑n)) (T ℝ ↑n)| = 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
⊢ z ∈ {l₀}ᶜ → ℘[L] z = (z - l₀) ^ (-2) • ((z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2)

Tactic:
(hz : _ ≠ _)

Goal state after:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
⊢ ℘[L] z = (z - l₀) ^ (-2) • ((z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = eval y (∑ p ∈ f.support, f p • p)

Tactic:
Polynomial.eval_finsetSum

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = ∑ i ∈ f.support, eval y (f i • i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ 1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)) = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

Tactic:
one_div_add_one_div

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ (x - (↑n + 1) + (x + (↑n + 1))) / ((x - (↑n + 1)) * (x + (↑n + 1))) = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

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

Tactic:
apply DifferentiableOn.add <;> refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_

Goal state after:
case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0

case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
by
  rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
  exact hf.neg.integral_le_sum_Ico hab

Goal state after:
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
η : yoneda.obj X ⟶ F.obj j
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((ConcreteCategory.hom
                    ((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))).toFun
                η).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (((ConcreteCategory.hom (↾fun g ↦ g ≫ colimit.ι F j)).toFun η).app Y)).toFun f

Tactic:
dsimp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, yonedaEquiv]

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
η : yoneda.obj X ⟶ F.obj j
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom ((colimit F).map (Quiver.Hom.op f)))
      ((ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv)
        ((ConcreteCategory.hom (colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)) j))
          ((ConcreteCategory.hom (η.app (op X))) (𝟙 X)))) =
    (ConcreteCategory.hom ((colimit.ι F j).app Y)) ((ConcreteCategory.hom (η.app Y)) f)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1

Tactic:
by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi

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

Goal state before:
pp: α : 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'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : (pointwiseProduct F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : (pointwiseProduct F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
⊢ y = (hom (colimit.ι (pointwiseProduct F) k)) yk

Tactic:
by
      simp only [k, yk, colimit.w_apply, hyk₀]

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

Goal state before:
pp: case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), (hom (colimit.ι (F s) (k s))) (p s) = (hom (Pi.π (fun s ↦ colimit (F s)) s)) x
x✝ : Discrete α
s : α
⊢ (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s }))
      ((hom (colimitPointwiseProductToProductColimit F))
        ((hom (colimit.ι (pointwiseProduct F) k)) ((hom (productIso ((Functor.pi F).obj k)).inv) p))) =
    (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s })) x

Tactic:
have := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s)
      ((Types.productIso _).inv p)

Goal state after:
case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), (hom (colimit.ι (F s) (k s))) (p s) = (hom (Pi.π (fun s ↦ colimit (F s)) s)) x
x✝ : Discrete α
s : α
this :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p) =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p)
⊢ (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s }))
      ((hom (colimitPointwiseProductToProductColimit F))
        ((hom (colimit.ι (pointwiseProduct F) k)) ((hom (productIso ((Functor.pi F).obj k)).inv) p))) =
    (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s })) x
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

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

Tactic:
rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)
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 A : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
m : ↑M
⊢ Sigma.ι (fun x ↦ G) m ≫ d g = (ModuleCat.Hom.hom g) m

Tactic:
by
  simp [d]

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

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

Tactic:
Over.w

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ Φ.obj.hom.app X = Φ.ι.app X
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 : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = 0
⊢ a = 0

Tactic:
← apply_zero f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0
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 : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
erw [← (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality_assoc
    ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)]

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 G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

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

Tactic:
exact ⟨h _ hX, hY⟩

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:
intro _ ⟨_, k, hk, hf⟩
    let := Fork.IsLimit.mono hk
    exact P.prop_of_mono k.ι hf.1

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
this : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f
⊢ L.map φ.f ≫ L.map f = 0

Tactic:
rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
x y : N₁ ⋊[φ₁] G₁
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩

Tactic:
replace h := DFunLike.ext_iff.1 (h x.right) y.left

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
x y : N₁ ⋊[φ₁] G₁
h : (fn.comp (MulEquiv.toMonoidHom (φ₁ x.right))) y.left = ((MulEquiv.toMonoidHom (φ₂ (fg x.right))).comp fn) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))
x y : N₁ ⋊[φ₁] G₁
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩

Tactic:
replace h := DFunLike.ext_iff.1 (h x.right) y.left

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Group N
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h : (MulEquiv.trans (φ₁ x.right) fn) y.left = (fn.trans (φ₂ (fg x.right))) y.left
⊢ ⟨fn (x * y).left, fg (x * y).right⟩ = ⟨fn x.left, fg x.right⟩ * ⟨fn y.left, fg y.right⟩
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
⊢ PreservesFiniteLimits (forget V G)

Tactic:
by
  change PreservesFiniteLimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance
  apply comp_preservesFiniteLimits

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

Goal state before:
pp: case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
h : H
⊢ X.ρ h ≫ g.hom = g.hom ≫ Y.ρ h

Tactic:
obtain ⟨a, rfl⟩ := f_surj h

Goal state after:
case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : Abelian D := abelian L P
⊢ IsIso (L.map f) ↔ P.isoModSerre f

Tactic:
isIso_iff_mono_and_epi,

Goal state after:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : Abelian D := abelian L P
⊢ Mono (L.map f) ∧ Epi (L.map f) ↔ P.isoModSerre f
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_3
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
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt},
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = ↑((h X).desc' s.π ⋯)

Tactic:
intro m hm
      rw [← cancel_epi (adj₁.counit.app X)]
      apply hm.trans ((h _).desc' s.π _).2.symm

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

Goal state before:
pp: case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.of f✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.of f✝))

Tactic:
| of =>

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
⊢ ∀ (s : LeftExtension f (𝟙 a ≫ h)) (τ : (LeftExtension.mk u adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯

Tactic:
intro s τ₀
    ext
    /- We need to specify the type of `τ` to use the notation `⊗≫`. -/
    let τ : u ≫ h ⟶ s.extension := τ₀.right
    have hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit := by
      simpa [bicategoricalComp] using LeftExtension.w τ₀
    calc τ
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 _ := by
        rw [adj.right_triangle]; bicategory
      _ = 𝟙 _ ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ _ ≫ _ ◁ τ) ⊗≫ 𝟙 _ := by
        rw [rightZigzag]; bicategory
      _ = 𝟙 _ ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 _ := by
        rw [← whisker_exchange]; bicategory
      _ = _ := by
        rw [hτ]; dsimp only [StructuredArrow.homMk_right]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inl hb

Goal state after: