Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

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

Tactic:
induction this using Submodule.span_induction with
  | zero => simp
  | add x y hx hy hhx hhy =>
    simp only [RingHom.coe_comp, Function.comp_apply, map_add, ge_iff_le]
    exact ((valuation O K).map_add _ _).trans <| sup_le_iff.mpr ⟨hhx, hhy⟩
  | smul a x₀ hx hx1 =>
    simp only [Algebra.smul_def, RingHom.coe_comp, Function.comp_apply, map_mul, ge_iff_le]
    refine mul_le_one' ?_ hx1
    rw [RingHom.algebraMap_toAlgebra, awayMap_fromZeroRingHom 𝒜 (hxdi j) (mul_comm (x j) (x i₀)),
      ← awayMap_fromZeroRingHom 𝒜 (hxdi i₀) rfl a, hφ'1]
    change valuation O K (φ.comp (fromZeroRingHom 𝒜 (.powers (x j))) a) ≤ 1
    simp only [← hcomm, RingHom.coe_comp, Function.comp_apply, ← Valuation.mem_integer_iff,
      IsFractionRing.coe_inj, exists_eq, mem_integer_iff]
  | mem x1 h =>
    obtain ⟨a, ai, hai, rfl⟩ := h
    simp only [smul_eq_mul] at hai
    have H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j) := by
      convert!
        SetLike.mul_mem_graded (SetLike.prod_pow_mem_graded 𝒜 d x ai fun _ _ ↦ hxdi _)
          (SetLike.pow_mem_graded (a * (d j - 1)) (hxdi i₀)) using 2
      simp only [smul_eq_mul, hai]
      cases h : d j
      · cases (hdi j).ne' h
      · simp only [add_tsub_cancel_right]; ring
    suffices valuation O K (φ (Away.mk 𝒜 (hxdi j) _ _ H) /
          φ (Away.isLocalizationElem (hxdi j) (hxdi i₀)) ^ a) ≤ 1 by
      convert! this
      rw [eq_div_iff (pow_ne_zero _ hunit.ne_zero), ← hφ'1, ← hφ'1, RingHom.comp_apply,
        ← map_pow, ← map_mul]
      congr
      ext
      simp only [awayMap_mk, Away.val_mk, val_pow, Localization.mk_pow, Localization.mk_mul,
        Localization.mk_eq_mk_iff, Localization.r_iff_exists, val_mul]
      use 1
      simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow]
      cases h : d j
      · cases (hdi j).ne' h
      · rw [Nat.add_sub_cancel]; ring
    rw [map_div₀, div_le_iff₀ ((pow_pos ((Valuation.pos_iff _).mpr hunit.ne_zero) _).trans_eq
      (Valuation.map_pow _ _ _).symm), one_mul, ← pow_le_pow_iff_left₀ zero_le zero_le
        (mul_pos (hdi j) (Finset.prod_pos fun i _ => hdi i)).ne.symm]
    calc
      _ = (∏ i, ψ i ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) := by
          simp only [ψ, ← map_pow, ← map_prod, ← map_mul]
          congr 2
          apply (show Function.Injective (algebraMap (Away 𝒜 (x j)) (Localization.Away (x j)))
            from val_injective _)
          simp only [map_pow, map_prod, map_mul]
          simp only [HomogeneousLocalization.algebraMap_apply, Away.val_mk, Localization.mk_pow,
            Localization.mk_prod, Localization.mk_mul]
          rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
          use 1
          simp only [OneMemClass.coe_one, ← pow_mul, Submonoid.coe_mul,
            SubmonoidClass.coe_finsetProd, one_mul]
          simp_rw [← mul_assoc, Finset.prod_erase_mul _ d (h := Finset.mem_univ _), mul_assoc,
            ← mul_assoc (Finset.prod ..), Finset.prod_erase_mul _ d (h := Finset.mem_univ _),
            SubmonoidClass.coe_pow, ← pow_mul, Finset.prod_pow_eq_pow_sum,
            ← pow_add, mul_pow, ← Finset.prod_pow, ← pow_mul]
          congr 3
          · simp only [mul_comm _ (∏ i, d i), mul_assoc, mul_left_comm _ (∏ i, d i),
              mul_comm (d _) (ai _), ← Finset.mul_sum, hai]
            cases h : d j
            · cases (hdi j).ne' h
            · simp; ring
          · ext i; congr 1; ring
          · ring
      _ ≤ (∏ i : ι, ψ i₀ ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1)) := by
          gcongr with i; exacts [fun i _ ↦ zero_le, zero_le, hi₀ i]
      _ = ψ i₀ ^ (d i₀ * a * d j) := by
          rw [Finset.prod_pow_eq_pow_sum, ← pow_add]
          simp_rw [mul_comm (d _) (ai _), hai]
          cases h : d j
          · cases (hdi j).ne' h
          · simp; ring_nf
      _ = valuation O K ((φ _) ^ a) ^ (d j * ∏ i, d i) := by
          · simp only [ψ, ← map_pow]
            congr 2
            rw [← pow_mul, ← pow_mul, ← mul_assoc, ← mul_assoc, ← mul_assoc,
              Finset.univ.prod_erase_mul d (h := Finset.mem_univ _),
              mul_comm _ a, mul_right_comm]

Goal state after: