mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ IsColimit
    (((evaluation SimplexCategoryᵒᵖ (Type u)).obj n).mapCocone
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))

Tactic:
have h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n)
        (fun i j ↦ (V i j).obj n) :=
      { eq_inf := by simp [h.eq_inf]
        iSup_eq := by simp [← h.iSup_eq] }
    exact (Multicofork.isColimitMapEquiv _ _).2
      (Types.isColimitOfMulticoequalizerDiagram h')

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

Goal state before:
pp: case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∉ Δ[n].nonDegenerate n

Tactic:
nonDegenerate_top_dim

Goal state after:
case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∉ {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
⊢ False

Tactic:
have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
⊢ ∀ (a b : X₁ ⊕ X₂),
    Rel f g a b →
      (match a with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂) =
        match b with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂

Tactic:
by
    rintro _ _ ⟨t⟩
    exact ConcreteCategory.congr_hom s.condition t

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

Goal state before:
pp: case none
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj none
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom (h.cocone.ι.app none)) x) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom (h.cocone.ι.app none)) x

Tactic:
exact Or.inl ⟨t x, by simp; rfl⟩

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

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

Tactic:
fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)

Goal state after:
case commf
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 1 ⋯).hom

case commg
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

case comminl
⊢ (stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₁ ≫ (Iso.refl Λ[2, 0].toSSet).hom

case comminr
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 0].toSSet).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂

Tactic:
fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)

Goal state after:
case commf
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

case commg
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 1 2 ⋯).hom

case comminl
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom

case comminr
⊢ (stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₁₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ f.vertex j = g.vertex j

pp: case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ f.vertex j = g.vertex j

Tactic:
· rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]

Goal state after:
case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ f.vertex j = g.vertex j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (X.spine a hₐ ((ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i = (X.spine m hₘ Δ).vertex ((Hom.toOrderHom φ.hom) i)

Tactic:
dsimp only [spine_vertex]
  rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp',
    SimplexCategory.const_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (𝟙 (homEquiv (𝟙 a))) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
homEquiv_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
by simp [id_hComp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (Hom.base η) (𝟙 (homEquiv (𝟙 b))) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
homEquiv_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (Hom.base η) (𝟙 (𝟙 b.toBase)) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g), hComp (𝟙 (𝟙 a)) η = (eqToIso ⋯).hom ≫ η ≫ (eqToIso ⋯).inv

Tactic:
by simp [id_hComp]

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 X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ ((ρ_ (X' ⟶[V] Y)).inv ≫ (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X' Y Y') ≫
      (λ_ (X' ⟶[V] Y')).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y') ≫ eComp V X X' 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:
rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc,
    whisker_exchange_assoc, ← e_assoc, leftUnitor_tensor_inv_assoc,
    associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc,
    ← comp_whiskerRight_assoc, whisker_exchange_assoc,
    MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    𝟙 (ForgetEnrichment.of V (ForgetEnrichment.to W X))

Tactic:
rw [← ForgetEnrichment.homOf_eId]

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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : ForgetEnrichment W (TransportEnrichment F D)
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (ForgetEnrichment.homTo W (𝟙 X))) =
    ForgetEnrichment.homOf V (eId V (ForgetEnrichment.to W X))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map (⦋1⦌.const ⦋0⦌ 0).op))
      ((ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x)) =
    (ConcreteCategory.hom (X.map α.right.unop.hom.op))
      ((ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1))) x)

Tactic:
refine congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_

Goal state after:
case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1))) x
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₁ f
h : r.deg X = r.deg Y
⊢ MorphismProperty.identities C f

Tactic:
by_contra

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₁ f
h : r.deg X = r.deg Y
this : ¬MorphismProperty.identities C f
⊢ False
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₂ f
h : r.deg X = r.deg Y
⊢ MorphismProperty.identities C f

Tactic:
by_contra

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : W₂ f
h : r.deg X = r.deg Y
this : ¬MorphismProperty.identities C f
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case zero
i : Fin (0 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (0 + 1)
hf : P_δ f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of j f hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · simp at hf'

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

Goal state before:
pp: case comp_σ.id
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ ∃ z e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩

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

Goal state before:
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)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
← epi_iff_surjective

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₁ : Epi f.hom
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
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₁ : Epi f.hom
h₂ : Mono f.hom
⊢ W f

Tactic:
obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)

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 hb : a ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := a }, property := hb }
h : a + a = c + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

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

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

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsUpperSet s
a : { x // P x }
ma : a ∈ s
b : α
x : ↑a ≤ b
y : P b
⊢ b ∈ Subtype.val '' s

Tactic:
by simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]

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

Goal state before:
pp: case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
exact Finset.singleton_nonempty _

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

Goal state before:
pp: case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
exact Finset.singleton_nonempty _

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

Goal state before:
pp: case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
exact Finset.singleton_nonempty _

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

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

Tactic:
map'_last

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 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 ι
⊢ Monotone f.filtration

Tactic:
by
  intro i₁ i₂ h
  conv_lhs => rw [filtration_def]
  simp only [sup_le_iff, iSup_le_iff, le_filtration, true_and]
  intro j hj c
  exact f.subcomplex_le_filtration c (lt_of_lt_of_le hj h)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ Y
h✝ : ExtremalEpi p
hi : ∀ (j : ι), ∃ a, (fun f ↦ f ≫ i) a = c.inj j ≫ p
⊢ IsIso i

Tactic:
choose φ hφ using hi

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ Y
h✝ : ExtremalEpi p
φ : (j : ι) → s j ⟶ X
hφ : ∀ (j : ι), (fun f ↦ f ≫ i) (φ j) = c.inj j ≫ p
⊢ IsIso i
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
J : Type u'
inst✝ : Category.{v', u'} J
hJ : HasCardinalLT (Arrow J) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
obtain ⟨S, ⟨e⟩⟩ := SmallCategoryCardinalLT.exists_equivalence κ J hJ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
J : Type u'
inst✝ : Category.{v', u'} J
hJ : HasCardinalLT (Arrow J) κ
S : SmallCategoryCardinalLT κ
e : SmallCategoryCardinalLT.categoryFamily κ S ≌ J
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J
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
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ ofSimplex
      ((ConcreteCategory.hom ((f.filtration (Order.succ j)).toSSet.map g₁.op))
        ((ConcreteCategory.hom ((f.b j).app (op ⦋s₁.dim⦌))) s₁.simplex)) =
    ofSimplex
      ((ConcreteCategory.hom ((f.filtration (Order.succ j)).toSSet.map g₂.op))
        ((ConcreteCategory.hom ((f.b j).app (op ⦋s₂.dim⦌))) s₂.simplex))

Tactic:
simp [← dsimp% (f.b j).naturality_apply, hg₁, hg₂, dsimp% h]

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

Goal state before:
pp: case inl.inl
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ

Tactic:
φ_of_lt _ _ _ (by grind)

Goal state after:
case inl.inl
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < (objEquiv (x.cast hd).simplex) (i.castSucc.succ.castPred ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
this : innerAnodyneExtensions sq₁₂.ι
⊢ innerFibrations p

Tactic:
by rwa [← innerFibration_iff]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (hl.δ.dim + 1)
ht : IsIndex hl.δ ⋯ t
⊢ False

Tactic:
dsimp at t ht

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
t : Fin (d + 1)
ht : IsIndex hl.δ ⋯ t
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
hst : s.x = ⋯.δ
this : IsType₂ s.x
⊢ False

Tactic:
exact this _ _ _ s.isIndex

Goal state after: