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

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsConstant J F

Tactic:
F.isConstant_iff_isIso_counit_app (hT := hT)

Goal state after:
C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    (precoverage P).coverings S

Tactic:
· rw [Scheme.presieve₀_mem_precoverage_iff]
      exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (uliftYoneda.{w, v, u}.obj (F ⋙ uliftFunctor.{v, w}).reprX) R

Tactic:
dsimp only [uliftYoneda, Functor.comp_obj, Functor.whiskeringRight_obj_obj]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (yoneda.obj (F ⋙ uliftFunctor.{v, w}).reprX ⋙ uliftFunctor.{w, v}) R
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : J.Subcanonical
ι : Type u_1
inst✝² : CoproductsOfShapeDisjoint C ι
inst✝¹ : HasPullbacks C
inst✝ : HasStrictInitialObjects C
hcov : ∀ {X : ι → C} {c : Cofan X} (x : IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt
htriv : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
⊢ PreservesColimitsOfShape (Discrete ι) J.yoneda

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_of_discrete
  refine fun X ↦ ⟨fun {c : Cofan X} hc ↦ ⟨(Limits.Cofan.isColimitMapCoconeEquiv _ _ _).symm ?_⟩⟩
  have (i : ι) : Mono (c.inj i) := .of_coproductDisjoint hc _
  refine isColimitCofanMkYoneda _ _ (hcov hc) htriv fun hij Y a b hab ↦ ⟨?_⟩
  exact .ofCoproductDisjointOfCommSq hij hc _ _ hab

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    c.cofan₁.ι.app { as := i } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x ↦
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι }

Tactic:
IsColimit.fac

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι }.ι.app
      { as := i }
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ Nonempty (AttachCells g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
constructor
  · rintro ⟨c⟩
    exact c.pushouts_coproducts
  · rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩
    rw [coproducts_iff] at h
    obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
    let π (i : ι) : α := ((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose
    let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) :=
      eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)
    let e₁ (i : ι) : F₁.obj ⟨i⟩ ≅ A (π i) := Arrow.leftFunc.mapIso (e i)
    let e₂ (i : ι) : F₂.obj ⟨i⟩ ≅ B (π i) := Arrow.rightFunc.mapIso (e i)
    exact ⟨{
      ι := ι
      π := π
      cofan₁ := Cofan.mk c₁.pt (fun i ↦ (e₁ i).inv ≫ c₁.ι.app ⟨i⟩)
      cofan₂ := Cofan.mk c₂.pt (fun i ↦ (e₂ i).inv ≫ c₂.ι.app ⟨i⟩)
      isColimit₁ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₁ i)) _).1
          (IsColimit.ofIsoColimit h₁ (Cocone.ext (Iso.refl _) (by simp)))
      isColimit₂ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
          (IsColimit.ofIsoColimit h₂ (Cocone.ext (Iso.refl _) (by simp)))
      hm i := by simp [e₁, e₂]
      isPushout := sq, .. }⟩

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

Goal state before:
pp: case inr
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
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi]
      congr 1
      apply Arrow.functor_ext
      rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
      dsimp
      generalize_proofs
      rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ p ^ 1 ∣ n

Tactic:
pow_one

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ p ∣ n
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : 1 < padicNorm p a
⊢ ¬a.isInt = true

Tactic:
by
  contrapose! H
  rw [Rat.eq_num_of_isInt H]
  apply padicNorm.of_int

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ^ 1 ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
pow_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a.natAbs * b.natAbs) = padicValNat p a.natAbs + padicValNat p b.natAbs

Tactic:
padicValNat.mul

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p a.natAbs + padicValNat p b.natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs

case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.natAbs ≠ 0

case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.natAbs ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑(f - 0) j) < ε

Tactic:
intro j hj

Goal state after:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
⊢ padicNorm p (↑(f - 0) j) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : f.norm = padicNorm p (↑f (stationaryPoint hf))
h : ↑f (stationaryPoint hf) = 0
⊢ f.norm = 0

Tactic:
simpa [h] using heq

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

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

Tactic:
by_cases hx : ‖x‖ ≤ 1
    · use (⟨x, hx⟩, 1)
      rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]
    · set n := Int.toNat (-x.valuation) with hn
      have hn_coe : (n : ℤ) = -x.valuation := by
        rw [hn, Int.toNat_of_nonneg]
        rw [Right.nonneg_neg_iff]
        rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
        exact hx.le
      set a := x * (p : ℚ_[p]) ^ n with ha
      have ha_norm : ‖a‖ = 1 := by
        have hx : x ≠ 0 := by
          intro h0
          rw [h0, norm_zero] at hx
          exact hx zero_le_one
        rw [ha, padicNormE.mul, Padic.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx,
          ← zpow_add', hn_coe, neg_neg, neg_add_cancel, zpow_zero]
        exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))
      use
        (⟨a, le_of_eq ha_norm⟩,
          ⟨(p ^ n : ℤ_[p]), mem_nonZeroDivisors_iff_ne_zero.mpr (NeZero.ne _)⟩)
      simp only [a, map_pow, map_natCast, algebraMap_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
⊢ IsIso c.inl

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
h : c.inl = c.inr
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ IsIso c.inl
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
⊢ c.inl = c.inr

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PushoutCocone.IsColimit.desc' hc (𝟙 Y) (𝟙 Y) (by simp)

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ c.inl = c.inr
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h.h.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
N✝ i✝ : ℕ
a✝ : i✝ ≥ N✝
N : (f - const (padicNorm p) (↑f i✝)).norm < ε
⊢ { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Padic.mk f - ↑(↑f i✝)) < ε

Tactic:
use N

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
⊢ ∀ j ≥ max N N2, padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
intro j hj

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: 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 φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i.succ + q
⊢ n + 1 ≤ ↑i + q

Tactic:
simp only [Fin.val_succ] at hj₂

Goal state after:
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 φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(padicValNat p 1) = 0

Tactic:
padicValNat_one_right,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑x.valuation) (if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hxy, if_pos rfl]
    exact le_top

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ φ ≫ X.δ (j.succ.pred ⋯) ≫ X.σ (⟨b, ⋯⟩.castLT ⋯) = 0

pp: case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b, ⋯⟩.succ < j.succ

Tactic:
Fin.pred_succ,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ φ ≫ X.δ j ≫ X.σ (⟨b, ⋯⟩.castLT ⋯) = 0

case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ⟨b, ⋯⟩.succ < j.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
⊢ A₁ = A₂

Tactic:
by
  rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
  rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
  simp only at h₁
  subst h₁
  simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂
  simp only [h₂]

Goal state after:
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)
⊢ ∀ x ∈ {i | ↑i < q},
    (((P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ X.σ i) ≫
        (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
      0

Tactic:
intro j hj

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)
j : Fin (n + 1)
hj : j ∈ {i | ↑i < q}
⊢ (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    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
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
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
n : ℕ
⊢ S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)

Tactic:
rw [c₁, c₂]

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 : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ map K A.e.op) ≫ map K θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op

Tactic:
change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ ((splitting K).ι (unop A.fst).len ≫ (obj K).map A.e.op) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (functor ⋙ inverse).map φ ≫ { f := { f := fun n ↦ Q.p.f n, comm' := ⋯ }, comm := ⋯ } =
    { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ } ≫ (𝟭 (Karoubi (HomologicalComplex C c))).map φ

Tactic:
by
        ext
        dsimp
        simp only [HomologicalComplex.comp_p_d, HomologicalComplex.p_comp_d]

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

Goal state before:
pp: case nil
α : Type u_1
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast ⋯ ⋯ Path.nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
⊢ pathToList (listToPath []) = []

Tactic:
| nil =>

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

Goal state before:
pp: case h_map
A : TopCat
B : TopCat
x₀ : ↑A
x₁ : ↑B
y₀ : ↑A
y₁ : ↑B
f : { as := (x₀, x₁) } ⟶ { as := (y₀, y₁) }
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).map f ≍ (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).map f

Tactic:
simpa [-Path.Homotopic.prod_projLeft_projRight] using! Path.Homotopic.prod_projLeft_projRight f

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
⊢ PathConnectedSpace X

Tactic:
obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : (ContinuousMap.id X).Homotopy (const X p)
⊢ PathConnectedSpace X
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
by
  simp only [simplyConnectedSpace_iff, equiv_punit_iff_unique,
    FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]
  intros
  exact ⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩

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

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p

Tactic:
dsimp only [prodToProdTopI]

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : range (𝟙 A.toFunctor ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ 𝟙 A.toFunctor ≫ f = 𝟙 A.toFunctor ≫ g
⊢ Subfunctor.equalizer f g = A ↔ f = g

Tactic:
simp only [Category.id_comp, range_ι] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
⊢ Subfunctor.equalizer f g = A ↔ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case mpr
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1

Tactic:
rintro ⟨k, h₁, h₂⟩
    exact ⟨k.rev, by grind⟩

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

Goal state before:
pp: case mpr
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ¬j_1 = i.rev ∧ ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ¬j_1 = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1

Tactic:
· rintro ⟨k, h₁, h₂⟩
    exact ⟨k.rev, by grind⟩

Goal state after:
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)
⊢ ∀ (a : Fin (n + 1 + 1)), ¬a = i → yonedaEquiv (stdSimplex.δ a) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)

Tactic:
intro j hj

Goal state after:
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
⊢ yonedaEquiv (stdSimplex.δ j) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)