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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 1 + ↑i = ↑i + 1

Tactic:
add_comm

Goal state after:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ ↑i + 1 = ↑i + 1
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ (Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝) = x✝

Tactic:
apply Functor.ext
    · rintro ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟨⟩⟩⟩⟩
      simp only [eqToHom_refl, Category.comp_id, Category.id_comp]
      exact (Functor.map_id _ _).symm
    · intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
⊢ (((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
      (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y) =
    ((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫ eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)

Tactic:
ext ⟨x, f⟩

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
x : ((Center.ofBraided (Type v)).obj (unop α)).fst
f : X ⟶[Type v] Y
⊢ (ConcreteCategory.hom
          ((((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
            (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y))).toFun
      (x, f) =
    (ConcreteCategory.hom
          (((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫
            eComp (Type v) (F.obj X) (G.obj X) (G.obj Y))).toFun
      (x, f)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ B✝ : Center C
f : A✝ ⟶ B✝
i : IsIso ((forget C).map f)
⊢ IsIso f

Tactic:
by dsimp at i; change IsIso (isoMk f).hom; infer_instance

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
x✝ : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
by
    obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f
    rw [morphismPropertyHomMk_eq_strictMap]
    refine strictMap_multiplicativeClosure_le _ _ _ ?_
    rw [Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk]
    exact map_mem_strictMap _ _ _ (by simp)

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₂ α
⊢ Skeletal C

Tactic:
intro X Y ⟨e⟩

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ X = Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.σ_comp_σ H

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

Goal state before:
pp: n i j : ℕ
hi : i < n + 2
hj : j < n + 2
H : i ≤ j
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simpa

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

Goal state before:
pp: n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simpa

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

Goal state before:
pp: case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
        convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind

Goal state after:
case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝¹ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this✝ : a < m + 2
this : σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j) = σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a)
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
⊢ j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
grind [lt_and_eval_eq_eval_add_one_of_mem_isAdmissible,
    mem_isAdmissible_of_lt_and_eval_eq_eval_add_one]

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

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

Tactic:
simpa

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

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

Tactic:
simpa

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

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

Tactic:
simpa

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
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ (ConcreteCategory.hom (X.map φ.op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ φ fac_aux₁._proof_1))) x

Tactic:
obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
      Hom.ext_one_left _ _ rfl rfl⟩
  exact fac_aux₂ _ _ _ _ _ _ (by lia)

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

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

Tactic:
simpa

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

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

Tactic:
simpa

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

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

Tactic:
intro i hi

Goal state after:
case inl.inl.inl.right
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
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
i : Fin (n + 1)
hi : i < z
⊢ ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
simpa

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

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y } ↔
    ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x

Tactic:
by
  constructor
  · rintro ⟨_, ⟨f, ⟨_, h₁⟩, h₂⟩⟩
    obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f
    exact ⟨i, h₁, fun j hj ↦ SimplexCategory.δ_injective (h₂ _ ⟨inferInstance, hj⟩)⟩
  · rintro ⟨i, h₁, h₂⟩
    refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
    obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f
    obtain rfl : j = i := h₂ _ h₄
    rfl

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

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

Tactic:
simpa

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x.simplex ∈ (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)

Tactic:
← this

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex ∈
    (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.succ.castSucc ≤ x.castSucc.castSucc

Tactic:
simpa

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc.castSucc < i.succ.castSucc

Tactic:
simpa

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

Goal state before:
pp: n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
simpa

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f₁ f₂ : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
x✝¹ : Mono f₁ ∧ (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
x✝ : Mono f₂ ∧ (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
left✝¹ : Mono f₁
hf₁ : (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
left✝ : Mono f₂
hf₂ : (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
⊢ f₁ = f₂

Tactic:
by
    exact Nonsingular.injective_map _ y.nonDegenerate (by rw [hf₁, hf₂])

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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑s).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑s).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }

Tactic:
refine ⟨s, Or.inr ?_⟩
      simp [(P.isUniquelyCodimOneFace s).δ_index]

Goal state after:
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 : ℕ
α : 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
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))

Tactic:
dsimp [β]

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
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -((-1) ^ (n + 2 + (n + 1)) • H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj : j ≤ i
c : f.Cell j
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
obtain hj | rfl := hj.lt_or_eq

Goal state after:
case a.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
j : ι
hj✝ : j ≤ i
c : f.Cell j
hj : j < i
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

case a.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
j : ι
c : f.Cell j
hi : ¬IsMax j
hj : j ≤ j
⊢ (↑(P.p c.s)).subcomplex ≤ f.filtration j ⊔ ⨆ c, (↑(P.p c.s)).subcomplex
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
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ HasCardinalLT (Arrow Kᵒᵖ) κ

Tactic:
simpa

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
Y : J
hY : ⊤ Y
e : F.obj Y ≅ X
⊢ isCardinalPresentable C κ X

Tactic:
exact isCardinalPresentable_of_iso e κ

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₁

Tactic:
simpa

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₂

Tactic:
simpa

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

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : X✝ ⟶ Y✝
x✝ : isomorphisms SSet e
f : Y✝ ⟶ Z✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
hP' : P.IsInner
⊢ strongInnerAnodyneExtensions (e ≫ f)

Tactic:
refine ⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance, inferInstance⟩

Goal state after:
X✝ Y✝ Z✝ : SSet
e : X✝ ⟶ Y✝
x✝ : isomorphisms SSet e
f : Y✝ ⟶ Z✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
hP' : P.IsInner
⊢ (Subcomplex.range f).preimage (Iso.refl Z✝).hom = Subcomplex.range (e ≫ f)
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ IsIndex x hd i.succ

Tactic:
isIndex_succ

Goal state after:
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
h₁ : (x.cast hd).simplex.1 i.castSucc = k.castSucc
h₂ : (x.cast hd).simplex.2 i.castSucc = (x.cast hd).simplex.2 (min x hd)
⊢ (x.cast hd).simplex.1 i.castSucc = k.castSucc ∧
    (x.cast hd).simplex.1 i.succ = k.succ ∧ (x.cast hd).simplex.2 i.succ = (x.cast hd).simplex.2 i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
simp only [mem_finset_iff]
    simp only [Monoidal.tensorObj_obj, S.cast_dim, S.cast_simplex_rfl, prod_δ_fst,
      stdSimplex.δ_apply, Fin.succAbove_castSucc_self]
    exact hl.simplex_fst_succ

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

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

Tactic:
← hst

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

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0

pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n = 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0

Tactic:
· rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n = 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ j.castSucc < i.castSucc.succ

Tactic:
simpa

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

Goal state before:
pp: p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ ≤ j.castSucc

Tactic:
simpa

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

Goal state before:
pp: p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ 0) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
this : ⟨↑(s₁ 0) + ↑1, ⋯⟩ = OrderHom.id 0
⊢ False

Tactic:
simp at this

Goal state after: