-- Mathlib/RingTheory/Perfection.lean
theorem preVal_add (x y : ModP O p) :
    preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
rw [hy0, add_zero]

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O p x ≤ preVal K v O p x ⊔ preVal K v O p 0

Proof state:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : ¬x + y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hy0 : ¬y = 0
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + y = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + y) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p y

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O p x ≤ preVal K v O p x ⊔ preVal K v O p 0

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ v ((algebraMap O K) r + (algebraMap O K) s) ≤ v ((algebraMap O K) r) ⊔ v ((algebraMap O K) s)

Tactic:
exact v.map_add _ _

Result:
no goals

Proof state:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Tactic:
rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, RingHom.map_add]

Result:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ v ((algebraMap O K) r + (algebraMap O K) s) ≤ v ((algebraMap O K) r) ⊔ v ((algebraMap O K) s)

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x = 0
⊢ preVal K v O p y ≤ preVal K v O p 0 ⊔ preVal K v O p y

Tactic:
exact le_max_right _ _

Result:
no goals

Proof state:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ 0 ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
hy0 : ¬y = 0
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + y = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + y) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p y

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y

Result:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Proof state:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
by_cases hxy0 : x + y = 0

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : ¬x + y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Proof state:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Tactic:
by_cases hy0 : y = 0

Result:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ preVal K v O p (x + y) ≤ preVal K v O p x ⊔ preVal K v O p y

Proof state:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Tactic:
rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢

Result:
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) ⊔ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)