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✝⁶ : (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₂ : fibrations C (h.p ≫ pullback.snd p g)
⊢ sq.HasLift

Tactic:
rw [← fibration_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₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ m = hc.desc (isPushout.multicofork h h' s)

Tactic:
apply Multicofork.IsColimit.hom_ext hc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ ∀ (a : J.R), c.π a ≫ m = c.π a ≫ hc.desc (isPushout.multicofork h h' s)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].toSSet.HasDimensionLT n

Tactic:
by
  rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]
  intro i
  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

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

Goal state before:
pp: case mp
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
⊢ ∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1

Tactic:
exact ⟨k.rev, by simpa, fun l hl ↦ by grind [h₂ l.rev]⟩

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

Goal state before:
pp: case refine_1
n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
exact ⟨fun h => (equivPushout' f g).symm.injective h,
    fun h => (equivPushout' f g).injective h⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η ≍ η

Tactic:
rw [id_eq, ← Functor.map_id]
  exact congr_arg_heq (·.toFunctor.map η) (e_id_comp (V := Cat) a b)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β Y.fst).hom ▷ U ≫ ((Y ⊗ X).snd.β U).hom = ((X ⊗ Y).snd.β U).hom ≫ U ◁ (X.snd.β Y.fst).hom

Tactic:
by
      dsimp
      simp only [Category.assoc]
      rw [← IsIso.inv_comp_eq, IsIso.Iso.inv_hom, ← HalfBraiding.monoidal_assoc,
        ← HalfBraiding.naturality_assoc, HalfBraiding.monoidal]
      simp

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 : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    ForgetEnrichment.homOf W (eId W X)

Tactic:
TransportEnrichment.eId_eq,

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 : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V X))
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk.cons
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y b✝ c✝ : V
a✝ : Quiver.Path x b✝
f : b✝ ⟶ c✝
h : motive ((quotientFunctor V).map a✝)
⊢ motive ((quotientFunctor V).map (a✝.cons f))

Tactic:
simpa using! comp_homMk _ f h

Goal state after:
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, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x

Tactic:
let α : (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) ⟶
        (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) :=
            StructuredArrow.homMk ((Hom.tr (⦋1⦌.const ⦋0⦌ 0)).op) (by simp; rfl)

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 (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
X : C₃
Y : C₂
x✝¹ x✝ : C₁
g : x✝¹ ⟶ x✝
⊢ ((X✝.flip₁₃.obj X).obj Y).map g ≫ ((f.app x✝).app Y).app X =
    ((f.app x✝¹).app Y).app X ≫ ((Y✝.flip₁₃.obj X).obj Y).map g

Tactic:
by
          simp [← NatTrans.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
X : C₁
Y : C₃
x✝¹ x✝ : C₂
g : x✝¹ ⟶ x✝
⊢ ((X✝.flip₂₃.obj X).obj Y).map g ≫ ((f.app X).app x✝).app Y =
    ((f.app X).app x✝¹).app Y ≫ ((Y✝.flip₂₃.obj X).obj Y).map g

Tactic:
by
          simp [← NatTrans.comp_app]

Goal state after:
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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
Zf : C
f₁ : X ⟶ Zf
f₂ : Zf ⟶ Z
hf₁ : W₁ f₁
hf₂ : W₂ f₂
fac_f : f₁ ≫ f₂ = f
eq_f : r.degHom f = r.deg Zf
Zg : C
g₁ : Z ⟶ Zg
g₂ : Zg ⟶ Y
hg₁ : W₁ g₁
hg₂ : W₂ g₂
fac_g : g₁ ≫ g₂ = g
eq_g : r.degHom g = r.deg Zg
Zh : C
h₁ : Zf ⟶ Zh
h₂ : Zh ⟶ Zg
hh₁ : W₁ h₁
hh₂ : W₂ h₂
fac_h : h₁ ≫ h₂ = f₂ ≫ g₁
eq_h : r.degHom (f₂ ≫ g₁) = r.deg Zh
factfg : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Zh, i := f₁ ≫ h₁, p := h₂ ≫ g₂, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.degHom (f ≫ g) ≤ r.deg Z

Tactic:
rw [r.degHom_eq factfg]

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 Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
Zf : C
f₁ : X ⟶ Zf
f₂ : Zf ⟶ Z
hf₁ : W₁ f₁
hf₂ : W₂ f₂
fac_f : f₁ ≫ f₂ = f
eq_f : r.degHom f = r.deg Zf
Zg : C
g₁ : Z ⟶ Zg
g₂ : Zg ⟶ Y
hg₁ : W₁ g₁
hg₂ : W₂ g₂
fac_g : g₁ ≫ g₂ = g
eq_g : r.degHom g = r.deg Zg
Zh : C
h₁ : Zf ⟶ Zh
h₂ : Zh ⟶ Zg
hh₁ : W₁ h₁
hh₂ : W₂ h₂
fac_h : h₁ ≫ h₂ = f₂ ≫ g₁
eq_h : r.degHom (f₂ ≫ g₁) = r.deg Zh
factfg : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Zh, i := f₁ ≫ h₁, p := h₂ ≫ g₂, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.deg factfg.Z ≤ r.deg Z
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case comp_of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
m : ℕ
k : Fin (m + 1)
g : x✝ ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h_rec :
  ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk (m + 1)) (h₂ : x✝ = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ g = standardσ L ⋯
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : x✝ = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯

Tactic:
obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec

Goal state after:
case comp_of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
m₁ b₁ : ℕ
h₁' : mk m₁ = mk (m + 1)
g : mk (m₁ + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h' : L₁.length = b₁
hL₁ : IsAdmissible m₁ L₁
e₁ : g = standardσ L₁ ⋯
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m₁ + b₁) = mk (m_1 + b)) (h : L.length = b),
      IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))

Tactic:
inverse_map_mkHom_homMk_id,

Goal state after:
X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) =
    (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) (homMk (e.tensor (Edge.id z))))
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: X✝ Y✝ : SemiSimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toSimplexCategory.map a₁✝ = toSimplexCategory.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext : 2

Goal state after:
X✝ Y✝ : SemiSimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toSimplexCategory.map a₁✝ = toSimplexCategory.map a₂✝
x✝ : Fin (X✝.len + 1)
⊢ (homEquiv a₁✝) x✝ = (homEquiv a₂✝) x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, (f i).castSucc < x

Tactic:
intro h' i hi
    by_contra!
    exact hi.not_ge (by simpa using h' i.castSucc (by simpa))

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : WithInitial.of x ⊗ WithInitial.of y ⟶ WithInitial.of z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
⊢ f = g

Tactic:
change (tensorObjOf x y) ⟶ z at f g

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ (ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z ∈
      (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))).nonDegenerate n ↔
    StrictMono ⇑(objEquiv z)

Tactic:
PartialOrder.mem_nerve_nonDegenerate_iff_strictMono

Goal state after:
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ StrictMono ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj ↔ StrictMono ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ Subcomplex.range φ = ⨆ j, Subcomplex.range (c.ι.app j ≫ φ)

Tactic:
by
  conv_lhs => rw [← Category.id_comp φ]
  simp_rw [Subcomplex.range_comp, Subcomplex.range_eq_top, ← iSup_range_eq_top_of_isColimit hc,
    Subcomplex.image_iSup]

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

Goal state before:
pp: 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)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'

Tactic:
obtain ⟨j₁, α, hα⟩ : ∃ (j₁ : J) (α : j₀ ⟶ j₁), ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (F.obj k').map (X.map α) ((F.map φ).app _ (z k)) =
        (F.obj k').map (X.map α) (z k') := by
    have H {k k' : K} (φ : k ⟶ k') :=
      (Types.FilteredColimit.isColimit_eq_iff' (ht := hF k')
        (x := (F.map φ).app _ (z k)) (y := z k')).1 (by
          dsimp at hz ⊢
          simpa only [← NatTrans.naturality_apply, ← hz] using! y.2 φ)
    let j {k k' : K} (φ : k ⟶ k') : J := (H φ).choose
    let g {k k' : K} (φ : k ⟶ k') : j₀ ⟶ j φ := (H φ).choose_spec.choose
    have hg {k k' : K} (φ : k ⟶ k') :
        (F.obj k').map (X.map (g φ)) ((F.map φ).app _ (z k)) =
          (F.obj k').map (X.map (g φ)) (z k') := (H φ).choose_spec.choose_spec
    obtain ⟨j₁, α, β, hα⟩ : ∃ (j₁ : J) (α : j₀ ⟶ j₁)
        (β : ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), j φ ⟶ j₁),
        ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ := by
      let j'' (f : Arrow K) : J := j f.hom
      let ψ (f : Arrow K) : j₀ ⟶ IsCardinalFiltered.max j'' hK :=
        g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
      refine ⟨IsCardinalFiltered.coeq ψ hK, IsCardinalFiltered.toCoeq ψ hK,
        fun k k' φ ↦ IsCardinalFiltered.toMax j'' hK φ ≫ IsCardinalFiltered.coeqHom ψ hK,
        fun k k' φ ↦ ?_⟩
      simpa [ψ] using! (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm
    exact ⟨j₁, α, fun k k' φ ↦ by simp [hα φ, hg]⟩

Goal state after:
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)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
⊢ ∃ j x', x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    (dNext (n + 1)) (ToChainHomotopy.hom H) + (prevD (n + 1)) (ToChainHomotopy.hom H) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)

Tactic:
dNext_eq (i' := n) (w := by simp),

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1) +
        (prevD (n + 1)) (ToChainHomotopy.hom H) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc ≠ (k.castSucc, (x.cast hd).simplex.2 (min x hd))

Tactic:
intro h
        rw [Prod.ext_iff] at h
        dsimp at h
        obtain ⟨h₁, h₂⟩ := h
        apply hx _ hd i.succ
        rw [isIndex_succ]
        refine ⟨h₁, ?_, by aesop⟩
        have := φ_succAbove x hd (min x hd)
        rw [Fin.succAbove_castSucc_self] at this
        rw [← φ_succ_fst x hd, this, hi]
        dsimp

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
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ StrictMono ⇑{ toFun := φ x hd, monotone' := ⋯ }

Tactic:
exact hx.strictMono_φ hd

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
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (min x hd).castSucc)) (hx.simplex hd) =
    (x.cast hd).simplex

Tactic:
by
  apply objEquiv.injective
  ext i : 2
  dsimp only [simplex]
  rw [objEquiv_δ_apply, Equiv.apply_symm_apply, OrderHom.coe_mk, φ_succAbove]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x.toS = s.x.cast ⋯

Tactic:
S.ext_iff'

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ ∃ (h : (ht.type₁ ⋯).x.dim = (s.x.cast ⋯).dim), ((ht.type₁ ⋯).x.cast h).simplex = (s.x.cast ⋯).simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.e_6
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
⊢ (min ⋯.δ ⋯).castSucc.succAbove ((min s.δ ⋯).predAbove i) = i

Tactic:
exact Fin.succAbove_predAbove hi

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

Goal state before:
pp: case pos
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ x.toS =
    { dim := (hx.type₁ hd).d,
      simplex :=
        (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (hx.type₁ hd).index.castSucc))
          ((hx.type₁ hd).x.cast ⋯).simplex }

Tactic:
S.ext_iff'

Goal state after:
case pos
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ ∃ (h :
    x.dim =
      { dim := (hx.type₁ hd).d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (hx.type₁ hd).index.castSucc))
              ((hx.type₁ hd).x.cast ⋯).simplex }.dim),
    (x.cast h).simplex =
      { dim := (hx.type₁ hd).d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (hx.type₁ hd).index.castSucc))
              ((hx.type₁ hd).x.cast ⋯).simplex }.simplex