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

Goal state before:
pp: case e_a.e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x✝ : Away 𝒜 t
⊢ ((IsLocalization.Away.awayToAwayRight x (f s)).comp (IsLocalization.map (Localization.Away x) f ⋯)) (val x✝) =
    ((IsLocalization.map (Localization.Away x') f ⋯).comp
        (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯))
      (val x✝)

Tactic:
congr 1

Goal state after:
case e_a.e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t : A
d : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
H' : f (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x✝ : Away 𝒜 t
⊢ (IsLocalization.Away.awayToAwayRight x (f s)).comp (IsLocalization.map (Localization.Away x) f ⋯) =
    (IsLocalization.map (Localization.Away x') f ⋯).comp
      (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : 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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      (basicOpenIsoSpecAway (f x.snd.fst)).hom ≫
        Spec.map
            (CommRingCat.ofHom (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)) ≫
              CommRingCat.ofHom (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯)) ≫
          Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers x.snd.fst))) =
    X.toSpecΓ ∣_ PrimeSpectrum.basicOpen (f x.snd.fst) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen (f x.snd.fst)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) A) ≫ CommRingCat.ofHom f)

Tactic:
congr 1

Goal state after:
case e_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 = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (basicOpenIsoSpecAway (f x.snd.fst)).hom ≫
      Spec.map
          (CommRingCat.ofHom (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)) ≫
            CommRingCat.ofHom (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯)) ≫
        Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers x.snd.fst))) =
    Scheme.Opens.ι (PrimeSpectrum.basicOpen (f x.snd.fst)) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) A) ≫ CommRingCat.ofHom f)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f hf).hom p))
          ((ConcreteCategory.hom
              ((structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)
                ((ProjectiveSpectrum.comap f hf) p) ⋯))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))

Tactic:
PresheafedSpace.stalkMap_germ_apply

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
p : ProjectiveSpectrum ℬ
c : NumDenSameDeg 𝒜 ((ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl
⊢ Localization.mk (f ↑c.num) ⟨f ↑c.den, ⋯⟩ =
    val
      ((CommRingCat.Hom.hom (CommRingCat.ofHom ↑(stalkIso' ℬ p)))
        ((ConcreteCategory.hom
            ((toSheafedSpace ℬ).presheaf.germ
              ((Opens.map (sheafedSpaceMap f hf).hom.base).obj (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)) p ⋯))
          ((ConcreteCategory.hom
              ((sheafedSpaceMap f hf).hom.c.app (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
            (sectionInBasicOpen 𝒜 ((ProjectiveSpectrum.comap f hf) p) c))))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ ModuleCat.Hom.hom
      (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
        (modulesSpecToSheaf.map (tilde.map ((modulesSpecToSheaf.map f).hom.app (op ⊤))) ≫
                modulesSpecToSheaf.map N.fromTildeΓ).hom.app
          (op (PrimeSpectrum.basicOpen (unop r)))) =
    ModuleCat.Hom.hom
      (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
        (modulesSpecToSheaf.map M.fromTildeΓ ≫ modulesSpecToSheaf.map f).hom.app
          (op (PrimeSpectrum.basicOpen (unop r))))

Tactic:
congr 1

Goal state after:
case h
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec (CommRingCat.of ↑R)).Modules
f : M ⟶ N
r : (InducedCategory (TopologicalSpace.Opens ↥(Spec (CommRingCat.of ↑R))) PrimeSpectrum.basicOpen)ᵒᵖ
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map (tilde.map ((modulesSpecToSheaf.map f).hom.app (op ⊤))) ≫
              modulesSpecToSheaf.map N.fromTildeΓ).hom.app
        (op (PrimeSpectrum.basicOpen (unop r))) =
    tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map M.fromTildeΓ ≫ modulesSpecToSheaf.map f).hom.app (op (PrimeSpectrum.basicOpen (unop r)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫
        (modulesSpecToSheaf.map (tilde.map (toOpen M ⊤)) ≫ modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom.app
          (op (basicOpen (unop r)))) =
    ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r))))

Tactic:
congr 1

Goal state after:
case h
R : CommRingCat
M✝ M : ModuleCat ↑R
r : (InducedCategory (Opens ↥(Spec (CommRingCat.of ↑R))) basicOpen)ᵒᵖ
⊢ toOpen M (basicOpen (unop r)) ≫
      (modulesSpecToSheaf.map (tilde.map (toOpen M ⊤)) ≫ modulesSpecToSheaf.map (tilde M).fromTildeΓ).hom.app
        (op (basicOpen (unop r))) =
    toOpen M (basicOpen (unop r)) ≫ (modulesSpecToSheaf.map (𝟙 (tilde M))).hom.app (op (basicOpen (unop r)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ ((basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯) ≫
      (basicOpen 𝒜 s).ι =
    (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv) ≫ (basicOpen 𝒜 s).ι

Tactic:
congr 1

Goal state after:
case e_a
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ (basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ =
    Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ (algebraMap (↥A) (Localization.AtPrime P)) (↑t * x) = (algebraMap (↥A) (Localization.AtPrime P)) (↑s * y)

Tactic:
congr 1

Goal state after:
case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
this : ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
⊢ ↑t * x = ↑s * y
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case pos
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 : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ product ∈ q.asIdeal

Tactic:
apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)
          rw [(_ : m • n = _)]
          · mem_tac
          · simp only [smul_eq_mul, mul_comm]

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

Goal state before:
pp: case refine_2.refine_3
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ Away.mk 𝒜 hf a (∏ i, v i ^ (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i) ⋯ =
    Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯

Tactic:
congr 1

Goal state after:
case refine_2.refine_3.e_x
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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ ∏ i, v i ^ (fun i ↦ if hi : i ∈ s then ai ⟨i, hi⟩ else 0) i = ∏ i, (v ∘ Subtype.val) i ^ ai i
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
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
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (g i ^ n • ψ t')

Tactic:
congr 1

Goal state after:
case h.e_6
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)) := ⋯
i : ι
n : ℕ
t' : ↑Γ(M, basicOpen (g i))
ht' : (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) t' = g i ^ n • f ^ n • s' i
ψ : Module.End ↑R ↑Γ(M, basicOpen (g i))
hψ : (algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ n) * ψ = 1
⊢ t' = g i ^ n • ψ t'
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
⊢ ⋯.HasLift

Tactic:
let lft := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ w.symm

Goal state after:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing✝ : CommRing R
domain✝ : IsDomain R
valuationRing✝ : ValuationRing R
K : Type u
field✝ : Field K
algebra✝ : Algebra R K
isFractionRing✝ : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
⊢ ⋯.HasLift
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
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv

Tactic:
rw [awayToΓ, Category.assoc, ← Category.assoc _ (Iso.inv _),
    Iso.eq_comp_inv, Category.assoc, Category.assoc, Presheaf.Γgerm]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ awayToSection 𝒜 f ≫
      (structureSheaf 𝒜).obj.map (homOfLE ⋯).op ≫
        (Proj.restrict ⋯).presheaf.germ ⊤ x True.intro ≫ (Proj.restrictStalkIso ⋯ x).hom =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)

Tactic:
obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e

Goal state after:
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
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
hc : ↑⟨c, hcx⟩ * (↑z.den * ↑y.num) = ↑⟨c, hcx⟩ * (↑y.den * ↑z.num)
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hxj
σ : 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
⊢ (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))

Tactic:
convert! SetLike.pow_mem_graded _ _ using 2

Goal state after:
case hxj.convert_8
σ : 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
⊢ SetLike.GradedMonoid 𝒜

case hxj.convert_12
σ : 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
⊢ x ∈ 𝒜 (d + e)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯)) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F)

Tactic:
congr 1

Goal state after:
case h₀
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯) = CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ CommRingCat.ofHom F
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h₁
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯)) =
    Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight ≫ CommRingCat.ofHom F)

Tactic:
congr 1

Goal state after:
case h₁
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
e₁ : pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
  Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd)) :=
  congrHom ⋯ ⋯ ≪≫ pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 ↑i.snd) (Away 𝒜 ↑j.snd)
e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (CommRingCat.of (Away 𝒜 (↑i.snd * ↑j.snd))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd →+* Away 𝒜 (↑i.snd * ↑j.snd) :=
  (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯).toRingHom
this : Function.Surjective ⇑F
⊢ CommRingCat.ofHom (awayMap 𝒜 ⋯ ⋯) = CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight ≫ CommRingCat.ofHom F
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case right
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsAffine Z ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
hZ : IsAffine Z
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
exact this.right

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: ⊢ @IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

Tactic:
by
  rw [isProper_eq, IsSeparated.eq_valuativeCriterion, ValuativeCriterion.eq,
    UniversallyClosed.eq_valuativeCriterion]
  simp_rw [inf_assoc]
  ext X Y f
  change _ ∧ _ ∧ _ ∧ _ ∧ _ ↔ _ ∧ _ ∧ _ ∧ _ ∧ _
  tauto

Goal state after: