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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
⊢ φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
have hnaq_shift (d : ℕ) : n + d = a + d + q := by lia
  rw [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl),
    hσ'_eq hnaq (c_mk (n + 1) n rfl), hσ'_eq (hnaq_shift 1) (c_mk (n + 2) (n + 1) rfl)]
  simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp,
    comp_add]
  simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]
  -- cleaning up the first sum
  rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
  swap
  · rintro ⟨k, hk⟩
    suffices φ ≫ X.δ (⟨a + 2 + k, by lia⟩ : Fin (n + 2)) = 0 by
      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
    convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)
    dsimp
    lia
  -- cleaning up the second sum
  rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
  swap
  · rintro ⟨k, hk⟩
    rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
    · intro h
      replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
      lia
    · dsimp [Fin.cast, Fin.pred]
      rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
      lia
    · simp only [Fin.lt_def]
      dsimp [Fin.natAdd, Fin.cast]
      lia
  simp only [assoc]
  conv_lhs =>
    congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
  dsimp [Fin.cast, Fin.castLE, Fin.castLT]
  /- the purpose of the following `simplif` is to create three subgoals in order
      to finish the proof -/
  have simplif :
    ∀ a b c d e f : Y ⟶ X _⦋n + 1⦌, b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f := by
    intro a b c d e f h1 h2 h3
    rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
  apply simplif
  · -- b = f
    rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
    exact ⟨a, by lia⟩
  · -- d + e = 0
    rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
      X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
    simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
      add_neg_cancel]
  · -- c + a = 0
    rw [← Finset.sum_add_distrib]
    apply Finset.sum_eq_zero
    rintro ⟨i, hi⟩ _
    simp only
    have hia : (⟨i, by lia⟩ : Fin (n + 2)) ≤
        Fin.castSucc (⟨a, by lia⟩ : Fin (n + 1)) := by
      rw [Fin.le_iff_val_le_val]
      dsimp
      lia
    generalize_proofs
    rw [← Fin.succ_mk (n + 1) a ‹_›, ← Fin.castSucc_mk (n + 2) i ‹_›,
      δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]
    congr 2
    ring

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b, ⋯⟩.succ < j.succ

Tactic:
dsimp
    rw [Fin.lt_def, Fin.val_succ]
    linarith

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0

Tactic:
Fin.sum_univ_two,

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ ((-1) ^ ↑0 • X.δ 0 + (-1) ^ ↑1 • X.δ 1) ≫ (1 • X.σ 0) +
        X.σ 0 ≫ 𝟙 (X _⦋1⦌) ≫ (-1 • X.σ 1) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → A.EqId

Tactic:
intro h
    rcases A with ⟨_, ⟨f, hf⟩⟩
    simp only at h
    subst h
    refine ext _ _ rfl ?_
    simp only [eqToHom_refl, comp_id]
    exact eq_id_of_epi f

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁.Hom S₂
h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
⊢ Φ₁ = Φ₂

Tactic:
rcases Φ₁ with ⟨F₁, f₁, c₁⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₂ : S₁.Hom S₂
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = Φ₂.f n
⊢ { F := F₁, f := f₁, comm := c₁ } = Φ₂
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ factorThruImage (θ.unop ≫ A.e) = e

Tactic:
exact SimplexCategory.factorThruImage_eq fac

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : ⦋n✝ + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ PInfty.f (n✝ + 1) = 0

Tactic:
· obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
    rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]

Goal state after:
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
n : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ∑ j, (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n

Tactic:
Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    (s.πSummand (IndexSet.id (op ⦋n⦌)) ≫ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌))) ≫ PInfty.f n

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ∀ (x : IndexSet (op ⦋n⦌)), x ≠ IndexSet.id (op ⦋n⦌) → (s.πSummand x ≫ (s.cofan (op ⦋n⦌)).inj x) ≫ PInfty.f n = 0
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (j : J), (Functor.pi' fun j ↦ s.proj j) ≫ (piLimitFan F).proj j = s.proj j

Tactic:
by
      intros
      dsimp only [piLimitFan]
      simp [comp_eq_comp]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
t : ↑I
x : X
hx : x ∈ S
⊢ F (t, x) = f₁ x

Tactic:
rw [F.eq_fst t hx, ← F.eq_fst 1 hx, F.apply_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p

Tactic:
by
  induction p using Path.Homotopic.Quotient.ind
  simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]
  congr

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

Goal state before:
pp: case mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
⊢ ((mk γ₀).trans (mk γ₁)).trans γ₂ = (mk γ₀).trans ((mk γ₁).trans γ₂)

Tactic:
| mk γ₁ =>

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

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
i : Fin (n + 1)
⊢ i ∈ Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ∪ {i✝} ↔ i ∈ Set.univ

Tactic:
simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex (j.succAbove i) = f.vertex i.succ

Tactic:
Fin.succAbove_of_le_castSucc j i h

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ f.vertex i.succ = f.vertex i.succ
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (A'.map φ)) a)) =
    x.app Δ ((ConcreteCategory.hom (f.app Δ)) a) ≫ G.map φ

Tactic:
by
    rw [← x.naturality φ (f.app Δ a), f.naturality_apply φ a]

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

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ (ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a) =
    (ConcreteCategory.hom ((Opposite.unop A).map φ)) ((ConcreteCategory.hom (f.unop.app X)) a)

Tactic:
exact ConcreteCategory.congr_hom (f.unop.naturality φ) a

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

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

Tactic:
rw [← whisker_exchange]; monoidal

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

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
ext x; fin_cases x; rfl

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

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
ext x; fin_cases x; rfl

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
      (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y))) ⋯).hom =
    (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
      (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)

Tactic:
ext y : 2
        obtain ⟨y, rfl⟩ := y.mk_surjective
        cat_disch

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

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
⊢ 1 = (ConcreteCategory.hom f) i

Tactic:
have := f.toOrderHom.monotone hij

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
this : (Hom.toOrderHom f) j ≤ (Hom.toOrderHom f) i
⊢ 1 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₂.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
| Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
    (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) (Fin.natAdd (x₁.len + 1) i)

Tactic:
Fin.addCases_right

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₂.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
| Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ Nonempty (P.pairing.WeakRankFunction ℕ) ↔ Nonempty (P.WeakRankFunction ℕ)

Tactic:
exact (P.weakRankFunctionEquiv ℕ).symm.nonempty_congr

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ f ≫ inv (pullback.snd i b) ≫ pullback.fst i b = t

Tactic:
← cancel_mono i,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ (f ≫ inv (pullback.snd i b) ≫ pullback.fst i b) ≫ i = t ≫ i
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ G, ∃ (_ : P G), ∃ f, ¬A.Factors f

Tactic:
by_contra!
  exact hA (hP.subobject_eq_top this)

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
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), (fun f ↦ f ≫ i) (φ j) = p.ι.app j
c : Cocone p.diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
⊢ { pt := Y, ι := p.ι }.ι.app j ≫ p.isColimit.desc c ≫ i = { pt := Y, ι := p.ι }.ι.app j ≫ 𝟙 Y

Tactic:
dsimp at hφ ⊢

Goal state after:
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
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), φ j ≫ i = p.ι.app j
c : Cocone p.diag := { pt := X, ι := { app := φ, naturality := ⋯ } }
j : J
⊢ p.ι.app j ≫ p.isColimit.desc c ≫ i = p.ι.app j ≫ 𝟙 Y
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
h.isPresentable_eq_retractClosure

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure
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) κ
S : SmallCategoryCardinalLT κ
e : SmallCategoryCardinalLT.categoryFamily κ S ≌ J
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
rw [isClosedUnderColimitsOfShape_iff_of_equivalence _ e.symm]

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 (SmallCategoryCardinalLT.categoryFamily κ S)
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
⊢ (x.cast hd).simplex.1 (min x hd) = k.succ

Tactic:
rw [← mem_finset_iff]
  apply Finset.min'_mem

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)
this : l.l ≫ (G.map f₁.op).app X₃ = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.fst
⊢ sq₁₂.inr ≫ sq₁₂.ι ≫ adj₂.homEquiv.symm l.l = sq₁₂.inr ≫ Arrow.Hom.left α

Tactic:
simp only [sq₁₂.inr_ι_assoc, ← adj₂.homEquiv_symm_naturality_one,
            this, Equiv.symm_apply_apply, arrowHomEquiv_apply_right_fst, Arrow.mk_left]

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
⊢ HasLiftingProperty sq₁₂.ι p

Tactic:
let sq₁₃ := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom i p

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 := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty sq₁₂.ι p
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
⊢ HasLiftingProperty sq₁₂.ι p

Tactic:
let sq₁₃ := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom i p

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 := Functor.PullbackObjObj.ofHasPullback internalHom i p
⊢ HasLiftingProperty sq₁₂.ι p
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 : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1 + 1)
hx : IsIndex x ⋯ i
⊢ i ≠ 0

Tactic:
rintro rfl; simp at hx

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k

Tactic:
rw [stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)]

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          stdSimplex.objMk₁ (Fin.pred 1 ⋯)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: 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✝ : Arrow C₃
⊢ {
            app := fun X₂ ↦
              Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                  (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                ⋯,
            naturality := ⋯ }.app
        ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
      (G.leibnizPullback.obj (op X₁)).map
        ({
              app := fun 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)))
                  ⋯,
              naturality := ⋯ }.app
          x✝) =
    𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)

Tactic:
by
    ext
    · simp [← homEquiv_naturality_three]
    · apply pullback.hom_ext <;> simp [← homEquiv_naturality_three]

Goal state after: