mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    ∑ j_1, ((s.πSummand j_1 ≫ (s.cofan (op ⦋i⦌)).inj j_1) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌))

Tactic:
Finset.sum_eq_single (IndexSet.id (op ⦋i⦌)),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ s.πSummand (IndexSet.id (op ⦋i⦌)) ≫
      (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) =
    ((s.πSummand (IndexSet.id (op ⦋i⦌)) ≫ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌))) ≫ K[X].d i j) ≫
      s.πSummand (IndexSet.id (op ⦋j⦌))

case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ ∀ b ∈ Finset.univ,
    b ≠ IndexSet.id (op ⦋i⦌) →
      ((s.πSummand b ≫ (s.cofan (op ⦋i⦌)).inj b) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) = 0

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ IndexSet.id (op ⦋i⦌) ∉ Finset.univ →
    ((s.πSummand (IndexSet.id (op ⦋i⦌)) ≫ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌))) ≫ K[X].d i j) ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) =
      0
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ ∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y),
    (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫ CategoryTheory.eqToHom ⋯

Tactic:
intros; ext; simp

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x ∈ {1}
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } x =
    p.toContinuousMap x

Tactic:
· rw [Set.mem_singleton_iff] at hx
      rw [hx]
      simp [hf₁]

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

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

Tactic:
apply Localization.fac

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
this : IsCofibrant h.Z
⊢ IsFibrant h.Z

Tactic:
isFibrant_iff_of_isTerminal h.p terminalIsTerminal

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
this : IsCofibrant h.Z
⊢ Fibration h.p
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
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : k = J.fst default
⊢ I.right k = I.right (J.fst default)

Tactic:
simp [hk]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ¬∀ (x : Fin (n + 3)), x ∈ S
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
not_forall

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ∃ x, x ∉ S
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
this : Sᶜ.card + S.card = Fintype.card (Fin (n + 1 + 1))
⊢ Sᶜ.card = 1

Tactic:
rw [Fintype.card_fin] at this

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
this : Sᶜ.card + S.card = n + 1 + 1
⊢ Sᶜ.card = 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: ⊢ ∂Δ[0] = ⊥

Tactic:
by
  ext m x
  simp only [boundary, Nat.reduceAdd, Set.mem_ofPred_eq, Subfunctor.bot_obj, Set.bot_eq_empty,
    Set.mem_empty_iff_false, iff_false, Decidable.not_not]
  intro x
  exact ⟨0, by subsingleton⟩

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
⊢ A.toSSet.degenerate i = ⊤

Tactic:
ext ⟨a, ha⟩
    rw [A.mem_degenerate_iff]
    simp only [Set.top_eq_univ, Set.mem_univ, iff_true]
    obtain hi | rfl := hi.lt_or_eq
    · simp [Δ[n].degenerate_eq_univ_of_hasDimensionLT (n + 1) i]
    · rw [mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_top_dim]
      rintro rfl
      exact h (le_antisymm (by simp) (by simpa [← ofSimplex_objEquiv_symm_id]))

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

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n].Subcomplex
h : A ≤ ∂Δ[n]
⊢ A ≠ ⊤

pp: case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
· rintro rfl
    exact lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))

Goal state after:
case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ A ≤ ∂Δ[n]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ¬∀ (x : Fin (n + 1)), x ∈ {i, a, b}
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
not_forall

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ∃ x, x ∉ {i, a, b}
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ¬∀ (x : Fin (n + 4)), x ∈ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1

Tactic:
not_forall

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ x, x ∉ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : l ∉ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1

Tactic:
simp only [mem_insert, mem_singleton, not_or] at hl

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
l : Fin (n + 4)
hl : ¬l = i ∧ ¬l = ⟨k, ⋯⟩ ∧ ¬l = ⟨k + 1, ⋯⟩ ∧ ¬l = ⟨k + 2, ⋯⟩
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case e'_2
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom e.hom.hom) ((ConcreteCategory.hom c.inl) x₁)

pp: case e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inr) x₂ = (ConcreteCategory.hom e.hom.hom) ((ConcreteCategory.hom c.inr) x₂)

Tactic:
· exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁

Goal state after:
case e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inr) x₂ = (ConcreteCategory.hom e.hom.hom) ((ConcreteCategory.hom c.inr) x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
rw [pushoutCocone_inl_eq_inr_iff_of_iso
    (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
    (by simp))]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom (Pushout.cocone f g).inl) x₁ = (ConcreteCategory.hom (Pushout.cocone f g).inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : ℕ
y : Δ[d] _⦋n⦌
hy₁ : y ∈ Δ[d].nonDegenerate n
hy₂ : ↑⟨y, hy₁⟩ ∈ ∂Δ[d].obj (op ⦋n⦌)
⊢ ⟨y, hy₂⟩ ∈ ∂Δ[d].toSSet.nonDegenerate n

Tactic:
by simpa [Subcomplex.mem_nonDegenerate_iff]

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

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
rw [← spine_arrow, spine_δ_arrow_lt sx _ hlt]
    dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]
    dsimp
    apply congr_arg
    apply Subtype.ext
    dsimp [horn.face, CosimplicialObject.δ]
    rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_lt hlt]
    rfl

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
f g : X ⟶ Y
w : f.f = g.f
⊢ f = g

Tactic:
cases f; cases g; congr

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
f : X ⟶ Y
inst✝ : IsIso f.f
U : C
⊢ inv f.f ▷ U ≫ (X.snd.β U).hom = (Y.snd.β U).hom ≫ U ◁ inv f.f

Tactic:
by simp [← cancel_epi (f.f ▷ U), ← comp_whiskerRight_assoc,
      ← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ x₁ = y₁

Tactic:
by rw [← e.tgt_eq, ← e'.tgt_eq, 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 j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + 0 = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
rintro i j hij hj hik
      obtain rfl : i = j := hik
      have : mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by rfl) =
        ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩ := Hom.ext_one_left _ _
      rw [this]
      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)
      conv_rhs => dsimp; rw [dsimp% s.π.naturality_apply α x]
      rw [op_comp, Functor.map_comp]
      simp only [types_comp_apply]
      refine congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_
      unfold strArrowMk₂
      rw [lift, StrictSegal.spineToSimplex_vertex]
      congr

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 Y : C
e : X ≅ Y
⊢ r.degHom e.hom = r.deg Y

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
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
e : X ≅ Y
⊢ r.degHom e.hom ≤ r.deg Y

case refine_2
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
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'

Tactic:
by rw [δ_comp_σ_of_le h]

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

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

Tactic:
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.Augmented.Monoidal

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (x ⊗ WithInitial.star)

Tactic:
cases x <;>
  rfl

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

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (WithInitial.star ⊗ x)

Tactic:
cases x <;>
  rfl

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ ((SSet.N.orderIsoOfIso e).symm y.toN).simplex ∉ A.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e).symm y.toN).dim⦌)

Tactic:
obtain rfl : A.preimage e.inv = B := by aesop
    exact y.notMem

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

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
have e₁ := inr'_eval (tensorObjOf x y) z i

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ :
  (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ

Tactic:
rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

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

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
      rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
      simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
      intro j hj
      by_cases! h : j.castSucc < i
      · simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
      · rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

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

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

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

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

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n ↔ orderHomOfSimplex z hn = OrderHom.id

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
⊢ orderHomOfSimplex z hn = OrderHom.id

case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • X.δ x_1 ≫ H.h x + -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • H.h x_1 ≫ Y.δ x +
      H.h 0 ≫ Y.δ 0

Tactic:
let α (x : Fin (n + 1) × Fin (n + 2)) := (-1) ^ ((x.1 + x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • X.δ x_1 ≫ H.h x + -∑ x, ∑ x_1, (-1) ^ (↑x + ↑x_1) • H.h x_1 ≫ Y.δ x +
      H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) = ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) ≤ ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

case refine_2
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f) ≤ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f)
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
⊢ ∀ (i : X₁.N) (i_1 : X₂.N),
    (Subcomplex.range (yonedaEquiv.symm i.simplex ⊗ₘ yonedaEquiv.symm i_1.simplex)).toSSet.HasDimensionLT n

Tactic:
intro x₁ x₂

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
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
k : J
u : j ⟶ k
hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u
⊢ f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
by simpa [← cancel_epi h.r] using hj

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
⊢ Mono c.ιSigmaStdSimplex

Tactic:
rw [NatTrans.mono_iff_mono_app]
  rintro ⟨⟨d⟩⟩
  rw [mono_iff_injective]
  intro x y h
  simpa [f.ιSigmaStdSimplex_eq_iff] using h.symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
this : IsSplitEpi i
⊢ IsIso i

Tactic:
by
    obtain ⟨r, fac⟩ := this
    exact ⟨r, by simp [← cancel_mono i, fac]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
⊢ F.isDenseAt.IsClosedUnderIsomorphisms

Tactic:
isDenseAt_eq_isPointwiseLeftKanExtensionAt

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
⊢ (LeftExtension.mk (𝟭 D) F.rightUnitor.inv).isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X✝ : SSet
A : X✝.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
j : ℕ
hj : ¬IsMax j
X Y : SSet
c : P.rankFunction.Cell j
⊢ SSet.anodyneExtensions (P.rankFunction.basicCell j c)

Tactic:
exact .horn_ι c.index

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions ≤ anodyneExtensions

Tactic:
by
  rw [anodyneExtensions_eq_llp_rlp, innerAnodyneExtensions_eq_llp_rlp, le_llp_iff_le_rlp,
    rlp_llp_rlp]
  exact antitone_rlp innerHornInclusions_le_J

Goal state after: