mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case zero
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
n : ℕ
⊢ G.map ((P 0).f n) = (P 0).f n

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hqn : 0 ≤ q
⊢ (P (q + 1)).f 0 = (P q).f 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

Tactic:
induction x using Quotient.inductionOn with | _ f

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
⊢ ⟦f⟧ ≠ 0 → ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑↑n).valuation = ↑(padicValInt p n)

Tactic:
valuation_ratCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ padicValRat p ↑n = ↑(padicValInt p n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑↑n).valuation = ↑(padicValNat p n)

Tactic:
valuation_ratCast,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValRat p ↑n = ↑(padicValNat p n)
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (Q 0).f (n + 1) = ∑ i with ↑i < 0, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
| zero =>

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

Goal state before:
pp: case neg.h.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ Fin.succ 0 < j.succ.succ

Tactic:
· simp only [Fin.succ_lt_succ_iff, j.succ_pos]

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + 0
⊢ X.σ i ≫ (P 0).f (n + 1) = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
exact le_valuation_add hxy

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

Goal state before:
pp: case neg.zero
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
i : Fin (0 + 1)
h : ¬0 + 1 ≤ ↑i + q
hi : 0 = ↑i + q
⊢ X.σ i ≫ (P (q + 1)).f (0 + 1) = 0

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

Tactic:
· fin_cases i
        dsimp at h hi
        rw [show q = 0 by lia]
        change X.σ 0 ≫ (P 1).f 1 = 0
        simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]
        rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]
        dsimp [P_zero]
        rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]
        rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
        simp only [add_neg_cancel, add_zero, zero_add]

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

Goal state before:
pp: case succ.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = f
⊢ DegeneraciesVanish f

Tactic:
degeneraciesVanish_succ_iff,

Goal state after:
case succ.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf : QInfty.f (n + 1) ≫ f = 0
this : (PInfty.f (n + 1) + QInfty.f (n + 1)) ≫ f = f
⊢ ∀ (i : Fin (n + 1)), X.σ i ≫ f = 0
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✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B = 0

Tactic:
dsimp [πSummand]
  rw [ι_desc, dif_neg h.symm]

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

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
inst✝ : IsIso (N₁.map f)
h₂ : ∀ (i : ℕ), (inv (N₁.map f)).f.f i ≫ PInfty.f i ≫ f.app (op ⦋i⦌) = PInfty.f i
h₃ :
  ∀ (n : ℕ), PInfty.f n ≫ (inv (N₁.map f)).f.f n ≫ f.app (op ⦋n⦌) = (inv (N₁.map f)).f.f n ≫ PInfty.f n ≫ f.app (op ⦋n⦌)
h₁ : ∀ (i : ℕ), PInfty.f i ≫ f.app (op ⦋i⦌) ≫ (inv (N₁.map f)).f.f i = PInfty.f i
⊢ IsIso (f.app (op ⦋0⦌))

Tactic:
| zero =>

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₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f =
    eqToHom ⋯ ≫
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              N₁ ⋙
                (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map
          f ≫
        eqToHom ⋯

Tactic:
· ext n
    dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
    simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f,
      assoc, comp_id, PInfty_f_naturality, app_p_comp,
      karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl,
      PInfty_f_naturality_assoc, app_comp_p, PInfty_f_idem_assoc]

Goal state after:
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
⊢ (𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂ = 𝟙 N₂

Tactic:
ext P : 2
  dsimp only [NatTrans.comp_app, NatTrans.hcomp_app, Functor.comp_map, Functor.associator,
    NatTrans.id_app, Functor.comp_obj]
  rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]

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

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ≫ piToPiTop X = 𝟙 (π.obj (TopCat.of ((i : I) → ↑(X i))))

Tactic:
change CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 _

Goal state after:
I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (initial.to X)
⊢ IsCofibrant h.Z

Tactic:
isCofibrant_iff_of_isInitial h.i initialIsInitial

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (initial.to X)
⊢ Cofibration h.i
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
⊢ ((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.unit

Tactic:
by
  intro
  simp only [Functor.id_obj, inverseImage_iff, isomorphisms.iff]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
⊢ ((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.counit

Tactic:
by
  intro
  simp only [Functor.id_obj, inverseImage_iff, isomorphisms.iff]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ PreservesColimit F functorToTypes

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (colimitCocone F).isColimit
    apply Types.FilteredColimit.isColimitOf
    · rintro ⟨x, hx⟩
      simp only [colimitCocone_cocone_pt, iSup_eq_iUnion, mem_iUnion] at hx
      obtain ⟨i, hi⟩ := hx
      exact ⟨i, ⟨x, hi⟩, rfl⟩
    · intro i j ⟨x, hx⟩ ⟨y, hy⟩ h
      obtain rfl : x = y := by simpa using h
      exact ⟨IsFiltered.max i j, IsFiltered.leftToMax i j, IsFiltered.rightToMax i j, rfl⟩

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f))) =
    (ConcreteCategory.hom (Y.map f.op)) c.simplex

Tactic:
simp only [← yonedaEquiv_symm_app_objEquiv_symm, ← ι_b_ι]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f))) =
    (ConcreteCategory.hom ((c.ιSigmaStdSimplex ≫ b i d ≫ ((skeletonOfMono i) (d + 1)).ι).app (op n)))
      (stdSimplex.objEquiv.symm f)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌) ≫ X.map (mkOfSucc k).op)) (horn.face i j hj)

Tactic:
← σ₀.naturality

Goal state after:
case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
rw [SimplicialObject.δ_def, ← Functor.map_comp_apply, ← op_comp,
      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i.succ).op)) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case zero
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ { s // X.spine 0 s = p }

Tactic:
| zero =>

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

Goal state before:
pp: case zero
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋0⦌
⊢ spineToSimplex h (X.spine 0 s) = s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f : a ⟶ b
g : b ⟶ c
⊢ homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g

Tactic:
unfold homEquiv
  simp only [Equiv.trans_apply]
  rw [eHomEquiv_comp]
  rfl

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 Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (X ⟶[V] Y) ◁ (ρ_ (𝟙_ V)).hom ≫
          (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
            (X ⟶[V] Y) ◁ (ρ_ (Y ⟶[V] Y')).inv ≫
              (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
whiskerLeft_rightUnitor_assoc,

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
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (α_ (X ⟶[V] Y) (𝟙_ V) (𝟙_ V)).inv ≫
          (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).hom ≫
            (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
              (X ⟶[V] Y) ◁ (ρ_ (Y ⟶[V] Y')).inv ≫
                (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                  (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: case mp
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ morphismPropertyHomMk V f → (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f

Tactic:
rintro ⟨_⟩
    exact MorphismProperty.map_mem_strictMap _ _ _ ⟨_⟩

Goal state after:
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 j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + 0 = 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

Tactic:
| zero =>

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 : W₂.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
by
    simpa [MorphismProperty.identities_op_iff] using hf'

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 : W₁.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
by
    simpa [MorphismProperty.identities_op_iff] using hf'

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

Goal state before:
pp: case zero
i : Fin (0 + 1)
i' : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
i' : Fin (n + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
cases n with
  | zero => exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [switch_δ_σ₀]⟩
  | succ n =>
    obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'
    · exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [h]⟩
    · exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩

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

Goal state before:
pp: case zero
i : Fin (0 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (0 + 1)
hf : P_δ f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
| zero =>

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

Goal state before:
pp: case comp_σ.comp_of.zero
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
j : Fin (0 + 1)
g : y✝ ⟶ mk (0 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
| zero =>

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

Goal state before:
pp: case comp_σ.comp_of
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
g : y✝ ⟶ mk (n' + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩

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

Goal state before:
pp: case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk (n' + 1)
j : Fin (n' + 1)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m

Tactic:
obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩

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

Goal state before:
pp: case nil
L : List ℕ
j m₁ m₂ : ℕ
hL : IsAdmissible m₂ []
hk : m₂ + [].length = m₁
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ [] hk))) ⟨j, hj⟩) = simplicialEvalσ [] j

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

Goal state after:
case nil
L : List ℕ
j m₁ : ℕ
hj : j < m₁ + 1
hL : IsAdmissible m₁ []
hk : m₁ + [].length = m₁
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ [] hk))) ⟨j, hj⟩) = simplicialEvalσ [] j
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case mk.mk.zero
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 }
h : a + b = 0
⊢ W f

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
x✝ : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t

Tactic:
simp_all only [IsRelUpperSet, true_and]

Goal state after:
α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
b : α
hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s
ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ t
x✝ : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k

Tactic:
toMk₁_of_castSucc_lt i.succ k (by simpa),

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = 0
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)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∈ S
⊢ False

Tactic:
have := S.min'_le _ hi

Goal state after:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∈ S
this : S.min' ⋯ ≤ i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ j)) = ↑((ConcreteCategory.hom g) (Fin.cast ⋯ j))

Tactic:
cases j using Fin.addCases (m := x.len + 1) (n := y.len + 1) with
    | left j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
      simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j
    | right j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂
      simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j

Goal state after: