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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ J Λ[n, i].ι

Tactic:
by
  obtain _ | n := n
  · exact (NeZero.ne 0 rfl).elim
  · simp only [J, iSup_iff]
    exact ⟨n, ⟨i⟩⟩

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

Tactic:
rw [← (equivalence_rel' f g).quot_mk_eq_iff]

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ x ∈ (X.skeleton n).obj (op ⦋i⦌)

Tactic:
obtain ⟨j, f, _, y, rfl⟩ := X.exists_nonDegenerate x
  suffices Subcomplex.ofSimplex y.1 ≤ X.skeleton n from
    (X.skeleton n).map _ (this _ (Subcomplex.mem_ofSimplex_obj _))
  exact le_trans (by exact le_trans (by rfl) (le_iSup _ y))
    (le_iSup _ ⟨j, lt_of_le_of_lt
      (SimplexCategory.len_le_of_epi f) hi⟩)

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

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc i) ⋯ hm).op))
      ((ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x) =
    (ConcreteCategory.hom (Y.map (tr (mkOfSucc i) ⋯ hm).op))
      ((ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x)

Tactic:
by simp [← NatTrans.naturality_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝² : BinaryFan X Y
x✝¹ : x✝².pt ⟶ of (↑X × ↑Y)
h1 : x✝¹ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝².fst
h2 : x✝¹ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝².snd
x✝ : ↑x✝².pt
⊢ (x✝¹.toFunctor.obj x✝).2 = ((x✝².fst.toFunctor.prod' x✝².snd.toFunctor).toCatHom.toFunctor.obj x✝).2

Tactic:
by simp [← h2]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯

Tactic:
cases β

Goal state after:
case refl.refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
β : f ⟶ g
base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝ }.base = base β
⊢ { base' := base'✝ } = β

Tactic:
cases β

Goal state after:
case mk'.mk'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
X Y : CatEnrichedOrdinary C
f g : X ⟶ Y
base'✝¹ base'✝ : homEquiv f ⟶ homEquiv g
H : { base' := base'✝¹ }.base = { base' := base'✝ }.base
⊢ { base' := base'✝¹ } = { base' := base'✝ }
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯

Tactic:
cases β

Goal state after:
case refl.refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
⊢ F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) ≫ f.app d✝ =
    (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g

Tactic:
have := a.naturality g h
      change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _
      aesop

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

Goal state before:
pp: case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
X Y : Cat.FreeRefl (OneTruncation₂ V)
fst✝¹ fst✝ : OneTruncation₂ V
e : fst✝¹ ⟶ fst✝
⊢ morphismPropertyHomMk V ((quotientFunctor V).map (Cat.FreeRefl.homMk ⟨fst✝¹, ⟨fst✝, e⟩⟩.snd.snd))

Tactic:
exact morphismPropertyHomMk_of_edge e

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
by simp only [Fin.mk_le_mk]; omega

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
⊢ ⟨i + k, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
by simp only [Fin.mk_le_mk]; omega

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
⊢ (if j₁.castSucc < i then 0 else 1) ≤ if j₂.castSucc < i then 0 else 1

Tactic:
split_ifs <;> grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → l ≤ k.as

Tactic:
by
      rintro (h | h)
      exacts [(f.le_right _ h).trans (Path.le g), (g.le_right l h)]

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.S
hxy' :
  { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }
⊢ x.IsUniquelyCodimOneFace y

Tactic:
by simpa using hxy'.of_iso e.symm

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p t)).cast ⋯).simplex }
⊢ s = t

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl,
      (P.isUniquelyCodimOneFace t).δ_index rfl] at h
    rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff]

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

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ (X₁ ⊗ X₂).HasDimensionLT n

Tactic:
by
  rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_subcomplexOfSimplex_prod_eq_top]
  simp only [Subcomplex.ofSimplexProd_eq_range, hasDimensionLT_iSup_iff]
  intro x₁ x₂
  have := X₁.dim_lt_of_nonDegenerate ⟨_, x₁.nonDegenerate⟩ d₁
  have := X₂.dim_lt_of_nonDegenerate ⟨_, x₂.nonDegenerate⟩ d₂
  have := (Δ[x₁.dim] ⊗ Δ[x₂.dim]).hasDimensionLT_of_le (x₁.dim + x₂.dim + 1) n
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : isCardinalPresentable C κ X
⊢ isCardinalPresentable C κ Y

Tactic:
rw [isCardinalPresentable_iff] at hX ⊢
    exact h.isCardinalPresentable κ

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

Goal state before:
pp: case a.mem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : X.N
hs : s.subcomplex ≤ c.horn.image c.map
hs' : s.subcomplex ≤ A
⊢ s.subcomplex ≤ f.filtration j

Tactic:
| mem s hs' =>

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ Y
h✝ : ExtremalEpi p
⊢ IsIso i

Tactic:
replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ Y
h✝ : ExtremalEpi p
hi : ∀ (j : ι), ∃ a, (fun f ↦ f ≫ i) a = c.inj j ≫ p
⊢ IsIso i
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
⊢ Q ◁ inl ≫ Q ◁ hP.desc h k w = Q ◁ h

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
⊢ Q ◁ (inl ≫ hP.desc h k w) = Q ◁ h
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
⊢ Q ◁ inr ≫ Q ◁ hP.desc h k w = Q ◁ k

Tactic:
← MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
⊢ Q ◁ (inr ≫ hP.desc h k w) = Q ◁ k
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
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ f ▷ Z ▷ W ≫ (α_ B Z W).hom ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
associator_naturality_left_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ (α_ A Z W).hom ≫ f ▷ (Z ⊗ W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1.inl
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
⊢ min x hd ≤ i

pp: case refine_1.inr
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
⊢ min x hd ≤ i

Tactic:
· by_contra! h'
      have := stdSimplex.monotone_apply (x.cast hd).simplex.1 h'.le
      dsimp at this
      rw [simplex_fst_min, ← not_lt] at this
      tauto

Goal state after:
case refine_1.inr
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
⊢ min x hd ≤ i
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₃
⊢ (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α) ≫ (Arrow.mk sq₁₃.π).hom) ≫ sq₁₃.fst =
    ((Arrow.mk f₂).hom ≫ ⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ≫
      sq₁₃.fst

Tactic:
simp [← adj₂.homEquiv_naturality_two,
                ← adj₂.homEquiv_naturality_one,
                sq₁₂.isPushout.w_assoc]

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 : ℕ
hd : x.dim = d
⊢ (φ x hd (min x hd).succ).2 = (φ x hd (min x hd).castSucc).2

Tactic:
by
  have := φ_succAbove x hd (min x hd)
  simp_all [φ_castSucc]

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.simplex hd ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)

Tactic:
by
  refine fun h ↦ (x.cast hd).notMem ?_
  rw [← hx.δ_simplex hd]
  exact (Subcomplex.unionProd.{u} Λ[m + 1, k.castSucc] ∂Δ[n]).map
    (SimplexCategory.δ (min x hd).castSucc).op h

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ ht.type₁ ⋯ = s

Tactic:
Type₁.ext_iff,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x = s.x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
| φ s.δ ⋯ s.index.castSucc

Tactic:
rw [← s.isIndex.min_δ]

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
| φ s.δ ⋯ (min ⋯.δ ⋯).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.e_6
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ (min ⋯.δ ⋯).castSucc
⊢ s.index.castSucc.succAbove ((min s.δ ⋯).predAbove i) = i

Tactic:
rw [← s.isIndex.min_δ]

Goal state after:
case neg.e_6
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i ≠ (min ⋯.δ ⋯).castSucc
⊢ (min ⋯.δ ⋯).castSucc.succAbove ((min s.δ ⋯).predAbove i) = 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
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:
Type₁.ext_iff,

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 : { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } = { dim := t.d + 1, simplex := (t.x.cast ⋯).simplex }
⊢ s.x = t.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 : ℕ
s t : Type₁ k n
hst :
  { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ False

Tactic:
replace hst : s.x = t.isIndex.δ := by
      rwa [Subcomplex.N.ext_iff, N.ext_iff, ← s.x.cast_eq_self s.hd]

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

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

Tactic:
split_ifs <;> grind

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

Goal state before:
pp: case inr.left.inr
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
i : Fin (d + 1)
⊢ is.castSucc.succAbove i ∈ Ss ↔ is.castSucc.succAbove i ∈ Finset.image is.castSucc.succAbove Sδ

Tactic:
· simp [hSs]

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 + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, Fin.castSucc 0].unionProd ∂Δ[n]).op.preimage
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
          Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n]).hom =
    Λ[m + 1, k].unionProd ∂Δ[n]

Tactic:
dsimp
          rw [hk, Subcomplex.preimage_comp,
            Subcomplex.preimage_op_unionProd,
            Subcomplex.preimage_unionProd,
            op_boundary, op_horn, Fin.rev_zero]

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

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairing k.castSucc n).IsRegular

Tactic:
rw [pairing_castSucc]

Goal state after:
case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairingCore k n).pairing.IsRegular
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

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
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)

Tactic:
apply pullback.hom_ext <;> simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

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

Goal state before:
pp: case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      0 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 0

Tactic:
rw [spineEquiv_f₂_arrow_zero]

Goal state after:
case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ f₁
      ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op))
        ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x)) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 0