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

Goal state before:
pp: X : SSet
f g : ∂Δ[0].toSSet ⟶ X
⊢ f = g

Tactic:
ext _ ⟨x, hx⟩

Goal state after:
X : SSet
f g : ∂Δ[0].toSSet ⟶ X
n✝ : SimplexCategoryᵒᵖ
x : Δ[0].obj n✝
hx : x ∈ ∂Δ[0].obj n✝
⊢ (ConcreteCategory.hom (f.app n✝)).toFun ⟨x, hx⟩ = (ConcreteCategory.hom (g.app n✝)).toFun ⟨x, hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Subfunctor.equalizer σ₁ σ₂ = Λ[n + 1, i]

Tactic:
apply le_antisymm (Subfunctor.equalizer_le σ₁ σ₂)

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ Λ[n + 1, i] ≤ Subfunctor.equalizer σ₁ σ₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ : X₂
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) y₃

Tactic:
obtain ⟨x₁, rfl, rfl⟩ := exists_of_isPullback h₂ x₂ y₃ eq

Goal state after:
case inl.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₁ : X₁
hy₃ : (ConcreteCategory.hom l) x₁ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq :
  (ConcreteCategory.hom k) ((ConcreteCategory.hom r) ((ConcreteCategory.hom t) x₁)) =
    (ConcreteCategory.hom k) ((ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁))
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x₁) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face ({↑j}ᶜ ⊓ {↑k}ᶜ)

Tactic:
congr

Goal state after:
n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ {↑j, ↑k}ᶜ = {↑j}ᶜ ⊓ {↑k}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ Sigma.ι (fun x ↦ ∂Δ[d].toSSet) c ≫ t i d ≫ r i d = Sigma.ι (fun x ↦ ∂Δ[d].toSSet) c ≫ l i d ≫ b i d

Tactic:
simp [← cancel_mono (Subcomplex.ι _)]

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

Goal state before:
pp: X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + ↑k' = ↑k
⊢ f.arrow ⟨j + ↑k', ⋯⟩ = f.arrow k

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }

Tactic:
congr

Goal state after:
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_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✝ }

Tactic:
congr

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
⊢ F_map = G_map
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
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = { out := β }.out.app X
⊢ { out := α } = { out := β }

Tactic:
congr

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = { out := β }.out.app X
⊢ α = β
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf V
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g))) =
    ForgetEnrichment.homOf V
      ((λ_ (𝟙_ V)).inv ≫
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
            (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
congr

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g)) =
    (λ_ (𝟙_ V)).inv ≫
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
          (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
        eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
x y : V
e : x ⟶ y
⊢ MorphismProperty.ofHoms (fun e ↦ homMk e.snd.snd) (homMk e)

Tactic:
MorphismProperty.ofHoms_iff

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
x y : V
e : x ⟶ y
⊢ ∃ i, Arrow.mk (homMk e) = Arrow.mk (homMk i.snd.snd)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case id
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
x✝ : V
⊢ homMk (𝟙rq x✝) = homMk default

Tactic:
congr

Goal state after:
case id
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
x✝ : V
⊢ 𝟙rq x✝ = default
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x y
⊢ MorphismProperty.ofHoms (fun e ↦ homMk e.snd.snd) (homMk e)

Tactic:
MorphismProperty.ofHoms_iff

Goal state after:
V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x y
⊢ ∃ i, Arrow.mk (homMk e) = Arrow.mk (homMk i.snd.snd)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ Path.vertex
      {
        vertex := fun i ↦
          (ConcreteCategory.hom
              (s.π.app
                (StructuredArrow.mk
                  (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).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 := ⋯ }
      ⟨i, ⋯⟩ =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op))) x

Tactic:
congr

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

Goal state before:
pp: case H.H
n✝¹ n✝ : ℕ
h : n✝¹ = n✝
⊢ mk n✝¹ = mk n✝

Tactic:
congr

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

Goal state before:
pp: case comp_of.inr.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len

Tactic:
exact Nat.lt_succ_of_lt h'

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

Goal state before:
pp: m : ℕ
L : List ℕ
⊢ (List.IsChain (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k) ↔
    List.Pairwise (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

Tactic:
List.isChain_iff_pairwise

Goal state after:
m : ℕ
L : List ℕ
⊢ (List.Pairwise (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k) ↔
    List.Pairwise (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ L[k] < m + L.length

Tactic:
hL.le,

Goal state after:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ m + k < m + L.length
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
⊢ W f

Tactic:
generalize h : a + b = c

Goal state after:
case mk.mk
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
c : ℕ
h : a + b = c
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f))

Tactic:
exact (homEquiv f).injective

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelUpperSet'✝¹ : IsRelUpperSet carrier✝¹ P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ } =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelLowerSet'✝¹ : IsRelLowerSet carrier✝¹ P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ } =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj : (ConcreteCategory.hom f) i = (fun i ↦ i) ⟨1, ⋯⟩
⊢ i ∈ S

Tactic:
simpa [S]

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

Goal state before:
pp: case mk
ι : Type u_1
x✝¹ : PreAbstractSimplicialComplex ι
faces✝ : Set (Finset ι)
isRelLowerSet_faces✝ : IsRelLowerSet faces✝ Finset.Nonempty
x✝ : (fun K ↦ K.faces) { faces := faces✝, isRelLowerSet_faces := isRelLowerSet_faces✝ } = (fun K ↦ K.faces) x✝¹
⊢ { faces := faces✝, isRelLowerSet_faces := isRelLowerSet_faces✝ } = x✝¹

Tactic:
congr

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ (opEquiv.symm x).IsUniquelyCodimOneFace (opEquiv.symm y)

Tactic:
by
  obtain ⟨d, x, rfl⟩ := x.mk_surjective
  obtain ⟨d', y, rfl⟩ := y.mk_surjective
  obtain rfl : d' = d + 1 := hxy.dim_eq
  simp only [opEquiv_symm_apply, iff]
  refine ⟨(hxy.index rfl).rev, by simpa using hxy.δ_index rfl, fun i hi ↦ ?_⟩
  obtain ⟨i, rfl⟩ := i.rev_surjective
  simpa [← hxy.δ_eq_iff rfl] using hi

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ ∀ ⦃b : Fin (m + 2)⦄, x ≤ b → map' f x ≤ map' f b

Tactic:
y

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
⊢ x ≤ y → map' f x ≤ map' f y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ ⋯.index hd = ⋯.index hd

Tactic:
congr

Goal state after:
case e_y
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ (↑((P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩)).toS =
    { dim := (↑(P.p x)).dim,
      simplex :=
        (CategoryTheory.ConcreteCategory.hom (e.symm.hom.app (Opposite.op { len := (↑(P.p x)).dim })))
          (↑(P.p x)).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
h : ∀ (x : Fin (n + 1)), ⟨↑(z.1 x) + ↑(z.2 x), ⋯⟩ = x
⊢ ↑((objEquiv z) a).1 + ↑((objEquiv z) a).2 = ↑((objEquiv z) b).1 + ↑((objEquiv z) b).2

Tactic:
simp only [hab]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
⊢ h.type₁ s ≠ h.type₂ t

Tactic:
simpa only [ne_eq, N.ext_iff, SSet.N.ext_iff] using! h.type₁_ne_type₂' s t

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

Goal state before:
pp: X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ ∃ i i_1, (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)

Tactic:
have hx₁ : x₁ ∈ (⊤ : X₁.Subcomplex).obj _ := by simp

Goal state after:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : x₁ ∈ ⊤.obj m
⊢ ∃ i i_1, (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : A.N
a✝ : s.subcomplex ≤ ⊤
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ ⨆ i, f.filtration i

Tactic:
refine le_trans ?_
      (le_trans (f.subcomplex_le_filtration ⟨t, rfl⟩ (Order.lt_succ _)) (le_iSup _ _))

Goal state after:
case notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : A.N
a✝ : s.subcomplex ≤ ⊤
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex
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
j : ι
c : f.Cell j
d : ℕ
x : Δ[c.dim + 1] _⦋d⦌
⊢ ∀ ⦃a₂ : (fun X ↦ X) (Δ[c.dim + 1] _⦋d⦌)⦄,
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) x =
        (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) a₂ →
      x = a₂

Tactic:
y

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
d : ℕ
x y : Δ[c.dim + 1] _⦋d⦌
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) x =
      (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) y →
    x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

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

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
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

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.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

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

Goal state after:
Module: Mathlib.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
⊢ Sigma.ι (fun c ↦ c.horn.toSSet) c ≫ f.t j ≫ homOfLE ⋯ = Sigma.ι (fun c ↦ c.horn.toSSet) c ≫ f.m j ≫ f.b j

Tactic:
simp [← cancel_mono (Subcomplex.ι _)]

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 : ι
s : (range (f.m j)).N
⊢ (f.mapN s).simplex ∈ X.nonDegenerate (f.mapN s).dim

Tactic:
by
  obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s
  · rw [f.mapN_type₁]
    exact (P.p c.s).val.nonDegenerate
  · rw [f.mapN_type₂]
    exact c.s.val.nonDegenerate

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

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Cell.type₂ f c = Cell.type₂ f c'

Tactic:
congr

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ c = c'