mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)

Tactic:
stalkMap_toSpec 𝒜 f x f_deg hm

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso
    ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)
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 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
    Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd))

Tactic:
refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 (i.2 : A)) (Away 𝒜 (j.2 : A))
    · simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]; rfl
    · simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]; rfl

Goal state after:
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
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
refine ⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ _ ?_,
      𝒰.map_prop _, hy⟩

Goal state after:
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
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
x : ↥X.left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ 𝒰.toPresieveOverProp p (Hom.asOverProp (𝒰.f (𝒰.idx x)) S)
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U ∈ (smallGrothendieckTopology P S) U

Tactic:
rw [Scheme.mem_smallGrothendieckTopology]

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
⊢ ∃ 𝒰 x,
    ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
      𝒰.toPresieveOverProp h ≤ (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ (Sieve.ofArrows
      (fun i ↦
        (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
      fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯) ∈
    (smallGrothendieckTopology P S) X

Tactic:
rw [Scheme.mem_smallGrothendieckTopology]

Goal state after:
S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
⊢ ∃ 𝒰_1 x,
    ∃ (h : ∀ (j : 𝒰_1.I₀), P (𝒰_1.X j ↘ S)),
      𝒰_1.toPresieveOverProp h ≤
        (Sieve.ofArrows
            (fun i ↦
              (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj
                ((fun i ↦ affineOverMk (𝒰.f i ≫ X.hom) ⋯) i))
            fun i ↦ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯).arrows
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
f : ↑R
hf : basicOpen f ≤ basicOpen g
⊢ basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)

Tactic:
← SpecMap_preimage_basicOpen,

Goal state after:
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
f : ↑R
hf : basicOpen f ≤ basicOpen g
⊢ basicOpen f = ψ ''ᵁ Spec.map a ⁻¹ᵁ basicOpen f
Module: Mathlib.CategoryTheory.Sites.Point.Basic

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✝⁵ : 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 Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallySurjective J f
X : C
z : ToType (Q.obj (op X))
Y : C
g : Y ⟶ unop (op X)
t : ToType (P.obj (op Y))
ht : (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (Q.map g.op)) z
y : Φ.fiber.obj Y
⊢ ∃ a,
    (ConcreteCategory.hom (Φ.presheafFiber.map f)) a =
      (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) Q)) z

Tactic:
exact ⟨Φ.toPresheafFiber Y y P t, by simp [← toPresheafFiber_w, ← ht]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

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✝⁶ : 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
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
⊢ IsIso (Φ.presheafFiber.map f)

Tactic:
obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf

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✝⁶ : 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
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : J.WEqualsLocallyBijective A
inst✝ : (forget A).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
left✝ : Presheaf.IsLocallyInjective J f
right✝ : Presheaf.IsLocallySurjective J f
⊢ IsIso (Φ.presheafFiber.map 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
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
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
⊢ presheafObjπ data G₀ X i₁ ≫ G₀.obj.map (c ≫ b₁).op = presheafObjπ data G₀ X i₂ ≫ G₀.obj.map (c ≫ b₂).op

Tactic:
simpa [fac₁, fac₂] using presheafObj_condition_assoc _ _ _ _ _ _ _

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
⊢ (Sieve.generate R).EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (yoneda.obj Y) (Sieve.generate R).arrows

Tactic:
Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case e_6.e_6
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := ⋯
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := ⋯
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := ⋯
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (Away.isLocalizationElem ⋯ ⋯ ^ ∏ k ∈ Finset.univ.erase i₀, d k) ^ (d i₀ * a * d j) =
    (Away.isLocalizationElem ⋯ ⋯ ^ a) ^ (d j * ∏ k, d k)

Tactic:
← pow_mul,

Goal state after:
case e_6.e_6
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ Away.isLocalizationElem ⋯ ⋯ ^ ((∏ k ∈ Finset.univ.erase i₀, d k) * (d i₀ * a * d j)) =
    (Away.isLocalizationElem ⋯ ⋯ ^ a) ^ (d j * ∏ k, d k)
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
⊢ CoverPreserving (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck
    (K.toGrothendieck.over S) (Over.forget P ⊤ S)

Tactic:
have := MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
  rw [toGrothendieck_comap_forget_eq_restrictedTopology _ H]
  exact Functor.coverPreserving_restrictedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S)

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
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j =
    (presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv) ≫
      presheafObjπ data G₀ (F.obj ((data X).X i)) j

Tactic:
rw [assoc, presheafMap_π, presheafObjObjIso, presheafObjObjIso.inv_π data G₀]

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 : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj ((data X).X i))).f j)
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
⊢ CoverPreserving (topology S) (proetaleTopology.over S) (ProEt.forget S)

Tactic:
exact coverPreserving_comap_forget _ proetalePrecoverage_le_precoverage_weaklyEtale

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

Goal state before:
pp: case refine_3
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
y : (CategoryTheory.yoneda.obj E).obj (Opposite.op Z)
hty : (fun t_1 ↦ t.IsAmalgamation t_1) y
⊢ y = Over.homMk a ⋯

Tactic:
refine Over.OverMorphism.ext (huniq _ ?_)
    rintro W p ⟨V, v, _, ⟨i⟩, rfl⟩
    have := congr($(hty _ (Sieve.ofArrows_mk _ _ i)).left)
    dsimp at this
    simp [Presieve.FamilyOfElements.comp_of_compatible _
      hg.familyOfElements_compatible.sieveExtend (Sieve.ofArrows_mk _ _ i),
      Presieve.extend_agrees hg.familyOfElements_compatible (.mk i), this]

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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
    exact Types.FilteredColimit.isColimitOf' _ _
      (surjectivity hc hXκ) (injectivity hc hXκ)

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = Order.pred ↑i

Tactic:
by
  rw [coe_pred_of_mem]
  apply Order.le_pred_of_lt
  exact lt_of_le_of_ne (α := Set.Ici j) bot_le (Ne.symm (by simpa using hi))

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
A : Subobject X
hA : A ≠ ⊤
⊢ ∃ A', ∃ (h : A < A'), (generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)

Tactic:
induction A using Subobject.ind with

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)
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
A : Subobject X
hA : A ≠ ⊤
⊢ A < ⋯.choose

Tactic:
exact (exists_larger_subobject hG A hA).choose_spec.choose

Goal state after:
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 κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f.hom)))
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk g.hom)))
h₁ :
  (Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ

Tactic:
have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
    ((Functor.whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)

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 κ
f g : Arrow C
φ : f ⟶ g
e₁ : ((𝟭 (Arrow C)).obj (Arrow.mk f.hom)).right ≅ ((iteration I κ).obj (Arrow.mk f.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk f.hom)))
e₂ : ((𝟭 (Arrow C)).obj (Arrow.mk g.hom)).right ≅ ((iteration I κ).obj (Arrow.mk g.hom)).right :=
  asIso (Arrow.Hom.right ((ιIteration I κ).app (Arrow.mk g.hom)))
h₁ :
  (Arrow.Hom.left ((iteration I κ).map φ) ≫ ((iteration I κ).obj g).hom) ≫ e₂.inv =
    (((iteration I κ).obj f).hom ≫ Arrow.Hom.right ((iteration I κ).map φ)) ≫ e₂.inv
h₂ : Arrow.Hom.right φ ≫ e₂.hom = e₁.hom ≫ Arrow.Hom.right ((iteration I κ).map φ)
⊢ objMap I κ φ ≫ ((iteration I κ).obj (Arrow.mk g.hom)).hom ≫ e₂.inv =
    (((iteration I κ).obj (Arrow.mk f.hom)).hom ≫ e₁.inv) ≫ Arrow.Hom.right φ
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
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts

Tactic:
apply transfiniteCompositions_monotone

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts ≤ (coproducts.{w, v, u} (monomorphisms C)).pushouts
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

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

Tactic:
rw [Finset.sum_range_succ] at hn0 ⊢

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (x y : ℤ_[p]), dist x y = ‖-x + y‖

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩
    exact dist_eq_norm_neg_add x y

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

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1

Tactic:
exact Nat.lt_succ_self _

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ ↑r * ↑r.den = ↑r.num

Tactic:
rw_mod_cast [@Rat.mul_den_eq_num r]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x < 1 ↔ ↑p ∣ x

Tactic:
simp [lt_iff_le_and_ne, padicValuation_eq_one_iff, Int.padicValuation_le_one]

Goal state after: