mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Monoidal

Goal state before:
pp: ⊢ (ConcreteCategory.hom symm) 1 = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Monoidal

Goal state before:
pp: ⊢ (ConcreteCategory.hom symm) 0 = 1

Tactic:
by aesop

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i ↦ ⟦a✝ i⟧) = (fun i ↦ ⟦a✝ i⟧) i

Tactic:
simp only [Quotient.mk''_eq_mk]

Goal state after:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i ↦ Quotient.mk (a✝ i)) = Quotient.mk (a✝ i)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
⊢ ∀ (X : ↑(π.obj A) × ↑(π.obj B)),
    (prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X = (𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X

Tactic:
intros; ext <;> simp <;> rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : f.Nullhomotopic
g : C(X, Y)
⊢ (f.comp g).Nullhomotopic

Tactic:
by
  obtain ⟨y, hy⟩ := hf
  use y
  exact .comp hy (.refl g)

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p₁ : Path x₀ x₁
p₂ : Path x₂ x₃
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ x₀ = x₂

Tactic:
convert! hp 0 <;> simp

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

Goal state before:
pp: case pos.right
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ≤ 1

Tactic:
rw [mul_assoc]
      apply mul_le_one₀ <;> grind

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

Goal state before:
pp: case pos
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 ∈ I

pp: case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I

Tactic:
· constructor
    · apply mul_nonneg <;> grind
    · rw [mul_assoc]
      apply mul_le_one₀ <;> grind

Goal state after:
case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
⊢ ((mk γ₀).trans (mk γ₁)).trans γ₂ = (mk γ₀).trans ((mk γ₁).trans γ₂)

Tactic:
induction γ₂ using Quotient.ind with

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f f = A

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : objMk OrderHom.id ∈ (face {i}ᶜ).obj (op ⦋n⦌)
⊢ i ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom (objEquiv (objMk OrderHom.id))) ⊤

Tactic:
by aesop

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

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
l : Fin (d + 1)
x✝ : j l = k.rev
⊢ (j l.rev.rev).rev = k

Tactic:
by aesop

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

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬j x = k
l : Fin (d + 1)
x✝ : (j l.rev).rev = k.rev
⊢ j l.rev = k

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ S = Finset.univ ∨ S = {j}ᶜ → {j}ᶜ ⊆ S

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (stdSimplex.δ i)

Tactic:
rw [← ι_ι]
  infer_instance

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

Goal state before:
pp: n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
⊢ f = g

Tactic:
ext m ⟨x, hx⟩

Goal state after:
n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx : x ∈ ∂Δ[n + 1].obj m
⊢ (ConcreteCategory.hom (f.app m)).toFun ⟨x, hx⟩ = (ConcreteCategory.hom (g.app m)).toFun ⟨x, hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : j ≠ i
⊢ Subfunctor.range (stdSimplex.δ j) ≤ Λ[n + 1, i]

Tactic:
simpa using face_le_horn _ _ h

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} j).hom, Iso.hom_inv_id_assoc]

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij = (stdSimplex.faceSingletonComplIso j).hom ≫ faceι i j hij
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

Tactic:
rintro ⟨_⟩
    exact ⟨_, rfl, rfl⟩

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

Goal state before:
pp: case inr.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₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃

Tactic:
obtain rfl := H x₃ y₃ hx₃ hy₃ eq

Goal state after:
case inr.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₃
hx₃ hy₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) x₃
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
⊢ t ≫ r = l ≫ b

Tactic:
by simp only [← cancel_mono k, Category.assoc, facr, facb, h₁.w]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ ((Functor.const ↑chosenTerminal).obj (x✝.obj { down := { as := () } })).map { down := { down := { down := ⋯ } } } =
    x✝.map { down := { down := { down := ⋯ } } }

Tactic:
exact (Functor.map_id _ _).symm

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ X.spine 0 (p.vertex 0) = p

Tactic:
by aesop

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
⊢ ∀ (n : ℕ), X.spine n ∘ StrictSegalCore.spineToSimplex h = id

Tactic:
by aesop

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
⊢ StrictSegalCore.spineToSimplex h ∘ X.spine n = id

Tactic:
by aesop

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : Center C
f : X ⟶ Y
inst✝ : IsIso f.f
⊢ IsIso f

Tactic:
change IsIso (isoMk f).hom
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
x✝ : F.HomObj G A
⊢ (fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ })
      ((fun a ↦
          {
            app := fun X ↦
              ↾fun x ↦
                match x with
                | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
            naturality := ⋯ })
        x✝) =
    x✝

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
x✝ : F ⊗ A ⟶ G
⊢ (fun a ↦
        {
          app := fun X ↦
            ↾fun x ↦
              match x with
              | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
          naturality := ⋯ })
      ((fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ }) x✝) =
    x✝

Tactic:
by aesop

Goal state after:
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
D : Type u''
inst✝¹ : Category.{v'', u''} D
inst✝ : EnrichedOrdinaryCategory V D
X : ForgetEnrichment V D
⊢ (eHomEquiv V).symm (homTo V (𝟙 X)) = 𝟙 («to» V X)

Tactic:
rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]

Goal state after:
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 : TransportEnrichment F (ForgetEnrichment V D)
⊢ (forgetEnrichmentEquivFunctor F D e h).map
        ((NatIso.ofComponents (fun x ↦ Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj x)) ⋯).hom.app
          X) ≫
      (NatIso.ofComponents
              (fun x ↦ Iso.refl ((forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h).obj x))
              ⋯).hom.app
        ((forgetEnrichmentEquivFunctor F D e h).obj X) =
    𝟙 ((forgetEnrichmentEquivFunctor F D e h).obj X)

Tactic:
simp only [Functor.id_obj, forgetEnrichmentEquivFunctor_obj, Functor.comp_obj,
      forgetEnrichmentEquivInverse_obj, ForgetEnrichment.to_of, NatIso.ofComponents_hom_app,
      Iso.refl_hom, forgetEnrichmentEquivFunctor_map, h, Category.comp_id]

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 : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))) =
    𝟙 (ForgetEnrichment.of W X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e e' : Edge x₀ x₁
h : e.edge = e'.edge
⊢ e = e'

Tactic:
by aesop

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg X
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ r.deg X = r.deg Z

Tactic:
by aesop

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg Y
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ r.deg Z = r.deg Y

Tactic:
by aesop

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

Goal state before:
pp: m a : ℕ
L : List ℕ
⊢ IsAdmissible m (a :: L) ↔ a ≤ m ∧ (∀ (x : 0 < L.length), a < L[0]) ∧ IsAdmissible (m + 1) L

Tactic:
cases L

Goal state after:
case nil
m a : ℕ
⊢ IsAdmissible m [a] ↔ a ≤ m ∧ (∀ (x : 0 < [].length), a < [][0]) ∧ IsAdmissible (m + 1) []

case cons
m a head✝ : ℕ
tail✝ : List ℕ
⊢ IsAdmissible m (a :: head✝ :: tail✝) ↔
    a ≤ m ∧ (∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]) ∧ IsAdmissible (m + 1) (head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
⊢ IsAdmissible (m + 1) L

Tactic:
cases L

Goal state after:
case nil
m a : ℕ
h : IsAdmissible m [a]
⊢ IsAdmissible (m + 1) []

case cons
m a head✝ : ℕ
tail✝ : List ℕ
h : IsAdmissible m (a :: head✝ :: tail✝)
⊢ IsAdmissible (m + 1) (head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < L[0]
⊢ IsAdmissible m (a :: L)

Tactic:
cases L

Goal state after:
case nil
m a : ℕ
ha : a ≤ m
hL : IsAdmissible (m + 1) []
ha' : ∀ (x : 0 < [].length), a < [][0]
⊢ IsAdmissible m [a]

case cons
m a : ℕ
ha : a ≤ m
head✝ : ℕ
tail✝ : List ℕ
hL : IsAdmissible (m + 1) (head✝ :: tail✝)
ha' : ∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]
⊢ IsAdmissible m (a :: head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) L → ∀ j ≤ m, IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j (a :: L))

Tactic:
cases L

Goal state after:
case cons.nil
a m j : ℕ
hj : j ≤ m
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) [] → ∀ j ≤ m, IsAdmissible m (simplicialInsert j [])
hL : IsAdmissible (m + 1) [a]
⊢ IsAdmissible m (simplicialInsert j [a])

case cons.cons
a m j : ℕ
hj : j ≤ m
head✝ : ℕ
tail✝ : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) (head✝ :: tail✝) → ∀ j ≤ m, IsAdmissible m (simplicialInsert j (head✝ :: tail✝))
hL : IsAdmissible (m + 1) (a :: head✝ :: tail✝)
⊢ IsAdmissible m (simplicialInsert j (a :: head✝ :: tail✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) ≫
      𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y₁)).obj
          (mk z)) =
    𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y₀)).obj
          (mk z)) ≫
      (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (homMk e, 𝟙 (mk z))))

Tactic:
rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
v : ι
⊢ {v} ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
grind [Set.mem_iInter, Finset.singleton_nonempty, singleton_mem]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ A.preimage e.inv = B

Tactic:
by aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x✝ : A.N
⊢ (fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ })
      ((fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
by aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x✝ : B.N
⊢ (fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ })
      ((fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
by aesop

Goal state after:
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 y : ↑P.II
⊢ ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑y, ⋯⟩ ↔ x = y

Tactic:
by aesop

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)
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₁ x✝¹ = γ₁ x✝ → x✝¹ = x✝

Tactic:
by aesop

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 γ₁
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₂ x✝¹ = γ₂ x✝ → x✝¹ = x✝

Tactic:
by aesop

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 γ₂
x✝¹ x✝ : Fin (n + 1)
⊢ γ₃ x✝¹ = γ₃ x✝ → x✝¹ = x✝

Tactic:
by aesop

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 γ₃
x✝¹ x✝ : Fin (n + 1)
⊢ γ₄ x✝¹ = γ₄ x✝ → x✝¹ = x✝

Tactic:
by aesop

Goal state after: