mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ A ≤ Subfunctor.equalizer f g → Subfunctor.equalizer f g = A

Tactic:
intro h
    exact le_antisymm (equalizer_le f g) h

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

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Subcomplex.ofSimplex
      ((ConcreteCategory.hom ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌))) (stdSimplex.objEquiv.symm q)) ≤
    Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))

Tactic:
apply Subcomplex.ofSimplex_map_le

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

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

Tactic:
obtain ⟨i, hi⟩ := i
    by_cases hk : k = 0
    · subst hk
      have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last,
        Fin.val_zero, AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false,
        Fin.val_one, Nat.reduceEqDiff, mem_singleton, or_self, or_false] at this
      simp only [Fin.lt_def, Fin.val_last] at hₙ
      lia
    · 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.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
k : J
α : j ⟶ k
hk : (hom (f.app k)) ((hom (F₁.map α)) x₁) = (hom (f.app k)) ((hom (F₁.map α)) y₁)
⊢ (hom (c₁.ι.app j)) x₁ = (hom (c₁.ι.app j)) y₁

Tactic:
← c₁.w α,

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
j : J
x₁ y₁ : F₁.obj j
h : (hom (c₂.ι.app j)) ((hom (f.app j)) x₁) = (hom (c₂.ι.app j)) ((hom (f.app j)) y₁)
k : J
α : j ⟶ k
hk : (hom (f.app k)) ((hom (F₁.map α)) x₁) = (hom (f.app k)) ((hom (F₁.map α)) y₁)
⊢ (hom (F₁.map α ≫ c₁.ι.app k)) x₁ = (hom (F₁.map α ≫ c₁.ι.app k)) y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ X.skeleton n

Tactic:
exact le_trans (by exact le_trans (by rfl) (le_iSup _ y))
    (le_iSup _ ⟨j, lt_of_le_of_lt
      (SimplexCategory.len_le_of_epi f) hi⟩)

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Subcomplex.range (∂Δ[d].ι ≫ c.map) ≤ (skeletonOfMono i) d

Tactic:
simp [Subcomplex.range_comp, Subcomplex.image_le_iff]

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

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
SimplicialObject.δ_def,

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (X.map (δ 0).op)) x) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫
            (X.1 ◁ (Y.1 ◁ f ≫ (HalfBraiding.β Y.2 U').hom)) ⊗≫
              (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by monoidal
          _ = 𝟙 _ ⊗≫
            X.1 ◁ (HalfBraiding.β Y.2 U).hom ⊗≫
              (X.1 ◁ f ≫ (HalfBraiding.β X.2 U').hom) ▷ Y.1 ⊗≫ 𝟙 _ := by
            rw [HalfBraiding.naturality]; monoidal
          _ = _ := by rw [HalfBraiding.naturality]; monoidal

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, ⋯⟩
α : 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 (X.map α.right.unop.hom.op))
      ((ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1))) x)

Tactic:
rw [op_comp, Functor.map_comp]

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 ≫ X.map (⦋1⦌.const ⦋0⦌ 0).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)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : degeneracies.multiplicativeClosure f✝
h : degeneracies g✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ g✝)

Tactic:
| comp_of _ _ _ h =>

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

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure f✝
h : faces g✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ g✝)

Tactic:
| comp_of _ _ _ h =>

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

Goal state before:
pp: m : ℕ
L : List ℕ
⊢ IsAdmissible m L ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

Tactic:
induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩

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

Goal state before:
pp: case mk.mk.zero
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 ⋯ ⋯)
ha hb : 0 ≤ d
h : 0 + 0 = 0
⊢ W (𝟙 { obj := { len := 0 }, property := ha })

Tactic:
apply MorphismProperty.id_mem

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

Goal state before:
pp: case neg.zero
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
hb : 0 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : a + 0 = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
t : Fin (1 + 1)
⊢ (ConcreteCategory.hom (X.map ((mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯).op ≫ (mkOfSucc 1).op)))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (X.map (mkOfSucc 1).op))
      ((ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10))) x)

Tactic:
have : α.hom ≫ (mkOfSucc 1).op = α₀.hom :=
              Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
            rw [dsimp% [α] this]
            dsimp [α₀] at h₀ ⊢
            rw [h₀, ← dsimp% [α₀] ConcreteCategory.congr_hom (s.w β₀) x]
            rfl

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

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)

Tactic:
rw [Fin.castPred_castSucc]

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x = y

Tactic:
injection h

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

Goal state before:
pp: case inl.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)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
map'_eq_last_iff

Goal state after:
case inl.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)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : ∀ (i : Fin (n + 1)), (f i).castSucc < y.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc
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 = Fin.last (n + 1)

Tactic:
map'_eq_last_iff

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 : ∀ (i : Fin (m + 1)), (g i).castSucc < x.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc
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 φ

Tactic:
rw [← Category.id_comp φ]

Goal state after:
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 (𝟙 c.pt ≫ φ)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda F).map j.hom ≫ φ s = (restrictedULiftYoneda F).map (s.ι.app j)
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
m : ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).pt ⟶ s.pt
hm : ∀ (j : CostructuredArrow F Y), ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app j ≫ m = s.ι.app j
⊢ (restrictedULiftYoneda F).map m = (restrictedULiftYoneda F).map (h.preimage (φ s))

Tactic:
by
          ext ⟨_⟩ ⟨_⟩
          simp [φ, ← hm]

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

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty j sq₁₃.π

Tactic:
apply hj

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃ : internalHom.PullbackObjObj i p := ⋯
⊢ innerFibrations sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
⊢ innerAnodyneExtensions sq₁₂.ι

Tactic:
by
  intro E B p hp
  let sq₁₃ := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom i p
  rw [internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃]
  apply hj
  rw [← innerFibration_iff] at hp ⊢
  exact innerFibration_pullbackObjObjπ sq₁₃

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

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃ : internalHom.PullbackObjObj i p := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty j sq₁₃.π

Tactic:
apply hj

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃ : internalHom.PullbackObjObj i p := ⋯
⊢ fibrations SSet sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.left.inl
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ is.castSucc ∈ Ss ↔ is.castSucc ∈ Finset.image is.castSucc.succAbove Sδ

Tactic:
have : is.castSucc ∉ Ss := fun h ↦ by
            have : s.1 is.castSucc ≤ k.castSucc := by
              simpa using (hs.simplex_fst_le_castSucc_iff is.castSucc).2 (by simp)
            simp_all [Ss]

Goal state after:
case inr.left.inl
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : is.castSucc ∉ Ss
⊢ is.castSucc ∈ Ss ↔ is.castSucc ∈ Finset.image is.castSucc.succAbove Sδ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁.h₀
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ pushout.inl ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
          Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
            ⋯) =
    pushout.inl ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        (Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝².right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                ((G.map (unop (op X₁)).hom.op).app x✝².right)))
            ⋯ ≫
          (𝟭 (Arrow C₃)).map x✝)

Tactic:
simp [← homEquiv_symm_naturality_two,
        ← homEquiv_symm_naturality_three]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        ((G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
          Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom)
                ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
            ⋯) =
    pushout.inr ((F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj x✝²).left)
        ((F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj x✝²).hom) ≫
      Arrow.Hom.left
        (Arrow.homMk
            (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
              (adj₂.homEquiv.symm
                (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                  ((G.map (unop (op X₁)).hom.op).app x✝².right)))
              ⋯)
            (adj₂.homEquiv.symm
              (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom)
                ((G.map (unop (op X₁)).hom.op).app x✝².right)))
            ⋯ ≫
          (𝟭 (Arrow C₃)).map x✝)

Tactic:
simp [← homEquiv_symm_naturality_two,
        ← homEquiv_symm_naturality_three]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ stdSimplex.δ i.succ ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
by rw [CosimplicialObject.δ_comp_σ_succ_assoc]

Goal state after: