mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
rw [norm_eq_zpow_neg_valuation hx0]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0

Tactic:
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]

Goal state after:
case neg.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
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
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ ∀ x ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
    K[X].d i j ≫ (s.πSummand x ≫ (s.cofan (op ⦋j⦌)).inj x) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
      s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
        (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
· intro A hA
      simp only [Finset.mem_compl, Finset.mem_singleton] at hA
      simp only [assoc, ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ _ hA, comp_zero]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
      s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
        (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋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
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)) ≫ PInfty.f (unop (A.pull θ).fst).len ≫ X.map (A.pull θ).e.op =
    PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ

Tactic:
erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ PInfty.f (unop A.fst).len ≫ X.map (image.ι (θ.unop ≫ A.e)).op ≫ X.map (A.pull θ).e.op =
    PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: case ε
X✝ : Type u_1
Y✝ : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y✝
f g : C(X✝, Y✝)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hequiv : X ≃ₕ Y
⊢ map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid Y)

Tactic:
simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using asIso (homotopicMapsNatIso hequiv.right_inv.some)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
h : HomRel.CompClosure (homRel C) x✝¹ x✝
⊢ RightHomotopyClass.mk x✝¹.hom = RightHomotopyClass.mk x✝.hom

Tactic:
by
    simpa [RightHomotopyClass.mk_eq_mk_iff] using! h

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A

Tactic:
refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩
  · replace h := h.trans hA
    rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h
    apply h
    rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]
  · rw [Subcomplex.le_iff_contains_nonDegenerate]
    intro d x hx
    by_cases! hd : d < n
    · simp [horn_obj_eq_univ i d]
    · obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x
      dsimp at hS
      simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢
      obtain hd | rfl := hd.lt_or_eq
      · obtain rfl : S = .univ := by
          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)
        exact (h (le_trans (by simp) hx)).elim
      · replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
        obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩
        exact face_le_horn _ _ (by rintro rfl; tauto)

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

Goal state before:
pp: case inl
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi✝ : n ≤ i
a : Δ[n] _⦋i⦌
ha : a ∈ A.obj (op ⦋i⦌)
hi : n < i
⊢ a ∈ Δ[n].degenerate i

pp: case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∈ Δ[n].degenerate n

Tactic:
· simp [Δ[n].degenerate_eq_univ_of_hasDimensionLT (n + 1) i]

Goal state after:
case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∈ Δ[n].degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ stdSimplex.objEquiv.symm f ∉ Λ[n, i].obj (op d)

Tactic:
rw [mem_horn_iff, ne_eq, not_not]
  ext i
  simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩

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

Goal state before:
pp: case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inl z₁)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)

Tactic:
inl_rel'_inl_iff

Goal state after:
case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) y₀✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

Tactic:
· rw [inr_rel'_inr_iff] at hyz
        subst hyz
        apply Rel'.inl_inr

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

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

Tactic:
inl_rel'_inl_iff

Goal state after:
case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) s✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ f.vertex j = g.vertex j

Tactic:
hk,

Goal state after:
case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ f.vertex k.castSucc = g.vertex k.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
⊢ P f

Tactic:
by
  suffices generators.multiplicativeClosure' ≤ P by
    rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',
      multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
  intro _ _ f hf
  induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp (𝟙 _) i id)
    · simpa using! (σ_comp (𝟙 _) i id)
  | id n => exact id
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp g i hrec)
    · simpa using! (σ_comp g i hrec)

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

Goal state before:
pp: L : List ℕ
⊢ Monotone (simplicialEvalσ L)

Tactic:
by
  induction L <;> grind [Monotone]

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

Goal state before:
pp: 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 ⋯ ⋯)
ha hb : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : 0 + 0 = 0
⊢ f = 𝟙 { obj := { len := 0 }, property := ha }

Tactic:
ext i : 3

Goal state after:
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 ⋯ ⋯)
ha hb : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : 0 + 0 = 0
i : Fin ({ obj := { len := 0 }, property := ha }.obj.len + 1)
⊢ (Hom.toOrderHom f.hom) i = (Hom.toOrderHom (𝟙 { obj := { len := 0 }, property := ha }).hom) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f

Tactic:
change W.inverseImage (Truncated.inclusion (max a.len b.len))
    (Truncated.Hom.tr f (ha := by simp) (hb := by simp))

Goal state after:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W.inverseImage (Truncated.inclusion (max a.len b.len)) (Truncated.Hom.tr f ⋯ ⋯)
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ δ j ≫ toMk₁ i = toMk₁ (i.pred ⋯)

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
  rw [Fin.pred_succ]
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  change toMk₁ i.succ (j.succAbove k) = _
  dsimp
  rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]
  grind [Fin.succAbove]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂

Tactic:
ext i : 3

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂)) i =
    (SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂)) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂

Tactic:
ext i : 3

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₂.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inr' x₁ x₂ ≫ tensorHomOf f₁ f₂)) i =
    (SimplexCategory.Hom.toOrderHom (WithInitial.down f₂ ≫ inr' y₁ y₂)) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inr' y z ≫ inr' x (tensorObjOf y z)

Tactic:
ext i : 3

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inr' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inr' y z ≫ inr' x (tensorObjOf y z))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inl' x y ≫
      inl' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl' x (tensorObjOf y z)

Tactic:
ext i : 3

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inl' x y ≫
          inl' (tensorObjOf x y) z ≫
            WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr' x y ≫
      inl' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl' y z ≫ inr' x (tensorObjOf y z)

Tactic:
ext i : 3

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (inr' x y ≫
          inl' (tensorObjOf x y) z ≫
            WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom))
      i =
    (SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z))) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
⊢ objEquiv ↑z₁ = objEquiv ↑z₂

Tactic:
ext i : 3

Goal state after:
case fst
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).1 = ((objEquiv ↑z₂) i).1

case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ : SSet
p q : ℕ
x₁ : X₁ _⦋p⦌
x₂ : X₂ _⦋q⦌
⊢ (ofSimplex x₁).prod (ofSimplex x₂) = range (yonedaEquiv.symm x₁ ⊗ₘ yonedaEquiv.symm x₂)

Tactic:
by
  simp [Subcomplex.range_tensorHom, Subcomplex.range_eq_ofSimplex]

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
j : ι
c : f.Cell j
d : ℕ
x y : Δ[c.dim + 1] _⦋d⦌
h :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) x =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌))) y
⊢ x = y

Tactic:
simpa [f.ιSigmaStdSimplex_eq_iff] using h.symm

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

Goal state before:
pp: 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

Tactic:
rintro rfl
          exact c.subcomplex_not_le_image_horn hs

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

Tactic:
obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le P
  exact ⟨Q, inferInstance, hP.of_le_isoClosure h₂ (h₁.trans hP.le_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 : ι
⊢ Function.Injective f.mapN

Tactic:
by
  intro s t h
  obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s <;>
    obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t <;>
    simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
  · obtain rfl : c = c' := by ext : 1; exact P.p.injective h
    rfl
  · exact (P.ne _ _ h).elim
  · exact (P.ne _ _ h.symm).elim
  · congr; aesop

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : IsCardinalLocallyPresentable C κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_small_generator C κ

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasColimitsOfSize.{w, w, v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : IsCardinalLocallyPresentable C κ
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
hi : (x.cast hd).simplex.2 l.castSucc = j
⊢ (x.cast hd).simplex.2 (l.castSucc.succAbove l) = j

Tactic:
Fin.succAbove_castSucc_self,

Goal state after:
case refine_1.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
hi : (x.cast hd).simplex.2 l.castSucc = j
⊢ (x.cast hd).simplex.2 l.succ = j
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi : i.castSucc < min x hd
⊢ φ x hd i.castSucc.castSucc < φ x hd i.castSucc.succ

Tactic:
φ_of_lt _ _ _ (by grind),

Goal state after:
case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi : i.castSucc < min x hd
⊢ (objEquiv (x.cast hd).simplex) (i.castSucc.castSucc.castPred ⋯) < φ x hd i.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
rw [← ht.min_eq, hl.min_δ]

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
obtain hi | rfl | hi := lt_trichotomy i l.castSucc

Goal state after:
case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : i < l.castSucc
⊢ i = l.castSucc ∨ i = l.succ

case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex
⊢ l.castSucc = l.castSucc ∨ l.castSucc = l.succ

case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ