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

Goal state before:
pp: case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₁ f c = Cell.type₁ f c'

pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₁ f c = Cell.type₂ f c'

pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₂ f c = Cell.type₁ f c'

pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₂ f c = Cell.type₂ f c'

Tactic:
<;>

Goal state after:
case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₁ f c = Cell.type₁ f c'

case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₁ f c = Cell.type₂ f c'

case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')
⊢ Cell.type₂ f c = Cell.type₁ f c'

case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')
⊢ Cell.type₂ f c = Cell.type₂ f c'
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case inst.zero
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.zero)
    Cardinal.aleph0

pp: case inst.one
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.one)
    Cardinal.aleph0

Tactic:
<;>

Goal state after:
case inst.zero
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.zero)
    Cardinal.aleph0

case inst.one
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.one)
    Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case inst.zero
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Z Cardinal.aleph0

pp: case inst.one
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Y Cardinal.aleph0

Tactic:
<;>

Goal state after:
case inst.zero
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Z Cardinal.aleph0

case inst.one
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Y Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
hf : strongAnodyneExtensions f
⊢ strongAnodyneExtensions (f ≫ e)

Tactic:
by
    obtain ⟨_, P, hP⟩ := hf
    refine ⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance⟩
    simp [Subcomplex.preimage_inv, Subcomplex.range_comp]

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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
⊢ ∀ (a : Fin (n + 2 + 1)) (b : Fin (n + 1 + 1)),
    ((∃ a_1, ∃ b_1 ≤ a_1.castSucc, b_1.castSucc = a ∧ a_1.succ = b) ∨
        ∃ a_1 b_1, a_1.castSucc < b_1 ∧ b_1.succ = a ∧ a_1.castSucc = b) →
      ∀ (a_2 : Fin (n + 2 + 1)) (b_1 : Fin (n + 1 + 1)),
        ((∃ a, a.castSucc.succ = a_2 ∧ a.succ = b_1) ∨ ∃ a, a.castSucc.succ = a_2 ∧ a.castSucc = b_1) ∨
            a_2 = 0 ∧ b_1 = 0 ∨ a_2 = Fin.last (n + 2) ∧ b_1 = Fin.last (n + 1) →
          a = a_2 → ¬b = b_1

Tactic:
rintro ⟨a, _⟩ ⟨b, _⟩ (⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩ | ⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩) _ _
      ((⟨⟨i, _⟩, h₄, h₅⟩ | ⟨⟨i, _⟩, h₄, h₅⟩) | (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)) <;>
        simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢ <;> grind

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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
⊢ isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ

Tactic:
intro X hX

Goal state after:
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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : isCardinalPresentable C κ X
⊢ P.colimitsCardinalClosure κ X
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ inl ▷ Q ≫ hP.desc h k w ▷ Q = h ▷ Q

Tactic:
rw [← comp_whiskerRight, IsPushout.inl_desc]

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

Goal state before:
pp: case h₀
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₁ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₁ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

pp: case h₁
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₂ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₂ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

Tactic:
<;>

Goal state after:
case h₀
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₁ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₁ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

case h₁
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₂ S T ≫
      ⋯.isoPushout.hom ≫
        (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    ι₂ S T ≫ (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ⋯.isoPushout.hom ≫ (Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) (Arrow.mk S.ι).hom (Arrow.mk T.ι).hom).ι =
    (S.unionProd T).ι ≫ (Iso.refl (X ⊗ Y)).hom

Tactic:
apply (unionProd.isPushout S T).hom_ext <;>
      simp [Limits.pushout.inl_desc, Limits.pushout.inr_desc]

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

Goal state before:
pp: case inl.inr
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd (min x hd).castSucc

Tactic:
φ_castSucc

Goal state after:
case inl.inr
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < (k.castSucc, (x.cast hd).simplex.2 (min x hd))
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
this : y < l
⊢ False

Tactic:
Fin.succAbove_of_castSucc_lt _ _ (by grind)

Goal state after:
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 y.castSucc = k.succ
this : y < l
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y : WalkingIso
x✝ : zero ⟶ y
⊢ WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y

pp: case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y : WalkingIso
x✝ : one ⟶ y
⊢ WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y : WalkingIso
x✝ : zero ⟶ y
⊢ WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y

case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
y : WalkingIso
x✝ : one ⟶ y
⊢ WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      zero (𝟙 zero) =
    𝟙 (WalkingIso.rec X Y zero)

pp: case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      one (𝟙 one) =
    𝟙 (WalkingIso.rec X Y one)

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      zero (𝟙 zero) =
    𝟙 (WalkingIso.rec X Y zero)

case one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      one (𝟙 one) =
    𝟙 (WalkingIso.rec X Y one)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case false
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := false } } =
    F.obj { as := { down := false } }

pp: case true
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := true } } =
    F.obj { as := { down := true } }

Tactic:
<;>

Goal state after:
case false
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := false } } =
    F.obj { as := { down := false } }

case true
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).obj { as := { down := true } } =
    F.obj { as := { down := true } }
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : zero ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

pp: case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : one ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : zero ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : one ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

pp: case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

pp: case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

pp: case one.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
<;>

Goal state after:
case zero.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case one.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ F.map iso.hom = F.map f

pp: case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ F.map iso.inv = F.map f

Tactic:
<;>

Goal state after:
case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ F.map iso.hom = F.map f

case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ F.map iso.inv = F.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ φ s.δ ⋯ (min ⋯.δ ⋯).castSucc = (objEquiv (s.x.cast ⋯).simplex) s.index.castSucc

Tactic:
φ_castSucc

Goal state after:
case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (k.castSucc, (s.δ.cast ⋯).simplex.2 (min s.δ ⋯)) = (objEquiv (s.x.cast ⋯).simplex) s.index.castSucc
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso (X.hom ▷ I)
this : IsPushout (X.hom ▷ I) (X.left ◁ i.to W) ((i.ofIso (zeroMul i).symm).to (X.left ⊗ W)) (𝟙 (X.left ⊗ W))
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (i.to W)).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (i.to W)).hom) ≫
      this.isoPushout.symm.hom ≫ X.hom ▷ W =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (i.to W)).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (i.to W)).hom) ≫
      (ofHasPushout (curriedTensor C) X.hom (Arrow.mk (i.to W)).hom).ι ≫
        (Iso.refl (((curriedTensor C).obj X.right).obj (Arrow.mk (i.to W)).right)).hom

Tactic:
simp [pushout.inr_desc]

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
b : X
hb' : b ∈ s.finset
hb : f b ∈ Finset.image (⇑f) s.finset
h : ⟨b, hb'⟩ ≤ ⟨a, ha'⟩
⊢ ⟨f a, ha⟩ ≤ ⟨f b, hb⟩ ∨ ⟨f b, hb⟩ ≤ ⟨f a, ha⟩

Tactic:
· exact Or.inr (f.monotone h)

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: case left
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X)

pp: case right
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (ZerothHomotopy ↑X)

Tactic:
<;>

Goal state after:
case left
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X)

case right
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (ZerothHomotopy ↑X)