mathlib-initiative/mathlib-tactics huggingface dataset:
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) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
          ((X ⟶[V] Y) ⊗ Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ (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:
whisker_exchange_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) ◁ (eHomEquiv V) g ≫
        (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫ eComp V X Y Y' ▷ 𝟙_ V ≫ (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' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
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''
⊢ eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g'

Tactic:
dsimp [eHomWhiskerLeft]
  rw [assoc, assoc, eHomEquiv_comp, MonoidalCategory.whiskerLeft_comp_assoc,
    MonoidalCategory.whiskerLeft_comp_assoc, ← e_assoc, tensorHom_def,
    MonoidalCategory.whiskerRight_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
    MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
    whiskerLeft_rightUnitor_assoc, whiskerLeft_rightUnitor_inv_assoc,
    triangle_assoc_comp_left_inv_assoc, MonoidalCategory.whiskerRight_id_assoc,
    Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,
    associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

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

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

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

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

Goal state before:
pp: case mp
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m → (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

pp: case mpr
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m → (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m

Tactic:
· rintro ⟨⟨x₁, x₂⟩, h⟩
    rw [Prod.eq_iff_fst_eq_snd_eq] at h
    exact ⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩

Goal state after:
case mpr
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m → (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.inv, map_id := ⋯ } ≫ { toPrefunctor := e.hom, map_id := h_id } = 𝟙 (of W)

Tactic:
apply forgetToQuiv.map_injective
    exact e.inv_hom_id

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicL f g
⊢ HomotopicL g f

Tactic:
rcases hfg with ⟨hfg⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL g f
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : HomotopicL f g
hgh : HomotopicL g h
⊢ HomotopicL f h

Tactic:
rcases hfg with ⟨hfg⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hgh : HomotopicL g h
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL f h
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicR f g
⊢ HomotopicR g f

Tactic:
rcases hfg with ⟨hfg⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR g f
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
⊢ HomotopicR f h

Tactic:
rcases hfg with ⟨hfg⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hgh : HomotopicR g h
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR f h
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
fac fac' : W₁.MapFactorizationData W₂ f
⊢ ∃ (h : fac.Z = fac'.Z), fac.i = fac'.i ≫ eqToHom ⋯ ∧ fac.p = eqToHom h ≫ fac'.p

Tactic:
by
  have := r.subsingleton_mapFactorizationData f
  obtain rfl : fac = fac' := Subsingleton.elim _ _
  simp

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)

Tactic:
ext y
      obtain ⟨y, rfl⟩ := y.mk_surjective
      simp
      rfl

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)

Tactic:
ext y
      obtain ⟨y, rfl⟩ := y.mk_surjective
      simp
      rfl

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

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

Tactic:
by simpa [S]

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
⊢ m = ↾fun x ↦ lift sx s x

Tactic:
by
    ext x
    apply sx.spineInjective (X := X)
    -- simp? [spineEquiv] says:
    simp only [spineEquiv, RightExtension.coneAt_pt, rightExtensionInclusion_left,
      TypeCat.Fun.toFun_apply, Equiv.coe_fn_mk, lift, Nat.reduceAdd, ObjectProperty.ι_obj,
      const_obj_obj, comp_obj, proj_obj, mk_right, op_obj, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      spine_spineToSimplex_apply]
    ext i
    · exact ConcreteCategory.congr_hom (hm (StructuredArrow.mk
        (Y := op ⦋0⦌2) (⦋0⦌.const ⦋n⦌ i).op)) x
    · exact ConcreteCategory.congr_hom (hm (.mk (Y := op ⦋1⦌2)
        (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)

Tactic:
by
  dsimp [inr', inr, MonoidalCategoryStruct.leftUnitor, MonoidalCategoryStruct.whiskerRight,
    tensorHom, WithInitial.down, leftUnitor, tensorObj]
  ext
  simp [OrderEmbedding.toOrderHom]

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{?u.4, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ ∀ (j : Discrete PEmpty.{1}), ((Functor.empty SSet).obj j).Finite

Tactic:
rintro ⟨⟨⟩⟩

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ A ⊔ ⨆ j, ⨆ (_ : j < Order.succ i), ⨆ c, (↑(P.p c.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ A ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex ∧
    ∀ i_1 < Order.succ i,
      ∀ (i_3 : f.Cell i_1), (↑(P.p i_3.s)).subcomplex ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex ≤ f.filtration (Order.succ i)

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration i ≤ f.filtration (Order.succ i) ∧
    ∀ (i_1 : f.Cell i), (↑(P.p i_1.s)).subcomplex ≤ f.filtration (Order.succ i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ⊔ ⨆ j, ⨆ (_ : j < i), ⨆ c, (↑(P.p c.s)).subcomplex ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
simp only [sup_le_iff, iSup_le_iff]

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j ∧
    ∀ i_1 < i, ∀ (i_3 : f.Cell i_1), (↑(P.p i_3.s)).subcomplex ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration m ≤ ⨆ i, f.filtration ↑i

Tactic:
· conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]
    exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦
      (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans
        (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.mpr hj⟩))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ (α_ Z W X).inv ≫ (Z ⊗ W) ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ (α_ Z W X).inv ≫ h ▷ X ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.castSucc < (x.cast hd).simplex.1 i
⊢ min x hd ≤ i

pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : min x hd ≤ i
⊢ k.castSucc < (x.cast hd).simplex.1 i

Tactic:
· rw [Fin.castSucc_lt_iff_succ_le] at h
    obtain h | h := h.lt_or_eq
    · by_contra! h'
      have := stdSimplex.monotone_apply (x.cast hd).simplex.1 h'.le
      dsimp at this
      rw [simplex_fst_min, ← not_lt] at this
      tauto
    · exact Finset.min'_le _ _ (by simpa using h.symm)

Goal state after:
case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : min x hd ≤ i
⊢ k.castSucc < (x.cast hd).simplex.1 i
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case h₀
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
this : (Arrow.Hom.left β ≫ sq₁₃.π) ≫ sq₁₃.snd = (f₂ ≫ Arrow.Hom.right β) ≫ sq₁₃.snd
⊢ sq₁₂.inl ≫
      ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)

Tactic:
simp only [Category.assoc, sq₁₃.π_snd] at this

Goal state after:
case h₀
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
this : Arrow.Hom.left β ≫ (G.obj (op Y₁)).map f₃ = f₂ ≫ Arrow.Hom.right β ≫ sq₁₃.snd
⊢ sq₁₂.inl ≫
      ⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯ ≫
        (Arrow.mk f₃).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inr
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 + 1)
hi : min x hd < i
⊢ φ x hd i.castSucc < φ x hd i.succ

Tactic:
· rw [φ_of_gt _ _ _ (by grind), φ_of_gt _ _ _ (by grind)]
    exact hx' (by grind)

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

Goal state before:
pp: case pos
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
generalize hd : x.dim = d

Goal state after:
case pos
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }
Module: Mathlib.Topology.Homotopy.TopCat.ToSSet

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
h : Homotopy f g
⊢ ⊥.ι ▷ SSet.stdSimplex.obj { len := 1 } ≫
      TopCat.toSSet.obj X ◁ SSet.stdSimplex.toSSetObjI ≫ μ TopCat.toSSet X I ≫ TopCat.toSSet.map h.h =
    SemiCartesianMonoidalCategory.fst ⊥.toSSet (SSet.stdSimplex.obj { len := 1 }) ≫
      SSet.Subcomplex.isInitialBot.to ⊥.toSSet ≫ ⊥.ι

Tactic:
ext _ ⟨⟨_, ⟨⟩⟩, _⟩

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

Goal state before:
pp: ⊢ yonedaEquiv.symm ((ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 1 (op ⦋0⦌))) = stdSimplex.δ 0 ≫ toSSetObjI

pp: ⊢ stdSimplex.δ 0 ≫ toSSetObjI = yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
· simp [← yonedaEquiv_symm_comp, stdSimplex.δ_zero_eq_const]

Goal state after:
⊢ stdSimplex.δ 0 ≫ toSSetObjI = yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 1)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : Semifield S
inst✝¹ : LinearOrder S
v w : AbsoluteValue R S
inst✝ : IsStrictOrderedRing S
h : ∀ (x : R), v x < 1 ↔ w x < 1
x y : R
h✝ : v x = 0
⊢ v x ≤ v y ↔ w x ≤ w y

pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : Semifield S
inst✝¹ : LinearOrder S
v w : AbsoluteValue R S
inst✝ : IsStrictOrderedRing S
h : ∀ (x : R), v x < 1 ↔ w x < 1
x y : R
hy₀ : v x ≠ 0
⊢ v x ≤ v y ↔ w x ≤ w y

Tactic:
· simp_all

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : Semifield S
inst✝¹ : LinearOrder S
v w : AbsoluteValue R S
inst✝ : IsStrictOrderedRing S
h : ∀ (x : R), v x < 1 ↔ w x < 1
x y : R
hy₀ : v x ≠ 0
⊢ v x ≤ v y ↔ w x ≤ w y