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

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X n).Factors (PInfty.f n)

Tactic:
by
  rcases n with _ | n
  · apply top_factors
  · rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
    intro i _
    apply kernelSubobject_factors
    exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ (N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Tactic:
by
  rw [N₁Γ₀_inv_app]
  apply id_comp

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom

Tactic:
let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
  have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj
    (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom
  dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
  exact h

Goal state after:
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
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ (((Γ₀.splitting K[X]).cofan Δ).inj A ≫
      (Γ₀.obj K[X]).map θ ≫ (Γ₀.splitting K[X]).desc Δ' fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) =
    ((Γ₀.splitting K[X]).cofan Δ).inj A ≫
      ((Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫
        ((toKaroubi (SimplicialObject C)).obj X).X.map θ

Tactic:
simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc,
              Splitting.ι_desc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)) ≫ PInfty.f (unop (A.pull θ).fst).len ≫ X.map (A.pull θ).e.op =
    PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ (image.ι (θ.unop ≫ A.e)).op ≫ (A.pull θ).e.op = A.e.op ≫ θ

Tactic:
simp only [← op_comp]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ

Tactic:
exact Quiver.Hom.unop_inj (A.fac_pull θ)

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : A.EqId
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
dsimp at h
          subst h
          rw [Splitting.cofan_inj_πSummand_eq_id]
          dsimp
          rw [comp_id, Splitting.cofan_inj_πSummand_eq_id_assoc]

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ ∀ (X_1 : (i : I) → ↑(π.obj (X i))),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1

pp: I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫ CategoryTheory.eqToHom ⋯

Tactic:
· intros; rfl

Goal state after:
I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1

Tactic:
· intros; rfl

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then (F.eval x.1).extend (2 * ↑x.2) else (G.eval x.1).extend (2 * ↑x.2 - 1)) =
    if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

Tactic:
split_ifs <;> exact Path.extend_apply _ _

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

Goal state before:
pp: case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ p₁.Homotopic p₂

Tactic:
← eq

Goal state after:
case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hloops : ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)
x y : Y
p₁ p₂ : Path x y
⊢ mk p₁ = mk p₂
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
by
  rw [weakEquivalence_iff]
  change weakEquivalences _ (CofibrantObject.homMk (bifibrantResolutionMap f).hom)
  rw [← weakEquivalence_iff, ← weakEquivalence_precomp_iff (iBifibrantResolutionObj X₁),
    bifibrantResolutionMap_fac, weakEquivalence_precomp_iff]
  infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i} = Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall] at h ⊢

Goal state after:
n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
⊢ ↑⟨a, ha⟩ ∈ Δ[n].degenerate i ↔ ⟨a, ha⟩ ∈ ⊤

Tactic:
simp only [Set.top_eq_univ, Set.mem_univ, iff_true]

Goal state after:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
⊢ a ∈ Δ[n].degenerate i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].op.preimage (stdSimplex.opIso ⦋n⦌).inv = Λ[n, i.rev]

Tactic:
ext ⟨⟨d⟩⟩ j
  simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_horn_iff_notMem_range, Set.mem_range, not_exists, ne_eq,
    exists_prop, stdSimplex.opObjEquiv_opObjEquiv_symm_apply]
  constructor
  · rintro ⟨k, h₁, h₂⟩
    exact ⟨k.rev, by simpa, fun l hl ↦ by grind [h₂ l.rev]⟩
  · rintro ⟨k, h₁, h₂⟩
    exact ⟨k.rev, by grind⟩

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
h : (hom φ) x₁ = (hom φ) y₁
⊢ ∃ j x₁' y₁', x₁ = (hom (c₁.ι.app j)) x₁' ∧ y₁ = (hom (c₁.ι.app j)) y₁'

Tactic:
obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
      obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁
      exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ ∀ (a b : X₁ ⊕ X₂), Rel f g a b → Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
rintro _ _ ⟨⟩

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel' f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) =
    Quot.mk (Rel' f g) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
φ : Δ[n + 1] ⟶ Z
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t
⊢ ∀ (j : Fin (n + 2)) (hj : j ≠ i), horn.ι i j hj ≫ Λ[n + 1, i].ι ≫ φ = horn.ι i j hj ≫ t

Tactic:
simpa using hφ

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂

Tactic:
exact (horn.isColimit 1).fac _ (.right ⟨2, by simp⟩)

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

Goal state before:
pp: case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).succ

pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ

Tactic:
· exact p.arrow_tgt 0

Goal state after:
case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
let triangle : (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ :=
        horn.primitiveTriangle i h₀ hₙ k (by grind)

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p✝ : X.Path n
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (p.arrow 0) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
by
      rw [p.arrow_tgt 0]
      exact Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

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

Tactic:
cases g

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }
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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g'

Tactic:
by
  dsimp [eHomWhiskerLeft]
  rw [assoc, assoc, eHomEquiv_comp, MonoidalCategory.whiskerLeft_comp_assoc,
    MonoidalCategory.whiskerLeft_comp_assoc, ← e_assoc, tensorHom_def,
    MonoidalCategory.whiskerRight_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
    MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
    whiskerLeft_rightUnitor_assoc, whiskerLeft_rightUnitor_inv_assoc,
    triangle_assoc_comp_left_inv_assoc, MonoidalCategory.whiskerRight_id_assoc,
    Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,
    associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₂
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ ↑a = standardσ (t ++ L₁) ⋯ ≫ σ ↑a

Tactic:
obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind

Goal state after:
case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + t.length + 1 + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₃ + t.length + 1
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ ↑a = standardσ (t ++ L₁) ⋯ ≫ σ ↑a
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inl
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : ∃ i, ∃ (_ : i ∈ x✝), a✝ ∈ i.faces
⊢ a✝ ∈ (fun K ↦ K.faces) L

Tactic:
obtain ⟨K, hK, htK⟩ := ht

Goal state after:
case right.inl
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
K : AbstractSimplicialComplex ι
hK : K ∈ x✝
htK : a✝ ∈ K.faces
⊢ a✝ ∈ (fun K ↦ K.faces) L
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
K : AbstractSimplicialComplex ι
x✝ : Finset ι
ht : x✝ ∈ (fun K ↦ K.faces) ⊥
⊢ x✝ ∈ (fun K ↦ K.faces) K

Tactic:
by
    obtain ⟨v, hv⟩ := ht
    exact hv ▸ K.singleton_mem v

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
j : StructuredArrow (op ⦋n⦌) (inclusion 2).op
⊢ (↾fun x ↦ lift sx s x) ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j

Tactic:
by
    ext x
    obtain ⟨⟨i, hi⟩, ⟨f : _ ⟶ _⟩, rfl⟩ := j.mk_surjective
    obtain ⟨i, rfl⟩ : ∃ j, ⦋j⦌ = i := ⟨_, i.mk_len⟩
    dsimp at hi ⊢
    apply sx.spineInjective
    ext k
    · dsimp only [spineEquiv, Equiv.coe_fn_mk]
      rw [dsimp% show op f = f.op from rfl]
      rw [spine_map_vertex, spine_spineToSimplex_apply, spine_vertex]
      let α : strArrowMk₂ f hi ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ (f.toOrderHom k)) :=
        StructuredArrow.homMk ((Hom.tr (⦋0⦌.const _ (by exact k))).op) (by simp; rfl)
      exact ConcreteCategory.congr_hom (s.w α).symm x
    · dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
      rw [← Functor.map_comp_apply]
      let α : strArrowMk₂ f ⟶ strArrowMk₂ (mkOfSucc k ≫ f) :=
        StructuredArrow.homMk (Hom.tr (mkOfSucc k)).op (by simp)
      exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans
        (ConcreteCategory.congr_hom (s.w α).symm x)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → i.as ≤ l

Tactic:
rintro (h | h)

Goal state after:
case inl
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ i.as ≤ l

case inr
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ g.I
⊢ i.as ≤ l
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → l ≤ k.as

Tactic:
rintro (h | h)

Goal state after:
case inl
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ f.I
⊢ l ≤ k.as

case inr
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
h : l ∈ g.I
⊢ l ≤ k.as
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
⊢ x ≤ y → map' f x ≤ map' f y

Tactic:
hxy

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
⊢ map' f x ≤ map' f y
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ x ∈ (Δ[p] ⊗ Δ[q]).degenerate n ↔ x ∈ ⊤

Tactic:
simp only [Set.top_eq_univ, Set.mem_univ, iff_true]

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ x ∈ (Δ[p] ⊗ Δ[q]).degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
⊢ ∀ (k : SimplexCategoryᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom ((yonedaEquiv.symm x).app k))

Tactic:
intro ⟨⟨k⟩⟩ i j hij

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j
⊢ i = j
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Subcomplex.range f = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
range_eq_iSup_of_isColimit (coproductIsCoproduct X) f

Goal state after:
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
hxy : c.s = c'.s
⊢ False

Tactic:
hxy

Goal state after:
case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c'.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
hxy : c.s = c'.s
⊢ 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 : ι
s : (range (f.m j)).N
⊢ ∃ c, s = Cell.type₁ f c ∨ s = Cell.type₂ f c

Tactic:
by
  obtain ⟨d, s, hs, hs', rfl⟩ := s.mk_surjective
  obtain ⟨x, s, rfl⟩ := f.ιSigmaStdSimplex_jointly_surjective s
  replace hs' : s ∉ (horn _ x.index).obj _ :=
    fun h ↦ hs' ⟨x.ιSigmaHorn.app _ ⟨_, h⟩, by rw [← NatTrans.comp_app_apply]; simp⟩
  obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective s
  rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs
  obtain hd | rfl := (SimplexCategory.le_of_mono g).lt_or_eq
  · rw [Nat.lt_succ_iff] at hd
    obtain hd | rfl := hd.lt_or_eq
    · exact (hs' (by simp [horn_obj_eq_univ x.index d (by lia)])).elim
    · obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono g
      obtain rfl := (objEquiv_symm_δ_notMem_horn_iff _ _).mp hs'
      exact ⟨x, Or.inr rfl⟩
  · obtain rfl := SimplexCategory.eq_id_of_mono g
    exact ⟨x, Or.inl rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts

Tactic:
have := P.isClosedUnderColimitsOfShape_colimitsCardinalClosure κ
    WalkingParallelPair (HasCardinalLT.of_le (by
      simp only [hasCardinalLT_aleph0_iff]
      infer_instance)
    (Cardinal.IsRegular.aleph0_le Fact.out))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts