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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∈
    X.nonDegenerate n

Tactic:
nonDegenerate_iff_of_mono,

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∈ Δ[n + 1].nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ (↑x).IsUniquelyCodimOneFace (↑(h.pairing.p x)).toS

Tactic:
obtain ⟨s, rfl⟩ := h.equivII.surjective x

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ (↑(h.equivII s)).IsUniquelyCodimOneFace (↑(h.pairing.p (h.equivII s))).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ ∀ {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ 0

Tactic:
obtain ⟨s, rfl⟩ := h.equivII.surjective x

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ∀ {d : ℕ} (hd : (↑(h.equivII s)).dim = d), ⋯.index hd ≠ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
x : ↑h.pairing.II
⊢ ∀ {d : ℕ} (hd : (↑x).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
obtain ⟨s, rfl⟩ := h.equivII.surjective x

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ∀ {d : ℕ} (hd : (↑(h.equivII s)).dim = d), ⋯.index hd ≠ Fin.last (d + 1)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    ((evaluation D C).obj k).mapCone (combine f g c hc)

Tactic:
refine Cone.ext (Iso.refl _) ?_
      rintro (_ | _ | _)
      all_goals cat_disch

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

Goal state before:
pp: case a.notMem.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ P.AncestralRel t c.s

Tactic:
replace hs : t.val.subcomplex ≤ c.horn.image c.map := by
          obtain rfl | rfl := ht
          · exact hs
          · refine le_trans ?_ hs
            rw [← S.le_def]
            exact (P.isUniquelyCodimOneFace t).le

Goal state after:
case a.notMem.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ P.AncestralRel t c.s
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
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌)))) ∈
    (f.sigmaStdSimplex j).nonDegenerate (c.dim + 1)

Tactic:
nonDegenerate_iff_of_mono,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))) ∈ Δ[c.dim + 1].nonDegenerate (c.dim + 1)
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
j : ι
c : f.Cell j
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) ∈
    (f.sigmaStdSimplex j).nonDegenerate c.dim

Tactic:
nonDegenerate_iff_of_mono,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ c.index) ∈ Δ[c.dim + 1].nonDegenerate c.dim
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
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs hs'✝ =
        Cell.type₂ f c

Tactic:
nonDegenerate_iff_of_mono,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : stdSimplex.objEquiv.symm g ∈ Δ[x.dim + 1].nonDegenerate d
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
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 : f.Cell j
⊢ c.ιSigmaStdSimplex ≫ f.b j = c.mapToSucc

Tactic:
simp [b]

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✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ A.obj d ∨ ∃ i ≤ j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

Tactic:
obtain hx | ⟨i, hi, c, hx⟩ := hx

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ A.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x
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:
refine (isColimitMapCoconePushoutCoconeEquiv _ _).symm
      (IsPushout.isColimit ?_)

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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsPushout (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.t j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (homOfLE ⋯))
    (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable

Goal state before:
pp: case refine_2
X : SSet
inst✝ : X.Finite
⊢ Epi (Sigma.desc fun s ↦ yonedaEquiv.symm s.simplex)

Tactic:
simp only [← Subcomplex.range_eq_top_iff, range_eq_iSup_sigma_ι,
        colimit.ι_desc, Cofan.mk_ι_app, ← N.iSup_subcomplex_eq_top,
        Subcomplex.range_eq_ofSimplex, Equiv.apply_symm_apply]

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

Goal state before:
pp: ⊢ modelCategoryQuillen.J.rlp.llp =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts

Tactic:
llp_rlp_of_hasSmallObjectArgument

Goal state after:
⊢ (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerHornInclusions.rlp.llp =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

Tactic:
llp_rlp_of_hasSmallObjectArgument

Goal state after:
⊢ (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
hA : strongInnerAnodyneExtensions A.ι
⊢ ∃ B P, ∃ (h : P.IsRegular), P.IsInner ∧ B = A

Tactic:
obtain ⟨_, P₁, _, P₂⟩ := hA

Goal state after:
X : SSet
A : X.Subcomplex
left✝ : Mono A.ι
P₁ : (Subcomplex.range A.ι).Pairing
w✝ : P₁.IsRegular
P₂ : P₁.IsInner
⊢ ∃ B P, ∃ (h : P.IsRegular), P.IsInner ∧ B = A
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
i : Fin (d + 1)
hi : (x.cast hd).simplex.1 i = k.succ
⊢ l.succ ≤ i

Tactic:
simp [← hl.succ_le_simplex_fst_iff, ← hi]

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
⊢ innerFibrations sq₁₃.π

Tactic:
intro _

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✝ : SSet
⊢ ∀ ⦃Y : SSet⦄ (g : X✝ ⟶ Y), innerHornInclusions g → HasLiftingProperty g sq₁₃.π
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
⊢ J.rlp sq₁₃.π

Tactic:
intro _

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
X✝ : SSet
⊢ ∀ ⦃Y : SSet⦄ (g : X✝ ⟶ Y), J g → HasLiftingProperty g sq₁₃.π
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
⊢ anodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp
  let sq₁₃ := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom i p
  rw [internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃]
  apply hj
  rw [← HomotopicalAlgebra.fibration_iff] at hp ⊢
  exact fibration_pullbackObjObjπ sq₁₃

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 + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
⊢ IsType₂ hl.δ

Tactic:
intro _

Goal state after:
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
d✝ : ℕ
⊢ ∀ (hd_1 : hl.δ.dim = d✝) (l_1 : Fin (d✝ + 1)), ¬IsIndex hl.δ hd_1 l_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
change φ s.δ rfl i = _

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

Goal state before:
pp: case neg
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.δ ⋯ i = (objEquiv (s.x.cast ⋯).simplex) i

Tactic:
φ_of_ne _ rfl _ hi

Goal state after:
case neg
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
⊢ (objEquiv (s.δ.cast ⋯).simplex) ((min s.δ ⋯).predAbove i) = (objEquiv (s.x.cast ⋯).simplex) i
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 : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : ¬IsType₂ x
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
simp only [IsType₂, not_forall, not_not] at hx

Goal state after:
case neg
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
hx : ∃ x_1, ∃ (h : x.dim = x_1), ∃ x_2, IsIndex x ⋯ x_2
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }
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
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₂
x✝ : x✝² ⟶ x✝¹
⊢ Arrow.Hom.right
      ((𝟭 (Arrow C₂)).map x✝ ≫
        Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝¹.left) ((F.obj X₁.left).map x✝¹.hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝¹).right))) ⋯)
          ⋯) =
    Arrow.Hom.right
      (Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
          (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app x✝².left) ((F.obj X₁.left).map x✝².hom)))
            (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj x✝²).right))) ⋯)
          ⋯ ≫
        (F.leibnizPushout.obj X₁ ⋙ G.leibnizPullback.obj (op X₁)).map x✝)

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

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 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 [St, mem_finset_iff] using ht.simplex_fst_succ

Goal state after:
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, ⋯⟩
⊢ x.subcomplex ⊓ y.subcomplex ≤
    Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

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 : X.PtSimplex n x
i : Fin (n + 1)
⊢ stdSimplex.δ i.castSucc ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
rw [CosimplicialObject.δ_comp_σ_self_assoc]

Goal state after:
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
⊢ stdSimplex.δ j.castSucc.castSucc ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = f.op.map

Tactic:
by
    rw [stdSimplex.δ_comp_yonedaEquiv_symm, op_δ, Equiv.apply_symm_apply,
      ← stdSimplex.yonedaEquiv_δ_comp, opEquiv_symm_apply_map, ← h.δ_succ_succ_map,
      Fin.rev_castSucc, Fin.rev_castSucc, ← hij, Fin.rev_rev]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ 𝔠 ≤ #𝕜

Tactic:
suffices ∃ f : (ℕ → Bool) → 𝕜, range f ⊆ univ ∧ Continuous f ∧ Injective f by
    rcases this with ⟨f, -, -, f_inj⟩
    simpa using lift_mk_le_lift_mk_of_injective f_inj
  apply Perfect.exists_nat_bool_injection _ univ_nonempty
  refine ⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩
  rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, c_pos, hc⟩
  have A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 (x + 0)) :=
    tendsto_const_nhds.add (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc)
  rw [add_zero] at A
  have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A U hU
  rcases B.exists with ⟨n, hn⟩
  refine ⟨x + c^n, by simpa using hn, ?_⟩
  simp only [add_ne_left]
  apply pow_ne_zero
  simpa using c_pos

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
⊢ HasFPowerSeriesOnBall f p x r

Tactic:
have hg : HasFPowerSeriesOnBall g p x p.radius := by
    simpa using (p.hasFPowerSeriesOnBall (by order)).comp_sub x

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
⊢ HasFPowerSeriesOnBall f p x r
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt f z₀ ≠ 0 ↔ AnalyticAt 𝕜 f z₀ ∧ f z₀ = 0

Tactic:
simp [analyticOrderAt_eq_zero]

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
by_cases hf : AnalyticAt 𝕜 f z₀
  · refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.neg]
    exact (Equiv.neg _).exists_congr <| by simp [neg_eq_iff_eq_neg]
  · rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt <| analyticAt_neg.not.2 hf]

Goal state after: