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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')

Tactic:
let g {k k' : K} (φ : k ⟶ k') : j₀ ⟶ j φ := (H φ).choose_spec.choose

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl
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 : Mono g
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⦌)
hd : d ≤ x.dim
⊢ ∃ 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:
obtain hd | rfl := hd.lt_or_eq

Goal state after:
case inl.inl
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 : Mono g
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⦌)
hd✝ : d ≤ x.dim
hd : d < x.dim
⊢ ∃ 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

case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
hd : x.dim ≤ x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
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 κ
inst✝ : LocallySmall.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨J, _, _, ⟨hX⟩⟩ := h.exists_colimitsOfShape X
  obtain ⟨κ', _, le, hκ'⟩ : ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'),
      HasCardinalLT (Arrow J) κ' := by
    obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))
    exact ⟨κ', ⟨h₁⟩,
      le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
      h₂ (Sum.inl ⟨⟩)⟩
  have := hX.isCardinalPresentable h.le_isCardinalPresentable _ le hκ'
  exact isPresentable_of_isCardinalPresentable _ κ'

Goal state after:
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
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
⊢ ∃ j φ₁ φ₂, φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂

Tactic:
obtain ⟨j₁, f₁, hf₁⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₁
        obtain ⟨j₂, f₂, hf₂⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₂
        exact ⟨IsFiltered.max j₁ j₂, f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂),
          f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂), by simpa, by simpa⟩

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
⊢ IsCardinalPresentable (freeYoneda X M) κ

Tactic:
let e : coyoneda.obj (op (freeYoneda X M)) ≅
      (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u} :=
    NatIso.ofComponents (fun P ↦ Equiv.toIso (freeYonedaHomEquiv.trans Equiv.ulift.symm))
  constructor
  intro J _ _
  have := preservesColimitsOfShape_of_isCardinalPresentable M κ J
  exact preservesColimitsOfShape_of_natIso e.symm

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

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hA : ∃ P, ∃ (_ : ObjectProperty.Small.{w, v', u'} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable A κ
⊢ IsCardinalLocallyPresentable (Cᵒᵖ ⥤ A) κ

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

Goal state after:
A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ IsCardinalLocallyPresentable (Cᵒᵖ ⥤ 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
⊢ (x.cast hd).simplex.1 (min x hd) = k.succ

Tactic:
← mem_finset_iff

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
⊢ min x hd ∈ finset x hd
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
this : i ≤ l.castSucc
| k.castSucc

Tactic:
← hl.simplex_fst_castSucc

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
i : Fin (d + 1)
hi : ¬(x.cast hd).simplex.1 i < k.succ
this : i ≤ l.castSucc
| (x.cast hd).simplex.1 l.castSucc
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorRight X₃.left).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left ≫
        (α_ X₁.right X₂.right X₃.left).hom ≫
          X₁.right ◁
              pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
            pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) =
    (tensorRight X₃.left).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      ((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom ≫
        Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
          pushout.desc
            (X₁.right ◁
                pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
              (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            ⋯

Tactic:
simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc,
            ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := ⋯
hY₃ : IsTerminal ((G.flip.obj Y₃).obj (op X₁)) := ⋯
⊢ IsIso ((G.obj (op X₁)).map f₃)

pp: case sq
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := ⋯
hY₃ : IsTerminal ((G.flip.obj Y₃).obj (op X₁)) := ⋯
⊢ CommSq ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)

Tactic:
· exact isIso_of_isTerminal hX₃ hY₃ _

Goal state after:
case sq
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj X₃)
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.flip.obj Y₃)
h : IsInitial X₁
hX₃ : IsTerminal ((G.flip.obj X₃).obj (op X₁)) := ⋯
hY₃ : IsTerminal ((G.flip.obj Y₃).obj (op X₁)) := ⋯
⊢ CommSq ((IsTerminal.isTerminalObj (G.flip.obj X₃) (op X₁) (IsInitial.op C₁ h)).from ((G.obj (op Y₁)).obj Y₃))
    (𝟙 ((G.obj (op Y₁)).obj Y₃)) ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

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

Tactic:
· rw [stdSimplex.δ_objMk₁_of_lt, Fin.pred_succ]
      rw [Fin.castSucc_lt_succ_iff, ← Fin.castSucc_succ]
      simp only [Fin.castSucc_le_castSucc_iff]
      exact hij.trans (j.castSucc_le_succ)

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

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ (sSetTopAdj.homEquiv Δ[0] X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((ConcreteCategory.hom f) default))

Tactic:
rw [Adjunction.homEquiv_unit, TopCat.toSSetObj₀Equiv_symm_apply, this]

Goal state after:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ SSet.const (TopCat.toSSetObj₀Equiv.symm default) ≫ TopCat.toSSet.map f =
    SSet.const
      ((X.toSSetObjEquiv (op ⦋0⦌)).symm { toFun := fun x ↦ (ConcreteCategory.hom f) default, continuous_toFun := ⋯ })
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (Unique (ZerothHomotopy ↑X))

Tactic:
by
    rw [unique_iff_subsingleton_and_nonempty]
    constructor <;> infer_instance

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
⊢ #↑s = #E

Tactic:
obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1

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‖
⊢ #↑s = #E
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
h's : s.Nonempty
⊢ 𝔠 ≤ #↑s

Tactic:
by
  simpa [cardinal_eq_of_isOpen 𝕜 hs h's] using continuum_le_cardinal_of_module 𝕜 E

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ (s ∩ (fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t') = ∅

Tactic:
inter_comm s,

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ ((fun t ↦ [c + x -[ℝ] c + t • y] ∩ s) t' ∩ s) = ∅
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ (s ∩ (fun t ↦ [c - x -[ℝ] c + t • y] ∩ s) t') = ∅

Tactic:
inter_comm s,

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c - x -[ℝ] c + t • y] ∩ ((fun t ↦ [c - x -[ℝ] c + t • y] ∩ s) t' ∩ s) = ∅
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos.inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
⊢ v 0 ^ (log (w a) / log (v a)) = w 0

Tactic:
simp [zero_rpow (by linarith [h.log_div_log_pos ha₀ ha₁])]

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

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

Tactic:
simp [hf]

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
ε : ℝ
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ E ≃ₜ F

Tactic:
by
  refine
    (hf.toOpenPartialHomeomorph _ _ hc isOpen_univ).toHomeomorphOfSourceEqUnivTargetEqUniv rfl ?_
  rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]
  exact hf.surjective hc

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: n : ℕ
x : ℂ
hx : x ∈ slitPlane
h_eq : deriv log =ᶠ[𝓝 x] Inv.inv
⊢ iteratedDeriv n Inv.inv x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)

Tactic:
iteratedDeriv_eq_iterate,

Goal state after:
n : ℕ
x : ℂ
hx : x ∈ slitPlane
h_eq : deriv log =ᶠ[𝓝 x] Inv.inv
⊢ deriv^[n] Inv.inv x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1

Tactic:
suffices ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ -(-1 : ℂ) ^ n / n)) =
      FormalMultilinearSeries.ofScalars ℂ (fun n ↦ iteratedDeriv n log 1 / (n.factorial : ℂ))) by
    convert! AnalyticAt.hasFPowerSeriesAt _ using 1 <;> try infer_instance
    exact analyticAt_clog (by simp)

Goal state after:
⊢ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt (fun x ↦ log (1 + x)) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 0

Tactic:
convert HasFPowerSeriesAt.comp_sub hasFPowerSeriesAt_clog_one (-1) using 3 <;> ring

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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
ho : analyticOrderAt f z₀ = ↑(n + 1)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k : ℕ
hk : 0 < n + 1
⊢ iteratedDeriv 0 f z₀ = 0

Tactic:
iteratedDeriv_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
ho : analyticOrderAt f z₀ = ↑(n + 1)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k : ℕ
hk : 0 < n + 1
⊢ f z₀ = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
rw [hg_nc]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
this : analyticOrderAt (fun x ↦ (f ∘ g) x - (f ∘ g) z₀) z₀ = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤