[GOAL]
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
⊢ OneHom.toFun (↑src✝) 0 = 0
[PROOFSTEP]
convert f.lift_eq (P := Γ) _ 0
[GOAL]
case h.e'_2.h.e'_1
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
⊢ 0 = ↑(Submonoid.LocalizationMap.toMap f) 0
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
⊢ 0 = ↑↑v.toMonoidWithZeroHom 0
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
x y : B
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
          map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
          map_mul' :=
            (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      (x + y) ≤
    max
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
        x)
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
        y)
[PROOFSTEP]
obtain ⟨a, b, s, rfl, rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y :=
  by
  obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
  obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
  use a * t, b * s, s * t
  constructor <;>
    · rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
      ring_nf
[GOAL]
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
x y : B
⊢ ∃ a b s, Submonoid.LocalizationMap.mk' f a s = x ∧ Submonoid.LocalizationMap.mk' f b s = y
[PROOFSTEP]
obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
[GOAL]
case intro.intro
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
y : B
a : A
s : { x // x ∈ S }
⊢ ∃ a_1 b s_1,
    Submonoid.LocalizationMap.mk' f a_1 s_1 = Submonoid.LocalizationMap.mk' f a s ∧
      Submonoid.LocalizationMap.mk' f b s_1 = y
[PROOFSTEP]
obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
[GOAL]
case intro.intro.intro.intro
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ ∃ a_1 b_1 s_1,
    Submonoid.LocalizationMap.mk' f a_1 s_1 = Submonoid.LocalizationMap.mk' f a s ∧
      Submonoid.LocalizationMap.mk' f b_1 s_1 = Submonoid.LocalizationMap.mk' f b t
[PROOFSTEP]
use a * t, b * s, s * t
[GOAL]
case h
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ Submonoid.LocalizationMap.mk' f (a * ↑t) (s * t) = Submonoid.LocalizationMap.mk' f a s ∧
    Submonoid.LocalizationMap.mk' f (b * ↑s) (s * t) = Submonoid.LocalizationMap.mk' f b t
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ Submonoid.LocalizationMap.mk' f (a * ↑t) (s * t) = Submonoid.LocalizationMap.mk' f a s
[PROOFSTEP]
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
[GOAL]
case h.left
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ ↑(Submonoid.LocalizationMap.toMap f) (↑s * (a * ↑t)) = ↑(Submonoid.LocalizationMap.toMap f) (↑s * ↑t * a)
[PROOFSTEP]
ring_nf
[GOAL]
case h.right
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ Submonoid.LocalizationMap.mk' f (b * ↑s) (s * t) = Submonoid.LocalizationMap.mk' f b t
[PROOFSTEP]
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
[GOAL]
case h.right
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a : A
s : { x // x ∈ S }
b : A
t : { x // x ∈ S }
⊢ ↑(Submonoid.LocalizationMap.toMap f) (↑t * (b * ↑s)) = ↑(Submonoid.LocalizationMap.toMap f) (↑s * ↑t * b)
[PROOFSTEP]
ring_nf
[GOAL]
case intro.intro.intro.intro
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
          map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
          map_mul' :=
            (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      (Submonoid.LocalizationMap.mk' f a s + Submonoid.LocalizationMap.mk' f b s) ≤
    max
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
        (Submonoid.LocalizationMap.mk' f a s))
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
        (Submonoid.LocalizationMap.mk' f b s))
[PROOFSTEP]
convert_to f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := src✝.toFun, map_zero' := (_ : OneHom.toFun (↑src✝) 0 = 0) },
          map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1),
          map_mul' :=
            (_ : ∀ (x y : B), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      (Submonoid.LocalizationMap.mk' f a s + Submonoid.LocalizationMap.mk' f b s) =
    ↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f (a + b) s)
[PROOFSTEP]
refine' congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 _)
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ (Submonoid.LocalizationMap.mk' f a s + Submonoid.LocalizationMap.mk' f b s) * ↑(algebraMap A B) ↑s =
    ↑(algebraMap A B) (a + b)
[PROOFSTEP]
rw [add_mul, _root_.map_add]
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ Submonoid.LocalizationMap.mk' f a s * ↑(algebraMap A B) ↑s +
      Submonoid.LocalizationMap.mk' f b s * ↑(algebraMap A B) ↑s =
    ↑(algebraMap A B) a + ↑(algebraMap A B) b
[PROOFSTEP]
iterate 2 erw [IsLocalization.mk'_spec]
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ Submonoid.LocalizationMap.mk' f a s * ↑(algebraMap A B) ↑s +
      Submonoid.LocalizationMap.mk' f b s * ↑(algebraMap A B) ↑s =
    ↑(algebraMap A B) a + ↑(algebraMap A B) b
[PROOFSTEP]
erw [IsLocalization.mk'_spec]
[GOAL]
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑(algebraMap A B) a + Submonoid.LocalizationMap.mk' f b s * ↑(algebraMap A B) ↑s =
    ↑(algebraMap A B) a + ↑(algebraMap A B) b
[PROOFSTEP]
erw [IsLocalization.mk'_spec]
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f (a + b) s) ≤
    max (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f a s))
      (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f b s))
[PROOFSTEP]
iterate 3 rw [f.lift_mk']
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f (a + b) s) ≤
    max (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f a s))
      (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f b s))
[PROOFSTEP]
rw [f.lift_mk']
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑↑v.toMonoidWithZeroHom (a + b) * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹ ≤
    max (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f a s))
      (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f b s))
[PROOFSTEP]
rw [f.lift_mk']
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑↑v.toMonoidWithZeroHom (a + b) * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹ ≤
    max (↑↑v.toMonoidWithZeroHom a * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹)
      (↑(Submonoid.LocalizationMap.lift f h) (Submonoid.LocalizationMap.mk' f b s))
[PROOFSTEP]
rw [f.lift_mk']
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑↑v.toMonoidWithZeroHom (a + b) * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹ ≤
    max (↑↑v.toMonoidWithZeroHom a * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹)
      (↑↑v.toMonoidWithZeroHom b * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹)
[PROOFSTEP]
rw [max_mul_mul_right]
[GOAL]
case intro.intro.intro.intro.convert_3
A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ Ideal.primeCompl (supp v)
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : Submonoid.LocalizationMap S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : { x // x ∈ S }), IsUnit (↑↑v.toMonoidWithZeroHom ↑s) := fun s => Iff.mpr isUnit_iff_ne_zero (hS s.property)
src✝ : B →* Γ := Submonoid.LocalizationMap.lift f h
a b : A
s : { x // x ∈ S }
⊢ ↑↑v.toMonoidWithZeroHom (a + b) * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹ ≤
    max (↑↑v.toMonoidWithZeroHom a) (↑↑v.toMonoidWithZeroHom b) *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑v.toMonoidWithZeroHom) S) h) s)⁻¹
[PROOFSTEP]
apply mul_le_mul_right' (v.map_add a b)
