mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: A : TopCat
B : TopCat
⊢ prodToProdTop A B ≫ (projLeft A B).prod' (projRight A B) = 𝟙 (CategoryTheory.Grpd.of (↑(π.obj A) × ↑(π.obj B)))

Tactic:
change prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B) = 𝟭 _
    apply CategoryTheory.Functor.hext; · intros; ext <;> simp <;> rfl
    rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ ⟨f₀, f₁⟩
    have : Path.Homotopic.projLeft ((prodToProdTop A B).map (f₀, f₁)) = f₀ ∧
      Path.Homotopic.projRight ((prodToProdTop A B).map (f₀, f₁)) = f₁ :=
        And.intro (Path.Homotopic.projLeft_prod f₀ f₁) (Path.Homotopic.projRight_prod f₀ f₁)
    cat_disch

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ PathConnectedSpace X

Tactic:
rw [pathConnectedSpace_iff_eq]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : CofibrantObject C
⊢ weakEquivalences (HoCat C) (HoCat.ιCompResolutionNatTrans.app X)

Tactic:
rw [← weakEquivalence_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : CofibrantObject C
⊢ WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ weakEquivalences C (HoCat.pResolutionObj X)

Tactic:
rw [← weakEquivalence_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ WeakEquivalence (HoCat.pResolutionObj X)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ homEquivLeft (LeftHomotopyClass.mk f) = toHoCat.map (homMk f)

Tactic:
simp [homEquivLeft]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) (bifibrantResolutionMap f)

Tactic:
rw [← weakEquivalence_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ weakEquivalences (HoCat C) (HoCat.adj.unit.app X)

Tactic:
rw [← weakEquivalence_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adj.unit.app X)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case mp
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
      c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
        d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩

Goal state after:
case mp.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i₁ i₂ : J.R
x₁ : d.right i₁
x₂ : d.right i₂
h : c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂

case mp.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: case hinj
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⟩
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
      (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) ⟨y, hy⟩

Tactic:
obtain rfl : x = y := by simpa using h

Goal state after:
case hinj
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
hy : x ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨x, hy⟩
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) ⟨x, hx⟩ =
      (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) ⟨x, hy⟩
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u''
inst✝ : Category.{v'', u''} J
⊢ (isomorphisms C).functorCategory J = isomorphisms (J ⥤ C)

Tactic:
by
  ext _ _ f
  simp only [functorCategory, isomorphisms.iff, NatTrans.isIso_iff_isIso_app]

Goal state after:
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
⊢ (X.spine (n + 1)
          ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)))).arrow
      k =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
spine_δ_arrow_gt sx _ hgt

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
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.succ =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (Y₂.snd.β U).hom) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
rw [f.comm]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ X₁.fst Y.fst U).hom ≫
        X₁.fst ◁ (Y.snd.β U).hom ≫ (α_ X₁.fst U Y.fst).inv ≫ (X₁.snd.β U).hom ▷ Y.fst ≫ (α_ U X₁.fst Y.fst).hom) ≫
      U ◁ f.f ▷ Y.fst

Tactic:
rw [f.comm]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ ((X₁.snd.β U).hom ≫ U ◁ f.f) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ X₁.fst Y.fst U).hom ≫
        X₁.fst ◁ (Y.snd.β U).hom ≫ (α_ X₁.fst U Y.fst).inv ≫ (X₁.snd.β U).hom ▷ Y.fst ≫ (α_ U X₁.fst Y.fst).hom) ≫
      U ◁ f.f ▷ Y.fst
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
y : V.HomotopyCategory
x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
h : (mk x).as.as = y.as.as
⊢ mk x = y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
h : (mk x).as.as = (mk y).as.as
⊢ mk x = mk y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W X : Truncated 2
inst✝ : Subsingleton (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
y : X.HomotopyCategory
x : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ mk x = y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
V W X : Truncated 2
inst✝ : Subsingleton (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
x y : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ mk x = mk y
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
⊢ r.degHom f ≤ r.deg X

Tactic:
by
  simpa using r.degHom_le (𝟙 X) f

Goal state after:
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
e : X ≅ Y
⊢ r.deg X = r.deg Y

Tactic:
by
  have {X Y : C} (e : X ≅ Y) : r.deg X ≤ r.deg Y := by
    rw [← r.degHom_id X, ← e.hom_inv_id]
    apply r.degHom_le
  exact le_antisymm (this e) (this e.symm)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.zero
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
j : Fin (0 + 1)
g : y✝ ⟶ mk (0 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) L → ∀ j ≤ m, IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j (a :: L))

Tactic:
| cons a L h_rec =>

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₁ m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hk : m₂ + (a :: L).length = m₁
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) hk))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j

Tactic:
| cons a L h_rec =>

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
          (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
          (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)).app
      y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
          (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
          (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)).app
      (mk y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
⊢ standardσ (simplicialInsert j (a :: L)) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
| cons a L h_rec =>

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)).app
      y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)).app
      (mk y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)).app
      y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)).app
      (mk y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      (mk y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
⊢ j ∈ a :: L

Tactic:
| cons a L h_rec =>

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      y

Tactic:
obtain ⟨y, rfl⟩ := y.mk_surjective

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      (mk y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

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

Tactic:
· rwa [Fin.predAbove_of_le_castSucc _ _ hk', Fin.castSucc_castPred]

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : ¬k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)

Goal state after:
case inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc