-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
/-- Ultrametric property of a p-adic valuation. -/
lemma add_eq_min {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0)
    (hval : padicValRat p q ≠ padicValRat p r) :
    padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p r ≤ padicValRat p q
h3 : padicValRat p (r + q) ⊓ padicValRat p q ≤ padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
rw [add_comm] at h3

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p r ≤ padicValRat p q
h3 : padicValRat p (q + r) ⊓ padicValRat p q ≤ padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p r ≤ padicValRat p q
h3 : padicValRat p (q + r) ⊓ padicValRat p q ≤ padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p (-r) ≤ padicValRat p (q + r + -r)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p (-r) ≤ padicValRat p (q + r + -r)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p (-r) ≤ padicValRat p (q + r + -r)
h3 : padicValRat p (r + q) ⊓ padicValRat p (-q) ≤ padicValRat p (r + q + -q)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
have h1 := min_le_padicValRat_add (p := p) hqr

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p (-r) ≤ padicValRat p (q + r + -r)
h3 : padicValRat p (r + q) ⊓ padicValRat p (-q) ≤ padicValRat p (r + q + -q)
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r

Tactic:
rw [add_neg_cancel_right, padicValRat.neg] at h2 h3

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)
h2 : padicValRat p (q + r) ⊓ padicValRat p r ≤ padicValRat p q
h3 : padicValRat p (r + q) ⊓ padicValRat p q ≤ padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q ⊓ padicValRat p r