mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
⊢ f ≫ PInfty.f n = 0 ↔ f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0

Tactic:
by
  constructor
  · intro h
    rcases n with _ | n
    · dsimp at h
      rw [comp_id] at h
      rw [h, zero_comp]
    · have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
      dsimp at h'
      rw [comp_id, comp_add, h, zero_add] at h'
      rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
        Finset.sum_eq_zero]
      intro i _
      simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]
  · intro h
    rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_zero]
    intro A
    by_cases hA : A.EqId
    · dsimp at hA
      subst hA
      rw [assoc, reassoc_of% h, zero_comp]
    · simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i ↦ π.obj (X i))

Tactic:
exact Grpd.piLimitFanIsLimit _

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ LeftHomotopyRel f g

Tactic:
rw [← LeftHomotopyClass.mk_eq_mk_iff]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ LeftHomotopyClass.mk f = LeftHomotopyClass.mk g
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

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
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A✝ B✝ X✝ Y✝ : C
x✝⁴ : A✝ ⟶ B✝
x✝³ : X✝ ⟶ Y✝
x✝² : Cofibration x✝⁴
x✝¹ : WeakEquivalence x✝⁴
x✝ : Fibration x✝³
⊢ HasLiftingProperty x✝⁴ x✝³

Tactic:
by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

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
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A✝ B✝ X✝ Y✝ : C
x✝⁴ : A✝ ⟶ B✝
x✝³ : X✝ ⟶ Y✝
x✝² : Cofibration x✝⁴
x✝¹ : Fibration x✝³
x✝ : WeakEquivalence x✝³
⊢ HasLiftingProperty x✝⁴ x✝³

Tactic:
by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
i : C
x : A.toFunctor.obj i
⊢ ↑x ∈ (Subfunctor.equalizer f g).obj i ↔ (ConcreteCategory.hom (f.app i)) x = (ConcreteCategory.hom (g.app i)) x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : ∃ a, Sᶜ = {a}
⊢ ∃ j, S = {j}ᶜ

Tactic:
obtain ⟨j, hS⟩ := hS

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ ∃ j, S = {j}ᶜ
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝⁷ : Category.{v'', u''} J
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : (monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K
inst✝¹ : HasPullbacks C
inst✝ : HasIterationOfShape K C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
rw [← functorCategory_monomorphisms]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝⁷ : Category.{v'', u''} J
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : (monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K
inst✝¹ : HasPullbacks C
inst✝ : HasIterationOfShape K C
⊢ ((monomorphisms C).functorCategory J).IsStableUnderTransfiniteCompositionOfShape K
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝³ : Category.{v'', u''} J
K' : Type u'
inst✝² : (monomorphisms C).IsStableUnderCoproductsOfShape K'
inst✝¹ : HasCoproductsOfShape K' C
inst✝ : HasPullbacks C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderCoproductsOfShape K'

Tactic:
rw [← functorCategory_monomorphisms]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝³ : Category.{v'', u''} J
K' : Type u'
inst✝² : (monomorphisms C).IsStableUnderCoproductsOfShape K'
inst✝¹ : HasCoproductsOfShape K' C
inst✝ : HasPullbacks C
⊢ ((monomorphisms C).functorCategory J).IsStableUnderCoproductsOfShape K'
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ ∀ {x y z : X₁ ⊕ X₂}, Rel' f g x y → Rel' f g y z → Rel' f g x z

Tactic:
rintro x y z (_ | ⟨_, _, h⟩ | s | _) hyz

Goal state after:
case refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x z : X₁ ⊕ X₂
hyz : Rel' f g x z
⊢ Rel' f g x z

case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) z
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) z

case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s : S
hyz : Rel' f g (Sum.inr ((ConcreteCategory.hom g) s)) z
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) z

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s✝ : S
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) z
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) z
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: ⊢ innerHornInclusions = ⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι

Tactic:
by
  ext
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain @⟨n, i, h0, hn⟩ := h
    simp only [iSup_iff, ofHoms_iff, Subtype.exists, exists_prop]
    use n, i
  · simp only [iSup_iff, ofHoms_iff] at h
    obtain ⟨n, ⟨i, h0, hn⟩, _, _⟩ := h
    exact horn_ι_mem_innerHornInclusions h0 hn

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case pos
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∈ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : ((skeletonOfMono i) d).preimage c.map = ⊤
⊢ c.simplex ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌)))

Tactic:
have := h.symm.le _ (show stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ _ by simp)

Goal state after:
case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
h : ((skeletonOfMono i) d).preimage c.map = ⊤
this : stdSimplex.objEquiv.symm (𝟙 ⦋d⦌) ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋d⦌)
⊢ c.simplex ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaBoundary ≫ t i d ≫ ((skeletonOfMono i) d).ι =
    ∂Δ[d].ι ≫ c.ιSigmaStdSimplex ≫ b i d ≫ ((skeletonOfMono i) (d + 1)).ι

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaBoundary ≫ l i d = ∂Δ[d].ι ≫ c.ιSigmaStdSimplex

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ c.ιSigmaStdSimplex ≫ b i d ≫ ((skeletonOfMono i) (d + 1)).ι = c.map

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))

Tactic:
SSet.yonedaEquiv_map,

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (stdSimplex.objEquiv.symm (SimplexCategory.δ j)))
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))

Tactic:
SSet.yonedaEquiv_map,

Goal state after:
case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (stdSimplex.objEquiv.symm (SimplexCategory.δ j)))
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
by cases α; cases β; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f f' : a ⟶ b
α : f = f'
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

Tactic:
by cases α; cases β; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
⊢ F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) ≫ f.app d✝ =
    (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g

Tactic:
have := a.naturality g h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
this :
  F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) = a.app c✝ h ≫ X✝.map g
⊢ F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) ≫ f.app d✝ =
    (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eHomEquiv V) (P.ι.map (f ≫ g)) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝

Tactic:
rw [Functor.map_comp, eHomEquiv_comp]

Goal state after:
V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (λ_ (𝟙_ V)).inv ≫
      ((eHomEquiv V) (P.ι.map f) ⊗ₘ (eHomEquiv V) (P.ι.map g)) ≫ eComp V (P.ι.obj X✝) (P.ι.obj Y✝) (P.ι.obj Z✝) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
⊢ ∀ (x y : Paths V) (f₁ f₂ : x ⟶ y),
    FreeReflRel V x y f₁ f₂ → (Paths.lift F.toPrefunctor).map f₁ = (Paths.lift F.toPrefunctor).map f₂

Tactic:
rintro _ _ _ _ ⟨h⟩

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
x✝ Y : Paths V
⊢ (Paths.lift F.toPrefunctor).map (𝟙rq x✝).toPath = (Paths.lift F.toPrefunctor).map Quiver.Path.nil
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₁ =
        (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₂

Tactic:
rintro _ _ _ _ ⟨h⟩

Goal state after:
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝ ≫ Quiver.Hom.toPath e₁₂✝)) =
    (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝))
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₁ f
h : r.deg X = r.deg Y
⊢ MorphismProperty.identities C f

Tactic:
by
  by_contra
  exact h.not_gt (r.lt₁ _ hf this)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
f : V ⟶ W
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₁ =
        (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₂

Tactic:
rintro _ _ _ _ ⟨h⟩

Goal state after:
V W : Truncated 2
f : V ⟶ W
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
⊢ (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝ ≫ Quiver.Hom.toPath e₁₂✝)) =
    (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ map' f 0 = 0

Tactic:
by
  simp [← Fin.castSucc_zero, -Fin.castSucc_zero', map'_eq_castSucc_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)), a ≤ b → (a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2)
⊢ StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)

Tactic:
simp only [Fin.strictMono_iff_lt_succ]

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)), a ≤ b → (a < b ↔ ↑a.1 + ↑a.2 < ↑b.1 + ↑b.2)
⊢ (∀ (i : Fin n), (orderHomOfSimplex x hm) i.castSucc < (orderHomOfSimplex x hm) i.succ) ↔
    ∀ (i : Fin n), (objEquiv x) i.castSucc < (objEquiv x) i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i = f.filtration m

Tactic:
by
  apply le_antisymm
  · simp only [iSup_le_iff, Subtype.forall, Set.mem_Iio]
    intro j hj
    exact f.filtration_monotone hj.le
  · conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]
    exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦
      (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans
        (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.mpr hj⟩))⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ IsSplitEpi i

Tactic:
obtain ⟨J, _, ⟨p⟩⟩ := hP Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
⊢ IsSplitEpi i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

Tactic:
by
  rw [innerAnodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ pushout.inl f g ▷ Q ≫ hP.isoPushout.inv ▷ Q = inl ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ pushout.inr f g ▷ Q ≫ hP.isoPushout.inv ▷ Q = inr ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ inl ▷ Q ≫ hP.isoPushout.hom ▷ Q = pushout.inl f g ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ inr ▷ Q ≫ hP.isoPushout.hom ▷ Q = pushout.inr f g ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ pushout.inl f g ▷ Q ≫ (pushoutSymmetry f g).hom ▷ Q = pushout.inr g f ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ pushout.inr f g ▷ Q ≫ (pushoutSymmetry f g).hom ▷ Q = pushout.inl g f ▷ Q

Tactic:
simp [← comp_whiskerRight]

Goal state after: