mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
⊢ Mono f

Tactic:
refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
    ((inferInstance : Mono (colim.map φ)))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
⊢ Arrow.mk f ≅ Arrow.mk (colim.map φ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
i : J
hi₀ : i = s.top
⊢ HasColimitsOfShape α C

Tactic:
induction i using SuccOrder.limitRecOn with

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
w✝⁴ : Type w
w✝³ : LinearOrder w✝⁴
w✝² : SuccOrder w✝⁴
w✝¹ : OrderBot w✝⁴
w✝ : WellFoundedLT w✝⁴
hf : W.transfiniteCompositionsOfShape w✝⁴ f
⊢ W.rlp.llp f

Tactic:
exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * q.num)

Tactic:
simpa [finite_int_prime_iff, hqz, hc2] using hd

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A = ⊤
⊢ A ≤ largerSubobject hG A

Tactic:
subst hA
    simp only [largerSubobject_top, le_refl]

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
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑q.den * ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

Tactic:
rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]

Goal state after:
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
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

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)

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.num * r.num)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : ↑p ≠ 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD maximalIdeal ℤ_[p] ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD maximalIdeal ℤ_[p] ^ n • ⊤]

Tactic:
simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.sub_mem, maximalIdeal_eq_span_p,
      Ideal.span_singleton_pow, ← norm_le_pow_iff_mem_span_pow] at hx ⊢

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖x‖ * ‖↑p ^ n‖ = 1

Tactic:
Padic.norm_p_pow,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖x‖ * ↑p ^ (-↑n) = 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Goal state after:
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
P : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
g : M ⟶ N
x✝ : Cᵒᵖ
b✝ : unop (Φ.fiber.op.obj x✝)
⊢ (Φ.skyscraperPresheafHomEquiv (f ≫ g)).app x✝ ≫ Pi.π (fun t ↦ N) b✝ =
    ((Φ.skyscraperPresheafHomEquiv f).app x✝ ≫ Limits.Pi.map fun x ↦ g) ≫ Pi.π (fun t ↦ N) b✝

Tactic:
skyscraperPresheafHomEquiv_app_π

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
P : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
g : M ⟶ N
x✝ : Cᵒᵖ
b✝ : unop (Φ.fiber.op.obj x✝)
⊢ Φ.toPresheafFiber (unop x✝) b✝ P ≫ f ≫ g =
    ((Φ.skyscraperPresheafHomEquiv f).app x✝ ≫ Limits.Pi.map fun x ↦ g) ≫ Pi.π (fun t ↦ N) b✝
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
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective fun x ↦ Φ.presheafFiber.map f ≫ x

Tactic:
← Function.Bijective.of_comp_iff' Φ.skyscraperPresheafHomEquiv.bijective

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
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective (⇑Φ.skyscraperPresheafHomEquiv ∘ fun x ↦ Φ.presheafFiber.map f ≫ x)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg

Tactic:
exact le_rfl

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

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
⊢ ∃ i, (s i) default = X.hom x

Tactic:
have := Set.mem_univ (X.hom x)
      simp only [← hs, Functor.id_obj, Set.mem_iUnion, Set.mem_range] at this
      obtain ⟨i, y, hy⟩ := this
      obtain rfl := Subsingleton.elim y default
      exact ⟨i, hy⟩

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.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
⊢ ∃ b snd fst, IsPullback fst (F.map snd) f g

pp: case refine_2
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.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
⊢ P snd

Tactic:
all_goals obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g

Goal state after:
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.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ ∃ b snd fst, IsPullback fst (F.map snd) f g

case refine_2
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.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ P snd
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ (((P q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1)) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
v.comp_P_eq_self,

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
simp only [id_comp, eqToHom_refl, comp_id]

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + (q + 1)
⊢ X.σ i ≫ (P (q + 1)).f (n + 1) = 0

Tactic:
by_cases h : n + 1 ≤ (i : ℕ) + q
    · rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
    · replace hi : n = i + q := by lia
      rcases n with _ | n
      · fin_cases i
        dsimp at h hi
        rw [show q = 0 by lia]
        change X.σ 0 ≫ (P 1).f 1 = 0
        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]
        rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]
        dsimp [P_zero]
        rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]
        rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
        simp only [add_neg_cancel, add_zero, zero_add]
      · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]
        have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
        dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]
        rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]
        intro j hj
        simp only [Finset.mem_univ, Finset.mem_filter] at hj
        obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
        rw [add_comm] at hk
        have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
        have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
        rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]
        simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]
        lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (b : Splitting.IndexSet Δ),
    Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) b ≫
        (Iso.refl (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))).pt).hom =
      (Splitting.cofan' (fun n ↦ K.X n) (obj K)
            (fun n ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ).inj
        b

Tactic:
by
      intro A
      dsimp [Splitting.cofan']
      rw [comp_id, Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl), Γ₀.Obj.Termwise.mapMono_id]
      dsimp
      rw [id_comp]
      rfl

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✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.cofan_inj_eq, assoc,
    degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ (((N₁ ⋙ Γ₂).obj X).X.map θ ≫ (Γ₀.splitting K[X]).desc Δ' fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) =
    ((Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫
      ((toKaroubi (SimplicialObject C)).obj X).X.map θ

Tactic:
apply (Γ₀.splitting K[X]).hom_ext'
            intro A
            change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _
            simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc,
              Splitting.ι_desc]
            erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]
            dsimp only [toKaroubi]
            simp only [← X.map_comp]
            congr 2
            simp only [← op_comp]
            exact Quiver.Hom.unop_inj (A.fac_pull θ)

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

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as

Tactic:
apply Prod.ext <;> simp

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).obj X✝).as = X✝.as.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projRight A B).obj X✝).as = X✝.as.2
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_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    Path.Homotopic.Quotient.trans ⟦Path.refl X_1.as⟧ f = f

Tactic:
rintro _ _ ⟨f⟩; exact Quotient.sound ⟨Path.Homotopy.reflTrans f⟩

Goal state after:
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 = n + 1
⊢ Sᶜ.card = 1

Tactic:
have := S.card_compl_add_card

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 : S.card = n + 1
this : Sᶜ.card + S.card = Fintype.card (Fin (n + 1 + 1))
⊢ Sᶜ.card = 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 < n ∨ 2 = n

Tactic:
← le_iff_lt_or_eq

Goal state after:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 ≤ n
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

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

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

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

Tactic:
· obtain z₁ | z₂ := z
      · rw [inl_rel'_inl_iff] at hyz
        obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz
        · exact Rel'.inl_inl _ _ h
        · obtain rfl := (mono_iff_injective f).1 inferInstance h''
          exact Rel'.inl_inl _ _ (h.trans h')
      · rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr

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

case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
z : X₁ ⊕ X₂
s✝ : S
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) z
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) z
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ Λ[2, 0] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
· rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
⊢ Mono k

Tactic:
subst facr facb

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
⊢ Mono k
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ Λ[2, 1] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
· rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
· rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

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

Goal state before:
pp: case hᵥ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (0 + 1)
⊢ f.vertex i = g.vertex i

pp: case hₐ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i

Tactic:
· fin_cases i; exact h

Goal state after:
case hₐ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
k : Fin (0 + 1)
ksucc : Fin (0 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ k = 0

Tactic:
by omega

Goal state after: