[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
f g : Valuation R Γ₀
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
g : Valuation R Γ₀
toFun✝ : R → Γ₀
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } x *
        ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } y
map_add_le_max'✝ :
  ∀ (x y : R),
    ZeroHom.toFun
        (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ })
        (x + y) ≤
      max
        (ZeroHom.toFun
          (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ })
          x)
        (ZeroHom.toFun
          (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ })
          y)
h :
  (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
        map_add_le_max' := map_add_le_max'✝ } =
    (fun f => f.toFun) g
⊢ {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
      map_add_le_max' := map_add_le_max'✝ } =
    g
[PROOFSTEP]
congr
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
⊢ v.toFun = ↑v
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
⊢ ↑v.toMonoidWithZeroHom = ↑v
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
⊢ ∀ (x y : R), ↑v (x + y) ≤ ↑v x ∨ ↑v (x + y) ≤ ↑v y
[PROOFSTEP]
intro x y
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≤ ↑v x ∨ ↑v (x + y) ≤ ↑v y
[PROOFSTEP]
rw [← le_max_iff, ← ge_iff_le]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ max (↑v x) (↑v y) ≥ ↑v (x + y)
[PROOFSTEP]
apply map_add
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ (i : ι), i ∈ s → ↑v (f i) ≤ g
⊢ ↑v (∑ i in s, f i) ≤ g
[PROOFSTEP]
refine' Finset.induction_on s (fun _ => v.map_zero ▸ zero_le') (fun a s has ih hf => _) hf
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) ≤ g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) ≤ g) → ↑v (∑ i in s, f i) ≤ g
hf : ∀ (i : ι), i ∈ insert a s → ↑v (f i) ≤ g
⊢ ↑v (∑ i in insert a s, f i) ≤ g
[PROOFSTEP]
rw [Finset.forall_mem_insert] at hf 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) ≤ g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) ≤ g) → ↑v (∑ i in s, f i) ≤ g
hf : ↑v (f a) ≤ g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) ≤ g
⊢ ↑v (∑ i in insert a s, f i) ≤ g
[PROOFSTEP]
rw [Finset.sum_insert has]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) ≤ g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) ≤ g) → ↑v (∑ i in s, f i) ≤ g
hf : ↑v (f a) ≤ g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) ≤ g
⊢ ↑v (f a + ∑ x in s, f x) ≤ g
[PROOFSTEP]
exact v.map_add_le hf.1 (ih hf.2)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ (i : ι), i ∈ s → ↑v (f i) < g
⊢ ↑v (∑ i in s, f i) < g
[PROOFSTEP]
refine' Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg)) (fun a s has ih hf => _) hf
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ∀ (i : ι), i ∈ insert a s → ↑v (f i) < g
⊢ ↑v (∑ i in insert a s, f i) < g
[PROOFSTEP]
rw [Finset.forall_mem_insert] at hf 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (∑ i in insert a s, f i) < g
[PROOFSTEP]
rw [Finset.sum_insert has]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (f a + ∑ x in s, f x) < g
[PROOFSTEP]
exact v.map_add_lt hf.1 (ih hf.2)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁵ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
v✝ : Valuation R Γ₀
x✝ y✝ z : R
S : Type u_7
inst✝ : Ring S
f : S →+* R
v : Valuation R Γ₀
src✝ : S →*₀ Γ₀ := MonoidWithZeroHom.comp v.toMonoidWithZeroHom (RingHom.toMonoidWithZeroHom f)
x y : S
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := ↑v ∘ ↑f, map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
          map_one' := (_ : ZeroHom.toFun (↑src✝) 1 = 1),
          map_mul' :=
            (_ : ∀ (x y : S), ZeroHom.toFun (↑src✝) (x * y) = ZeroHom.toFun (↑src✝) x * ZeroHom.toFun (↑src✝) y) })
      (x + y) ≤
    max
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := ↑v ∘ ↑f, map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : ZeroHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : S), ZeroHom.toFun (↑src✝) (x * y) = ZeroHom.toFun (↑src✝) x * ZeroHom.toFun (↑src✝) y) })
        x)
      (ZeroHom.toFun
        (↑{ toZeroHom := { toFun := ↑v ∘ ↑f, map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_one' := (_ : ZeroHom.toFun (↑src✝) 1 = 1),
            map_mul' :=
              (_ : ∀ (x y : S), ZeroHom.toFun (↑src✝) (x * y) = ZeroHom.toFun (↑src✝) x * ZeroHom.toFun (↑src✝) y) })
        y)
[PROOFSTEP]
simp only [comp_apply, map_add, f.map_add]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x - y) = ↑v (x + -y)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ max (↑v x) (↑v (-y)) = max (↑v x) (↑v y)
[PROOFSTEP]
rw [map_neg]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
g : (fun x => Γ₀) x
hx : ↑v x ≤ g
hy : ↑v y ≤ g
⊢ ↑v (x - y) ≤ g
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
g : (fun x => Γ₀) x
hx : ↑v x ≤ g
hy : ↑v y ≤ g
⊢ ↑v (x + -y) ≤ g
[PROOFSTEP]
exact v.map_add_le hx (le_trans (le_of_eq (v.map_neg y)) hy)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ↑v (x + y) = max (↑v x) (↑v y)
[PROOFSTEP]
suffices : ¬v (x + y) < max (v x) (v y)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
this : ¬↑v (x + y) < max (↑v x) (↑v y)
⊢ ↑v (x + y) = max (↑v x) (↑v y)
case this
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
[PROOFSTEP]
exact or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this
[GOAL]
case this
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
[PROOFSTEP]
intro h'
[GOAL]
case this
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
⊢ False
[PROOFSTEP]
wlog vyx : v y < v x generalizing x y
[GOAL]
case this.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ False
[PROOFSTEP]
refine' this h.symm _ (h.lt_or_lt.resolve_right vyx)
[GOAL]
case this.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ ↑v (y + x) < max (↑v y) (↑v x)
[PROOFSTEP]
rwa [add_comm, max_comm]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
vyx : ↑v y < ↑v x
⊢ False
[PROOFSTEP]
rw [max_eq_left_of_lt vyx] at h' 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ False
[PROOFSTEP]
apply lt_irrefl (v x)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ ↑v x < ↑v x
[PROOFSTEP]
calc
  v x = v (x + y - y) := by simp
  _ ≤ max (v <| x + y) (v y) := (map_sub _ _ _)
  _ < v x := max_lt h' vyx
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ ↑v x = ↑v (x + y - y)
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v y < ↑v x
⊢ ↑v (x + y) = ↑v x
[PROOFSTEP]
rw [add_comm]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v y < ↑v x
⊢ ↑v (y + x) = ↑v x
[PROOFSTEP]
exact map_add_eq_of_lt_right _ h
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
⊢ ↑v y = ↑v x
[PROOFSTEP]
have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = max (↑v (y - x)) (↑v x)
⊢ ↑v y = ↑v x
[PROOFSTEP]
rw [max_eq_right (le_of_lt h)] at this 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = ↑v x
⊢ ↑v y = ↑v x
[PROOFSTEP]
simpa using this
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x < 1
⊢ ↑v (1 + x) = 1
[PROOFSTEP]
rw [← v.map_one] at h 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x < ↑v 1
⊢ ↑v (1 + x) = 1
[PROOFSTEP]
simpa only [v.map_one] using v.map_add_eq_of_lt_left h
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x < 1
⊢ ↑v (1 - x) = 1
[PROOFSTEP]
rw [← v.map_one, ← v.map_neg] at h 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 - x) = 1
[PROOFSTEP]
rw [sub_eq_add_neg 1 x]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 + -x) = 1
[PROOFSTEP]
simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x✝ y z : R
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ 1 < ↑v x ↔ ↑v x⁻¹ < 1
[PROOFSTEP]
simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y z : R
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ 0 ∈
    { carrier := {x | ↑v x < ↑γ},
        add_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x < ↑γ} → y ∈ {x | ↑v x < ↑γ} → ↑v (x + y) < ↑γ) }.carrier
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y z : R
v : Valuation R Γ₀
γ : Γ₀ˣ
x✝ : R
x_in :
  x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑v x < ↑γ},
              add_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x < ↑γ} → y ∈ {x | ↑v x < ↑γ} → ↑v (x + y) < ↑γ) },
          zero_mem' := (_ : ↑v 0 < ↑γ) }.toAddSubsemigroup.carrier
⊢ -x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑v x < ↑γ},
              add_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x < ↑γ} → y ∈ {x | ↑v x < ↑γ} → ↑v (x + y) < ↑γ) },
          zero_mem' := (_ : ↑v 0 < ↑γ) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rwa [Set.mem_setOf, map_neg]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
v' : Valuation R Γ₀
h : v = v'
⊢ IsEquiv v v'
[PROOFSTEP]
subst h
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
⊢ IsEquiv v v
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ↑f
inf : Injective ↑f
h : IsEquiv v v'
H : StrictMono ↑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ ↑f (↑v r) ≤ ↑f (↑v s) ↔ ↑v r ≤ ↑v s
[PROOFSTEP]
rw [H.le_iff_le]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ↑f
inf : Injective ↑f
h : IsEquiv v v'
H : StrictMono ↑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ ↑v' r ≤ ↑v' s ↔ ↑f (↑v' r) ≤ ↑f (↑v' s)
[PROOFSTEP]
rw [H.le_iff_le]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r s : R
⊢ ↑v₁ r = ↑v₁ s ↔ ↑v₂ r = ↑v₂ s
[PROOFSTEP]
simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r : R
⊢ ↑v₁ r ≠ 0 ↔ ↑v₂ r ≠ 0
[PROOFSTEP]
have : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0 := not_congr h.val_eq
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r : R
this : ↑v₁ r ≠ ↑v₁ 0 ↔ ↑v₂ r ≠ ↑v₂ 0
⊢ ↑v₁ r ≠ 0 ↔ ↑v₂ r ≠ 0
[PROOFSTEP]
rwa [v₁.map_zero, v₂.map_zero] at this 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ IsEquiv v v'
[PROOFSTEP]
intro x y
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
[PROOFSTEP]
simp [hy, zero_iff]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
[PROOFSTEP]
rw [show y = 1 * y by rw [one_mul]]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ y = 1 * y
[PROOFSTEP]
rw [one_mul]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v (1 * y) ↔ ↑v' x ≤ ↑v' (1 * y)
[PROOFSTEP]
rw [← inv_mul_cancel_right₀ hy x]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹ * y) ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹ * y) ≤ ↑v' (1 * y)
[PROOFSTEP]
iterate 2 rw [v.map_mul _ y, v'.map_mul _ y]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹ * y) ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹ * y) ≤ ↑v' (1 * y)
[PROOFSTEP]
rw [v.map_mul _ y, v'.map_mul _ y]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' (1 * y)
[PROOFSTEP]
rw [v.map_mul _ y, v'.map_mul _ y]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' 1 * ↑v' y
[PROOFSTEP]
rw [v.map_one, v'.map_one]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y → ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
[PROOFSTEP]
intro H
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y → ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
[PROOFSTEP]
intro H
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
[PROOFSTEP]
apply mul_le_mul_right'
[GOAL]
case neg.mp.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) ≤ 1
[PROOFSTEP]
replace hy := v.ne_zero_iff.mpr hy
[GOAL]
case neg.mp.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
hy : ↑v y ≠ 0
⊢ ↑v' (x * y⁻¹) ≤ 1
[PROOFSTEP]
replace H := le_of_le_mul_right hy H
[GOAL]
case neg.mp.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v y ≠ 0
H : ↑v (x * y⁻¹) ≤ 1
⊢ ↑v' (x * y⁻¹) ≤ 1
[PROOFSTEP]
rwa [h] at H 
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
[PROOFSTEP]
apply mul_le_mul_right'
[GOAL]
case neg.mpr.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) ≤ 1
[PROOFSTEP]
replace hy := v'.ne_zero_iff.mpr hy
[GOAL]
case neg.mpr.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
hy : ↑v' y ≠ 0
⊢ ↑v (x * y⁻¹) ≤ 1
[PROOFSTEP]
replace H := le_of_le_mul_right hy H
[GOAL]
case neg.mpr.bc
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v' y ≠ 0
H : ↑v' (x * y⁻¹) ≤ 1
⊢ ↑v (x * y⁻¹) ≤ 1
[PROOFSTEP]
rwa [h]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : IsEquiv v v'
x : K
⊢ ↑v x ≤ 1 ↔ ↑v' x ≤ 1
[PROOFSTEP]
simpa using h x 1
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' → ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
intro h x
[GOAL]
case mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : IsEquiv v v'
x : K
⊢ ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
simpa using @IsEquiv.val_eq _ _ _ _ _ _ v v' h x 1
[GOAL]
case mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1) → IsEquiv v v'
[PROOFSTEP]
intro h
[GOAL]
case mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v'
[PROOFSTEP]
apply isEquiv_of_val_le_one
[GOAL]
case mpr.h
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
[PROOFSTEP]
intro x
[GOAL]
case mpr.h
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 ↔ ↑v' x ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mpr.h.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 → ↑v' x ≤ 1
[PROOFSTEP]
intro hx
[GOAL]
case mpr.h.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
cases' lt_or_eq_of_le hx with hx' hx'
[GOAL]
case mpr.h.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
have : v (1 + x) = 1 := by
  rw [← v.map_one]
  apply map_add_eq_of_lt_left
  simpa
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v (1 + x) = 1
[PROOFSTEP]
rw [← v.map_one]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v (1 + x) = ↑v 1
[PROOFSTEP]
apply map_add_eq_of_lt_left
[GOAL]
case h
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v x < ↑v 1
[PROOFSTEP]
simpa
[GOAL]
case mpr.h.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v (1 + x) = 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
rw [h] at this 
[GOAL]
case mpr.h.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
rw [show x = -1 + (1 + x) by simp]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ x = -1 + (1 + x)
[PROOFSTEP]
simp
[GOAL]
case mpr.h.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' (-1 + (1 + x)) ≤ 1
[PROOFSTEP]
refine' le_trans (v'.map_add _ _) _
[GOAL]
case mpr.h.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ max (↑v' (-1)) (↑v' (1 + x)) ≤ 1
[PROOFSTEP]
simp [this]
[GOAL]
case mpr.h.mp.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x = 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
rw [h] at hx' 
[GOAL]
case mpr.h.mp.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v' x ≤ 1
[PROOFSTEP]
exact le_of_eq hx'
[GOAL]
case mpr.h.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v' x ≤ 1 → ↑v x ≤ 1
[PROOFSTEP]
intro hx
[GOAL]
case mpr.h.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
cases' lt_or_eq_of_le hx with hx' hx'
[GOAL]
case mpr.h.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
have : v' (1 + x) = 1 := by
  rw [← v'.map_one]
  apply map_add_eq_of_lt_left
  simpa
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' (1 + x) = 1
[PROOFSTEP]
rw [← v'.map_one]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' (1 + x) = ↑v' 1
[PROOFSTEP]
apply map_add_eq_of_lt_left
[GOAL]
case h
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' x < ↑v' 1
[PROOFSTEP]
simpa
[GOAL]
case mpr.h.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
rw [← h] at this 
[GOAL]
case mpr.h.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
rw [show x = -1 + (1 + x) by simp]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ x = -1 + (1 + x)
[PROOFSTEP]
simp
[GOAL]
case mpr.h.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v (-1 + (1 + x)) ≤ 1
[PROOFSTEP]
refine' le_trans (v.map_add _ _) _
[GOAL]
case mpr.h.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ max (↑v (-1)) (↑v (1 + x)) ≤ 1
[PROOFSTEP]
simp [this]
[GOAL]
case mpr.h.mpr.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
rw [← h] at hx' 
[GOAL]
case mpr.h.mpr.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v x = 1
⊢ ↑v x ≤ 1
[PROOFSTEP]
exact le_of_eq hx'
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' → ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
[PROOFSTEP]
intro h x
[GOAL]
case mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : IsEquiv v v'
x : K
⊢ ↑v x < 1 ↔ ↑v' x < 1
[PROOFSTEP]
simp only [lt_iff_le_and_ne, and_congr ((isEquiv_iff_val_le_one _ _).1 h) ((isEquiv_iff_val_eq_one _ _).1 h).not]
[GOAL]
case mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1) → IsEquiv v v'
[PROOFSTEP]
rw [isEquiv_iff_val_eq_one]
[GOAL]
case mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1) → ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
intro h x
[GOAL]
case mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
⊢ ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : x = 0
⊢ ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
rw [(zero_iff _).2 hx, (zero_iff _).2 hx]
[GOAL]
case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : x = 0
⊢ 0 = 1 ↔ 0 = 1
[PROOFSTEP]
simp only [zero_ne_one]
[GOAL]
case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
⊢ ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
⊢ ↑v x = 1 → ↑v' x = 1
[PROOFSTEP]
intro hh
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
⊢ ↑v' x = 1
[PROOFSTEP]
by_contra h_1
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
⊢ False
[PROOFSTEP]
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
[GOAL]
case neg.mp
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
x✝ : ↑v' x < 1 ∨ ↑v' x > 1
⊢ False
[PROOFSTEP]
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
[GOAL]
case neg.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
h_2 : ↑v' x < 1
⊢ False
[PROOFSTEP]

| inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
[GOAL]
case neg.mp.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
h_2 : ↑v' x < 1
⊢ False
[PROOFSTEP]
simpa [hh, lt_self_iff_false] using h.2 h_2
[GOAL]
case neg.mp.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
h_2 : ↑v' x > 1
⊢ False
[PROOFSTEP]

| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
[GOAL]
case neg.mp.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x = 1
h_1 : ¬↑v' x = 1
h_2 : ↑v' x > 1
⊢ False
[PROOFSTEP]
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
[GOAL]
case neg.mp.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v x⁻¹ = 1
h_1 : ¬↑v' x = 1
h_2 : ↑v' x > 1
⊢ False
[PROOFSTEP]
exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
⊢ ↑v' x = 1 → ↑v x = 1
[PROOFSTEP]
intro hh
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
⊢ ↑v x = 1
[PROOFSTEP]
by_contra h_1
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
⊢ False
[PROOFSTEP]
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
[GOAL]
case neg.mpr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
x✝ : ↑v x < 1 ∨ ↑v x > 1
⊢ False
[PROOFSTEP]
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
[GOAL]
case neg.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
h_2 : ↑v x < 1
⊢ False
[PROOFSTEP]

| inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
[GOAL]
case neg.mpr.inl
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
h_2 : ↑v x < 1
⊢ False
[PROOFSTEP]
simpa [hh, lt_self_iff_false] using h.1 h_2
[GOAL]
case neg.mpr.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
h_2 : ↑v x > 1
⊢ False
[PROOFSTEP]

| inr h_2 =>
  rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
  exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
[GOAL]
case neg.mpr.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x = 1
h_1 : ¬↑v x = 1
h_2 : ↑v x > 1
⊢ False
[PROOFSTEP]
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh 
[GOAL]
case neg.mpr.inr
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
x : K
hx : ¬x = 0
hh : ↑v' x⁻¹ = 1
h_1 : ¬↑v x = 1
h_2 : ↑v x > 1
⊢ False
[PROOFSTEP]
exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
[PROOFSTEP]
rw [isEquiv_iff_val_lt_one]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1) ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
[PROOFSTEP]
exact (Equiv.subRight 1).surjective.forall
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
[PROOFSTEP]
apply isEquiv_iff_val_le_one
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
[PROOFSTEP]
tfae_have 1 ↔ 3
[GOAL]
case tfae_1_iff_3
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
[PROOFSTEP]
apply isEquiv_iff_val_eq_one
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
[PROOFSTEP]
tfae_have 1 ↔ 4
[GOAL]
case tfae_1_iff_4
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
[PROOFSTEP]
apply isEquiv_iff_val_lt_one
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
[PROOFSTEP]
tfae_have 1 ↔ 5
[GOAL]
case tfae_1_iff_5
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
[PROOFSTEP]
apply isEquiv_iff_val_sub_one_lt_one
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
tfae_1_iff_5 : IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
[PROOFSTEP]
tfae_finish
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁶ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝⁴ : CommRing R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : supp v = ⊤
⊢ ↑v 1 = 0
[PROOFSTEP]
rw [← mem_supp_iff, h]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁶ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝⁴ : CommRing R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
h : supp v = ⊤
⊢ 1 ∈ ⊤
[PROOFSTEP]
exact Submodule.mem_top
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁶ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝⁴ : CommRing R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
x y : R
hxy : x * y ∈ supp v
⊢ x ∈ supp v ∨ y ∈ supp v
[PROOFSTEP]
simp only [mem_supp_iff] at hxy ⊢
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁶ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝⁴ : CommRing R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
x y : R
hxy : ↑v (x * y) = 0
⊢ ↑v x = 0 ∨ ↑v y = 0
[PROOFSTEP]
rw [v.map_mul x y] at hxy 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁶ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁵ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝⁴ : CommRing R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
x y : R
hxy : ↑v x * ↑v y = 0
⊢ ↑v x = 0 ∨ ↑v y = 0
[PROOFSTEP]
exact eq_zero_or_eq_zero_of_mul_eq_zero hxy
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
⊢ ↑v (a + s) = ↑v a
[PROOFSTEP]
have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
  intro a' s' h'
  refine' le_trans (v.map_add a' s') (max_le le_rfl _)
  simp [h']
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
⊢ ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
[PROOFSTEP]
intro a' s' h'
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v (a' + s') ≤ ↑v a'
[PROOFSTEP]
refine' le_trans (v.map_add a' s') (max_le le_rfl _)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v s' ≤ ↑v a'
[PROOFSTEP]
simp [h']
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v (a + s) = ↑v a
[PROOFSTEP]
apply le_antisymm (aux a s h)
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v a ≤ ↑v (a + s)
[PROOFSTEP]
calc
  v a = v (a + s + -s) := by simp
  _ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h )
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v a = ↑v (a + s + -s)
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v (-s) = 0
[PROOFSTEP]
rwa [← Ideal.neg_mem_iff] at h 
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁵ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
S : Type u_7
inst✝ : CommRing S
f : S →+* R
x : S
⊢ x ∈ supp (comap f v) ↔ x ∈ Ideal.comap f (supp v)
[PROOFSTEP]
rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
[GOAL]
K : Type u_1
F : Type u_2
R✝ : Type u_3
inst✝² : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
R : Type ?u.4327439
Γ₀ : Type ?u.4327442
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
f g : AddValuation R Γ₀
⊢ (fun v => v.toFun) f = (fun v => v.toFun) g → f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
K : Type u_1
F : Type u_2
R✝ : Type u_3
inst✝² : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
R : Type ?u.4327439
Γ₀ : Type ?u.4327442
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
g : AddValuation R Γ₀
toMonoidWithZeroHom✝ : R →*₀ Multiplicative Γ₀ᵒᵈ
map_add_le_max'✝ :
  ∀ (x y : R),
    ZeroHom.toFun (↑toMonoidWithZeroHom✝) (x + y) ≤
      max (ZeroHom.toFun (↑toMonoidWithZeroHom✝) x) (ZeroHom.toFun (↑toMonoidWithZeroHom✝) y)
⊢ (fun v => v.toFun) { toMonoidWithZeroHom := toMonoidWithZeroHom✝, map_add_le_max' := map_add_le_max'✝ } =
      (fun v => v.toFun) g →
    { toMonoidWithZeroHom := toMonoidWithZeroHom✝, map_add_le_max' := map_add_le_max'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
K : Type u_1
F : Type u_2
R✝ : Type u_3
inst✝² : DivisionRing K
Γ₀✝ : Type u_4
Γ'₀ : Type u_5
R : Type ?u.4327439
Γ₀ : Type ?u.4327442
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
toMonoidWithZeroHom✝¹ : R →*₀ Multiplicative Γ₀ᵒᵈ
map_add_le_max'✝¹ :
  ∀ (x y : R),
    ZeroHom.toFun (↑toMonoidWithZeroHom✝¹) (x + y) ≤
      max (ZeroHom.toFun (↑toMonoidWithZeroHom✝¹) x) (ZeroHom.toFun (↑toMonoidWithZeroHom✝¹) y)
toMonoidWithZeroHom✝ : R →*₀ Multiplicative Γ₀ᵒᵈ
map_add_le_max'✝ :
  ∀ (x y : R),
    ZeroHom.toFun (↑toMonoidWithZeroHom✝) (x + y) ≤
      max (ZeroHom.toFun (↑toMonoidWithZeroHom✝) x) (ZeroHom.toFun (↑toMonoidWithZeroHom✝) y)
⊢ (fun v => v.toFun) { toMonoidWithZeroHom := toMonoidWithZeroHom✝¹, map_add_le_max' := map_add_le_max'✝¹ } =
      (fun v => v.toFun) { toMonoidWithZeroHom := toMonoidWithZeroHom✝, map_add_le_max' := map_add_le_max'✝ } →
    { toMonoidWithZeroHom := toMonoidWithZeroHom✝¹, map_add_le_max' := map_add_le_max'✝¹ } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom✝, map_add_le_max' := map_add_le_max'✝ }
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x y z : R
⊢ ∀ (x y : R), ↑v x ≤ ↑v (x + y) ∨ ↑v y ≤ ↑v (x + y)
[PROOFSTEP]
intro x y
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v x ≤ ↑v (x + y) ∨ ↑v y ≤ ↑v (x + y)
[PROOFSTEP]
rw [← @min_le_iff _ _ (v x) (v y) (v (x + y)), ← ge_iff_le]
[GOAL]
K : Type u_1
F : Type u_2
R : Type u_3
inst✝³ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≥ min (↑v x) (↑v y)
[PROOFSTEP]
apply map_add
