mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
⊢ ∀ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ X),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
i

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
⊢ ∀ (σ₀ : Λ[n + 2, i].toSSet ⟶ X),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (λ_ (X ⟶[V] Y)).inv ≫ F.map (eId V X ▷ X ⟶[V] Y) ≫ F.map (eComp V X X Y) = 𝟙 (F.obj (X ⟶[V] Y))

Tactic:
← F.map_comp

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map ((λ_ (X ⟶[V] Y)).inv ≫ (eId V X ▷ X ⟶[V] Y) ≫ eComp V X X Y) = 𝟙 (F.obj (X ⟶[V] Y))
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (ρ_ (X ⟶[V] Y)).inv ≫ F.map ((X ⟶[V] Y) ◁ eId V Y) ≫ F.map (eComp V X Y Y) = 𝟙 (F.obj (X ⟶[V] Y))

Tactic:
← F.map_comp

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map ((ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ eId V Y ≫ eComp V X Y Y) = 𝟙 (F.obj (X ⟶[V] Y))
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_obj : C → D
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ G_obj X ⟶[V] G_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Function.Injective (ForgetEnrichment.homTo W)

Tactic:
· intro f g w; apply_fun ForgetEnrichment.homOf W at w; simpa using w

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl V
f : x ⟶ y
⊢ f = homMk default

Tactic:
by
    induction f using hom_induction with
    | id => congr; subsingleton
    | @comp_homMk x y z _ g h =>
      obtain rfl := Subsingleton.elim y z
      obtain rfl := Subsingleton.elim g (𝟙rq _)
      simp [h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.succ))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.δ i))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_le H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝¹ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
x✝ : t = ∅ ∨ t = {v}
⊢ t ∈ {s | ∃ v, s = {v}}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝¹ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
x✝ : t = ∅ ∨ t = {v}
⊢ t ∈ {t | ∃ v, t = {v}}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x : Finset ι
x✝¹ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
x✝ : t = ∅ ∨ t = {v}
⊢ t ∈ {s | ∃ v, s = {v}}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with

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

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
⊢ ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
i

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
⊢ (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), (f i).castSucc < x
⊢ ∀ b ∈ finset f x, b = Fin.last (n + 1)

Tactic:
i

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), (f i).castSucc < x
i : Fin (n + 2)
⊢ i ∈ finset f x → i = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
⊢ ∀ i < y, (f i).castSucc < x

Tactic:
i

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
⊢ i < y → (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
⊢ ∀ b ∈ finset f x, y.castSucc ≤ b

Tactic:
i

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 2)
⊢ i ∈ finset f x → y.castSucc ≤ i
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)
⊢ (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂)) i =
    (SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂)) i

Tactic:
dsimp [tensorHomOf]

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)
⊢ (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 ⋯)) ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i)
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)
⊢ (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂ ≫ tensorHomOf f₁ f₂)) i =
    (SimplexCategory.Hom.toOrderHom (WithInitial.down f₂ ≫ inr' y₁ y₂)) i

Tactic:
dsimp [tensorHomOf]

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)
⊢ (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 ⋯)) ((SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x

Tactic:
obtain hx | rfl := hx.lt_or_eq

Goal state after:
case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x

case pos.inl.left.inr
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.castSucc.succAbove x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌)))

Tactic:
i

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i : Δ[n] _⦋k⦌
⊢ ∀ ⦃a₂ : Δ[n] _⦋k⦌⦄,
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
        (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) a₂ →
      i = a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝¹ : PartialOrder α
inst✝ : WellFoundedLT α
f : P.RankFunction α
⊢ WellFounded P.AncestralRel

Tactic:
by
  rw [wellFounded_iff_isEmpty_descending_chain]
  exact ⟨fun ⟨g, hg⟩ ↦ not_strictAnti_of_wellFoundedLT (f.rank ∘ g)
    (strictAnti_nat_of_succ_lt (fun n ↦ f.lt (hg n)))⟩

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

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

Tactic:
simpa using SSet.N.dim_lt_of_lt t.2.2

Goal state after:
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
    rintro _ rfl
    simpa using IsInner.ne_last s

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

Goal state before:
pp: case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤

Tactic:
have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)

Goal state after:
case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
this : IsEmpty ((fun X ↦ X) (X _⦋n⦌))
⊢ X.degenerate n = ⊤
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₂
i : Fin (d + 2)
hf : Mono (SimplexCategory.δ i)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ i).op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ { dim := hs.δ.dim, simplex := hs.δ.simplex } =
    { dim := d,
      simplex :=
        (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) ((Subcomplex.N.mk t ht₁ ht₂).cast ⋯).simplex }

Tactic:
rw [S.ext_iff']
      exact ⟨rfl, hδ.symm⟩

Goal state after:
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:
by
    apply PullbackObjObj.hom_ext
    all_goals simp [← Functor.map_comp]

Goal state after:
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.succ ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
CosimplicialObject.δ_comp_σ_succ_assoc

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ f.map = f.map
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : X
hx : x ∈ a.finset
⊢ ∃ x_1 ∈ b.finset, f x_1 = f x

Tactic:
exact ⟨x, h hx, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ 𝔠 ≤ #E

Tactic:
have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
    simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
  simpa using A.trans (Cardinal.mk_le_of_module 𝕜 E)

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 𝕜 𝕜 𝕜 := ⋯
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := ⋯
hg : HasFPowerSeriesOnBall g p x p.radius
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
⊢ Set.EqOn f g (Metric.eball x r)

Tactic:
apply hg' (Metric.isConnected_eball hr_pos).isPreconnected (show x ∈ Metric.eball x r by simpa) ?_

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
hg' :
  IsPreconnected (Metric.eball x r) →
    ∀ {z₀ : 𝕜}, z₀ ∈ Metric.eball x r → f =ᶠ[nhds z₀] g → Set.EqOn f g (Metric.eball x r)
⊢ f =ᶠ[nhds x] g
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: case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ y ∈ f '' closedBall b ε

Tactic:
have : CauchySeq u := by
    refine cauchySeq_of_le_geometric _ (↑f'symm.nnnorm * dist (f b) y) Icf' fun n ↦ ?_
    calc
      dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
      _ ≤ f'symm.nnnorm * dist (f (u n)) y := A _
      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        exact (D n).1
      _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring

Goal state after:
case inr
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) univ x

Tactic:
exact fa.cpow ga m

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
⊢ deriv^[n] Inv.inv x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)

Tactic:
iter_deriv_inv

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