mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
i j : (glueData hf).J
⊢ (ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i)) =
    (ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j))

Tactic:
apply yonedaEquiv.symm.injective

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
i j : (glueData hf).J
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map ((glueData hf).f i j).op)) (yonedaEquiv (f i))) =
    yonedaEquiv.symm
      ((ConcreteCategory.hom (F.obj.map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op))) (yonedaEquiv (f j)))
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: j : ℕ
⊢ ¬c.Rel 0 j

Tactic:
by
  intro hj
  dsimp at hj
  apply Nat.not_succ_le_zero j
  rw [Nat.succ_eq_add_one, hj]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind [hσ', hσ]` -/
  simp [hσ', hσ, ha]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map ((Q q).f n) = (Q q).f n

Tactic:
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f,
    P_add_Q_f]
  apply G.map_id

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ 0 ≤ Fin.castSucc 0

Tactic:
Fin.castSucc_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ 0 ≤ 0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝¹ : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst✝ : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ i ∈ Finset.univ, (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))

Tactic:
intro i _

Goal state after:
case succ
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).Factors ((P (n + 1)).f (n + 1))
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case e_a
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ image.ι (θ.unop ≫ A.e) = i

Tactic:
exact SimplexCategory.image_ι_eq fac

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ ∀ x ∈ {i | ↑i < n + 1},
    f ≫ ((P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
intro i _

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
i : Fin (n + 1)
a✝ : i ∈ {i | ↑i < n + 1}
⊢ f ≫ ((P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
                P).d
            i j

Tactic:
rintro _ n (rfl : n + 1 = _)
      ext
      have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
      dsimp [N₂, karoubiChainComplexEquivalence,
        KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
      simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id,
        karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
        ← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.NReflectsIso

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
n : ℕ
⊢ (((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f).f n).f =
    ((eqToHom ⋯ ≫
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map
                f ≫
              eqToHom ⋯).f
        n).f

Tactic:
dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi (SimplicialObject C)
f : P ⟶ Q
n : ℕ
⊢ PInfty.f n ≫ f.f.app (op ⦋n⦌) = ((eqToHom ⋯).f n).f ≫ ((PInfty.f n).f ≫ f.f.app (op ⦋n⦌)) ≫ ((eqToHom ⋯).f n).f
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ s.ι (unop A.fst).len ≫ X.map A.e.op ≫ PInfty.f j ≫ K[X].d j k = 0

Tactic:
degeneracy_comp_PInfty_assoc X j A.e hA,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ s.ι (unop A.fst).len ≫ 0 ≫ K[X].d j k = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
eq₁ :
  (N₂Γ₂.inv.app (N₂.obj P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
eq₂ :
  ((Γ₀.splitting (N₂.obj P).X).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n =
    PInfty.f n ≫ P.p.app (op ⦋n⦌)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n

Tactic:
simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_f, N₂_obj_p_f, assoc,
    eq₁, eq₂, PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ g₀ g₁ : C(X, Y)
F : f₀.Homotopy f₁
h₀ : f₀ = g₀
h₁ : f₁ = g₁
⊢ ∀ (x : X), F (1, x) = g₁ x

Tactic:
by simp [← h₁]

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

Goal state before:
pp: t : ↑I
⊢ transAssocReparamAux t ∈ I

Tactic:
unfold transAssocReparamAux

Goal state after:
t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (fibrations C).op.HasFactorization (trivialFibrations Cᵒᵖ)

Tactic:
trivialFibrations_op

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (fibrations C).op.HasFactorization (trivialCofibrations C).op
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (cofibrations C).HasFactorization (trivialFibrations C)

Tactic:
by rw [h₁, h₂']; infer_instance

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

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n].Subcomplex
h : A ≤ ∂Δ[n]
⊢ A ≠ ⊤

Tactic:
rintro rfl
    exact lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
this : #univ ≤ #{i, a, b}
⊢ False

Tactic:
simp only [card_univ, Fintype.card_fin] at this

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
this : n + 1 ≤ #{i, a, b}
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
rintro ⟨s, rfl, rfl⟩
    apply Rel'.inl_inr

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (inr f g))

Tactic:
intro x₂

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₂ : X₂
⊢ ∀ ⦃a₂ : (fun X ↦ X) X₂⦄, (ConcreteCategory.hom (inr f g)) x₂ = (ConcreteCategory.hom (inr f g)) a₂ → x₂ = a₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
rw [pushoutCocone_inl_eq_inr_iff_of_iso
    (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
    (by simp))]
  have := (mono_iff_injective f).2 h₁
  apply Pushout.inl_eq_inr_iff

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 1 + ↑i = ↑i.succ

Tactic:
by rw [Fin.val_succ, add_comm]

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
X X' : C
f : X ⟶ X'
Y Z : C
⊢ (λ_ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Z)).inv ≫
      (eHomEquiv V) f ▷ ((X' ⟶[V] Y) ⊗ Y ⟶[V] Z) ≫ (X ⟶[V] X') ◁ eComp V X' Y Z ≫ eComp V X X' Z =
    (((λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
simp [e_assoc']

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₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ f.f ▷ X₂.fst ▷ U ≫ ((Y₁.tensorObj X₂).snd.β U).hom ≫ U ◁ Y₁.fst ◁ g.f =
    ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ▷ X₂.fst ≫ Y₁.fst ◁ g.f)

Tactic:
whiskerRight_comm_assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ Y₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ f.f ▷ X₂.fst ≫ U ◁ Y₁.fst ◁ g.f =
    ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ▷ X₂.fst ≫ Y₁.fst ◁ g.f)
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : homMk f ≫ homMk g = homMk h
⊢ f.CompStruct g h

Tactic:
dsimp [homMk, CategoryStruct.comp] at fac

Goal state after:
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : ⟦f.comp g⟧ = ⟦h⟧
⊢ f.CompStruct g h
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case neg
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 : W₁ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X

Tactic:
· exact (r.lt₁ f hf hf').le

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

Goal state before:
pp: case h
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
f : x✝ ⟶ y✝
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)

Tactic:
induction f using Paths.induction with
  | id => exact generators.multiplicativeClosure.id_mem _
  | comp _ k h =>
    cases k
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i = 𝟙 (mk n)

Tactic:
cases i using Fin.lastCases
    · simp only [Fin.lastCases_last]
      exact δ_comp_σ_succ
    · simp only [Fin.lastCases_castSucc]
      exact δ_comp_σ_self

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
w✝² : SimplexCategoryGenRel
w✝¹ : mk n' ⟶ w✝²
w✝ : w✝² ⟶ mk n'
he₁ : P_σ w✝¹
hm₁ : P_δ w✝
h₁ : δ i ≫ σ j = w✝¹ ≫ w✝
⊢ (e ≫ δ i) ≫ σ j = (e ≫ w✝¹) ≫ w✝

Tactic:
by simp [← h₁]

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

Goal state before:
pp: case nil
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + [].length = m₂
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯

Tactic:
obtain rfl : m₃ = m₂ := by grind

Goal state after:
case nil
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + L₁.length = m₁
h' : m₃ + [].length = m₃
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯
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₁
⊢ homMk (Edge.id x) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom
              (fst (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x, y₁))) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (fst (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x, y₀))) ≫
      𝟙 (mk x)

Tactic:
Category.comp_id

Goal state after:
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₁
⊢ homMk (Edge.id x) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (fst (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x, y₀))) ≫
      𝟙 (mk x)
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₁
⊢ ((Functor.curry₃.obj
                ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                  (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                    inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
            (mk x)).map
        (homMk e) ≫
      (mkNatIso
          (fun z ↦
            Iso.refl
              ((((Functor.curry₃.obj
                            ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                        (mk x)).obj
                    (mk y₁)).obj
                (mk z)))
          ⋯).hom =
    (mkNatIso
          (fun z ↦
            Iso.refl
              ((((Functor.curry₃.obj
                            ((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                              (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                        (mk x)).obj
                    (mk y₀)).obj
                (mk z)))
          ⋯).hom ≫
      ((Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).obj (mk x)).map (homMk e)

Tactic:
by
        ext z
        obtain ⟨z, rfl⟩ := z.mk_surjective
        dsimp
        rw [Category.comp_id, Category.id_comp,
          inverse_map_mkHom_homMk_id, inverse_map_mkHom_id_homMk]

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

Goal state before:
pp: X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (Functor.currying₃.functor.map
            (mkNatIso
                (fun x ↦
                  mkNatIso
                    (fun y ↦
                      mkNatIso
                        (fun z ↦
                          Iso.refl
                            ((((Functor.curry₃.obj
                                          ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                                Z.HomotopyCategory).inverse ⋙
                                            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                              inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                      (mk x)).obj
                                  (mk y)).obj
                              (mk z)))
                        ⋯)
                    ⋯)
                ⋯).hom).app
        xyz ≫
      𝟙 (((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z)).obj xyz) =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)

Tactic:
Category.comp_id

Goal state after:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (Functor.currying₃.functor.map
          (mkNatIso
              (fun x ↦
                mkNatIso
                  (fun y ↦
                    mkNatIso
                      (fun z ↦
                        Iso.refl
                          ((((Functor.curry₃.obj
                                        ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory).inverse ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                    (mk x)).obj
                                (mk y)).obj
                            (mk z)))
                      ⋯)
                  ⋯)
              ⋯).hom).app
      xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
Eq.comm,

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = map' f (map' g x.castSucc)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
⊢ motive s

Tactic:
by_cases hs : s.subcomplex ≤ A
  · exact mem s hs
  · exact notMem (.mk' s (by simpa using hs))

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

Goal state before:
pp: X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ x f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) x.simplex = s

Tactic:
refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩
  simp only [← ofSimplex_le_iff] at h ⊢
  simpa using h

Goal state after: