mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m =
    {
      hom :=
        ⋯.extend
          {
            app := fun Y ↦
              ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
            naturality := ⋯ } }

Tactic:
ext : 1

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m.hom =
    {
        hom :=
          ⋯.extend
            {
              app := fun Y ↦
                ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
              naturality := ⋯ } }.hom
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩

Tactic:
h.src

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
h : ∀ (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x), MapEq F G k₁ k₂ h₁₂ h₂
k₁ : K
property✝ : k₁ ∈ Set.Iic x
k₂ : K
h₂ : k₂ ∈ Set.Iic x
f : ⟨k₁, property✝⟩ ⟶ ⟨k₂, h₂⟩
⊢ F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)

Tactic:
apply h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
x : FunctorObjIndex f πX
⊢ f x.i ≫ Sigma.ι (functorObjTgtFamily f πX) x ≫ ρFunctorObj f πX = x.t ≫ ιFunctorObj f πX

Tactic:
by
  simpa using (Sigma.ι (functorObjSrcFamily f πX) x ≫= functorObj_comm f πX).symm

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

Goal state before:
pp: case inr
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
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ False

Tactic:
exact hj hi.isMax

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)

Tactic:
simp [finite_int_prime_iff]

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
rw [add_comm, max_comm]
    exact this (le_of_not_ge hle)

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

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range (d + 1), F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)

Tactic:
Finset.sum_range_succ

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpenEmbedding Subtype.val

Tactic:
refine (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1}).isOpenEmbedding_subtypeVal
  simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using
    IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
⊢ padicValNat p (p ^ n * q ^ m) = n

Tactic:
by
  rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
← Nat.sub_add_comm <| digit_sum_le p k,

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (-↑f m)) (padicNorm p (↑f n))
⊢ False

Tactic:
rw [padicNorm.neg, max_comm] at hnam

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
set n := Int.toNat (-x.valuation) with hn

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1
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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
X✝ : Sheaf J A
Y✝ Y'✝ : A
f : Φ.sheafFiber.obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
⊢ (Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) (f ≫ g) =
    (Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) f ≫
      Φ.skyscraperSheafFunctor.map g

Tactic:
ext : 1

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
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
X✝ : Sheaf J A
Y✝ Y'✝ : A
f : Φ.sheafFiber.obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
⊢ ((Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) (f ≫ g)).hom =
    ((Φ.skyscraperPresheafHomEquiv.trans (fullyFaithfulSheafToPresheaf J A).homEquiv.symm) f ≫
        Φ.skyscraperSheafFunctor.map g).hom
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Presheaf.IsLocallySurjective J f

Tactic:
wlog hF₂ : ∃ (U : C), F₂ = shrinkYoneda.obj U generalizing F₁ F₂

Goal state after:
case inr
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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f

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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
hF₂ : ∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
⊢ Presheaf.IsLocallySurjective J f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
rw [PadicSeq.norm, dif_pos h] at hge
    exact not_lt_of_ge hge hε

Goal state after:
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 : ι
⊢ yoneda.map (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom = f i

Tactic:
apply yonedaEquiv.injective
  rw [yonedaGluedToSheaf, yonedaEquiv_apply, yonedaEquiv_apply,
    NatTrans.comp_app_apply, yoneda_map_app]
  simpa using! GlueData.sheafValGluedMk_val _ _ _ _

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

Goal state before:
pp: case refine_1
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
⊢ IsPullback fst (F✝.map snd) (f ≫ g) p

Tactic:
exact h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: case e_a
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : yoneda.map a ≫ f i = yoneda.map b ≫ f j
⊢ ⋯.fst' (f j) ≫ toGlued hf i = ⋯.snd (f j) ≫ toGlued hf j

Tactic:
exact ((glueData hf).glue_condition i j).symm.trans (by simp [toGlued])

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

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 1).f 1 = 0

Tactic:
simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 ≫ (P 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ hσ' 0 0 1 ⋯ +
        X.σ 0 ≫ (P 0).f 1 ≫ hσ' 0 1 2 ⋯ ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.inr.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ ⟨a + 1, ⋯⟩ = j.castSucc

pp: case neg.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)

Tactic:
· ext
      cases j
      dsimp
      dsimp only [Nat.succ_eq_add_one] at *
      lia

Goal state after:
case neg.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ ↑j + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = ↑j
haj : a < ↑j
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (⟨a, ⋯⟩.castLT ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop A.fst).len = (unop Δ).len

Tactic:
exact h

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

Goal state before:
pp: case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)

Tactic:
| _ n
   => 

Goal state after:
case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ f.app (op ⦋n⦌) = (s.cofan (op ⦋n⦌)).inj A ≫ g.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
x✝ : ℕ
⊢ f₁ x✝ = f₂ x✝

Tactic:
apply h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (if h : A = B then eqToHom ⋯ else 0) = 0

Tactic:
dif_neg h.symm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ 0 = 0
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₁Γ₀
h :
  (toKaroubi (ChainComplex C ℕ)).whiskerLeft
      ({ obj := fun G ↦ toKaroubi (ChainComplex C ℕ) ⋙ G,
            map := fun {X Y} α ↦ (toKaroubi (ChainComplex C ℕ)).whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.preimage
        e.hom) =
    e.hom
⊢ (toKaroubi (ChainComplex C ℕ)).whiskerLeft
      ({ obj := fun G ↦ toKaroubi (ChainComplex C ℕ) ⋙ G,
            map := fun {X Y} α ↦ (toKaroubi (ChainComplex C ℕ)).whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.preimage
        (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom) =
    N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom

Tactic:
exact h

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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
· have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
      dsimp at h'
      rw [comp_id, comp_add, h, zero_add] at h'
      rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
        Finset.sum_eq_zero]
      intro i _
      simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]

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

Goal state before:
pp: case mk.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
subst hk

Goal state after:
case mk.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
i : ⦋m⦌ ⟶ ⦋m + 1⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ m + 1
h₂ : ¬Isδ₀ i
⊢ PInfty.f (m + 1) ≫ X.map i.op = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
h₁ : ⦋m⦌.len ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
subst hk

Goal state after:
case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map i.op = 0
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂.map (𝟙 (N₁.obj X)) = 𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
Γ₂.map_id

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ 𝟙 (Γ₂.obj (N₁.obj X)) = 𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op

Tactic:
| _ n
   => 

Goal state after:
case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case neg.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

Tactic:
exact h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F G : ReflPrefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
obtain ⟨Fpre, Fid⟩ := F
  obtain ⟨Gpre, Gid⟩ := G
  obtain rfl : Fpre = Gpre := Prefunctor.ext' (V := V) (W := W) h_obj h_map
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm = G.symm.trans F.symm

Tactic:
ext : 1

Goal state after:
case fst
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.fst = (G.symm.trans F.symm).fst

case snd
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case neg
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ ↑x.1 * (2 - 2 * ↑x.2) ∈ I

Tactic:
· constructor
    · apply mul_nonneg <;> grind
    · apply mul_le_one₀ <;> grind

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
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (CofibrantObject C))

Tactic:
rintro X Y f g h

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
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject C)) f g