Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case right.add
σ : 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 x y : Away 𝒜 (x✝ i₀)
hx :
  x ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hy :
  y ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hhx : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) x) ≤ 1
hhy : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) y) ≤ 1
⊢ (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) (x + y)) ≤ 1

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, map_add, ge_iff_le]

Goal state after:
case right.add
σ : 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 x y : Away 𝒜 (x✝ i₀)
hx :
  x ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hy :
  y ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x✝ i ^ ai i) ⋯ = x}
hhx : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) x) ≤ 1
hhy : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) y) ≤ 1
⊢ (valuation O K) (φ' ((awayMap 𝒜 ⋯ ⋯) x) + φ' ((awayMap 𝒜 ⋯ ⋯) y)) ≤ 1