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

Goal state before:
pp: case e'_5.e'_5
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H✝ : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H✝
H : (toNormalization f ∣_ V y) ⁻¹ᵁ (V y).ι ⁻¹ᵁ (normalization f).basicOpen r = opensRange (X.homOfLE ⋯)
this :
  IsIso
    (appLE (toNormalization f) ((V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
      ((toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)) ⋯)
e_3✝ :
  Γ(normalization f, (normalization f).basicOpen r) =
    Γ(normalization f, (V y).ι ''ᵁ opensRange ((normalization f).homOfLE hrV))
e_4✝ :
  Γ(X, toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) =
    Γ(X, (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV))
⊢ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r =
    (toNormalization f ⁻¹ᵁ V y).ι ''ᵁ (toNormalization f ∣_ V y) ⁻¹ᵁ opensRange ((normalization f).homOfLE hrV)

Tactic:
simp [Scheme.Hom.image_preimage_eq_opensRange_inf, -Scheme.preimage_basicOpen,
        f.toNormalization.preimage_mono, hrV, H]

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

Goal state before:
pp: case e'_2.e'_7
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
x✝ : S
⊢ (φ.comp TensorProduct.includeRight.toRingHom) x✝ = ↑TensorProduct.includeRight x✝

Tactic:
simp [φ]

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

Goal state before:
pp: R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
R'' : Type u
inst✝¹⁰ : CommRing R''
inst✝⁹ : Algebra R' R''
inst✝⁸ : Algebra R R''
inst✝⁷ : IsScalarTower R R' R''
inst✝⁶ : Etale R' R''
Q : Ideal R''
inst✝⁵ : Q.IsPrime
inst✝⁴ : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝³ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝² : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝³ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
this✝² : P''.LiesOver P
inst✝¹ : (Ideal.comap φ P'').IsPrime
inst✝ : (Ideal.comap φ P'').LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap φ P'') = q
heP' : e ∉ Ideal.comap φ P''
H : ∀ (P''_1 : Ideal (R' ⊗[R] S)), P''_1.IsPrime → P''_1.LiesOver P → e ∉ P''_1 → P''_1 = Ideal.comap φ P''
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨Ideal.comap φ P'', ⋯⟩)
this✝¹ : (↑P'φ).LiesOver P
this✝ : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = Ideal.comap φ P''
this : ∀ (i : Fin (n + 1 + 1)), i ≠ 0 → e' i ∈ P''
x✝¹ : e' (Fin.castSucc 0) ∉ P''
x✝ : S
⊢ ((AlgHom.restrictScalars R φ).comp TensorProduct.includeRight) x✝ = TensorProduct.includeRight x✝

Tactic:
simp [φ]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom

Tactic:
simp [← whisker_exchange_assoc]

Goal state after:
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₂
β : r₁ ≅ r₂
⊢ (conjugateEquiv adj₂ adj₁).symm β.inv ≫ (conjugateEquiv adj₁ adj₂).symm β.hom = 𝟙 l₁

Tactic:
by
        rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_id]

Goal state after:
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 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ ¬{f} ⊆ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal

Tactic:
Set.singleton_subset_iff

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ M.presheaf.germ (f ''ᵁ Opposite.unop (Opposite.op U)) (f x) ⋯ ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
← germ_restrictStalkNatIso_hom_app f x M hxU,

Goal state after:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ (((restrictFunctor f).obj M).presheaf.germ U x hxU ≫ (restrictStalkNatIso f x).hom.app M) ≫
      (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Set.range ⇑(awayMapAux 𝒜 ⋯) ⊆ Set.range val

Tactic:
by
  rintro _ ⟨z, rfl⟩
  obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z
  use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩
  · simp [awayMapAux_mk 𝒜 (hx := hx)]
  · apply SetLike.mul_mem_graded ha
    exact SetLike.pow_mem_graded _ hg
  · rw [hx, mul_pow]
    apply SetLike.mul_mem_graded hb'
    exact SetLike.pow_mem_graded _ hg

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

Goal state before:
pp: case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f) = ProjectiveSpectrum.Proj.toSpec 𝒜 f

Tactic:
refine Eq.trans ?_ (ΓSpec.locallyRingedSpaceAdjunction.homEquiv_apply _ _ _).symm

Goal state after:
case e'_5
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3✝ : Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f) = (toLocallyRingedSpace 𝒜).restrict ⋯
e_4✝ :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f) =
    ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj ↑(basicOpen 𝒜 f)) ≫
      Spec.toLocallyRingedSpace.map (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f).op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
← SetLike.mem_coe

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ ↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case pos.refine_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ val (Away.mk 𝒜 hf j (∏ i, v i ^ ai i) ⋯) =
    (mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ }).val

Tactic:
simp only [val_mk, Away.val_mk]

Goal state after:
case pos.refine_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ∑ i, ai i • dv i = n
⊢ Localization.mk (∏ i, v i ^ ai i) ⟨f ^ j, ⋯⟩ =
    (mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ }).val
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X I)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I) x ∈ X.basicOpen (f r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I) x ∈ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r

Tactic:
← SetLike.mem_coe

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X I)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I) x ∈ X.basicOpen (f r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I) x ∈ ↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
⊢ Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ ∈
    ↑(Subalgebra.toSubmodule
        (Algebra.adjoin ↥(𝒜 0)
          {x |
            ∃ a ai,
              ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}))

Tactic:
have H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k := by
    rw [smul_eq_mul, tsub_mul, ← smul_eq_mul, ← hai]
    conv => enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
    simp_rw [smul_eq_mul, add_mul, Finset.sum_add_distrib,
      mul_assoc, ← Finset.mul_sum, mul_comm d, mul_comm (_ / _)]
    simp only [add_tsub_cancel_right]

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
⊢ Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ ∈
    ↑(Subalgebra.toSubmodule
        (Algebra.adjoin ↥(𝒜 0)
          {x |
            ∃ a ai,
              ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup W = ⊤
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
⊢ IsOpenCover fun j ↦ ↑j.snd

Tactic:
rw [IsOpenCover, iSup_sigma, ← cov]

Goal state after:
case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : iSup W = ⊤
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
⊢ ⨆ i, ⨆ j, ↑⟨i, j⟩.snd = iSup W
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case surj.refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (f ^ i * (↑a * b ^ m)) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (b * f ^ i * (↑a * b ^ (m - 1)))

Tactic:
rw [mul_comm b, mul_mul_mul_comm, ← pow_succ', mul_assoc, tsub_add_cancel_of_le (by lia)]

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

Goal state before:
pp: case neg
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }

Tactic:
let y0 : NumDenSameDeg 𝒜 (.powers g) :=
  { deg := j * (d * e)
    num := ⟨f ^ (j * e), by convert SetLike.pow_mem_graded _ hf; ring⟩
    den := ⟨g ^ (j * d), by convert SetLike.pow_mem_graded _ hg; ring⟩
    den_mem := ⟨_,rfl⟩ }

Goal state after:
case neg
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := ⟨f ^ (j * e), ⋯⟩, den := ⟨g ^ (j * d), ⋯⟩, den_mem := ⋯ }
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact

Tactic:
by
  rw [universallyClosed_eq_universallySpecializing, ValuativeCriterion.Existence.eq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case hR
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 := ⋯
T : Sieve W := ⋯
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y

Tactic:
intro Y

Goal state after:
case hR
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 ⋯)))
Y : C
⊢ ∀ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1.refine_1
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 : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
f : ↑R
hle : basicOpen f ≤ ⊤
s : ↑Γ(M, basicOpen f)
⊢ ∃ n t, (ConcreteCategory.hom (M.presheaf.map (homOfLE hle).op)) t = f ^ n • s

Tactic:
obtain ⟨n, y, hy⟩ := (hf f).surj _ _ s

Goal state after:
case refine_1.refine_1
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 : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
f : ↑R
hle : basicOpen f ≤ ⊤
s : ↑Γ(M, basicOpen f)
n : ℕ
y : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
hy : f ^ n • s = (φ f) y
⊢ ∃ n t, (ConcreteCategory.hom (M.presheaf.map (homOfLE hle).op)) t = f ^ n • s
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
· intro X Y f E h hE
    simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE ⊢
    infer_instance

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

Goal state before:
pp: case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    qcPrecoverage.coverings S

Tactic:
rw [Scheme.presieve₀_mem_qcPrecoverage_iff]
      exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩

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
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (yoneda.obj (F ⋙ uliftFunctor.{v, w}).reprX ⋙ uliftFunctor.{w, v}) R

Tactic:
isSheafFor_comp_uliftFunctor_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (yoneda.obj (F ⋙ uliftFunctor.{v, w}).reprX) R