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

Goal state before:
pp: case neg
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }

Tactic:
exact G.extendProp _

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
inst✝ : Nonempty Y
⊢ (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Tactic:
inhabit Y
  refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩ <;> 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
⊢ weakEquivalences (CofibrantObject C) f ↔ weakEquivalences (CofibrantObject C) g

Tactic:
by
    simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
    obtain ⟨P, ⟨h⟩⟩ := h
    apply h.weakEquivalence_iff

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

Goal state before:
pp: case inr
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
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
obtain ⟨X', i, _, _, _⟩ : ∃ (X' : C) (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i ∧
        IsFibrant X' :=
      ⟨_, FibrantObject.HoCat.iResolutionObj X, inferInstance, inferInstance, inferInstance⟩
    have _ := isCofibrant_of_cofibration i
    have hX' := this X' inferInstance
    have := Localization.inverts L (weakEquivalences _) i
      (by rwa [← weakEquivalence_iff])
    rw [← Function.Bijective.of_comp_iff _
      (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence Y i)]
    convert! (Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'
    ext f
    obtain ⟨f, rfl⟩ := f.mk_surjective
    simp

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

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
this : WeakEquivalence (pushout.inl f i ≫ h.i)
⊢ i ≫ pushout.inr f i ≫ h.i ≫ sq'.lift = f

Tactic:
simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left

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₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) (bifibrantResolutionMap f)
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ sq.HasLift

Tactic:
exact ⟨⟨{ l := sq'.lift ≫ h.p ≫ pullback.fst p g
              fac_right := by
                rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right] }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

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
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
i : J.R
⊢ π ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)) i ≫
      (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt).hom =
    (c.map F).π i

Tactic:
by dsimp only [Multicofork.π]; simp

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

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

Tactic:
rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsLimit (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.mapCone (PullbackCone.mk (t i d) (l i d) ⋯))

Tactic:
by
    refine (isLimitMapConePullbackConeEquiv _ _).2
      (IsPullback.isLimit ?_)
    dsimp
    rw [Types.isPullback_iff]
    refine ⟨NatTrans.congr_app (w i d) _,
      fun x₁ x₂ ⟨_, h⟩ ↦ injective_of_mono ((l i d).app (op ⦋n⦌)) h,
      fun ⟨x, hx⟩ y h ↦ ?_⟩
    rw [Subtype.ext_iff] at h
    dsimp at h
    subst h
    obtain ⟨c, y, rfl⟩ := ιSigmaStdSimplex_jointly_surjective y
    refine ⟨c.ιSigmaBoundary.app _ ⟨y, ?_⟩, ?_, ?_⟩
    · rw [dsimp% congr($(c.ι_b_ι).app (op ⦋n⦌) y)] at hx
      rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]
    · rw [Subtype.ext_iff]
      exact congr($(c.ι_t_ι_eq_ι_l_b_ι).app _ ⟨y, _⟩)
    · exact congr($(c.ι_l).app _ ⟨y, _⟩)

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).vertex i = f.vertex i.castSucc

Tactic:
by
  simp only [SimplicialObject.δ, spine_vertex]
  rw [← Functor.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
    spineToSimplex_vertex]
  simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]
  rw [Fin.succAbove_of_castSucc_lt j i h]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X.obj

Tactic:
← eHomEquiv_id

Goal state after:
V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = (eHomEquiv V) (𝟙 X.obj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ex : Edge x₀ x₁
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ey : Edge y₀ y₁
⊢ homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) =
    homMk ((Edge.id x₀).tensor ey) ≫ homMk (ex.tensor (Edge.id y₁))

Tactic:
rw [homMk_comp_homMk ((Edge.CompStruct.idComp ex).tensor (Edge.CompStruct.compId ey)),
    homMk_comp_homMk ((Edge.CompStruct.compId ex).tensor (Edge.CompStruct.idComp ey))]

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS
  refine ⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS
  refine ⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩

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

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)

Tactic:
intro L

Goal state after:
case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
⊢ L ∈ upperBounds x✝ → sSup x✝ ≤ L
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: 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 : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ y ≤ f z

Tactic:
by simpa using hz.1

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : z.castSucc ∈ finset f y
⊢ z.castSucc ∈ finset f x

pp: case inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
hz : Fin.last (n + 1) ∈ finset f y
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
· simp only [castSucc_mem_finset_iff] at hz ⊢
      exact hxy.trans hz

Goal state after:
case inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
hz : Fin.last (n + 1) ∈ finset f y
⊢ Fin.last (n + 1) ∈ finset f x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
b : B.N
hb : b ∈ (P.ofIso e hA).II
d : ℕ
hd : (↑⟨b, hb⟩).dim = d
⊢ ⋯.index hd ≠ 0

Tactic:
obtain ⟨a, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective b

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
d : ℕ
a : A.N
hb : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb⟩).dim = d
⊢ ⋯.index hd ≠ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
b : B.N
hb : b ∈ (P.ofIso e hA).II
d : ℕ
hd : (↑⟨b, hb⟩).dim = d
⊢ ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
obtain ⟨a, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective b

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝¹ : P.IsProper
inst✝ : P.IsInner
d : ℕ
a : A.N
hb : (N.orderIsoOfIso e hA).symm a ∈ (P.ofIso e hA).II
hd : (↑⟨(N.orderIsoOfIso e hA).symm a, hb⟩).dim = d
⊢ ⋯.index hd ≠ Fin.last (d + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : AugmentedSimplexCategory
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (x ⊗ y)

Tactic:
ext
  · simpa [inl, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (𝟙 x) (WithInitial.starInitial.to y) (𝟙 x) (𝟙 y))
  · simpa [inr, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (WithInitial.starInitial.to x) (𝟙 y) (𝟙 x) (𝟙 y))

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
⊢ ∀ {n : ℕ} (x : ↑(X.nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
by
    intro n ⟨x, hx⟩
    rw [← nonDegenerate_iff_of_mono f] at hx
    have := mono' _ hx
    rw [← SSet.yonedaEquiv_symm_comp] at this
    exact mono_of_mono _ f

Goal state after:
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
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx⟩)

Tactic:
rw [PartialOrder.mem_nerve_nonDegenerate_iff_injective] at hx

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
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: case hinj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun X ↦ X) ((X ⋙ c.pt).obj i)),
    (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) y →
      ∃ k f, (ConcreteCategory.hom ((X ⋙ c.pt).map f)) x = (ConcreteCategory.hom ((X ⋙ c.pt).map f)) y

Tactic:
exact isColimitMapCocone.injective c hc κ hK cX hF

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
X : C
⊢ IsIso (i.app (op X))

Tactic:
refine hP₂ _ (fun G hG f ↦ ?_)

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
X : C
G : A
hG : P G
f : G ⟶ P₂.obj (op X)
⊢ ∃ a, (fun f ↦ f ≫ i.app (op X)) a = f
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h : (objEquiv (x.cast hd).simplex) i.castSucc = (k.castSucc, (x.cast hd).simplex.2 (min x hd))
⊢ False

Tactic:
Prod.ext_iff

Goal state after:
case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
h :
  ((objEquiv (x.cast hd).simplex) i.castSucc).1 = (k.castSucc, (x.cast hd).simplex.2 (min x hd)).1 ∧
    ((objEquiv (x.cast hd).simplex) i.castSucc).2 = (k.castSucc, (x.cast hd).simplex.2 (min x hd)).2
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ (min ⋯.δ ⋯).castSucc
⊢ (objEquiv (s.δ.cast ⋯).simplex) ((min s.δ ⋯).predAbove i) = (objEquiv (s.x.cast ⋯).simplex) i

Tactic:
change objEquiv (s.x.cast s.hd).simplex
      (s.index.castSucc.succAbove ((min s.δ rfl).predAbove i)) = _

Goal state after:
case neg
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ (min ⋯.δ ⋯).castSucc
⊢ (objEquiv (s.x.cast ⋯).simplex) (s.index.castSucc.succAbove ((min s.δ ⋯).predAbove i)) =
    (objEquiv (s.x.cast ⋯).simplex) i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

Tactic:
simp only [Arrow.mk_left]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

Tactic:
simp only [Arrow.mk_left]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)).1 =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ).1

Tactic:
simpa [stdSimplex.δ_objEquiv_symm_apply,
        SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}] using!
          ConcreteCategory.congr_hom (X.δ_comp_σ_of_le hij) x

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

Goal state before:
pp: X : SSet
⊢ ⨆ i, i.subcomplex = ⊤

Tactic:
by
    rw [Subcomplex.eq_top_iff_contains_nonDegenerate]
    intro n x hx
    simp only [Subfunctor.iSup_obj, Set.mem_iUnion]
    exact ⟨N.mk x hx, Subcomplex.mem_ofSimplex_obj _⟩

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.succ.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv fg.map))

Tactic:
← h.δ_succ_castSucc_map,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ j.castSucc.succ.rev ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ (toSSet.obj X).IsConnected

Tactic:
rw [SSet.isConnected_iff_nonempty_unique]

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ Nonempty (Unique (toSSet.obj X).π₀)