mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt := ⋯
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ { down := s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) }.down = { down := x ≫ s.ι.app j }.down

Tactic:
simpa using

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
X : C
x : (yoneda.obj (F.obj j.left)).obj (F.op.obj (op X))
α : CostructuredArrow.mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x) ⋯
this : F.map (F.preimage x) ≫ s.ι.app j = s.ι.app (CostructuredArrow.mk (x ≫ j.hom))
⊢ s.ι.app (CostructuredArrow.mk (x ≫ j.hom)) = x ≫ s.ι.app j
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
⊢ (ObjectProperty.ofObj Subtype.val).IsSeparating

Tactic:
simpa using

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
⊢ P.IsSeparating
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
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
⊢ φ₁ ≫ (E.coconeAt X).ι.app j = φ₂ ≫ (E.coconeAt X).ι.app j

Tactic:
simpa using

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 κ
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
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
⊢ φ₁ ≫ (StructuredArrow.hom E).app j.left ≫ (StructuredArrow.right E).map j.hom =
    φ₂ ≫ (StructuredArrow.hom E).app j.left ≫ (StructuredArrow.right E).map j.hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
⊢ B = A

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
⊢ B = A
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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsColimit
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCocone (PushoutCocone.mk (homOfLE ⋯) (f.b j) ⋯))

Tactic:
by
    refine (isColimitMapCoconePushoutCoconeEquiv _ _).symm
      (IsPushout.isColimit ?_)
    refine Types.isPushout_of_isPullback_of_mono'
      ((f.isPullback j).map ((CategoryTheory.evaluation _ _).obj _))
      (f.range_homOfLE_app_union_range_b_app _ _) (fun x₁ x₂ hx₁ hx₂ h ↦ ?_)
    obtain ⟨s₁, g₁, _, hg₁⟩ := (Subcomplex.range (f.m j)).existsN x₁ hx₁
    obtain ⟨s₂, g₂, _, hg₂⟩ := (Subcomplex.range (f.m j)).existsN x₂ hx₂
    obtain rfl : s₁ = s₂ := f.isPushout_aux₃ (by
      dsimp
      rw [S.eq_iff_ofSimplex_eq, ← Subcomplex.ofSimplex_map_of_epi g₁,
        ← Subcomplex.ofSimplex_map_of_epi g₂]
      · simp [← dsimp% (f.b j).naturality_apply, hg₁, hg₂, dsimp% h]
      all_goals
      · rw [Subcomplex.mem_nonDegenerate_iff]
        apply f.isPushout_aux₁)
    obtain rfl := X.unique_nonDegenerate_map (x := (((f.b _)).app _ x₁).val)
      g₁ ⟨_, f.isPushout_aux₁ s₁⟩
        (by simp [mapN, ← hg₁, dsimp% NatTrans.naturality_apply (f.b j)])
      g₂ ⟨_, f.isPushout_aux₁ s₁⟩
        (by simp [mapN, dsimp% h, ← hg₂, dsimp% NatTrans.naturality_apply (f.b j)])
    rw [← hg₁, hg₂]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑P.op.II
hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.AncestralRel ((fun n ↦ ⟨N.opEquiv ↑(f n), ⋯⟩) (n + 1)) ((fun n ↦ ⟨N.opEquiv ↑(f n), ⋯⟩) n)

Tactic:
simpa using

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑P.op.II
hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.op.AncestralRel (f (n + 1)) (f 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 : ℕ
hd : x.dim = d
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ i ∈ finset x hd

Tactic:
simpa using

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ (x.cast hd).simplex.1 i = k.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h✝ : k.succ ≤ (x.cast hd).simplex.1 i
h : k.succ = (x.cast hd).simplex.1 i
⊢ i ∈ finset x hd

Tactic:
simpa using

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h✝ : k.succ ≤ (x.cast hd).simplex.1 i
h : k.succ = (x.cast hd).simplex.1 i
⊢ (x.cast hd).simplex.1 i = k.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
simpa using

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
⊢ (x.cast hd).simplex.1 l.succ = k.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
h₁ : ⋯.type₁ ⋯ = hl'.type₁
h₂ : ⋯.type₁ ⋯ = hl.type₁
⊢ x = y

Tactic:
exact congr_arg Type₁.x (h₂.symm.trans h₁)

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 : s.δ = t.δ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hs : s.δ = u
⊢ IsType₂ u

Tactic:
simpa using

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
h : s.δ = t.δ
u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hs : s.δ = u
⊢ IsType₂ u
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case refine_1
p : ℕ
x✝¹ x✝ : Fin (p + 1)
h :
  (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝¹ =
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
case refine_1
p : ℕ
x✝¹ x✝ : Fin (p + 1)
h :
  (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝¹ =
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) x✝
⊢ x✝¹ = x✝
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 d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
h : is.castSucc ∈ Ss
⊢ s.1 is.castSucc ≤ k.castSucc

Tactic:
simpa using

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
h : is.castSucc ∈ Ss
⊢ s.1 is.castSucc ≤ k.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A ≤ B.preimage f.map

Tactic:
simpa using

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A.image f.map ≤ B
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⦌
hx : x ∈ X.nonDegenerate n
⊢ X.ιNormalizedChainComplex x = Sigma.ι (fun x ↦ R) ⟨x, hx⟩

Tactic:
dsimp [ιNormalizedChainComplex, ιChainComplex]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Sigma.ι (fun x ↦ R) x ≫ (X.toNormalizedChainComplex R).f n = Sigma.ι (fun x ↦ R) ⟨x, hx⟩
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 d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ it.succ ∈ St

Tactic:
simpa using

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ t.1 it.succ = k.succ
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 Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x✝ : ↑(X.nonDegenerate n)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ (Cofan.mk (∐ fun x ↦ R) (Sigma.ι fun x ↦ R)).inj ⟨x, hx⟩ ≫
      (Iso.refl (Cofan.mk (∐ fun x ↦ R) (Sigma.ι fun x ↦ R)).pt).hom =
    (X.cofanNormalizedChainComplex R n).inj ⟨x, hx⟩

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x✝ : ↑(X.nonDegenerate n)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Sigma.ι (fun x ↦ R) ⟨x, hx⟩ = X.ιNormalizedChainComplex x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.right.inl
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ it.succ ∈ St ↔ it.succ ∈ Finset.image it.succ.succAbove Sδ ∪ {it.succ}

Tactic:
have : it.succ ∈ St := by
            simpa [St, mem_finset_iff] using ht.simplex_fst_succ

Goal state after:
case inr.right.inl
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := finset (Subcomplex.N.mk s hs₁ hs₂) ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := finset (Subcomplex.N.mk t ht₁ ht₂) ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := finset hs.δ ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
this : it.succ ∈ St
⊢ it.succ ∈ St ↔ it.succ ∈ Finset.image it.succ.succAbove Sδ ∪ {it.succ}
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 Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιNormalizedChainComplex x ≫ (normalizedChainComplexMap f R).f n =
    Y.ιNormalizedChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ (X.ιChainComplex x ≫ (X.toNormalizedChainComplex R).f n) ≫ (normalizedChainComplexMap f R).f n =
    Y.ιChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x) ≫ (Y.toNormalizedChainComplex R).f 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
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this : s.index = 0
⊢ IsIndex s.x ⋯ (Fin.succ 0)

Tactic:
simpa using

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
this : s.index = 0
⊢ IsIndex s.x ⋯ 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
obtain rfl | hj := (Fin.le_castSucc_iff.mpr hj).eq_or_lt

Goal state after:
case inl
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
hj : i.castSucc.castSucc < i.castSucc.succ
⊢ stdSimplex.δ i.castSucc.castSucc ≫ h.map = const x

case inr
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj✝ : j < i.castSucc.succ
hj : j < i.castSucc.castSucc
⊢ stdSimplex.δ j ≫ h.map = const x
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
x : α
hx : x ∈ s
⊢ x ∈ u

Tactic:
simpa using

Goal state after:
α ι : Type u
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
n : ℕ
h'f : ∀ (i : ι), #↑(f i) ≤ ↑n
ha : ↑n < ℵ₀
s : Finset α
hs : ↑s ⊆ t
A : ∀ x ∈ s, ∀ᶠ (i : ι) in l, x ∈ f i
B : ∀ᶠ (i : ι) in l, ∀ x ∈ s, x ∈ f i
i : ι
hi : ∀ x ∈ s, x ∈ f i
this : (i : ι) → Fintype ↑(f i)
u : Finset α := (f i).toFinset
x : α
hx : x ∈ s
⊢ x ∈ f i