mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.curry t) 1 = x₁

Tactic:
by simp

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✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (0, x) =
      f x

Tactic:
by simp

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✝ : IndiscreteTopology Y
f g : C(X, Y)
⊢ ∀ (x : X),
    {
            toFun := fun x ↦
              match x with
              | (t, a) => if t = 0 then f a else g a,
            continuous_toFun := ⋯ }.toFun
        (1, x) =
      g x

Tactic:
by simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x : ↑I × ↑I
⊢ ↑(σ x.1) + ↑x.1 = 1

Tactic:
by simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (0, x) = (p.map ⋯).toContinuousMap x

Tactic:
by simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
⊢ ∀ (x : ↑I), (⇑f ∘ ⇑F) (1, x) = (q.map ⋯).toContinuousMap x

Tactic:
by simp

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ ⟦p₁⟧ = (Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧)).trans ⟦p₂⟧

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 0, ⋯⟩ = x

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : { x // x ∈ s }
p : Path ↑x ↑x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ⟨p 1, ⋯⟩ = x

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (0, x_1), ⋯⟩ = p.toContinuousMap x_1

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (x_1 : ↑unitInterval), ⟨F (1, x_1), ⋯⟩ = (Path.refl x).toContinuousMap x_1

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
F : (p.map ⋯).Homotopy (Path.refl ↑x)
hF : ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
⊢ ∀ (t x_1 : ↑unitInterval),
    x_1 ∈ {0, 1} → { toFun := fun x_2 ↦ ⟨F (t, x_2), ⋯⟩, continuous_toFun := ⋯ } x_1 = p.toContinuousMap x_1

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
P : PathObject Y.obj
h : P.RightHomotopy f.hom g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
⊢ initial.to (resolutionObj Y) ≫ pResolutionObj Y = initial.to (resolutionObj X) ≫ pResolutionObj X ≫ f

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ (p.symm.trans (Path.refl x₀)).symm = (Path.refl x₀).trans p

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.symm.symm = p

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
⊢ IsIso (Functor.whiskerRight adj.unit W.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
⊢ ∀ (X : C₁), IsIso ((Functor.whiskerRight adj.unit W.Q).app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
⊢ G.IsLocalization W

Tactic:
have : IsIso (Functor.whiskerRight adj.unit W.Q) := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro X
    exact Localization.inverts W.Q W _ (hW' X)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
this : IsIso (Functor.whiskerRight adj.unit W.Q)
⊢ G.IsLocalization W
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))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

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), IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).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)
⊢ IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

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), IsIso ((HoCat.resolutionCompToLocalizationNatTrans L).app X)
Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
⊢ initial.to ((localizerMorphism C).functor.obj R₀.X₁) ≫ R₀.w =
    initial.to ((localizerMorphism C).functor.obj R.X₁) ≫ R.w

Tactic:
by simp

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
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (LeftHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩
  rw [← LeftHomotopyClass.mk_eq_mk_iff]
  exact (bijective_leftHomotopyClassToHom L X Y).1 (by simpa)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
⊢ (weakEquivalences (BifibrantObject C)).IsInvertedBy toHoCat

Tactic:
rw [inverts_iff_factors]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
⊢ ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g
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₂
⊢ ι.map (f ≫ X₂.iBifibrantResolutionObj) ≫
      terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)) =
    X₁.iBifibrantResolutionObj.hom ≫ terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (𝟙 X))) =
    toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (𝟙 (BifibrantObject.toHoCat.obj X.bifibrantResolutionObj))

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : CofibrantObject C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (f ≫ g))) =
    toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (BifibrantObject.toHoCat.map (bifibrantResolutionMap f) ≫
          BifibrantObject.toHoCat.map (bifibrantResolutionMap g))

Tactic:
by simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
f : C(X, Y)
⊢ ∀ {X_1 Y_1 Z : FundamentalGroupoid X} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    Path.Homotopic.Quotient.map (f_1 ≫ g) f = Path.Homotopic.Quotient.map f_1 f ≫ Path.Homotopic.Quotient.map g f

Tactic:
rintro _ _ _ ⟨p⟩ ⟨q⟩; exact congr_arg Quotient.mk'' (p.map_trans q f.continuous)

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

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
r : J.R
z : d.multispan.obj (WalkingMultispan.right r)
⊢ d.multispan.ιColimitType (WalkingMultispan.right r) z = d.multispan.ιColimitType (WalkingMultispan.right r) z

Tactic:
by simp

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

Goal state before:
pp: 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 : J.R
z : d.right i
⊢ c.ι (WalkingMultispan.right i) z =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ stdSimplex.objMk OrderHom.id ∈ ⊤.obj (op ⦋n⦌)

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
d : ℕ
hd✝ : n ≤ d
hd : n < d
hS : Finset.univ.card = d + 1
hx : stdSimplex.face Finset.univ ≤ A
⊢ stdSimplex.face {i}ᶜ ≤ stdSimplex.face Finset.univ

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ A ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: case refine_2
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
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx : x ∈ c.multicofork.pt
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx⟩

Tactic:
· simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq,
      Set.iSup_eq_iUnion, Set.mem_iUnion] at hx
    obtain ⟨i, hi⟩ := hx
    exact ⟨i, ⟨x, hi⟩, rfl⟩

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

Goal state before:
pp: n : ℕ
i k : Fin (n + 3)
m : SimplexCategoryᵒᵖ
⊢ stdSimplex.obj₀Equiv.symm k ∈ Λ[n + 2, i].obj (op ⦋0⦌)

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂

Tactic:
simp only [horn_eq_iSup, iSup_le_iff,
    Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
    ← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ ∀ (a : Fin (n + 1 + 1)), ¬a = i → yonedaEquiv (stdSimplex.δ a) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
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
    apply Rel'.refl

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ sq.lift ≫ p = b

Tactic:
by simp

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ σ₀ ≫ terminal.from S = Λ[n + 1, i].ι ≫ terminal.from Δ[n + 1]

Tactic:
by simp

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
⊢ σ₀ = Λ[n + 1, i].ι ≫ sq'.lift

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst✝ : X.KanComplex
hf : horn.IsCompatible f
⊢ ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ terminal.from X = stdSimplex.δ j ≫ terminal.from Δ[n + 1]

Tactic:
by simp

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
by simp

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst✝ : Mono f
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
by simp

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

Goal state before:
pp: S X : SSet
t : Limits.IsTerminal X
h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (t.from S)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h0 : 0 < i
hn : i < Fin.last (n + 2)
this : HasLiftingProperty Λ[n + 2, i].ι (t.from S) := h h0 hn
⊢ σ₀ = Λ[n + 2, i].ι ≫ ⋯.lift

Tactic:
by simp

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: X : SSet
⊢ ⨆ n, X.skeleton n ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 ≠ 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 ≠ 2

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ n ≤ n + 1

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
⊢ n < n + 1

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ⨆ n, (skeletonOfMono i) n ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)

Tactic:
refine ⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₄ : (fun X ↦ X) X₄
⊢ ∃ a, (ConcreteCategory.hom φ) a = x₄
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this✝ : Mono (φ ≫ k)
this : IsIso φ
⊢ t ≫ (Iso.refl X₂).hom = (Iso.refl X₁).hom ≫ t

Tactic:
by simp

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this✝ : Mono (φ ≫ k)
this : IsIso φ
⊢ l ≫ (Iso.refl X₃).hom = (Iso.refl X₁).hom ≫ l

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ n ≤ n + 1

Tactic:
by simp

Goal state after: