Theorem: Weight.BasicInterval.gt_of_mem_interior_feasible (Weights/BasicInterval.lean)

State before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
⊢ d < a + b
Tactic:
obtain ⟨k₁, k₂, hk₁, hk₂, h₁, h₂⟩ := exists_of_mem_interior hab
State after:
case intro.intro.intro.intro.intro
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ d < a + b

State before:
case intro.intro.intro.intro.intro
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ d < a + b
Tactic:
calc
  d < I.a₁ + I.a₂ + I.b₁ + I.b₂                       := hI.2.2
  _ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)                     := by abel
  _ ≤ k₁ * (I.a₁ + I.b₁) + k₂ * (I.a₂ + I.b₂)         :=
    Nat.add_le_add (Nat.le_mul_of_pos_left _ hk₁) (Nat.le_mul_of_pos_left _ hk₂)
  _ = k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂) := by ring
  _ = a + b                                           := by rw [h₁, h₂]
State after:
no goals

State before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ I.a₁ + I.a₂ + I.b₁ + I.b₂ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
Tactic:
abel
State after:
no goals

State before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ * (I.a₁ + I.b₁) + k₂ * (I.a₂ + I.b₂) = k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂)
Tactic:
ring
State after:
no goals

State before:
a b d : ℕ
I : BasicInterval
hI : feasible d I
hab : mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ * I.a₁ + k₂ * I.a₂ + (k₁ * I.b₁ + k₂ * I.b₂) = a + b
Tactic:
rw [h₁, h₂]
State after:
no goals