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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (cofibrations SSet).IsMultiplicative

Tactic:
cofibrations_eq

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsMultiplicative
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (cofibrations SSet).IsStableUnderRetracts

Tactic:
cofibrations_eq

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsStableUnderRetracts
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)

Tactic:
rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        apply Rel'.refl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c'.inl) x₁ = (ConcreteCategory.hom c'.inr) x₂ →
    (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

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

Goal state before:
pp: X : SSet
d n i : ℕ
hi : i < n
y : X _⦋↑⟨i, hi⟩⦌
hy : y ∈ X.nonDegenerate ↑⟨i, hi⟩
f : unop (op ⦋d⦌) ⟶ unop (op ⦋↑⟨i, hi⟩⦌)
hx : (ConcreteCategory.hom (X.map (op f))) y ∈ X.nonDegenerate d
this : Mono f
⊢ d < n

Tactic:
have : d ≤ i := SimplexCategory.len_le_of_mono f

Goal state after:
X : SSet
d n i : ℕ
hi : i < n
y : X _⦋↑⟨i, hi⟩⦌
hy : y ∈ X.nonDegenerate ↑⟨i, hi⟩
f : unop (op ⦋d⦌) ⟶ unop (op ⦋↑⟨i, hi⟩⦌)
hx : (ConcreteCategory.hom (X.map (op f))) y ∈ X.nonDegenerate d
this✝ : Mono f
this : d ≤ i
⊢ d < n
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ (isColimit i).desc hf.multicofork = f j hj

Tactic:
by
    rw [← cancel_epi (stdSimplex.faceSingletonComplIso j).inv]
    simpa using! (horn.isColimit.{u} i).fac hf.multicofork (.right ⟨j, hj⟩)

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPushout (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (t i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d)) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))

Tactic:
refine Types.isPushout_of_isPullback_of_mono' ?_ ?_ ?_

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPullback (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (t i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d)) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))

case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))) ⊔
      Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) =
    Set.univ

case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d)),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
        (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) x₃ =
            (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) y₃ →
          x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    sx.spineToSimplex l ⋯ (f.interval j l hjl)

Tactic:
by
  apply sx.spineInjective l
  dsimp only [spineEquiv, Equiv.coe_fn_mk]
  rw [spine_spineToSimplex_apply]
  convert! spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f
  exact sx.spine_spineToSimplex_apply m h f |>.symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

Tactic:
by
  rw [isCoskeletal_iff]
  exact isRightKanExtension_iff_isIso ((coskAdj n).unit.app X)
    ((coskAdj n).counit.app _) (𝟙 _) ((coskAdj n).left_triangle_components X)

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₀.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₀.hom.unop) x)

Tactic:
fin_cases x <;> rfl

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₁.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₁.hom.unop) x)

Tactic:
fin_cases x <;> rfl

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₂.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₂.hom.unop) x)

Tactic:
fin_cases x <;> rfl

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

Goal state before:
pp: case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Goal state after:
case inr.inr
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ ∧
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) ∧
        (∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧ x✝ ≤ m ↔
    List.IsChain (fun x1 x2 ↦ x1 < x2) (x✝ :: y✝ :: xs✝) ∧
      ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k

Tactic:
List.isChain_cons_cons,

Goal state after:
case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ ∧
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) ∧
        (∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ∧ x✝ ≤ m ↔
    (x✝ < y✝ ∧ List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)) ∧
      ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
β₂ : α ⟶ α₂ := ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₀)) x✝
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₂)) x✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 0).op).unop) x) = ↑((Hom.toOrderHom α₂.hom.unop) x)

Tactic:
fin_cases x <;> rfl

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
β₂ : α ⟶ α₂ := ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₀)) x✝
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₂)) x✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 1).op).unop) x) = ↑((Hom.toOrderHom α₀.hom.unop) x)

Tactic:
fin_cases x <;> rfl

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1)

Tactic:
induction L generalizing m k <;> grind [→ IsAdmissible.singleton]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.succ

Tactic:
by_cases! h : j.castSucc < i

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : j.castSucc < i
⊢ i.succAbove j < x.succ

case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
⊢ StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)

Tactic:
by
  have (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b) :
      a < b ↔ ((a.1 : ℕ) + a.2 < (b.1 : ℕ) + b.2) := by
    obtain ⟨h₁, h₂⟩ := hab
    rw [Prod.lt_iff]
    lia
  simp only [Fin.strictMono_iff_lt_succ]
  exact forall_congr' (fun i ↦ (this _ _ ((objEquiv x).monotone i.castSucc_le_succ)).symm)

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

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : StrictMono ⇑(orderHomOfSimplex x ⋯)
⊢ False

Tactic:
replace hx := Fintype.card_le_of_injective _ hx.injective

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : Fintype.card (Fin (n + 1)) ≤ Fintype.card (Fin (p + q + 1))
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
⊢ ⨆ x₁, ⨆ x₂, (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex) = ⊤

Tactic:
ext m ⟨x₁, x₂⟩
  simp only [Subfunctor.iSup_obj, Subcomplex.prod_obj, Set.mem_iUnion, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
  have hx₁ : x₁ ∈ (⊤ : X₁.Subcomplex).obj _ := by simp
  have hx₂ : x₂ ∈ (⊤ : X₂.Subcomplex).obj _ := by simp
  simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂
  obtain ⟨s₁, hs₁⟩ := hx₁
  obtain ⟨s₂, hs₂⟩ := hx₂
  exact ⟨s₁, s₂, hs₁, hs₂⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (NatIso.ofComponents
                        (fun X ↦
                          WalkingParallelPair.casesOn X
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.zero))
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.one)))
                        ⋯).inv).obj
                (Cofork.ofπ (f.app k) ⋯)).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (NatIso.ofComponents
                        (fun X ↦
                          WalkingParallelPair.casesOn X
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.zero))
                            (Iso.refl
                              ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                    (pullback.cone (f.app k) (f.app k)).snd).obj
                                WalkingParallelPair.one)))
                        ⋯).inv).obj
                (Cofork.ofπ (f.app k) ⋯)).pt).hom =
      (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app j

Tactic:
rintro (_ | _ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ Subobject.mk i = ⊤

Tactic:
refine hS₂ _ (fun G hG g ↦ ?_)

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (Subobject.mk i).Factors g
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X : C
⊢ ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p

Tactic:
obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X
    exact ⟨ι, s, hs, c, hc, p, inferInstance⟩

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 κ
⊢ g₁ = g₂

Tactic:
obtain ⟨j, φ₁, φ₂, rfl, rfl⟩ :
          ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X)
            (φ₁ φ₂ : G ⟶ Φ.obj j), φ₁ ≫ colimit.ι _ _ = g₁ ∧ φ₂ ≫ colimit.ι _ _ = g₂ := by
        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:
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)
⊢ φ₁ ≫ colimit.ι Φ j = φ₂ ≫ colimit.ι Φ j
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
l' : Fin d
hl' : IsIndex x hd l'.succ
⊢ min x hd = l'.succ

Tactic:
hl'.min_eq

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
l' : Fin d
hl' : IsIndex x hd l'.succ
⊢ l'.succ = l'.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
⊢ x = y

Tactic:
have h₁ := hl.isType₂_δ.type₁_eq_of_δ_eq hl'.type₁ h.symm rfl

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
h₁ : ⋯.type₁ ⋯ = hl'.type₁
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
⊢ ⨆ i, i.subcomplex = ⊤

Tactic:
Subcomplex.eq_top_iff_contains_nonDegenerate

Goal state after:
X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ 1 < Module.rank ℝ ↥E'

Tactic:
rwa [← (E.quotientEquivOfIsCompl E' hE').rank_eq]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
have : r (f x) = x := HasStrictFDerivAt.localInverse_apply_image ..

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f 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
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
⊢ F =ᶠ[𝓝 0] fun z ↦
    if z ∈ U then F z else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

Tactic:
by filter_upwards [hU0] using by simp +contextual

Goal state after: