mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹⁰ : Nonempty ↥G.left
this✝⁹ : IsProper (G ⊗ G).hom
this✝⁸ : JacobsonSpace ↥(G ⊗ G).left
this✝⁷ : Surjective G.hom
this✝⁶ : IsProper (Over.Hom.left (fst G G))
this✝⁵ : Surjective (Over.Hom.left (fst G G))
this✝⁴ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝³ : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝² : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝¹ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this✝ : IsProper (Over.Hom.left γ)
H✝ : ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ IsClosed (Set.range ⇑(Over.Hom.left γ))

Tactic:
exact γ.left.isClosedMap.isClosed_range

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ y ∈ V

Tactic:
suffices ∀ x, f x = y → f.QuasiFiniteAt x by simpa [V, not_imp_not]
    rintro x rfl
    have : Finite (f.fiber (f x)) := (f.fiberHomeo (f x)).finite_iff.mpr ‹_›
    exact Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber.mpr (isOpen_discrete _)

Goal state after:
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this✝² : FinitePresentation R S
x✝ : Algebra T (S ⊗[R] T) := TensorProduct.rightAlgebra
e : S ⊗[R] T ≃ₐ[T] T ⊗[R] S := AlgEquiv.ofRingEquiv ⋯
this✝¹ : FormallySmooth T (S ⊗[R] T)
e' : S ⊗[R] T ⊗[S] Ω[S⁄R] ≃ₗ[S ⊗[R] T] Ω[S ⊗[R] T⁄T] := KaehlerDifferential.tensorKaehlerEquiv R T S (S ⊗[R] T)
this✝ : Module.Flat (S ⊗[R] T) (S ⊗[R] T ⊗[S] Ω[S⁄R])
this : Module.Flat S Ω[S⁄R]
⊢ Module.Projective S Ω[S⁄R]

Tactic:
exact Module.Flat.projective_of_finitePresentation

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
x : P.CotangentSpace
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x

Tactic:
dsimp only [CotangentSpace] at x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
t : T
x : S ⊗[P.Ring] Ω[P.Ring⁄R]
⊢ (P.tensorCotangentSpace T) (t ⊗ₜ[R] x) = t • (CotangentSpace.map (toBaseChange T)) x
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hy : y ∈ Scheme.Hom.smoothLocus f
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
⊢ False

Tactic:
← hα',

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hy : (Over.Hom.left α.hom) x ∈ Scheme.Hom.smoothLocus f
⊢ False
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: case insert
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
a : S
s : Finset S
has : a ∉ s
IH : ∃ S' x x_1, ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑s ⊆ ↑f.range
⊢ ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, ↑(insert a s) ⊆ ↑f.range

Tactic:
| insert a s has IH =>

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ Function.Bijective ⇑(algebraMap R S)

Tactic:
rw [Function.Bijective, ← rankAtStalk_pos_iff_algebraMap_injective,
    ← rankAtStalk_le_one_iff_surjective]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
h : x ≠ 0
⊢ (ordMonoidWithZeroHom R) x = ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹

Tactic:
ordMonoidWithZeroHom_eq_intValuation (mem_nonZeroDivisors_of_ne_zero h)

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
h : x ≠ 0
⊢ ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹ =
    ((IsDiscreteValuationRing.maximalIdeal R).intValuation x)⁻¹
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (conjugateEquiv adj₁ adj₂) α =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom

Tactic:
rw [conjugateEquiv_apply, mateEquiv_apply']
  bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
⊢ ∃ a, pointsPi R X a = f

Tactic:
have (j₀ : _) := pointsPi_surjective_of_isAffine (ι := { i // j i = j₀ }) (R ·) (𝒰.X j₀)
    (fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f i.1) (by rcases i with ⟨i, rfl⟩; exact hj i))

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
this : ∀ (j₀ : 𝒰.I₀), ∃ a, pointsPi (fun x ↦ R ↑x) (𝒰.X j₀) a = fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f ↑i) ⋯
⊢ ∃ a, pointsPi R X a = f
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ
⊢ (fun I ↦ zeroLocus 𝒜 ↑I) I ≤ t ↔ I ≤ (fun t ↦ vanishingIdeal t) t

Tactic:
by
  simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using!
    subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: case neg
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
i : S
hi : i ∈ ↑s
hi0 : ¬n i = 0
⊢ i ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0}))

Tactic:
· exact Algebra.subset_adjoin (by simpa [hi0] using hi)

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

Goal state before:
pp: R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom (M.obj.map (basicOpen f).leTop.op ≫ φ.hom.app (op (basicOpen f))))

Tactic:
φ.hom.naturality

Goal state after:
R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f) (ModuleCat.Hom.hom (φ.hom.app (op ⊤) ≫ N.obj.map (basicOpen f).leTop.op))
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) y ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0

Tactic:
simp_rw [proj_apply]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ Localization.mk (↑(((decompose 𝒜) y) n) ^ m) ⟨f ^ n, ⋯⟩ = 0
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
⊢ False

Tactic:
have : IsUnit (Subring.inclusion hS.1 ⟨x⁻¹, h⟩) :=
    isUnit_iff_exists_inv.mpr ⟨⟨x, hx⟩, Subtype.ext (inv_mul_cancel₀ hx0)⟩

Goal state after:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
x : K
hx : x ∈ S.toSubring
h : x⁻¹ ∈ R.carrier
h' : x ∉ R.toLocalSubring.toSubring
hx0 : x ≠ 0
this : IsUnit ((Subring.inclusion ⋯) ⟨x⁻¹, h⟩)
⊢ False
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ Localization.mk ↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * n, num := ⟨(proj 𝒜 n) x ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0

Tactic:
simp_rw [proj_apply]

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ Localization.mk (↑(((decompose 𝒜) x) n) ^ m) ⟨f ^ n, ⋯⟩ = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h.refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
a : ToType ({ obj := M.presheaf, property := ⋯ }.obj.obj (op V))
ha : ∀ (i : ι), (ConcreteCategory.hom ({ obj := M.presheaf, property := ⋯ }.obj.map (homOfLE ⋯).op)) a = f ^ K • t i
⊢ ⨆ i, basicOpen f ⊓ basicOpen (g i) ≤ ⨆ i, basicOpen f ⊓ basicOpen (g i)

Tactic:
exact le_rfl

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

Goal state before:
pp: 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
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Presieve Y
V : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Cover (precoverage P) Y.left
h : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp p f) → Cover.Over S (V f H)
pV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f) (j : (V f H).I₀), Q ((V f H).X j ↘ S)
hV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f), T f H = (V f H).toPresieveOverProp ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp S ⋯).left := fun j ↦ V (Hom.asOverProp (𝒰.f j) S) ⋯
⊢ (𝒰.toPresieveOverProp p).bind T = Cover.toPresieveOverProp (Precoverage.ZeroHypercover.bind 𝒰 fun j ↦ 𝒱j j) ⋯

Tactic:
convert!
      Presieve.ofArrows_bind _ (fun j ↦ ((𝒰.f j).asOverProp S)) _
        (fun Y f H j ↦ ((V f H).X j).asOverProp S (pV _ _ _))
        (fun Y f H j ↦ ((V f H).f j).asOverProp S)

Goal state after:
case e'_2.e'_5
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
𝒰 : Cover (precoverage P) X.left
h✝ : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Presieve Y
V : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp p f → Cover (precoverage P) Y.left
h : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp p f) → Cover.Over S (V f H)
pV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f) (j : (V f H).I₀), Q ((V f H).X j ↘ S)
hV : ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp p f), T f H = (V f H).toPresieveOverProp ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp S ⋯).left := fun j ↦ V (Hom.asOverProp (𝒰.f j) S) ⋯
e_1✝ : Presieve X = Presieve (X.left.asOverProp S ⋯)
e_3✝ : X = X.left.asOverProp S ⋯
e_4✝ : 𝒰.toPresieveOverProp p ≍ Presieve.ofArrows (fun j ↦ (𝒰.X j).asOverProp S ⋯) fun j ↦ Hom.asOverProp (𝒰.f j) S
x✝² : Q.Over ⊤ S
x✝¹ : x✝² ⟶ X
x✝ : 𝒰.toPresieveOverProp p x✝¹
⊢ T x✝¹ x✝ = Presieve.ofArrows (fun j ↦ ((V x✝¹ x✝).X j).asOverProp S ⋯) fun j ↦ Hom.asOverProp ((V x✝¹ x✝).f j) S
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))),
    ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y

pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0

Tactic:
· intro x
    obtain ⟨n, t, ht⟩ := h.existence _ _ x
    use n, t, ht.symm

Goal state after:
case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))),
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0
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).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map e ≫ (data X).f j)

Tactic:
rw [fac₂, assoc, 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).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map d ≫ F.map b ≫ (data a.Y).f i ≫ a.f)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
E : PreZeroHypercover S
⊢ E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E

Tactic:
rw [← PreZeroHypercover.presieve₀_shrink, Scheme.qcPrecoverage,
    E.shrink.presieve₀_mem_precoverage_iff]

Goal state after:
S : Scheme
E : PreZeroHypercover S
⊢ qcCoverFamily.property E.shrink ↔ QuasiCompactCover E
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case succ
σ : 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)
n✝ : ℕ
h : d j = n✝ + 1
⊢ ψ i₀ ^ (a * d i₀ + d i₀ * a * (n✝ + 1 - 1)) = ψ i₀ ^ (d i₀ * a * (n✝ + 1))

Tactic:
simp; ring_nf

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₀ Y₀ : C₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
⊢ (inv data G₀ X₀ ≫ restriction data G₀ f) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op =
    IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
    ⟨_, J₀.pullback_stable b (cover_lift F J₀ _ (data (F.obj X₀)).mem₀)⟩ _ _ ?_

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₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
⊢ ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        ⟨Sieve.pullback b (Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀), ⋯⟩),
    ((inv data G₀ X₀ ≫ restriction data G₀ f) ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫ G₀.obj.map I.f.op =
      (IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj.map { Y := W₀, f := a, hf := ⋯ }.f.op) ≫ G₀.obj.map I.f.op
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

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

Tactic:
by
  apply MorphismProperty.locallyCoverDense_forget_of_le
  exact proetalePrecoverage_le_precoverage_weaklyEtale

Goal state after: