mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
k : K
⊢ IsCardinalPresentable (e.functor.obj (Y.obj k)) κ

Tactic:
;

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
k : K
⊢ IsCardinalPresentable (e.functor.obj (Y.obj k)) κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: 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 : P.p c.s = P.p c'.s
⊢ c.s = c'.s

Tactic:
;

Goal state after:
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 : P.p c.s = P.p c'.s
⊢ c.s = c'.s
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
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 : c.s = c'.s
⊢ c = c'

Tactic:
;

Goal state after:
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 : c.s = c'.s
⊢ c = c'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: this : ∀ (n : ℕ), IsSmall.{u, u, u + 1} (ofHoms fun p ↦ Λ[n + 2, ↑p].ι)
⊢ IsSmall.{u, u, u + 1} (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι)

Tactic:
exact isSmall_iSup _

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ i, f.filtration i)

Tactic:
;

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ i, f.filtration i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (n + 1)
this : x.simplex ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋x.dim⦌)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.2

Tactic:
simp [Subcomplex.mem_unionProd_iff, mem_boundary_iff_notMem_range] at this

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
i : Fin (n + 1)
this :
  (∀ (x_1 : Fin (n + 1)), ∃ x_2, x.simplex.2 x_2 = x_1) ∧ x.simplex.1 ∉ Λ[m + 1, k.castSucc].obj (Opposite.op ⦋x.dim⦌)
⊢ i ∈ Set.range ⇑(x.cast ⋯).simplex.2
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₂.homEquiv l.l ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.snd = Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α) ≫ sq₁₃.snd

Tactic:
· have := l.fac_right
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_snd, ← this, adj₂.homEquiv_naturality_three,
            arrowHomEquiv_apply_right_snd, Arrow.mk_right]

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
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
⊢ ↑i < ↑i + 1

Tactic:
;

Goal state after:
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
⊢ ↑i < ↑i + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inl
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 < (objEquiv (x.cast hd).simplex) (i.castSucc.succ.castPred ⋯)

Tactic:
exact hx' (Fin.lt_def.2 (by dsimp; grind))

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
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
⊢ i.castSucc ≤ min x hd

Tactic:
;

Goal state after:
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
⊢ i.castSucc ≤ min x hd
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
⊢ HasLiftingProperty Λ[n✝ + 2, k].ι sq₁₃.π

Tactic:
rw [← internalHomAdjunction₂.hasLiftingProperty_iff sq₁₂]

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
⊢ 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
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
⊢ i.castSucc ≤ i.succ

Tactic:
;

Goal state after:
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
⊢ i.castSucc ≤ i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
⊢ HasLiftingProperty Λ[m + 1, k].ι sq₁₃.π

Tactic:
rw [← internalHomAdjunction₂.hasLiftingProperty_iff sq₁₂]

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
⊢ HasLiftingProperty sq₁₂.ι p
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
⊢ C

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

Tactic:
;

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

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

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

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

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

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

Tactic:
;

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

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

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

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : SSet ⥤ C
⊢ (Sigma.ι (fun x ↦ F.obj Δ[n]) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)) ≫ Sigma.desc fun α ↦ F.map (yonedaEquiv.symm α)) =
    𝟙 (F.obj Δ[n])

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : SSet ⥤ C
⊢ (Sigma.ι (fun x ↦ F.obj Δ[n]) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)) ≫ Sigma.desc fun α ↦ F.map (yonedaEquiv.symm α)) =
    𝟙 (F.obj Δ[n])
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
hx : IsIndex x ⋯ 0
⊢ False

Tactic:
;

Goal state after:
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
hx : IsIndex x ⋯ 0
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
x : X.obj x✝²
⊢ (ConcreteCategory.hom (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝)).toFun x

Tactic:
;

Goal state after:
X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
x : X.obj x✝²
⊢ (ConcreteCategory.hom (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝)).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝¹ : SSet
x✝ : X ⟶ x✝¹
n✝ : SimplexCategoryᵒᵖ
x : X.obj n✝
⊢ (ConcreteCategory.hom (x✝.app n✝)).toFun x =
    (ConcreteCategory.hom ({ app := fun x ↦ ↾fun x_1 ↦ isEmptyElim x_1, naturality := ⋯ }.app n✝)).toFun x

Tactic:
;

Goal state after:
X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝¹ : SSet
x✝ : X ⟶ x✝¹
n✝ : SimplexCategoryᵒᵖ
x : X.obj n✝
⊢ (ConcreteCategory.hom (x✝.app n✝)).toFun x =
    (ConcreteCategory.hom ({ app := fun x ↦ ↾fun x_1 ↦ isEmptyElim x_1, naturality := ⋯ }.app n✝)).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x y : X _⦋0⦌
e : Edge x y
⊢ f x = f y

Tactic:
;

Goal state after:
X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x y : X _⦋0⦌
e : Edge x y
⊢ f x = f y
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
s : X _⦋0 + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
    (ConcreteCategory.hom (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s

Tactic:
;

Goal state after:
X Y Z : SSet
s : X _⦋0 + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
    (ConcreteCategory.hom (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X✝ Y Z X : SSet
s : SSet.evaluation _⦋0 + 1⦌.obj X
⊢ (ConcreteCategory.hom ((SSet.evaluation.map (SimplexCategory.δ 1).op ≫ toπ₀NatTrans).app X)).toFun s =
    (ConcreteCategory.hom ((SSet.evaluation.map (SimplexCategory.δ 0).op ≫ toπ₀NatTrans).app X)).toFun s

Tactic:
;

Goal state after:
X✝ Y Z X : SSet
s : SSet.evaluation _⦋0 + 1⦌.obj X
⊢ (ConcreteCategory.hom ((SSet.evaluation.map (SimplexCategory.δ 1).op ≫ toπ₀NatTrans).app X)).toFun s =
    (ConcreteCategory.hom ((SSet.evaluation.map (SimplexCategory.δ 0).op ≫ toπ₀NatTrans).app X)).toFun s
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

Tactic:
;

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬1 = n

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬1 = n
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

Tactic:
;

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left ≫ (G.obj (op f₁'.left)).map f₃.hom =
    sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right ≫ (G.map f₁'.hom.op).app f₃.right

Tactic:
;

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left ≫ (G.obj (op f₁'.left)).map f₃.hom =
    sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right ≫ (G.map f₁'.hom.op).app f₃.right
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    sq₁₃.snd ≫ (G.map f₁.hom.op).app f₃.right ≫ (G.obj (op f₁.left)).map (Arrow.Hom.right sq)

Tactic:
;

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    sq₁₃.snd ≫ (G.map f₁.hom.op).app f₃.right ≫ (G.obj (op f₁.left)).map (Arrow.Hom.right sq)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting

Goal state before:
pp: case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋m⦌, ⟨g, property✝⟩⟩

Tactic:
obtain rfl : f = g := unique_nonDegenerate_map _ _ _ _ rfl _ _ h

Goal state after:
case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
property✝ : Epi f
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso ⊤.ι

Tactic:
;

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso ⊤.ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = const (opObjEquiv.symm x)

Tactic:
by
    simp [stdSimplex.δ_comp_yonedaEquiv_symm, ← stdSimplex.yonedaEquiv_δ_comp,
      opObjEquiv_symm_yonedaEquiv_const, h.δ_map_of_lt k.rev (by grind)]

Goal state after:
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

Goal state before:
pp: n : SimplexCategory
⊢ Nonempty ↑(stdSimplex ℝ (Fin (n.len + 1)))

Tactic:
;

Goal state after:
n : SimplexCategory
⊢ Nonempty ↑(stdSimplex ℝ (Fin (n.len + 1)))
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

Goal state before:
pp: n : SimplexCategory
⊢ PathConnectedSpace ↑(stdSimplex ℝ (Fin (n.len + 1)))

Tactic:
;

Goal state after:
n : SimplexCategory
⊢ PathConnectedSpace ↑(stdSimplex ℝ (Fin (n.len + 1)))
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: case mk
X : TopCat
x✝ : ↑X
⊢ SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ (ZerothHomotopy.mk x✝)) =
    ZerothHomotopy.mk x✝

Tactic:
;

Goal state after:
case mk
X : TopCat
x✝ : ↑X
⊢ SSet.π₀.lift (ZerothHomotopy.mk ∘ ⇑toSSetObj₀Equiv) ⋯
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ ⇑toSSetObj₀Equiv.symm) ⋯ (ZerothHomotopy.mk x✝)) =
    ZerothHomotopy.mk x✝