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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Tactic:
rw [Ne] at h₁

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
⊢ B ≠ A → (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0

Tactic:
h₂

Goal state after:
case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
a✝ : B ∈ Finset.univ
h₂ : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = Path.cast ⋯ ⋯ a✝¹
⊢ listToPath (pathToList (a✝¹.cons a✝)) = Path.cast ⋯ ⋯ (a✝¹.cons a✝)

Tactic:
| cons _ _ ih =>

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

Goal state before:
pp: case pos
F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
h✝ : ↑t ≤ 1 / 2
⊢ { toFun := fun x ↦ (F.extend (2 * ↑t)) x, continuous_toFun := ⋯ } x = f₀ x

Tactic:
simp [HomotopyWith.extendProp F (2 * t) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Nullhomotopic

Tactic:
use hv.invFun ()

Goal state after:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ (ContinuousMap.id X).Homotopic (const X (hv.invFun ()))
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
this : WeakEquivalence (pushout.inl f i ≫ h.i)
⊢ i ≫ pushout.inr f i ≫ h.i ≫ sq'.lift = f

Tactic:
by
                simpa only [assoc, comp_id, pushout.condition_assoc] using
                  f ≫= sq'.fac_left

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (fibrations C).IsStableUnderRetracts

Tactic:
h₂

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((fibrations D).inverseImage e.functor).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((trivialCofibrations D).inverseImage e.functor).HasFactorization (fibrations C)

Tactic:
h₂

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ((trivialCofibrations D).inverseImage e.functor).HasFactorization ((fibrations D).inverseImage e.functor)
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
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ ∃ j, S = {j}ᶜ

Tactic:
exact ⟨j, by simp [← hS]⟩

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

Goal state before:
pp: case neg
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
exact Or.inr ⟨x₃, hx₃, h₂⟩

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

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha✝ : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb✝ : b ∈ {i}ᶜ
hab : a < b
ha : ¬a = i
hb : ¬b = i
⊢ (facePairComplIso a b hab).inv ≫ stdSimplex.δ (b.pred ⋯) ≫ f a ha✝ =
    Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso b).inv ≫ f b hb✝

Tactic:
homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred_assoc _ _ hab,

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha✝ : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb✝ : b ∈ {i}ᶜ
hab : a < b
ha : ¬a = i
hb : ¬b = i
⊢ (facePairComplIso a b hab).inv ≫ stdSimplex.δ (b.pred ⋯) ≫ f a ha✝ =
    (facePairComplIso a b hab).inv ≫ stdSimplex.δ (a.castPred ⋯) ≫ f b hb✝
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ (λ_ (X' ⟶[V] Z)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Z) ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
leftUnitor_inv_naturality_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Z)).inv ≫ 𝟙_ V ◁ eComp V X' Y Z ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Z) ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X' Y Y' ≫ (λ_ (X' ⟶[V] Y')).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y') ≫ eComp V X X' Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
leftUnitor_inv_naturality_assoc,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫ 𝟙_ V ◁ eComp V X' Y Y' ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y') ≫ eComp V X X' Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (Functor.LaxMonoidal.ε F ≫
        (λ_ (F.obj (𝟙_ V))).inv ≫
          Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫
            (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
              eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)

Tactic:
leftUnitor_inv_naturality_assoc,

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        𝟙_ W ◁ Functor.LaxMonoidal.ε F ≫
          Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫
            (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
              eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
y : FreeRefl V
x : V
f : mk x ⟶ y
⊢ motive f

Tactic:
| _ x
     => 

Goal state after:
case mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
y : FreeRefl V
x : V
f : mk x ⟶ y
⊢ motive f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case of.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
⊢ P (σ i)

Tactic:
simpa using! (σ_comp (𝟙 _) i id)

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

Goal state before:
pp: case inl.inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h✝ : i.succ ≤ i'
h : i.succ < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Goal state after:
case inl.inl
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
⊢ IsAdmissible m (a :: L) ↔ a ≤ m ∧ (∀ (x : 0 < L.length), a < L[0]) ∧ IsAdmissible (m + 1) L

Tactic:
by
  cases L <;> grind

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

Goal state before:
pp: m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ (mk m).1 + b = x.1

Tactic:
h₂

Goal state after:
m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ (mk m).1 + b = (mk (m + b)).1
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
K x✝¹ : PreAbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) K = (fun K ↦ K.faces) x✝¹
⊢ K = x✝¹

Tactic:
cases K

Goal state after:
case mk
ι : Type u_1
x✝¹ : PreAbstractSimplicialComplex ι
faces✝ : Set (Finset ι)
isRelLowerSet_faces✝ : IsRelLowerSet faces✝ Finset.Nonempty
x✝ : (fun K ↦ K.faces) { faces := faces✝, isRelLowerSet_faces := isRelLowerSet_faces✝ } = (fun K ↦ K.faces) x✝¹
⊢ { faces := faces✝, isRelLowerSet_faces := isRelLowerSet_faces✝ } = x✝¹
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl
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 : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
rw [hz, Eq.comm]

Goal state after:
case inl.inl.inl
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 : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc
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' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
rw [hz, Eq.comm]

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 : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : Fin ((unop (II ^⦋n + 1⦌)).len + 1)
⊢ (Hom.toOrderHom (II.δ i).unop) x✝ = (Hom.toOrderHom (σ i).op.unop) x✝

Tactic:
apply II.map'_succAboveOrderEmb

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ Fin.last ((↑(h.equivII s)).dim + 1)

Tactic:
simpa using IsInner.ne_last s

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 : ℕ
⊢ f.app (op ⦋n + 1⦌) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ hom H n (n + 1) +
        hom H (n + 1) (n + 2) ≫ ((alternatingFaceMapComplex C).obj Y).d (n + 2) (n + 1) +
      g.app (op ⦋n + 1⦌)

Tactic:
rw [← H.h_zero_comp_δ_zero, ← H.h_last_comp_δ_last]

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 : ℕ
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ hom H n (n + 1) +
        hom H (n + 1) (n + 2) ≫ ((alternatingFaceMapComplex C).obj Y).d (n + 2) (n + 1) +
      H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

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

Tactic:
exact le_trans (by rfl) (le_iSup _ i)

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

Goal state before:
pp: case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ ↑t < ↑(P.p c.s)

Tactic:
rw [Subcomplex.N.lt_iff, SSet.N.lt_iff]

Goal state after:
case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex < (↑(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
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
⊢ (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁

Tactic:
simp [y₁]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
Q : C
⊢ Q ◁ f ≫ Q ◁ pushout.inl f g = Q ◁ g ≫ Q ◁ pushout.inr f g

Tactic:
simp [← MonoidalCategory.whiskerLeft_comp, pushout.condition]

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

Goal state before:
pp: case refine_2
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
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j

Tactic:
obtain ⟨i, hi⟩ := mem_range_left x hd j hj
      dsimp at hi
      obtain rfl | ⟨i, rfl⟩ := Fin.eq_self_or_eq_succAbove l.castSucc i
      · exact (hj (by rw [← hi, hl.simplex_fst_castSucc])).elim
      · exact ⟨_, hi⟩

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

Goal state before:
pp: case mpr
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₃
h : ∀ (φ : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π), Nonempty (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty (Arrow.LiftStruct α)

Tactic:
exact ⟨(adj₂.liftStructEquiv sq₁₂ sq₁₃ α).symm (h _).some⟩

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
h : { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } = { dim := t.d + 1, simplex := (t.x.cast ⋯).simplex }
⊢ s = t

Tactic:
by
    rw [Type₁.ext_iff, Subcomplex.N.ext_iff, N.ext_iff]
    rwa [← s.x.toS.cast_eq_self s.hd, ← t.x.toS.cast_eq_self t.hd]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
⊢ X.ιNormalizedChainComplex x ≫ (X.normalizedChainComplex R).d (n + 1) n =
    ∑ i, (-1) ^ ↑i • X.ιNormalizedChainComplex ((ConcreteCategory.hom (SimplicialObject.δ X i)) x)

Tactic:
simp [ιNormalizedChainComplex, Preadditive.sum_comp,
    -ιChainComplex_toNormalizedChainComplex_f]

Goal state after: