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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : R.EffectiveEpimorphic
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor F R

Tactic:
Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda

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 F R
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : (Sieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀)).arrows d
hc :
  ((fun Y₀ a ha ↦
          Sieve.functorPullback F
            (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
              (data Y).toPreOneHypercover.sieve₀))
        Y₀ d hd).arrows
    c
⊢ (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op

Tactic:
have hc' := Sieve.ofArrows.fac hc

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : (Sieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀)).arrows d
hc :
  ((fun Y₀ a ha ↦
          Sieve.functorPullback F
            (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
              (data Y).toPreOneHypercover.sieve₀))
        Y₀ d hd).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
⊢ (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map { Y := U₀, f := c ≫ d, hf := ⋯ }.f.op
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ⋯
F : D ⥤ C := ⋯
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
⊢ ∀ (a : α), π a ≫ m = S.ι.app { obj := Over.mk (π a), property := ⋯ }

Tactic:
intro a

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      g₁ ≫ S.ι.app { obj := Over.mk (π a₁), property := ⋯ } = g₂ ≫ S.ι.app { obj := Over.mk (π a₂), property := ⋯ }
a : α
⊢ π a ≫ m = S.ι.app { obj := Over.mk (π a), property := ⋯ }
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B✝ : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B✝
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over B✝
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over B✝
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
h1 : ∃ a g, g ≫ π a = B.hom
h2 : ∃ g, g ≫ π h1.choose = B.hom
h3 : ∃ a g, g ≫ π a = A.hom
h4 : ∃ g, g ≫ π h3.choose = A.hom
⊢ Over.Hom.left q ≫ h2.choose ≫ π h1.choose = h4.choose ≫ π h3.choose

Tactic:
rw [h2.choose_spec, h4.choose_spec, Over.w]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ (Presieve.singleton f).EffectiveEpimorphic

Tactic:
Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ ∀ (Y_1 : Scheme), Presieve.IsSheafFor (yoneda.obj Y_1) (Presieve.singleton f)
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ (Presieve.singleton f).EffectiveEpimorphic

Tactic:
Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFinitePresentation f
inst✝¹ : Surjective f
inst✝ : Flat f
⊢ ∀ (Y_1 : Scheme), Presieve.IsSheafFor (yoneda.obj Y_1) (Presieve.singleton f)
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W} e h ↦
    { pt := W,
      ι :=
        {
          app := fun x ↦
            match x with
            | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT),
          naturality := ⋯ } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ m = H.desc (aux e ⋯)

Tactic:
apply H.uniq (aux e h)
      rintro ⟨T, a, (g : T.left ⟶ _), ha⟩
      dsimp
      simp only [← ha, Category.assoc, hm]
      apply h
      generalize_proofs h1 h2
      rwa [h2.choose_spec]

Goal state after:
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✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
⊢ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Tactic:
by
  refine (ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)
  refine ShortComplex.isoMk
    (IsColimit.coconePointUniqueUpToIso hc₁ (colimit.isColimit _))
    (IsColimit.coconePointUniqueUpToIso hc₂ (colimit.isColimit _))
    (IsColimit.coconePointUniqueUpToIso hc₃ (colimit.isColimit _))
    (hc₁.hom_ext (fun j ↦ ?_)) (hc₂.hom_ext (fun j ↦ ?_))
  · dsimp
    rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
  · dsimp
    rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a

Tactic:
intro a

Goal state after:
case le_succ
a : Fin 0
⊢ a ≤ ?succ a
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a

Tactic:
intro a

Goal state after:
case max_of_succ_le
a : Fin 0
⊢ ?succ a ≤ a → IsMax a
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b

Tactic:
intro a

Goal state after:
case succ_le_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → ?succ a ≤ b
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case succ
⊢ Fin 0 → Fin 0

Tactic:
intro a

Goal state after:
case succ
a : Fin 0
⊢ Fin 0
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a

Tactic:
intro a

Goal state after:
case pred_le
a : Fin 0
⊢ ?pred a ≤ a
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a

Tactic:
intro a

Goal state after:
case min_of_le_pred
a : Fin 0
⊢ a ≤ ?pred a → IsMin a
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b

Tactic:
intro a

Goal state after:
case le_pred_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a ≤ ?pred b
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: case pred
⊢ Fin 0 → Fin 0

Tactic:
intro a

Goal state after:
case pred
a : Fin 0
⊢ Fin 0
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
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'

Tactic:
apply Cofan.IsColimit.hom_ext c.isColimit₂

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
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u'
inst✝¹² : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝¹¹ : LinearOrder J
inst✝¹⁰ : SuccOrder J
inst✝⁹ : OrderBot J
inst✝⁸ : WellFoundedLT J
J'✝ : Type w'
inst✝⁷ : LinearOrder J'✝
inst✝⁶ : SuccOrder J'✝
inst✝⁵ : OrderBot J'✝
inst✝⁴ : WellFoundedLT J'✝
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : OrderBot J'
inst✝¹ : SuccOrder J'
inst✝ : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
⊢ W ((h.ofOrderIso e).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem (e j) (by simpa only [e.isMax_apply])
    rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
    have eq : Arrow.mk (homOfLE (e.monotone (Order.le_succ j))) =
      Arrow.mk (homOfLE (Order.le_succ (e j))) :=
        Arrow.ext rfl (e.map_succ j) rfl
    replace eq := congr_arg h.F.mapArrow.obj eq
    convert! this using 1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Φ.toSuccArrow X).hom = (Arrow.mk f).hom ≫ (eqToIso ⋯).hom

Tactic:
simp [hf.fac]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : i₁ < j
⊢ obj c j = obj c i₂

Tactic:
by subst h₂'; rfl

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

Goal state before:
pp: 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
⊢ map hj F τ j (Order.succ j) ⋯ ⋯ = (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
by
  dsimp [map]
  rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
    dif_pos (by rfl), Functor.map_id, comp_id, id_comp]

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

Goal state before:
pp: case inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃

Tactic:
rw [map_id, id_comp]

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

Goal state before:
pp: case neg
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 k₁ : J
h₁ : Order.IsSuccLimit k₁
h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration k₁
this✝ : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁), k₂ < k₁ → MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃
h₁₂ h₃ : k₁ ≤ k₁
h₄ : ¬k₁ < k₁
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < k₁
⊢ iter₁.F.obj ⟨k₁, h₃⟩ = iter₂.F.obj ⟨k₁, h₃⟩

Tactic:
simp only [obj_limit _ _ h₁, this]

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

Goal state before:
pp: case inl
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
hi₁✝ : i ≤ j
hi₁ : i < 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:
arrowSucc_def,

Goal state after:
case inl
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
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowSucc (functor hj iter) i hi = Φ.toSuccArrow ((functor hj iter).obj ⟨i, ⋯⟩)

Tactic:
arrowSucc_def,

Goal state after:
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowMap (functor hj iter) i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow ((functor hj iter).obj ⟨i, ⋯⟩)
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 Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)
a : G ⟶ X
ha :
  (fun x ↦ x ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)) a = pushout.inr (pullback.fst p f) (pullback.snd p f)
⊢ (ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) a = f

Tactic:
by simpa using ha =≫ pushout.desc p f pullback.condition

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1

Tactic:
rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
      intro h
      exact (Nat.not_lt_zero p h).elim

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

Goal state before:
pp: case zero
p m : ℕ
hp : Fact (Nat.Prime p)
h : 0 < p
⊢ padicValNat p (p * m + 0)! = padicValNat p (p * m)!

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ a, (padicValuation p) a = 0

Tactic:
| zero =>

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * ↑p) = padicValInt p a + 1

Tactic:
rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p ↑p = padicValInt p a + 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = ↑p ^ (-f.valuation)

Tactic:
rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg]

Goal state after:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp.refine_1
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
⊢ c.inl ≫ φ ≫ c.inl = c.inl ≫ 𝟙 c.pt

Tactic:
simp only [comp_id, reassoc_of% hφ₁]

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
⊢ Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
intro
    exact IsPushout.of_isColimit (PushoutCocone.isColimitMkIdId f)

Goal state after:
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
inst✝ : HasSheafify J (Type w)
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
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ IsIso f

Tactic:
by
        have : Epi f := by
          rw [← Sheaf.isLocallySurjective_iff_epi]
          exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)
        exact Balanced.isIso_of_mono_of_epi f

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

Goal state before:
pp: case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε

pp: case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε

Tactic:
· exact (div_le_iff₀ hε).mp (le_trans (le_of_lt hN) (mod_cast hi))

Goal state after:
case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f 0 = 0

Tactic:
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 ⋯ ≫ K[X].d 1 0 = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n m : ℕ
hnm : c.Rel m n
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌)

Tactic:
obtain rfl : n + 1 = m := hnm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ hσ' q n (n + 1) ⋯ = hσ' q n (n + 1) ⋯ ≫ f.app (op ⦋n + 1⦌)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (P 0).f 0 = 𝟙 (K[X].X 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ (P 0).f (n + 1) = φ

Tactic:
| zero =>

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
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯)

Tactic:
intro a

Goal state after:
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
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
a : C
⊢ ∀ (g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)),
    ∃ b snd fst, IsPullback fst (F.map snd) (pullback.lift (𝟙 X) (𝟙 X) ⋯) g
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 a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
intro a

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ P 0 = P 0 ≫ (alternatingFaceMapComplex C).map f

Tactic:
| zero =>

Goal state after: