-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) :
    padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r → padicNorm p r < padicNorm p q → padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (r + q) = padicNorm p r ⊔ padicNorm p q

Tactic:
exact this hne.symm (hne.lt_or_lt.resolve_right hlt)

Result:
no goals

Proof state:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p q ⊔ padicNorm p r ≤ padicNorm p (q + r)

Tactic:
rwa [max_eq_left_of_lt hlt]

Result:
no goals

Proof state:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

Tactic:
apply padicNorm.nonarchimedean

Result:
no goals

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
have hnge : padicNorm p r ≤ padicNorm p (q + r) := by
  apply le_of_not_gt
  intro hgt
  rw [max_eq_right_of_lt hgt] at this
  exact not_lt_of_ge this hlt

Result:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p q = padicNorm p (q + r + -r)

Tactic:
ring_nf

Result:
no goals

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
have : padicNorm p q ≤ padicNorm p (q + r) := by rwa [max_eq_left hnge] at this

Result:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
have : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r) :=
  calc
    padicNorm p q = padicNorm p (q + r + (-r)) := by ring_nf
    _ ≤ max (padicNorm p (q + r)) (padicNorm p (-r)) := padicNorm.nonarchimedean
    _ = max (padicNorm p (q + r)) (padicNorm p r) := by simp

Result:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
⊢ padicNorm p r ≤ padicNorm p (q + r)

Tactic:
apply le_of_not_gt

Result:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
⊢ ¬padicNorm p r > padicNorm p (q + r)

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
apply _root_.le_antisymm

Result:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) ≤ padicNorm p q ⊔ padicNorm p r

case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p q ⊔ padicNorm p r ≤ padicNorm p (q + r)

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) ⊔ padicNorm p (-r) = padicNorm p (q + r) ⊔ padicNorm p r

Tactic:
simp

Result:
no goals

Proof state:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False

Tactic:
exact not_lt_of_ge this hlt

Result:
no goals

Proof state:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
⊢ ¬padicNorm p r > padicNorm p (q + r)

Tactic:
intro hgt

Result:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False

Proof state:
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p q ≤ padicNorm p (q + r)

Tactic:
rwa [max_eq_left hnge] at this

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r → padicNorm p r < padicNorm p q → padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
rw [add_comm, max_comm]

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r → padicNorm p r < padicNorm p q → padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (r + q) = padicNorm p r ⊔ padicNorm p q

Proof state:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p (q + r) ⊔ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False

Tactic:
rw [max_eq_right_of_lt hgt] at this

Result:
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False