mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

pp: case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
h : ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
· rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
    intro x
    obtain ⟨y, hy⟩ := 𝒰.covers x
    refine ⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ _ ?_,
      𝒰.map_prop _, hy⟩
    use 𝒰.idx x

Goal state after:
case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
h : ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
⊢ ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (basicOpen 𝒜 ↑i).carrier
this : ⋃ i, ↑(basicOpen 𝒜 ↑i) = Set.univ
⊢ IsCompact Set.univ

Tactic:
← this

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
H : ∀ (i : ↥x), IsCompact (basicOpen 𝒜 ↑i).carrier
this : ⋃ i, ↑(basicOpen 𝒜 ↑i) = Set.univ
⊢ IsCompact (⋃ i, ↑(basicOpen 𝒜 ↑i))
Module: Mathlib.CategoryTheory.Limits.Elements

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  (hom ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i))
      ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd) =
    (hom (A.map (limit.π (F ⋙ π A) i))) ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)
⊢ (hom (limit.π ((F ⋙ π A) ⋙ A) i))
      ((preservesLimitIso A (F ⋙ π A)).toEquiv ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)) =
    (hom (limit.π ((F ⋙ π A) ⋙ A) i)) ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))

Tactic:
have h₂ := (c.π.app i).property

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : C ⥤ Type w
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : Small.{w, u₁} I
F : I ⥤ A.Elements
inst✝¹ : HasLimitsOfShape I C
inst✝ : PreservesLimitsOfShape I A
c : Cone F
i : I
h₁ :
  (hom ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i))
      ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd) =
    (hom (A.map (limit.π (F ⋙ π A) i))) ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)
h₂ : (hom (A.map ↑(c.π.app i))) (((Functor.const I).obj c.pt).obj i).snd = (F.obj i).snd
⊢ (hom (limit.π ((F ⋙ π A) ⋙ A) i))
      ((preservesLimitIso A (F ⋙ π A)).toEquiv ((hom (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)))) c.pt.snd)) =
    (hom (limit.π ((F ⋙ π A) ⋙ A) i)) ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))
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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
Z : C
g : Z ⟶ W
hg : S.arrows g
⊢ data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯) ∈ J₀ (Presieve.getFunctorPushforwardStructure ⋯).preobj

Tactic:
let str := Presieve.getFunctorPushforwardStructure hg.bindStruct.hg

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
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
hS : S ∈ J W
Z : C
g : Z ⟶ W
hg : S.arrows g
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hg).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
⊢ data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯) ∈ J₀ (Presieve.getFunctorPushforwardStructure ⋯).preobj
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝³ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory A FC
P : Cᵒᵖ ⥤ A
inst✝¹ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝ : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType (P.obj (op X))
Y : C
f : Y ⟶ X
y : Φ.fiber.obj Y
hf : (ConcreteCategory.hom (Φ.fiber.map f)) y = x
hf' : (ConcreteCategory.hom (P.map f.op)) z₁ = (ConcreteCategory.hom (P.map f.op)) z₂
⊢ ∃ j f,
    (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₁ =
      (ConcreteCategory.hom (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f)) z₂

Tactic:
exact ⟨⟨Y, y⟩, ⟨f, hf⟩, hf'⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ IsIso M.fromTildeΓ

Tactic:
rw [isIso_fromTildeΓ_iff_isLocalizing, isLocalizing_iff_aux]
  obtain ⟨ι, U, pres, hU, hU'⟩ := M.exists_isOpenCover_presentation
  obtain ⟨s, hs⟩ := hU.exists_finite_of_compactSpace
  choose κ hκ a ha using fun i : s ↦
    PrimeSpectrum.isBasis_basic_opens.exists_iSup_eq_of_isCompact (U i) (hU' i).isCompact
  refine Aux.of_eq_iSup_basicOpen _ (fun i : Sigma κ ↦ a _ i.2) ?_ ?_
  · rw [IsOpenCover] at hs
    rw [eq_comm, iSup_sigma, ← hs]
    exact iSup_congr fun i ↦ (ha i).symm
  · intro i
    let t := (Spec R).homOfLE (U := PrimeSpectrum.basicOpen (a _ i.2)) (V := U i.1)
      (by rw [ha]; exact le_iSup_of_le _ le_rfl)
    let iso : restrictFunctor (U i.1).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway _).inv ≫ t) ≅
        restrictFunctor (Spec.map (CommRingCat.ofHom <| algebraMap _ _)) :=
      (restrictFunctorComp _ _).symm ≪≫
        restrictFunctorCongr (by simp [t, basicOpenIsoSpecAway])
    let pres := SheafOfModules.Presentation.ofIsIso.{u, u, u} (iso.app M).hom <|
      presentationRestrict ((basicOpenIsoSpecAway _).inv ≫ t) (pres i.1)
    have : IsIso _ := isIso_fromTildeΓ_of_presentation (M.restrict _) pres
    rw [isIso_fromTildeΓ_iff_isLocalizing, isLocalizing_iff_aux] at this
    exact aux_basicOpen_of_aux_restrict _ _ this

Goal state after:
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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.functorPullback F (Sieve.pullback ((data a.Y).f i ≫ a.f) (data X).toPreOneHypercover.sieve₀), ⋯⟩),
    ((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
      (s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op

Tactic:
rintro ⟨X₀, b, ⟨_, c, _, h, fac₁⟩⟩

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
w✝¹ : C
c : F.obj X₀ ⟶ w✝¹
w✝ : w✝¹ ⟶ X
h : Presieve.ofArrows (data X).toPreOneHypercover.X (data X).toPreOneHypercover.f w✝
fac₁ : c ≫ w✝ = F.map b ≫ (data a.Y).f i ≫ a.f
⊢ ((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
      (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op =
    (s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
hP : P ≤ fun x x_1 f ↦ IsOpenMap ⇑f
X : Scheme
E : (precoverage P).ZeroHypercover X
⊢ QuasiCompactCover E.toPreZeroHypercover

Tactic:
exact .of_isOpenMap fun i ↦ hP _ (Scheme.Cover.map_prop E i)

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
R : Presieve S
x✝ : ∃ 𝒰, QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
𝒰 : Cover (precoverage P) S
left✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
h : R = 𝒰.presieve₀
⊢ 𝒰.presieve₀ ∈ qcPrecoverage.coverings S

Tactic:
simpa

Goal state after:
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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
i : (data X).I₀
p : F.obj X₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = f
⊢ restriction data G₀ f = presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
by
  simpa using restriction_map data G₀ f (𝟙 _) p (by simpa using fac)

Goal state after:
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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ hom data G₀ X₀ ≫ G₀.obj.map c.op = presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ p)

Tactic:
exact hom_map data G₀ c _ (by simp only [assoc, fac, hc])

Goal state after:
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 X
hR :
  Presieve.map (Over.forget P ⊤ S) 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) (Presieve.map (Over.forget P ⊤ S) R)) ∈
    (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)

Tactic:
simpa

Goal state after:
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
T : Presieve X
hR :
  Presieve.map (Over.forget P ⊤ S) T ∈
    (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) (Presieve.map (Over.forget P ⊤ S) T)) ∈
    (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)

Tactic:
simpa

Goal state after:
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
⊢ (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck =
    (Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)

Tactic:
have : (Over.forget P ⊤ S).LocallyCoverDense
      (K.comap (CategoryTheory.Over.forget S)).toGrothendieck := by
    rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]
    exact MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
  rw [Precoverage.comap_comp]
  simp_rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
  apply Precoverage.toGrothendieck_comap_eq_restrictedTopology
  intro X R hR
  obtain ⟨T, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve K H hR
  simpa

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + x₃ ≫ b

Tactic:
add_comm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₃ ≫ b + x₂ ≫ r = x₃ ≫ b + x₂ ≫ r
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝¹ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₃ : A₂ ⟶ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.X₁
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.f
⊢ (π₂ ≫ x₂) ≫ r = x₃ ≫ b

Tactic:
simpa

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

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
⊢ Function.Surjective fun j ↦ ⟨s j, ⋯⟩

Tactic:
rintro ⟨_, j, rfl⟩

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
F : J ⥤ MonoOver X
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this✝ : IsFiltered J
this : Mono f
h : ⨆ j, Subobject.mk (F.obj j).obj.hom = ⊤
s : J → Subobject X := fun j ↦ Subobject.mk (F.obj j).obj.hom
j : J
⊢ ∃ a, (fun j ↦ ⟨s j, ⋯⟩) a = ⟨s j, ⋯⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : PartialOrder J
F : J ⥤ C
J' : Type w'
inst✝¹ : PartialOrder J'
f : J' ≤i J
inst✝ : F.IsWellOrderContinuous
m' : J'
hm' : Order.IsSuccLimit m'
⊢ Order.IsSuccLimit ((Set.principalSegIio m').transInitial f).top

Tactic:
simpa

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
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
this : (iter₁.trunc ⋯).F = (iter₂.trunc ⋯).F
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
simp at this

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
this : restrictionLE iter₁.F ⋯ = restrictionLE iter₂.F ⋯
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : k₁ < j
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

Tactic:
dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]

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)
⊢ q.num /. ↑q.den ≠ 0

Tactic:
Rat.num_divInt_den

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)
⊢ q ≠ 0
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
⊢ r.num /. ↑r.den ≠ 0

Tactic:
Rat.num_divInt_den

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
⊢ r ≠ 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ (generatingMonomorphisms G).pushouts.rlp p

Tactic:
simpa

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den) + emultiplicity ↑p ↑q.den

Tactic:
add_comm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p) (q.num * ↑r.den) ≤ emultiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity (↑p) (q.num * ↑r.den) + emultiplicity ↑p ↑q.den ≤
    emultiplicity (↑p) (q.num * ↑r.den) + emultiplicity ↑p ↑q.den
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (q + r)

Tactic:
add_comm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (r + q)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ r + q ≠ 0

Tactic:
add_comm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ q + r ≠ 0