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

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n

Tactic:
rw [nonDegenerate_iff_injective_objEquiv]
    intro h a b hab
    simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h
    rw [← h a, ← h b, Fin.ext_iff]
    change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2
    simp only [hab]

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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ { dim := c.dim + 1, simplex := ((↑(P.p c.s)).cast ⋯).simplex }.subcomplex = (↑(P.p c.s)).subcomplex

Tactic:
← S.cast_eq_self _ (P.dim_p c.s)

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ { dim := c.dim + 1, simplex := ((↑(P.p c.s)).cast ⋯).simplex }.subcomplex = ((↑(P.p c.s)).cast ⋯).subcomplex
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₀ z, ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)

Tactic:
by
    have H (k : K) := Types.jointly_surjective_of_isColimit (hF k) (y.1 k)
    let j (k : K) : J := (H k).choose
    let z (k : K) : (F.obj k).obj (X.obj (j k)) := (H k).choose_spec.choose
    have hz (k : K) : (F.obj k).map (cX.ι.app (j k)) (z k) = y.1 k :=
      (H k).choose_spec.choose_spec
    exact ⟨IsCardinalFiltered.max j (hasCardinalLT_of_hasCardinalLT_arrow hK),
      fun k ↦ (F.obj k).map (X.map (IsCardinalFiltered.toMax j _ k)) (z k),
        fun k ↦ by rw [← hz, ← comp_apply, ← Functor.map_comp, cX.w]; rfl⟩

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

Goal state before:
pp: case a.notMem.refine_2.refine_1
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
⊢ t ≠ c.s

pp: case a.notMem.refine_2.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
⊢ ↑t < ↑(P.p c.s)

Tactic:
· rintro rfl
          exact c.subcomplex_not_le_image_horn hs

Goal state after:
case a.notMem.refine_2.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
⊢ ↑t < ↑(P.p c.s)
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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
j₁ : K → J := fun k ↦ ⋯.choose
f : (k : K) → j ⟶ j₁ k := fun k ↦ ⋯.choose
hf :
  ∀ (k : K),
    (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₁ k) =
      (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₂ k)
hK' : HasCardinalLT K κ
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
let ψ (k : K) : j ⟶ IsCardinalFiltered.max j₁ hK' :=
    f k ≫ IsCardinalFiltered.toMax j₁ hK' k

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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
j₁ : K → J := fun k ↦ ⋯.choose
f : (k : K) → j ⟶ j₁ k := fun k ↦ ⋯.choose
hf :
  ∀ (k : K),
    (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₁ k) =
      (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₂ k)
hK' : HasCardinalLT K κ
ψ : K → (j ⟶ IsCardinalFiltered.max j₁ hK') := fun k ↦ f k ≫ IsCardinalFiltered.toMax j₁ hK' k
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) 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 : ι
c : f.Cell j
⊢ { dim := c.dim + 1,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim + 1⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
              (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌)))) } =
    { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

Tactic:
← S.cast_eq_self _ (P.dim_p c.s)

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 : ι
c : f.Cell j
⊢ { dim := c.dim + 1,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim + 1⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
              (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌)))) } =
    { dim := ((↑(P.p c.s)).cast ⋯).dim, simplex := ((↑(P.p c.s)).cast ⋯).simplex }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: 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₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ (𝟭 C₂).map ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      (𝟭 C₂).map
        (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)

Tactic:
apply PullbackObjObj.hom_ext

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ ((𝟭 C₂).map ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.fst

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₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ ((𝟭 C₂).map ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
            (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)) ≫
      sq₁₃'.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: 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₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (𝟭 C₂).map ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      (𝟭 C₂).map
        (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
          (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)

Tactic:
apply PullbackObjObj.hom_ext

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ ((𝟭 C₂).map ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.fst

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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ ((𝟭 C₂).map ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.snd
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ ((𝟭 C₂).map ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.fst =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.fst

Tactic:
simp [← Functor.map_comp]

Goal state after:
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₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₃ Y₃ : C₃
f₃✝¹ : X₃ ⟶ Y₃
sq✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ ((𝟭 C₂).map ((G.obj (op f₁.right)).map (Arrow.Hom.left sq)) ≫ (Arrow.mk sq₁₃'.π).hom) ≫ sq₁₃'.snd =
    ((Arrow.mk sq₁₃.π).hom ≫
        (𝟭 C₂).map
          (⋯.lift (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq))
            (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ⋯)) ≫
      sq₁₃'.snd

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha : f a ∈ Finset.image (⇑f) s.finset
b : X
hb' : b ∈ s.finset
hb : f b ∈ Finset.image (⇑f) s.finset
h : ⟨b, hb'⟩ ≤ ⟨a, ha'⟩
⊢ ⟨f a, ha⟩ ≤ ⟨f b, hb⟩ ∨ ⟨f b, hb⟩ ≤ ⟨f a, ha⟩

Tactic:
exact Or.inr (f.monotone h)

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₀ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    (SSet.RelativeMorphism.botEquiv.symm (TopCat.toSSet.map f)).map

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ SSet.ι₁ ≫ TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    (SSet.RelativeMorphism.botEquiv.symm (TopCat.toSSet.map g)).map

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a

Tactic:
by
  rcases lt_or_ge a ℵ₀ with ha | ha
  /- case `a` finite. In this case, it suffices to show that any finite subset `s` of `t` has
  cardinality at most `a`. For this, we pick `i` such that `f i` contains all the points in `s`,
  and apply the assumption that the cardinality of `f i` is at most `a`.   -/
  · obtain ⟨n, rfl⟩ : ∃ (n : ℕ), a = n := lt_aleph0.1 ha
    apply mk_le_iff_forall_finset_subset_card_le.2 (fun s hs ↦ ?_)
    have A : ∀ x ∈ s, ∀ᶠ i in l, x ∈ f i := fun x hx ↦ ht x (hs hx)
    have B : ∀ᶠ i in l, ∀ x ∈ s, x ∈ f i := (s.eventually_all).2 A
    rcases B.exists with ⟨i, hi⟩
    have : ∀ i, Fintype (f i) := fun i ↦ (lt_aleph0_iff_fintype.1 ((h'f i).trans_lt ha)).some
    let u : Finset α := (f i).toFinset
    have I1 : s.card ≤ u.card := by
      have : s ⊆ u := fun x hx ↦ by simpa only [u, Set.mem_toFinset] using hi x hx
      exact Finset.card_le_card this
    have I2 : (u.card : Cardinal) ≤ n := by
      convert! h'f i; simp only [u, Set.toFinset_card, mk_fintype]
    exact I1.trans (Nat.cast_le.1 I2)
  -- case `a` infinite:
  · have : t ⊆ ⋃ i, f i := by
      intro x hx
      obtain ⟨i, hi⟩ : ∃ i, x ∈ f i := (ht x hx).exists
      exact mem_iUnion_of_mem i hi
    calc #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
      _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
      _ ≤ sum (fun _ ↦ a) := sum_le_sum _ _ h'f
      _ = #ι * a := by simp
      _ ≤ ℵ₀ * a := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha

Goal state after:
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 g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
· refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.congr hfg]
    congr! 3
    exact hfg.congr_left

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀
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
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)

Tactic:
by
  apply continuousOn_iff_continuous_domRestrict.2
  refine ((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous
  exact fun x hx => (hf.toPartialEquiv hc).map_target hx

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

Goal state before:
pp: case h₁
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.fst).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.fst).toFunctor

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₂
X Y : SSet
m : ℕ
⊢ (prodComparison hoFunctor X Δ[m] ≫ prod.snd).toFunctor =
    ((hoFunctor.map (prod.braiding X Δ[m]).hom ≫
          prodComparison hoFunctor Δ[m] X ≫ (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)).hom) ≫
        prod.snd).toFunctor

Tactic:
simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε

Tactic:
by
    simpa [dist_eq_norm] using tendsto_nhdsWithin_nhds.1 h ε ε_pos

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
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₀ = ⊤
hf' : ¬f (g z₀) = 0
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * ⊤

Tactic:
· rw [show analyticOrderAt f (g z₀) = 0 from ?_, zero_mul] <;>
      grind [hf.comp hg, AnalyticAt.analyticOrderAt_eq_zero]

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
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬AnalyticAt 𝕜 f (g z₀)
⊢ ¬AnalyticAt 𝕜 (f ∘ g) z₀

Tactic:
rwa [analyticAt_comp_iff_of_deriv_ne_zero hg hg']

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case succ
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
hm : MeromorphicAt (f ^ m) x
⊢ MeromorphicAt (f ^ (m + 1)) x

Tactic:
simpa only [pow_succ] using! hm.mul hf

Goal state after: