mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
⊢ Subsingleton (d.Extension val₀ (Order.succ i))

Tactic:
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
    have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
    have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
    simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂
    rw [h₁, h₂]
    congr 1
    exact congrArg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val))

Tactic:
← comp_apply,

Goal state after:
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (homOfLE ⋯).op)) (d.succ j hj e.val)
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE hij').op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
← comp_apply,

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (homOfLE hij').op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)

Tactic:
← comp_apply,

Goal state after:
case e_x
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op ≫ F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ monomorphisms C (hf.F.map (homOfLE ⋯))

Tactic:
refine (?_ : _ ≤ monomorphisms C) _ this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
κ : Cardinal.{w}
hκ' : κ.IsRegular
hκ : HasCardinalLT (Subobject G) κ
this✝² : Fact κ.IsRegular
this✝¹ : Nonempty κ.ord.ToType
this✝ : OrderBot κ.ord.ToType
A B X Y : C
i : A ⟶ B
hi : generatingMonomorphisms G i
f : X ⟶ Y
hf : HomotopicalAlgebra.RelativeCellComplex (fun x ↦ (generatingMonomorphisms G).homFamily) f
j : κ.ord.ToType
hj : ¬IsMax j
this : (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts (hf.F.map (homOfLE ⋯))
⊢ (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤ monomorphisms C
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
⊢ ‖z‖ = 1

Tactic:
rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ p - 1

Tactic:
exact le_sub_one_of_lt (Nat.Prime.one_lt hp.elim)

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) = 1 ↔ ¬↑p ∣ x

Tactic:
rw [← exp_zero, exp_injective.eq_iff]

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) = 0 ↔ ¬↑p ∣ x
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : Etale f
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
x : ↥X
s : ↥S
a : S.residueField s ⟶ CommRingCat.of Ω
hx : f x = ((SpecToEquivOfField Ω S).symm ⟨s, a⟩) default
⊢ f x = s

Tactic:
by simp [hx, SpecToEquivOfField]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
X✝ Y : D
P : MorphismProperty C
inst✝² : F✝.Faithful
inst✝¹ : F✝.Full
inst✝ : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F✝ P f
hg : relative F✝ P g
Z X : C
p : F✝.obj Z ⟶ H
fst : F✝.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F✝.map snd) (f ≫ g) p
⊢ (fst ≫ f) ≫ g = F✝.map snd ≫ ?m.66

Tactic:
by simpa using h.w

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = ‖-x + y‖

Tactic:
rw [add_comm, ← sub_eq_add_neg]
    change ‖x - y‖ = ‖y - x‖
    have : y - x = (-1) * (x - y) := by ring
    simp only [this, Norm.norm, map_mul, map_neg_eq_map, AbsoluteValue.map_one, one_mul]

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

Goal state before:
pp: case neg
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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ + (-φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩) ≫ X.δ j.succ = 0

Tactic:
neg_comp,

Goal state after:
case neg
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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ + -(φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩) ≫ X.δ j.succ = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₁.f n = Φ₂.f n

Tactic:
by
  rw [h]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (PInfty.f n ≫
      (PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
        (PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
          PInfty.f n ≫
            (Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) =
    PInfty.f n

Tactic:
simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (PInfty.f n ≫
      (Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) =
    PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom

Tactic:
have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj
    (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
h :
  ((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
          (toKaroubi (ChainComplex C ℕ))).map
      (((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
            (toKaroubi (ChainComplex C ℕ))).preimage
        e.hom) =
    e.hom
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e ≍ e' ↔ e' ≍ e

Tactic:
exact ⟨HEq.symm, HEq.symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝³ : Monoid M
inst✝² : Group G
N : Type v
inst✝¹ : Monoid N
C : Type v
inst✝ : Category.{w, v} C
f : C → G
⊢ ∀ (X : C), f X * (f X)⁻¹ = 𝟙 ()

Tactic:
intro
    simp only [SingleObj.id_as_one, mul_inv_cancel]

Goal state after:
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:
rw [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.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f g : X ⟶ Y
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom

Tactic:
rw [homRel_iff_rightHomotopyRel, leftHomotopyRel_iff_rightHomotopyRel]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g

Tactic:
refine ⟨fun h ↦ (LeftHomotopyRel.factorsThroughLocalization C h).map_eq L,
    fun h ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ LeftHomotopyRel f g
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
a b : Path X✝.as Y✝.as
h : a.Homotopy b
⊢ ⟦a.symm⟧ = ⟦b.symm⟧

Tactic:
exact Quotient.sound ⟨h.symm₂⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Goal state before:
pp: T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ i, bif i then x₃ else x₂) = x₄

Tactic:
← sq.sup_eq,

Goal state after:
T : Type u
inst✝ : CompleteLattice T
x₁ x₂ x₃ x₄ : T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ (⨆ i, bif i then x₃ else x₂) = x₂ ⊔ x₃
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
⊢ IsColimit (c.multicofork.map Set.functorToTypes)

Tactic:
by
  let e := (c.multispanIndex.map Set.functorToTypes).multispan
  apply _root_.Nonempty.some
  rw [Types.isColimit_iff_coconeTypesIsColimit,
    Functor.CoconeTypes.isMulticoequalizer_iff]
  refine ⟨fun i₁ i₂ ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h ↦ ?_, fun ⟨x, hx⟩ ↦ ?_⟩
  · dsimp at i₁ i₂ h₁ h₂
    obtain rfl : x₁ = x₂ := by simpa using h
    have eq₁ := e.ιColimitType_map (WalkingMultispan.Hom.fst (J := .prod ι) ⟨i₁, i₂⟩)
      ⟨x₁, by dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩⟩
    have eq₂ := e.ιColimitType_map (WalkingMultispan.Hom.snd (J := .prod ι) ⟨i₁, i₂⟩)
      ⟨x₁, by dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩⟩
    dsimp [e] at eq₁ eq₂
    rw [eq₁, eq₂]
  · simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq,
      Set.iSup_eq_iUnion, Set.mem_iUnion] at hx
    obtain ⟨i, hi⟩ := hx
    exact ⟨i, ⟨x, hi⟩, rfl⟩

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

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} = Set.univ

Tactic:
ext (_ | _)

Goal state after:
case false
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ false ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    false ∈ Set.univ

case true
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ true ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    true ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
j : Fin (n + 1 + 1)
hj : ¬j = i
⊢ (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j hj) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j hj)

Tactic:
by apply h

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

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : Fin i) (i_2 : ↑(X.nonDegenerate ↑i_1)), Subcomplex.ofSimplex ↑i_2 ≤ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
intro k x

Goal state after:
X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ Subcomplex.ofSimplex ↑x ≤ ⨆ i, ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d : ℕ
x : ↑(X.nonDegenerate d)
n : ℕ
⊢ ↑x ∈ (X.skeleton n).obj (op ⦋d⦌) ↔ d < n

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ X.mem_skeleton _⟩
  obtain ⟨x, hx⟩ := x
  simp only [skeleton, OrderHom.coe_mk, Subfunctor.iSup_obj,
    Set.iUnion_coe_set, Set.mem_iUnion, exists_prop] at h
  obtain ⟨⟨i, hi⟩, y, hy, ⟨f⟩, rfl⟩ := h
  have := X.mono_of_nonDegenerate ⟨_, hx⟩ f y rfl
  have : d ≤ i := SimplexCategory.len_le_of_mono f
  lia

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Function.Injective (ForgetEnrichment.homTo W)

Tactic:
intro f g w; apply_fun ForgetEnrichment.homOf W at w; simpa using w

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
e : X ≅ Y
⊢ r.degHom e.hom = r.deg Y

Tactic:
by
    refine le_antisymm ?_ ?_
    · simpa using r.degHom_comp_le_right e.hom (𝟙 Y)
    · simpa using r.degHom_comp_le_right e.inv e.hom

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ L[k] < m + L.length

Tactic:
by
  grw [hL.le, hk]

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

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

Tactic:
induction L generalizing m₁ m₂ with
  | nil =>
    obtain rfl : m₁ = m₂ := by grind
    simp [simplicialEvalσ]
  | cons a L h_rec =>
    simp only [List.length_cons] at hk
    subst hk
    set a₀ := hL.head
    have aux (t : Fin (m₂ + 2)) :
        (a₀.predAbove t : ℕ) = if a < ↑t then (t : ℕ) - 1 else ↑t := by
      simp only [Fin.predAbove, a₀]
      split_ifs with h₁ h₂ h₂
      · rfl
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁; grind
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
      · rfl
    have := h_rec _ _ hL.of_cons (by grind) hj
    have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
    simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
      toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom,
      SimplexCategory.comp_toOrderHom, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe,
      Function.comp_apply, Fin.predAboveOrderHom_coe, simplicialEvalσ, ha₀, ← this] using aux _

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

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (if i.castSucc < Fin.last (n + 1) then 0 else 1) = (ConcreteCategory.hom f) i

Tactic:
if_pos (by simp)

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hₐ
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
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
· exact ConcreteCategory.congr_hom (hm (.mk (Y := op ⦋1⦌2)
        (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
i : Fin (n + 1)
hi : i < z
⊢ f i < y

Tactic:
by simpa using hz.2 i hi

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

Goal state before:
pp: p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ x ∈ (Δ[p] ⊗ Δ[q]).degenerate n

Tactic:
by_contra hx

Goal state after:
p q n : ℕ
hn : p + q + 1 ≤ n
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hx : x ∉ (Δ[p] ⊗ Δ[q]).degenerate n
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.refine_1
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

Tactic:
refine le_trans ?_ (le_iSup _ ⊥)

Goal state after:
case a.refine_1
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 ≤ ⨆ (_ : ⊥ < i), f.filtration ⊥