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

Goal state before:
pp: case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x

Tactic:
conv_rhs => dsimp; rw [dsimp% s.π.naturality_apply α x]

Goal state after:
case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (X.map α.right.unop.hom.op))
      ((ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1))) x)
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
⊢ ∀ {X Y : A.HomotopyCategory₂} (f : X ⟶ Y), 𝟙 X ≫ f = f

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
X✝ Y✝ : A.HomotopyCategory₂
f✝ : X✝ ⟶ Y✝
f : Edge X✝.pt Y✝.pt
⊢ 𝟙 X✝ ≫ Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f = Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
⊢ ∀ {X Y : A.HomotopyCategory₂} (f : X ⟶ Y), f ≫ 𝟙 Y = f

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
X✝ Y✝ : A.HomotopyCategory₂
f✝ : X✝ ⟶ Y✝
f : Edge X✝.pt Y✝.pt
⊢ Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f ≫ 𝟙 Y✝ = Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : (∃ (h : x✝ = y✝), i = eqToHom h) ∨ x✝.len < y✝.len
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

Tactic:
rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr

Goal state after:
case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ x✝.len < z✝.len

case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ x✝.len < z✝.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha hb : a ≤ d
h : a + a = c + 1
h₁ : Epi (𝟙 { obj := { len := a }, property := ha }).hom
h₂ : Mono (𝟙 { obj := { len := a }, property := ha }).hom
⊢ W (𝟙 { obj := { len := a }, property := ha })

Tactic:
apply W.id_mem

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

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ((Hom.toOrderHom f) k) =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k

Tactic:
spine_vertex

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ((Hom.toOrderHom f) k) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋i⦌ k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 2)
⊢ i ∈ finset f x ↔ i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc

Tactic:
by
  simp [finset]

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
⊢ ∀ {n : ℕ} (x : ↑(X.nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
intro n

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
⊢ ∀ (x : ↑(X.nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
⊢ ∀ {n : ℕ} (x : ↑((nerve T).nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)

Tactic:
intro n

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
⊢ ∀ (x : ↑((nerve T).nonDegenerate n)), Mono (yonedaEquiv.symm ↑x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
⊢ ∃ u, ψ u = (↑↑t).toS

Tactic:
obtain ⟨f, _, hf⟩ := N.le_iff_exists_mono.1 t.2.2.le

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
t : T
f : ⦋(↑↑t).dim⦌ ⟶ ⦋(↑(P.p y)).dim⦌
w✝ : CategoryTheory.Mono f
hf : (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex = (↑↑t).simplex
⊢ ∃ u, ψ u = (↑↑t).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
this✝ : h.IsProper
this : IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ this.false
    ⟨fun n ↦ h.equivII (f n), fun n ↦ by simpa [ancestralRel_iff] using hf n⟩⟩

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ c.pt.HasDimensionLT n

Tactic:
← hasDimensionLT_subcomplex_top_iff,

Goal state after:
J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ ⊤.toSSet.HasDimensionLT n
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:
← hasDimensionLT_subcomplex_top_iff,

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ ⊤.toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ X₃ X₄ : SSet
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
inst✝¹ : X₂.Finite
inst✝ : X₃.Finite
Z✝ : SSet
x✝¹ x✝ : Z✝ ⟶ X₁
h : x✝¹ ≫ lift t l = x✝ ≫ lift t l
⊢ x✝¹ ≫ t = x✝ ≫ t

Tactic:
by simpa using h =≫ fst _ _

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✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
⊢ ∀ (s : X.N), s.subcomplex ≤ ⊤ → s.subcomplex ≤ ⨆ i, f.filtration i

Tactic:
intro s _

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : X.N
a✝ : s.subcomplex ≤ ⊤
⊢ s.subcomplex ≤ ⨆ i, f.filtration i
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.isoClosure ≤ isCardinalPresentable C κ

Tactic:
simpa only [ObjectProperty.isoClosure_le_iff] using h.le_isCardinalPresentable

Goal state after:
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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
⊢ ∃ a, (restrictedULiftYoneda F).map a = f

Tactic:
by
    let c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
      { pt := Z
        ι :=
          { app g := ((f.app (op g.left)) (ULift.up g.hom)).down
            naturality g₁ g₂ φ := by
              simpa [uliftFunctor, uliftYoneda,
                restrictedULiftYoneda, ← ULift.down_inj] using
                ((f.naturality_apply φ.left.op) (ULift.up g₂.hom)).symm } }
    refine ⟨(F.denseAt Y).desc c, ?_⟩
    ext ⟨X⟩ ⟨x⟩
    have := (F.denseAt Y).fac c (.mk x)
    dsimp [c] at this
    simpa using ULift.down_injective this

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

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

Tactic:
obtain ⟨_, P, hP⟩ := hf
    refine ⟨inferInstance, P.ofIso (Iso.refl _) ?_, inferInstance⟩
    simp [Subcomplex.range_comp, Subcomplex.range_eq_top e,
      Subcomplex.image_top]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
hP' : P.IsInner
⊢ strongInnerAnodyneExtensions (f ≫ e)

Tactic:
refine ⟨inferInstance, P.ofIso (asIso e).symm ?_, inferInstance, inferInstance⟩

Goal state after:
X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
hP' : P.IsInner
⊢ (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)
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 + 1)
⊢ l ∈ finset x hd ↔ (x.cast hd).simplex.1 l = k.succ

Tactic:
by
  simp [finset]

Goal state after:
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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Arrow.Hom.right
      ((fun α ↦
          Arrow.homMk (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α))
            (⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ⋯)
        ((fun β ↦
            Arrow.homMk
              (⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯)
              (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)) ⋯)
          β)) =
    Arrow.Hom.right β

Tactic:
apply sq₁₃.isPullback.hom_ext <;> simp

Goal state after:
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].ι
E B : SSet
⊢ ∀ (g : E ⟶ B), innerFibrations g → HasLiftingProperty sq₁₂.ι g

Tactic:
p

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].ι
E B : SSet
p : E ⟶ B
⊢ innerFibrations p → HasLiftingProperty sq₁₂.ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
⊢ ∀ (g : E ⟶ B), innerFibrations g → HasLiftingProperty sq₁₂.ι g

Tactic:
p

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
⊢ innerFibrations p → HasLiftingProperty sq₁₂.ι p
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].ι
E B : SSet
⊢ ∀ (g : E ⟶ B), fibrations SSet g → HasLiftingProperty sq₁₂.ι g

Tactic:
p

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].ι
E B : SSet
p : E ⟶ B
⊢ fibrations SSet p → HasLiftingProperty sq₁₂.ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
⊢ ∀ (g : E ⟶ B), fibrations SSet g → HasLiftingProperty sq₁₂.ι g

Tactic:
p

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
⊢ fibrations SSet p → HasLiftingProperty sq₁₂.ι p
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₁ ⋯).x.toN = s.x.toN

Tactic:
N.ext_iff

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (ht.type₁ ⋯).x.toS = s.x.toS
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.x.toN = t.x.toN

Tactic:
N.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.toS = t.x.toS
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,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s.δ.toN = t.δ.toN

Tactic:
N.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,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s.δ.toS = t.δ.toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (SimplicialObject.σ Δ[1] j)) (objMk₁ i) = objMk₁ i.castSucc

Tactic:
by
  ext k : 1
  exact ConcreteCategory.congr_hom (SimplexCategory.σ_comp_toMk₁_of_le _ _ h) k

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
n : ℕ
s : Type₁ k.succ n
h✝ : (pairingCore k.succ n).index s = 0
this : s.index = 0
hs : IsIndex s.x ⋯ (Fin.succ 0)
h : 0 = k.succ.castSucc
⊢ False

Tactic:
by simp [Fin.ext_iff] at h

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
          ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
        (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)).1 =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
        stdSimplex.objMk₁ j.castSucc.castSucc.succ).1

pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).2
      k

Tactic:
· simp [← SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).2
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)

Tactic:
intro n

Goal state after:
X : SSet
n : ℕ
⊢ X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
⊢ ∀ (n : ℕ) (x_1 : ↑(X.nonDegenerate n)),
    ↑x_1 ∈ (x.subcomplex ⊓ y.subcomplex).obj (op ⦋n⦌) →
      ↑x_1 ∈ (Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)).obj (op ⦋n⦌)

Tactic:
intro n

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
n : ℕ
⊢ ∀ (x_1 : ↑(X.nonDegenerate n)),
    ↑x_1 ∈ (x.subcomplex ⊓ y.subcomplex).obj (op ⦋n⦌) →
      ↑x_1 ∈ (Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)).obj (op ⦋n⦌)
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 + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ stdSimplex.δ i.succ ≫ r.map = g'.map

Tactic:
rw [δ_succ_map, hg]

Goal state after:
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
⊢ Continuous fun p ↦ ⟨↑p.1 • x + (1 - ↑p.1) • ↑p.2, ⋯⟩

Tactic:
· fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ (n : ℕ), c ^ n ≠ 0

Tactic:
intro n

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ c ^ n ≠ 0