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

Tactic:
rcases le_max_iff.1
    (ModP.preVal_add hv (coeff _ _ (max (max m n) k) f)
    (coeff _ _ (max (max m n) k) g)) with h | h

Result:
case neg.intro.intro.intro.inl
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
h :
  ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f + (coeff (ModP O p) p (m ⊔ n ⊔ k)) g) ≤
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f)
⊢ 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)

case neg.intro.intro.intro.inr
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
h :
  ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f + (coeff (ModP O p) p (m ⊔ n ⊔ k)) g) ≤
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) g)
⊢ 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
⊢ 0 ≤ valAux K v O p g

Tactic:
exact zero_le _

Result:
no goals

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 : ∃ 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

Tactic:
obtain ⟨m, hm⟩ := hf

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 : ℕ
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

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
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:
replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| 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
hg : ¬g = 0
hfg : ¬f + g = 0
hf : ∃ n, (coeff (ModP O p) p n) 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.inl
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
h :
  ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f + (coeff (ModP O p) p (m ⊔ n ⊔ k)) g) ≤
    ModP.preVal K v O p ((coeff (ModP O p) p (m ⊔ n ⊔ k)) f)
⊢ 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)

Tactic:
exact le_max_of_le_left (pow_le_pow_left' h _)

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

Tactic:
exact zero_le _

Result:
no goals