mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred i = ⟨Order.pred ↑i, ⋯⟩

Tactic:
ext
  simp only [coe_pred_of_not_isMin hi]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X

Tactic:
by
  constructor
  · rintro ⟨_⟩
    rfl
  · intro h
    rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]
    apply prop_toSucc

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case e_i
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : ¬i₁ ≤ j
⊢ i₁ = i₂

Tactic:
rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁ : i < Order.succ j
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i hi₁ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
by
    rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁
    obtain hi₁ | rfl := hi₁.lt_or_eq
    · rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
    · rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Φ.iter i₂).F i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
exact Arrow.ext (Iteration.congr_obj _ _ _ _ _)
    (Iteration.congr_obj _ _ _ _ _) (Iteration.congr_map _ _ _ _ _)

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
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
⊢ (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:
obtain hij | rfl := hij.lt_or_eq
    · have hij' : i ≤ j := (Order.lt_succ_iff_of_not_isMax hj).mp hij
      have := congr_arg (F.map (homOfLE hij').op) (d.map_succ j hj e.val)
      rw [e.map_limit i hi, ← comp_apply, ← map_comp, ← op_comp, homOfLE_comp] at this
      rw [this]
      congr
      ext ⟨⟨l, hl⟩⟩
      dsimp
      conv_lhs => rw [← d.map_succ j hj e.val]
      rw [← comp_apply, ← map_comp]
      rfl
    · exfalso
      exact hj hi.isMax

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X : C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
have : Nonempty κ.ord.ToType := by simp [κ]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X : C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this : Nonempty κ.ord.ToType
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
⊢ monomorphisms C i → HasLiftingProperty i p

Tactic:
(_ : Mono i)

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i p
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
I : MorphismProperty C
inst✝ : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
let e : ℕ ≃o Cardinal.aleph0.{w}.ord.ToType :=
    ULift.orderIso.{w}.symm.trans
      (OrderIso.ofRelIsoLT (Nonempty.some (by simp [← Ordinal.type_eq])))
  rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!

Tactic:
rw [add_succ, factorial_succ,
      padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
      hn <| lt_of_succ_lt h, ← add_succ,
      padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
        (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
      zero_add]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
by_cases hp : p = 1

Goal state after:
case pos
p : ℕ
a : ℤ
hp : p = 1
⊢ ↑p ^ padicValInt p a ∣ a

case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x := ⟨f₁, hy₁⟩
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x := ⟨f₂, hy₂⟩
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂

Tactic:
obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x := ⟨f₁, hy₁⟩
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x := ⟨f₂, hy₂⟩
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : q₁ ≫ α₁ = q₂ ≫ α₂
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U))
      ((ConcreteCategory.hom (Φ.obj.fiber.map t)) v) =
    (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t)

Tactic:
← Φ.obj.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U))
      ((ConcreteCategory.hom (Φ.obj.fiber.map t)) v) =
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (shrinkYoneda.{w, v, u}.map t)))
      ((ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app V)) v)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
s₀ : ↥S
hs₀ : s default = s₀
X : S.Etale
t : (pointSmallEtale s).fiber.obj X
⊢ (Over.Hom.left t) default ∈ ⇑X.hom ⁻¹' {s₀}

Tactic:
have := (Over.w t).symm

Goal state after:
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
s₀ : ↥S
hs₀ : s default = s₀
X : S.Etale
t : (pointSmallEtale s).fiber.obj X
this : (unop (op (Over.mk s))).hom = Over.Hom.left t ≫ ((Etale.forget S).obj X).hom
⊢ (Over.Hom.left t) default ∈ ⇑X.hom ⁻¹' {s₀}
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hb
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ r

Tactic:
induction r using Quotient.inductionOn

Goal state after:
case hb.h
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
a✝ : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ ⟦a✝⟧
Module: Mathlib.AlgebraicGeometry.Sites.Representability

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

Tactic:
rw [yonedaEquiv_naturality, Equiv.symm_apply_apply,
        Functor.map_comp_apply, yonedaEquiv_naturality, yonedaEquiv_naturality,
        Equiv.symm_apply_apply, ← Functor.map_comp_assoc,
        Functor.relativelyRepresentable.symmetry_fst, ((hf i).rep.isPullback' (f j)).w]

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
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)] at h
  intro a' g'
  obtain ⟨_, ⟨left⟩⟩ := pullback_map_diagonal_isPullback g g' (terminal.from X)
  let prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
    (preservesLimitIso _ (pair _ _) ≪≫ HasLimit.isoOfNatIso (pairComp _ _ _)).hom ≫ prod.map g g'
  let pbRepr :=
    (h prodMap).choose_spec.choose_spec.choose_spec.isLimit'.some.conePointUniqueUpToIso <|
    pasteHorizIsPullback rfl (IsPullback.of_vert_isIso_mono (snd := pullback.congrHom
      (terminal.comp_from g) (terminal.comp_from g') ≪≫ (prodIsoPullback _ _).symm ≪≫
      (HasLimit.isoOfNatIso (pairComp _ _ _)).symm ≪≫ (preservesLimitIso _ (pair _ _)).symm |>.hom)
    ⟨by cat_disch⟩).isLimit'.some left
  exact ⟨_, ⟨_, ⟨_, IsPullback.of_iso_pullback (fst := pbRepr.hom ≫ pullback.fst g g')
    (snd := F.map (Functor.preimage F (pbRepr.hom ≫ pullback.snd g g')))
    ⟨by simp [pullback.condition]⟩ pbRepr (by cat_disch) (by cat_disch)⟩⟩⟩

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

Goal state before:

Tactic:
‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := eq_padicNorm _
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∑ j, PInfty.f (n + 1) ≫ ((-1) ^ ↑j • X.δ j) = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
Finset.sum_eq_single (0 : Fin (n + 2))

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op

case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

case pos.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: α : Type u_1
l : List α
⊢ pathToList (listToPath l) = l

Tactic:
induction l with
  | nil => rfl
  | cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]

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

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

Tactic:
norm_num [ht]

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

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t = 0
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
norm_num [ht]

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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t = 1
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
norm_num [ht]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
set p₂ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans .id (.refl _)) (.trans (.refl _) .id)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (0, 0) (1, 1) := (Path.id.trans (Path.refl 1)).prod ((Path.refl 0).trans Path.id)
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } x = p.symm.toContinuousMap x

Tactic:
by
    rcases hx with hx | hx
    · rw [hx]
      simp
    · rw [Set.mem_singleton_iff] at hx
      rw [hx]
      simp

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 Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject C)) f g

Tactic:
areEqualizedByLocalization_iff L

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ L.map f = L.map g
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (d.multispan.map (WalkingMultispan.Hom.fst l))) z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
ιColimitType_map

Goal state after:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.left l) z = d.multispan.ιColimitType (WalkingMultispan.left l) z
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
⊢ ∃ j, S = {j}ᶜ

Tactic:
rw [Finset.card_eq_one] at hS

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : ∃ a, Sᶜ = {a}
⊢ ∃ j, S = {j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: ⊢ ∂Δ[0] = ⊥

Tactic:
ext m x

Goal state after:
m : SimplexCategoryᵒᵖ
x : Δ[0].obj m
⊢ x ∈ ∂Δ[0].obj m ↔ x ∈ ⊥.obj m
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case mpr
n : ℕ
A : Δ[n].Subcomplex
⊢ ∂Δ[n] ≤ A ∧ A ≠ ⊤ → A = ∂Δ[n]

Tactic:
rintro ⟨h₁, h₂⟩
    exact le_antisymm (by rwa [le_boundary_iff]) h₁

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsLimit (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.mapCone (PullbackCone.mk (t i d) (l i d) ⋯))

Tactic:
refine (isLimitMapConePullbackConeEquiv _ _).2
      (IsPullback.isLimit ?_)

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPullback (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (t i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d)) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
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)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.castSucc =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]

Goal state after:
case h.inl
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)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 1).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
  exact (horn.isColimit 2).fac _ (.right ⟨1, by simp⟩)

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

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
⊢ (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f) =
    ((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z)

Tactic:
by ext ⟨f, g⟩; exact F.map_comp f g

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

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
f : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f

Tactic:
obtain ⟨x₀, x₁, f, rfl⟩ := Truncated.Edge.exists_of_simplex f
    simpa using congr_arg Truncated.Edge.edge (ReflPrefunctor.congr_hom h f)

Goal state after: