Theorem: Int.nat_val_add_ge_min (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
cases lt_trichotomy (nat_valuation p a) (nat_valuation p b) with | inl h =>
  simp only [min, if_pos (le_of_lt h)]
  apply le_of_eq
  rw [nat_val_add_eq_min p a b h]
  rw [inf_eq_left]
  exact h.le
| inr h => cases h with
  | inl h =>
    simp only [min, if_pos (le_of_eq h)]
    sorry
  | inr h =>
    simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
    apply le_of_eq
    rw [nat_val_add_eq_min p b a h]
    simp
    exact h.le
State after:
no goals

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [min, if_pos (le_of_lt h)]
State after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Tactic:
apply le_of_eq
State after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (a + b)

State before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (a + b)
Tactic:
rw [nat_val_add_eq_min p a b h]
State after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p a

State before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p a
Tactic:
rw [inf_eq_left]
State after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ≤ nat_valuation p b

State before:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p a ≤ nat_valuation p b
Tactic:
exact h.le
State after:
no goals

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b ∨ nat_valuation p b < nat_valuation p a
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
cases h with
| inl h =>
simp only [min, if_pos (le_of_eq h)]
sorry
| inr h =>
simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
apply le_of_eq
rw [nat_val_add_eq_min p b a h]
simp
exact h.le
State after:
no goals

State before:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [min, if_pos (le_of_eq h)]
State after:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)

State before:
case inr.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a = nat_valuation p b
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (a + b)
Tactic:
sorry
State after:
no goals

State before:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
State after:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (b + a)

State before:
case inr.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b ≤ nat_valuation p (b + a)
Tactic:
apply le_of_eq
State after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (b + a)

State before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p (b + a)
Tactic:
rw [nat_val_add_eq_min p b a h]
State after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p b

State before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p a ⊓ nat_valuation p b = nat_valuation p b
Tactic:
simp
State after:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p b ≤ nat_valuation p a

State before:
case inr.inr.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p b < nat_valuation p a
⊢ nat_valuation p b ≤ nat_valuation p a
Tactic:
exact h.le
State after:
no goals