mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ WeakEquivalence (pushout.inl f i ≫ h.i)

Tactic:
rw [weakEquivalence_iff] at h₁ ⊢

Goal state after:
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₁ : weakEquivalences C ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ weakEquivalences C (pushout.inl f i ≫ h.i)
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)
⊢ WeakEquivalence (h.p ≫ pullback.snd p g)

Tactic:
rw [weakEquivalence_iff] at h₁ ⊢

Goal state after:
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₁ : weakEquivalences C (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ weakEquivalences C (h.p ≫ pullback.snd p g)
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Mono (equalizer.ι f g)

Tactic:
dsimp [equalizer.ι]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Mono (homOfLe ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
i : ↑{i✝}ᶜ
⊢ {↑i}ᶜ.card ≤ n

Tactic:
by simp [Finset.card_compl]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ {i}ᶜ.card ≤ n

Tactic:
by simp [Finset.card_compl]

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
i : Fin (0 + 1)
⊢ J Λ[0, i].ι

Tactic:
exact (NeZero.ne 0 rfl).elim

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

Goal state before:
pp: X : SSet
n : ℕ
| X.skeleton (n + 1)

Tactic:
dsimp [skeleton]

Goal state after:
X : SSet
n : ℕ
| ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f = g

Tactic:
by
  ext i
  · fin_cases i; exact h
  · fin_cases i

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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (ρ_ (X ⟶[V] Y)).hom ≫
        (ρ_ (X ⟶[V] Y)).inv ≫
          (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).inv ≫
            (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).hom ≫
              (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
                (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
                  (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
                    (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                      (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫
                        (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
Iso.hom_inv_id_assoc,

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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).inv ≫
        (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
              (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
                (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                  (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
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''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
            (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).inv ≫
              ((X ⟶[V] Y) ⊗ Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
Iso.hom_inv_id_assoc,

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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          ((X ⟶[V] Y) ⊗ Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
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 X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        ((λ_ (X' ⟶[V] Y)).inv ▷ Y ⟶[V] Y') ≫
          (α_ (𝟙_ V) (X' ⟶[V] Y) (Y ⟶[V] Y')).hom ≫
            (α_ (𝟙_ V) (X' ⟶[V] Y) (Y ⟶[V] Y')).inv ≫
              (((eHomEquiv V) f ▷ X' ⟶[V] Y) ▷ Y ⟶[V] Y') ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
Iso.hom_inv_id_assoc,

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
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        ((λ_ (X' ⟶[V] Y)).inv ▷ Y ⟶[V] Y') ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] Y) ▷ Y ⟶[V] Y') ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL g f

Tactic:
exact Quasicategory₂.fill31 hfg (idComp (id y)) (compId f)

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

Goal state before:
pp: case of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
⊢ P (σ i)

Tactic:
· simpa using! (comp_σ (𝟙 _) i id)

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

Goal state before:
pp: case of_comp
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝¹ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf : generators f
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (f ≫ g)

Tactic:
rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩

Goal state after:
case of_comp.inl
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
g : mk (n✝ + 1) ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (δ i ≫ g)

case of_comp.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
g : mk n✝ ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (σ i ≫ g)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono m

Tactic:
induction hm with

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

Goal state before:
pp: case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f

Tactic:
| _ a
   => 

Goal state after:
case mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := b, property := hb }
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : { len := a }.len ≤ d
b : ℕ
hb : { len := b }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
⊢ W f

Tactic:
| _ b
   => 

Goal state after:
case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : { len := a }.len ≤ d
b : ℕ
hb : { len := b }.len ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case neg
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

pp: case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
· obtain _ | b := b
      · exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim
      · obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁
        replace hf' : f = Hom.tr g' ≫ Hom.tr (SimplexCategory.δ i) :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)

Goal state after:
case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x = y

Tactic:
apply Path.ext

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x.I = y.I
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x.castSucc ≤ ({ toFun := i.predAbove, monotone' := ⋯ } x.succ).castSucc ∧
    ∀ i_1 < x.succ, ({ toFun := i.predAbove, monotone' := ⋯ } i_1).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i))

Tactic:
e₄

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this✝ : x₁.dim < d₁
this : x₂.dim < d₂
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n

Tactic:
have := (Δ[x₁.dim] ⊗ Δ[x₂.dim]).hasDimensionLT_of_le (x₁.dim + x₂.dim + 1) n

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this✝¹ : x₁.dim < d₁
this✝ : x₂.dim < d₂
this : (Δ[x₁.dim] ⊗ Δ[x₂.dim]).HasDimensionLT n
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : ExtremalEpi f
A : Subobject Y
hA : A.Factors f
⊢ A = ⊤

Tactic:
rw [← Subobject.isIso_arrow_iff_eq_top]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : ExtremalEpi f
A : Subobject Y
hA : A.Factors f
⊢ IsIso A.arrow
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
⊢ ExtremalEpi f ↔ StrongEpi f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩,
    fun _ ↦ inferInstance⟩
  have := ExtremalEpi.isIso f (pullback.lift _ _ sq.w)
    (pullback.snd _ _) (by simp)
  exact
    { l := inv (pullback.snd i b) ≫ pullback.fst _ _
      fac_left := by
        rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]
        congr 1
        rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]
      fac_right := by simp [pullback.condition] }

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌)))) ∈
    (f.sigmaStdSimplex j).nonDegenerate (c.dim + 1)

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
      Equiv.apply_symm_apply]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ Mono (𝟙 (unop (op ⦋c.dim + 1⦌)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) ∈
    (f.sigmaStdSimplex j).nonDegenerate c.dim

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
      Equiv.apply_symm_apply]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ Mono (SimplexCategory.δ c.index)
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

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

Tactic:
rw [← Subobject.isIso_arrow_iff_eq_top]

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