mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
⊢ R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X) →
    Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
      (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)

Tactic:
hR

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
⊢ Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
    (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ ∀ {S_1 : P.Over ⊤ S} {R : Presieve ((Over.forget P ⊤ S).obj S_1)},
    R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj S_1) →
      Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
        (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj S_1)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
⊢ ∀ {R : Presieve ((Over.forget P ⊤ S).obj X)},
    R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X) →
      Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
        (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
⊢ R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X) →
    Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
      (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)

Tactic:
hR

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁴ : P.IsStableUnderComposition
K : Precoverage C
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : K ≤ P.precoverage
this : (Over.forget P ⊤ S).LocallyCoverDense (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
R : Presieve ((Over.forget P ⊤ S).obj X)
hR : R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
⊢ Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R) ∈
    (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case right
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 : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))

Tactic:
intro X

Goal state after:
case right
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 : C
⊢ Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: ⊢ @Etale ≤ @WeaklyEtale

Tactic:
intro X

Goal state after:
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), Etale f → WeaklyEtale f
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
inst✝ : IsEmpty ↥S
⊢ ∀ (X : S.ProEt), ⊥ ∈ (topology S) X

Tactic:
intro X

Goal state after:
S : Scheme
inst✝ : IsEmpty ↥S
X : S.ProEt
⊢ ⊥ ∈ (topology S) X
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z
hR : Sieve.generate (Presieve.ofArrows (fun i ↦ (Over.forget X).obj (T i)) fun i ↦ (Over.forget X).map (g i)) ∈ J Z.left
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
hg : Presieve.Arrows.Compatible (CategoryTheory.yoneda.obj E.left) (fun i ↦ Over.Hom.left (g i)) fun i ↦
  Over.Hom.left (t (g i) ⋯) :=
  fun i j Z_1 gi gj hgij ↦
    id
      (congrArg Over.Hom.left
        (ht (Over.homMk gi rfl)
          (Over.homMk gj
            (id
              (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ (T j).hom = gi ≫ _a) (Eq.symm (Over.w (g i)))))
                (Eq.mpr
                  (id
                    (congrArg (fun _a ↦ gj ≫ (T j).hom = _a)
                      (id
                        (Eq.mp
                          (forall_congr fun {Z_2} ↦
                            forall_congr fun h ↦
                              congr (congrArg Eq (Category.assoc gi (Over.Hom.left (g i)) h))
                                (Category.assoc gj (Over.Hom.left (g j)) h))
                          (@Mathlib.Tactic.Reassoc.eq_whisker' C inst✝¹ Z_1 Z.left
                            (gi ≫ (fun i ↦ Over.Hom.left (g i)) i) (gj ≫ (fun i ↦ Over.Hom.left (g i)) j) hgij))
                        Z.hom)))
                  (Eq.mpr (id (congrArg (fun _a ↦ gj ≫ _a = gj ≫ Over.Hom.left (g j) ≫ Z.hom) (Eq.symm (Over.w (g j)))))
                    (Eq.refl (gj ≫ Over.Hom.left (g j) ≫ Z.hom)))))))
          (Sieve.ofArrows_mk T g i) (Sieve.ofArrows_mk T g j) (Over.OverMorphism.ext hgij)))
a : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)
ha : hg.familyOfElements.sieveExtend.IsAmalgamation a
huniq :
  ∀ (y : (CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left)),
    (fun t_1 ↦ hg.familyOfElements.sieveExtend.IsAmalgamation t_1) y → y = a
⊢ (fun t_1 ↦ t.IsAmalgamation t_1) (Over.homMk a ⋯)

Tactic:
rintro W p ⟨V, v, _, ⟨i⟩, rfl⟩
    refine Over.OverMorphism.ext ?_
    have := ha (g i).left (Sieve.ofArrows_mk _ _ i)
    dsimp at this
    simp [Category.assoc, this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i),
      Presieve.FamilyOfElements.comp_of_compatible _ ht (Sieve.ofArrows_mk _ _ i)]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso ((F y).obj j).obj.hom
⊢ ∃ j φ, y ≫ Y.map φ = 0

Tactic:
dsimp at h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
h : IsIso ((kernel.ι (g y)).app j)
⊢ ∃ j φ, y ≫ Y.map φ = 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
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 }

Tactic:
exact c.hm i

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

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

Tactic:
by
    have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij
    rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk]
    congr 1
    apply Arrow.functor_ext
    rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f
    dsimp
    rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc]
    rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))

Tactic:
have := hm.nonempty_Iio.to_subtype

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
m : J
hm : Order.IsSuccLimit m
this : Nonempty ↑(Set.Iio m)
⊢ IsColimit ((Set.principalSegIio m).cocone (functor hG A₀ J))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp ≤ (monomorphisms C).rlp

Tactic:
intro X

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), (generatingMonomorphisms G).rlp f → (monomorphisms C).rlp f
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts

Tactic:
intro X

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y),
    I.rlp.llp f → ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType).retracts f
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ ↑p ^ (-↑n)

Tactic:
split_ifs with hz

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:

Tactic:
_ ≤ p + k := by lia
      _ ≤ _ := Nat.add_le_mul hp.out.two_le (by lia)

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ log 2 n ≠ padicValNat 2 (n + 1)

Tactic:
by
  rw [Ne, log_eq_iff (by simp [hn])]
  rintro ⟨h1, h2⟩
  rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1
  rw [← add_one_le_iff, Nat.pow_succ] at h2
  refine not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd
  -- TODO(kmill): Why is this `p := 2` necessary?
  exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq

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

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

Tactic:
by
  constructor
  · intro hf
    simpa only [← cancel_epi f] using c.condition
  · intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
    rw [hf]

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
M : A
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((Φ.skyscraperPresheaf M).mapCone S.arrows.cocone.op))

Tactic:
intro X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
⊢ ∀ S ∈ J X, Nonempty (IsLimit ((Φ.skyscraperPresheaf M).mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
⊢ R ∈ J X → Nonempty (IsLimit ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op))

Tactic:
hR

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
⊢ Nonempty (IsLimit ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

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

Tactic:
simpa [← hg]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b

Tactic:
intro X

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
⊢ ∀ {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b
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 * ε

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

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✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)

Tactic:
dsimp at h

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) α =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op U))) β
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
⊢ (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
⊢ monomorphisms (Cᵒᵖ ⥤ Type v₁) f

Tactic:
suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
    ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩
  intro X a b h
  /- It suffices to show that the lifts of `a` and `b` to morphisms
  `X ⟶ hf.rep.pullback g` are equal, where `g = a ≫ f = a ≫ f`. -/
  suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
      hf.rep.lift b (𝟙 X) (by simp [← h]) by
    simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))
  -- This follows from the fact that the induced maps `hf.rep.pullback g ⟶ X` are mono.
  have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)
  simp only [← cancel_mono (hf.rep.snd (a ≫ f)), lift_snd]

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

Goal state before:
pp: case hbc.h₁.hbc
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
⊢ padicNormE (↑(limSeq f j) - ↑f j) + padicNormE (↑f j - ↑f (max N N2)) < ε / 3 + ε / 3

Tactic:
· apply _root_.add_lt_add
        · rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj
        · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
⊢ F.relativelyRepresentable (pullback.lift (𝟙 (F.obj a)) (𝟙 (F.obj a)) ⋯)

Tactic:
let pbIso := pullback.congrHom
    (terminal.comp_from _ : (g ≫ pullback.fst _ _) ≫ terminal.from X = terminal.from _)
    (terminal.comp_from _ : (g ≫ pullback.snd _ _) ≫ terminal.from X = terminal.from _) ≪≫
    (prodIsoPullback _ _).symm ≪≫ (HasLimit.isoOfNatIso (pairComp _ _ _)).symm ≪≫
    (preservesLimitIso _ (pair _ _)).symm
  rw [← comp_id (pullback.lift _ _), ← pbIso.hom_inv_id, ← Category.assoc]
  apply (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _
  exact map_preimage F (_ ≫ pbIso.hom) ▸ map F (F.preimage _)

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 0).f 1 +
      (X.σ 0 ≫ (P 0).f 1 ≫ (∑ i, (-1) ^ ↑i • X.δ i) ≫ ((-1) ^ 0 • X.σ ⟨0, ⋯⟩) +
        X.σ 0 ≫ (P 0).f 1 ≫ hσ' 0 1 2 ⋯ ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0

Tactic:
hσ'_eq' (add_zero 1).symm

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) ≫ ((-1) ^ 0 • X.σ ⟨0, ⋯⟩) +
        X.σ 0 ≫ (P 0).f 1 ≫ ((-1) ^ 1 • X.σ ⟨1, ⋯⟩) ≫ ∑ i, (-1) ^ ↑i • X.δ i) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ A.fst = Δ

Tactic:
dsimp at h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ Mono A.e

Tactic:
dsimp at h

Goal state after:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono A.e
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

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

Tactic:
dsimp at h

Goal state after:
case mp.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
f : Z ⟶ X _⦋0⦌
h : f ≫ 𝟙 (X _⦋0⦌) = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋0⦌)) = 0