mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map (op f)))
            (sx.spineToSimplex
              { 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 := ⋯ }))).vertex
      k =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).vertex k

Tactic:
rw [dsimp% show op f = f.op from rfl]

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)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map f.op))
            (sx.spineToSimplex
              { 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 := ⋯ }))).vertex
      k =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₂.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          toFun := fun i ↦
            Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
              (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i,
          monotone' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)))) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))

Tactic:
simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₂.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
⊢ {
        toFun := fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i,
        monotone' := ⋯ }
      (Fin.natAdd (x₁.len + 1) i) =
    Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i)
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 ⟨x, hx⟩
    rw [PartialOrder.mem_nerve_nonDegenerate_iff_injective] at hx
    simp only [NatTrans.mono_iff_mono_app, mono_iff_injective]
    intro ⟨⟨k⟩⟩ i j hij
    ext l : 1
    exact hx (Functor.congr_obj hij l)

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

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
g : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Mono g
⊢ monoOfLE h = g → (ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex

Tactic:
by rintro rfl; simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
⊢ h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t)

Tactic:
by
  simp [AncestralRel, Pairing.AncestralRel]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
⊢ ∑ x ∈ Sᶜ, α x = ∑ x ∈ Sᶜ, -β (γ₁ x)

Tactic:
refine Finset.sum_congr rfl (fun x hx ↦ ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ Sᶜ
⊢ α x = -β (γ₁ x)
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
⊢ ∑ x ∈ S, α x = ∑ x ∈ S, -β (γ₂ x)

Tactic:
refine Finset.sum_congr rfl (fun x hx ↦ ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
⊢ α x = -β (γ₂ x)
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
eq₄ : ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y
eq₅ : ∑ x, β (γ₄ x) = -∑ x, β (γ₃ x)
⊢ ∀ a ∈ Finset.image γ₁ Sᶜ, ∀ b ∈ Finset.image γ₂ S, a ≠ b

Tactic:
grind [Finset.mem_compl]

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
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ (coequalizer φ₁ φ₂)

Tactic:
apply ObjectProperty.prop_colimit
          rintro (_ | _)
          · exact P.le_colimitsCardinalClosure _ _ hG
          · exact j.left.2

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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
left✝ : Epi g₁
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₂
⊢ x₁ = x₂

Tactic:
rw [← hg₁, hg₂]

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

Goal state before:
pp: case refine_1
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
j : Fin (n + 1)
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

pp: case refine_2
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
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j

Tactic:
· obtain ⟨i, hi⟩ := mem_range_right x hd j
      dsimp at hi
      obtain rfl | ⟨i, rfl⟩ := Fin.eq_self_or_eq_succAbove l.castSucc i
      · refine ⟨l, ?_⟩
        rw [Fin.succAbove_castSucc_self, ← hi, ← hl.simplex_snd_succ]
        rfl
      · exact ⟨_, hi⟩

Goal state after:
case refine_2
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
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j
Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst✝¹ : Category.{v_4, u_4} J
P : J ⥤ C₁ᵒᵖ
inst✝ : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun s ↦ { pt := X₃, ι := { app := fun j ↦ adj₂.homEquiv.symm (s.π.app (unop j)), naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun s ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
j : J
⊢ adj₂.homEquiv ((hc' s).desc (cocone s)) ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j

Tactic:
dsimp
        rw [← dsimp% adj₂.homEquiv_naturality_one (c.π.app j).unop,
          dsimp% (hc' s).fac (cocone s) (op j)]
        simp [cocone]

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
t : Fin d
hl : IsIndex x hd t.succ.succ
ht : IsIndex hl.δ ⋯ t.succ
⊢ (objEquiv (x.cast hd).simplex) t.castSucc.castSucc = (objEquiv (x.cast hd).simplex) t.castSucc.succ

Tactic:
simp only [isIndex_succ] at hl ht

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
t : Fin d
hl✝ : IsIndex x hd t.succ.succ
hl :
  (x.cast hd).simplex.1 t.succ.castSucc = k.castSucc ∧
    (x.cast hd).simplex.1 t.succ.succ = k.succ ∧
      (x.cast hd).simplex.2 t.succ.succ = (x.cast hd).simplex.2 t.succ.castSucc
ht :
  ({ dim := d,
                  simplex :=
                    (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.succ.castSucc))
                      (x.cast hd).simplex }.cast
              ⋯).simplex.1
        t.castSucc =
      k.castSucc ∧
    ({ dim := d,
                    simplex :=
                      (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.succ.castSucc))
                        (x.cast hd).simplex }.cast
                ⋯).simplex.1
          t.succ =
        k.succ ∧
      ({ dim := d,
                    simplex :=
                      (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.succ.castSucc))
                        (x.cast hd).simplex }.cast
                ⋯).simplex.2
          t.succ =
        ({ dim := d,
                    simplex :=
                      (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.succ.castSucc))
                        (x.cast hd).simplex }.cast
                ⋯).simplex.2
          t.castSucc
⊢ (objEquiv (x.cast hd).simplex) t.castSucc.castSucc = (objEquiv (x.cast hd).simplex) t.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x) = (↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝

Tactic:
ext x; exact isEmptyElim x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case zero
X : SSet
x : X _⦋0⦌
f : X.op.PtSimplex 0 (opObjEquiv.symm x)
⊢ ∂Δ[0].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι

pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.op.PtSimplex (n + 1) (opObjEquiv.symm x)
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι

Tactic:
· ext

Goal state after:
case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.op.PtSimplex (n + 1) (opObjEquiv.symm x)
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case zero
X : SSet
x : X _⦋0⦌
g : X.PtSimplex 0 x
⊢ ∂Δ[0].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι

pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
g : X.PtSimplex (n + 1) x
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι

Tactic:
· ext

Goal state after:
case succ
X : SSet
x : X _⦋0⦌
n : ℕ
g : X.PtSimplex (n + 1) x
⊢ ∂Δ[n + 1].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι
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
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
r : ℕ∞
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = r
⊢ analyticOrderAt (deriv f) x + 1 = r

Tactic:
cases r with
  | top =>
    suffices analyticOrderAt (deriv f) x = ⊤ by simp_all
    simp only [analyticOrderAt_eq_top, sub_eq_zero] at h ⊢
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp h
    filter_upwards [hUo.mem_nhds hUx] with y hy
    simp [(eventuallyEq_of_mem (hUo.mem_nhds hy) hUf).deriv_eq]
  | coe r =>
    have hrne : r ≠ 0 := by
      intro hr
      rw [hr, ENat.natCast_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
      grind
    obtain ⟨s, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.pos_of_ne_zero hrne)
    rw [Nat.cast_succ]
    congr 1
    rw [analyticOrderAt_eq_natCast (by fun_prop)] at h
    obtain ⟨F, hFa, hFne, hfF⟩ := h
    simp only [sub_eq_iff_eq_add] at hfF
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)
    have : ∀ y ∈ U, deriv f y =
        (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y := by
      intro y hy
      rw [EventuallyEq.deriv_eq (eventually_of_mem (hUo.mem_nhds hy) (fun u hu ↦ (hUf u hu).1)),
        deriv_add_const, deriv_fun_smul (by fun_prop) (hUf y hy).2.differentiableAt]
      simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
    rw [analyticOrderAt_congr (eventually_of_mem (hUo.mem_nhds hUx) this)]
    have : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = s := by
      rw [analyticOrderAt_eq_natCast]
      · refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
        · simpa using ⟨by norm_cast, hFne⟩
        · simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..
      · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
        fun_prop
    rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]
    rw [this, ← ENat.add_one_le_iff (ENat.natCast_ne_top _), ← Nat.cast_add_one,
      natCast_le_analyticOrderAt (by fun_prop)]
    exact ⟨deriv F, hFa.deriv, by simp⟩

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
⊢ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
have ⟨g, hg, hg₀, hfg⟩ := (AnalyticAt.analyticOrderAt_eq_natCast hf).1 horder

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ (fun x1 x2 ↦ x1 + x2) n 1 • g z
⊢ analyticOrderAt (deriv f) z₀ = ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun t ↦ log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
rw [← h₁.hasDerivAt.deriv] at A

Goal state after:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun t ↦ log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x