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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫
        (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫
            Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫
          𝟙
            { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X,
              idem := ⋯ }

Tactic:
dsimp only [toKaroubi]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj { X := X, p := 𝟙 X, idem := ⋯ })) ≫
        (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G) (σ (t, snd✝).1, (t, snd✝).2) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)

Tactic:
trans_apply

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (if h : ↑(σ (t, snd✝).1, (t, snd✝).2).1 ≤ 1 / 2 then
      F (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2)
    else G (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1 - 1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2)) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
⊢ ∀ (t : ↑unitInterval),
    ∀ x ∈ S,
      { toFun := fun x ↦ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x =
        (ContinuousMap.pi f) x

Tactic:
intro t x hx

Goal state after:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst✝¹ : (i : I) → TopologicalSpace (X i)
inst✝ : TopologicalSpace A
f g : (i : I) → C(A, X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : ↑unitInterval
x : A
hx : x ∈ S
⊢ { toFun := fun x ↦ (Homotopy.pi fun i ↦ (homotopies i).toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x =
    (ContinuousMap.pi f) x
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ Path.Homotopic.pi (𝟙 x) = 𝟙 { as := fun i ↦ (x i).as }

Tactic:
change (Path.Homotopic.pi fun i => Path.Homotopic.Quotient.mk _) = _

Goal state after:
I : Type u
X : I → TopCat
x : (i : I) → ↑(π.obj (X i))
⊢ (Path.Homotopic.pi fun i ↦ Path.Homotopic.Quotient.mk (Path.refl (x i).as)) = 𝟙 { as := fun i ↦ (x i).as }
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ f x₁ = g x₃

Tactic:
convert! hfg 1 <;> simp only [Path.target]

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

Goal state before:
pp: case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl]

Goal state after:
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (((π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            𝟙
              ((π.map (TopCat.ofHom H.uliftMap)).obj
                ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 0 } }, { as := x₁ })))) ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))) ≫
        hcast ⋯ =
    H.diagonalPath' p
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl]

Goal state after:
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast ⋯ ≫
      (((π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            𝟙
              ((π.map (TopCat.ofHom H.uliftMap)).obj
                ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 1 } }, { as := x₀ })))) ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))) ≫
        hcast ⋯ =
    H.diagonalPath' p
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
⊢ ModelCategory C

Tactic:
have {X Y : C} (f : X ⟶ Y) [hf : Cofibration f] : Cofibration (e.functor.map f) := by
    simpa [cofibration_iff, h₁] using hf

Goal state after:
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)
⊢ ModelCategory C
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
x₂ : X
h₂ : x₂ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
simpa using h

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

Goal state before:
pp: J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩
⊢ x = y

Tactic:
simpa using h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂

pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)

Tactic:
· rintro ⟨_⟩
    rfl

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ (skeletonOfMono i) 0 = Subcomplex.range i

Tactic:
by
  simp [skeletonOfMono]

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1⦌
⊢ X.spine m ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1) x).interval 1 m ⋯

Tactic:
by
  obtain _ | m := m
  · ext
    simp [spine, Path.vertex, Truncated.Path.vertex,
      Truncated.spine, Path.interval, Truncated.Path.interval,
      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const]
    rfl
  · ext i
    dsimp
    rw [SimplicialObject.δ_def, ← Functor.map_comp_apply, ← op_comp,
      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]
    symm
    exact Path.arrow_interval _ _ _ _ _ _ (by rw [Fin.val_succ, add_comm])

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍ (x✝⁴.fst.toFunctor.prod' x✝⁴.snd.toFunctor).toCatHom.toFunctor.map x✝

Tactic:
by dsimp; rw [← h1, ← h2]; rfl

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

Goal state before:
pp: case mk
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
X✝ Y✝ : A.HomotopyCategory₂
f✝ : X✝ ⟶ Y✝
f : Edge X✝.pt Y✝.pt
⊢ Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f ≫ 𝟙 Y✝ = Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f

Tactic:
exact ((compStruct _ _).comp_unique (compId _) .refl .refl).congr_homotopyCategory₂HomMk

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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
let α₀ := strArrowMk₂ (mkOfLe (n := n) ⟨i + k, by omega⟩ ⟨j, by omega⟩
        (by simp only [Fin.mk_le_mk]; omega))

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
have h₂ : X.map α₂.hom (lift sx s x) = s.π.app α₂ x :=
        hk i (i + k) (by simp) (by lia) rfl

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom = (iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)

Tactic:
ext; apply id_prod_mapHomotopyCategory_comp_inverse

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (j.predAbove k).castSucc < i

Tactic:
Fin.predAbove_of_le_castSucc _ _ hk'

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : ofSimplex { dim := n, simplex := s }.toN.simplex ≤ A
⊢ ofSimplex s ≤ A

Tactic:
simpa using h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : h.ι
⊢ h.type₁ x = ↑(h.pairing.p (h.equivII x))

Tactic:
by
  simp +instances

Goal state after:
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✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌)))) ∉
    (range (f.m j)).obj (op ⦋c.dim + 1⦌)

Tactic:
rintro ⟨y, hy⟩

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
y : f.sigmaHorn j _⦋c.dim + 1⦌
hy :
  (ConcreteCategory.hom ((f.m j).app (op ⦋c.dim + 1⦌))) y =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False
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✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) ∉
    (range (f.m j)).obj (op ⦋c.dim⦌)

Tactic:
rintro ⟨y, hy⟩

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
y : f.sigmaHorn j _⦋c.dim⦌
hy :
  (ConcreteCategory.hom ((f.m j).app (op ⦋c.dim⦌))) y =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
X : C
A : Subobject X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ A = ⊤

Tactic:
· rw [Subobject.isIso_iff_mk_eq_top]
    refine hS₂ _ (fun G hG g ↦ ?_)
    rw [Subobject.mk_factors_iff]
    exact h G hG g

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
X : C
A : Subobject X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ A = ⊤
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
⊢ φ₁ ≫ colimit.ι Φ j = φ₂ ≫ colimit.ι Φ j

Tactic:
have : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair := by
        apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure
        refine .of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)
        simp only [hasCardinalLT_aleph0_iff]
        infer_instance

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ φ₁ ≫ colimit.ι Φ j = φ₂ ≫ colimit.ι Φ j
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
⊢ φ₁ ≫ (E.coconeAt X).ι.app j = φ₂ ≫ (E.coconeAt X).ι.app j

Tactic:
simpa using h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp.llp.rlp

Tactic:
rlp_llp_rlp

Goal state after:
⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp