[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)


[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ Subadditive.lim h ≤ u n / ↑n
[PROOFSTEP]
rw [Subadditive.lim]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n => u n / ↑n) '' Ici 1) ≤ u n / ↑n
[PROOFSTEP]
exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r
[PROOFSTEP]
induction k with
| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r
[PROOFSTEP]
induction k with
| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (Nat.zero * n + r) ≤ ↑Nat.zero * u n + u r
[PROOFSTEP]

| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (Nat.zero * n + r) ≤ ↑Nat.zero * u n + u r
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u r ≤ u r
[PROOFSTEP]
rfl
[GOAL]
case succ
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u (Nat.succ k * n + r) ≤ ↑(Nat.succ k) * u n + u r
[PROOFSTEP]

| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
case succ
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u (Nat.succ k * n + r) ≤ ↑(Nat.succ k) * u n + u r
[PROOFSTEP]
calc
  u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
  _ ≤ u n + u (k * n + r) := (h _ _)
  _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
  _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ (k + 1) * n + r = n + (k * n + r)
[PROOFSTEP]
ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = ↑(k + 1) * u n + u r
[PROOFSTEP]
simp
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = (↑k + 1) * u n + u r
[PROOFSTEP]
ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / ↑p < L
[PROOFSTEP]
refine
  .atTop_of_arithmetic hn fun r _ =>
    ?_
      /- `(k * u n + u r) / (k * n + r)` tends to `u n / n < L`, hence
        `(k * u n + u r) / (k * n + r) < L` for sufficiently large `k`. -/
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
  (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <|
    by simpa
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ↑n + 0 ≠ 0
[PROOFSTEP]
simpa
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) :=
  by
  rw [add_zero, add_zero] at A
  refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
  simp only [(· ∘ ·), add_div' _ _ _ hx, div_div_div_cancel_right _ hx, mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
⊢ Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
[PROOFSTEP]
rw [add_zero, add_zero] at A
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
⊢ Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
[PROOFSTEP]
refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
x : ℝ
hx : x ≠ 0
⊢ (u n + u r / x) / (↑n + ↑r / x) = (fun x => (x * u n + u r) / (x * ↑n + ↑r)) x
[PROOFSTEP]
simp only [(· ∘ ·), add_div' _ _ _ hx, div_div_div_cancel_right _ hx, mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
refine
  ((B.comp tendsto_nat_cast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk =>
    ?_
      /- Finally, we use an upper estimate on `u (k * n + r)` to get an estimate on
        `u (k * n + r) / (k * n + r)`. -/
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (n * k + r) / ↑(n * k + r) < L
[PROOFSTEP]
rw [mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L
[PROOFSTEP]
refine lt_of_le_of_lt ?_ hk
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) ≤ ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k
[PROOFSTEP]
simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) ≤ (↑k * u n + u r) / ↑(k * n + r)
[PROOFSTEP]
exact div_le_div_of_le (Nat.cast_nonneg _) (h.apply_mul_add_le _ _ _)
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
⊢ Tendsto (fun n => u n / ↑n) atTop (𝓝 (Subadditive.lim h))
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun l hl => _, fun L hL => _⟩
[GOAL]
case refine'_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩
[GOAL]
case refine'_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ u n / n < L :=
  by
  rw [Subadditive.lim] at hL
  rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
  rcases(mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
  exact ⟨n, zero_lt_one.trans_le hn, xL⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rw [Subadditive.lim] at hL
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ Set.Nonempty ((fun n => u n / ↑n) '' Ici 1)
[PROOFSTEP]
simp
[GOAL]
case intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
x : ℝ
hx : x ∈ (fun n => u n / ↑n) '' Ici 1
xL : x < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rcases(mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
[GOAL]
case intro.intro.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
n : ℕ
hn : n ∈ Ici 1
hx : u n / ↑n ∈ (fun n => u n / ↑n) '' Ici 1
xL : u n / ↑n < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
exact ⟨n, zero_lt_one.trans_le hn, xL⟩
[GOAL]
case refine'_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
[PROOFSTEP]
exact h.eventually_div_lt_of_div_lt npos.ne' hn