-- 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 : ℕ
hk : (coeff (ModP O p) p k) (f + g) ≠ 0
hm : (coeff (ModP O p) p (m ⊔ n ⊔ k)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n ⊔ k)) g ≠ 0
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) 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 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

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
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
rw [hg, add_zero, valAux_zero, max_eq_left]

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
⊢ 0 ≤ valAux K v O p f

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

Tactic:
replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| 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
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

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
⊢ valAux K v O p (f + g) ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
by_cases hfg : f + 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
hfg : f + 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
hfg : ¬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
⊢ 0 ≤ valAux K v O p f ⊔ valAux K v O p g

Tactic:
exact zero_le _

Result:
no goals

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

Tactic:
replace hn := coeff_ne_zero_of_le hn (le_trans (le_max_right 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 k : ℕ
hk : (coeff (ModP O p) p k) (f + g) ≠ 0
hm : (coeff (ModP O p) p (m ⊔ n ⊔ k)) f ≠ 0
hn : (coeff (ModP O p) p (m ⊔ n ⊔ k)) 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.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)

Tactic:
exact le_max_of_le_right (pow_le_pow_left' h _)

Result:
no goals