-- Mathlib/RingTheory/Perfection.lean
theorem valAux_add (f g : PreTilt O p) :
    valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Proof state:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
by_cases hf : f = 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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Proof state:
case neg.intro.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n k : ℕ
hm : (coeff (ModP O p) p (m ⊔ n ⊔ k)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n ⊔ k)) g ≠ 0
hk : (coeff (ModP O p) p (m ⊔ n ⊔ k)) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
rw [valAux_eq hv hm, valAux_eq hv hn, valAux_eq hv hk, RingHom.map_add]

Result:
case neg.intro.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n k : ℕ
hm : (coeff (ModP O p) p (m ⊔ n ⊔ k)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n ⊔ k)) g ≠ 0
hk : (coeff (ModP O p) p (m ⊔ n ⊔ k)) (f + g) ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f + (coeff (ModP O p) p (m ⊔ n ⊔ k)) g) ^ p ^ (m ⊔ n ⊔ k) ≤
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f) ^ p ^ (m ⊔ n ⊔ k) ⊔
      ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) g) ^ p ^ (m ⊔ n ⊔ k)

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
rw [hf, zero_add, valAux_zero, max_eq_right]

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f = 0
⊢ 0 ≤ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
by_cases hg : g = 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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : g = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hg : ∃ n, (coeff (ModP O p) p n) g ≠ 0
hfg : ∃ n, (coeff (ModP O p) p n) (f + g) ≠ 0
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
obtain ⟨n, hn⟩ := hg

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hfg : ∃ n, (coeff (ModP O p) p n) (f + g) ≠ 0
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hfg : ¬f + g = 0
hf : ∃ n, (coeff (ModP O p) p n) f ≠ 0
hg : ∃ n, (coeff (ModP O p) p n) g ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
replace hfg : ∃ n, coeff _ _ n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h

Result:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ∃ n, (coeff (ModP O p) p n) f ≠ 0
hg : ∃ n, (coeff (ModP O p) p n) g ≠ 0
hfg : ∃ n, (coeff (ModP O p) p n) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
hfg : f + g = 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
rw [hfg, valAux_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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : ¬f = 0
hg : ¬g = 0
hfg : f + g = 0
⊢ 0 ≤ valAux K v O p f ⊔ valAux K v O p g

Proof state:
case neg.intro.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
k : ℕ
hk : (coeff (ModP O p) p k) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
replace hm := coeff_ne_zero_of_le hm (le_trans (le_max_left m n) (le_max_left _ k))

Result:
case neg.intro.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
k : ℕ
hk : (coeff (ModP O p) p k) (f + g) ≠ 0
hm : (coeff (ModP O p) p (m ⊔ n ⊔ k)) f ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hfg : ∃ n, (coeff (ModP O p) p n) (f + g) ≠ 0
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
obtain ⟨k, hk⟩ := hfg

Result:
case neg.intro.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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
m : ℕ
hm : (coeff (ModP O p) p m) f ≠ 0
n : ℕ
hn : (coeff (ModP O p) p n) g ≠ 0
k : ℕ
hk : (coeff (ModP O p) p k) (f + g) ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g