Theorem: Weight.eq_right_of_add_le (Weights/Dimension2.lean)

State before:
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
⊢ a = I.a₂ ∧ b = I.b₂
Tactic:
refine Nat.eq_and_eq_of_coprime_coprime_mul_eq_mul hcop I.coprime₂ ?_
State after:
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
⊢ a * I.b₂ = b * I.a₂

State before:
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
⊢ a * I.b₂ = b * I.a₂
Tactic:
rcases eq_or_eq_or_mem_interior_of_mem hmem with left | right | interior
State after:
case inl
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
left : a * I.b₁ = b * I.a₁
⊢ a * I.b₂ = b * I.a₂

case inr.inl
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
right : a * I.b₂ = b * I.a₂
⊢ a * I.b₂ = b * I.a₂

case inr.inr
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
interior : BasicInterval.mem_interior a b I
⊢ a * I.b₂ = b * I.a₂

State before:
case inl
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
left : a * I.b₁ = b * I.a₁
⊢ a * I.b₂ = b * I.a₂
Tactic:
contradiction
State after:
no goals

State before:
case inr.inl
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
right : a * I.b₂ = b * I.a₂
⊢ a * I.b₂ = b * I.a₂
Tactic:
exact right
State after:
no goals

State before:
case inr.inr
d a b : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
hcop : Nat.Coprime a b
hmem : mem a b I
hbd : a + b ≤ d
hne : a * I.b₁ ≠ b * I.a₁
interior : BasicInterval.mem_interior a b I
⊢ a * I.b₂ = b * I.a₂
Tactic:
linarith only [gt_of_mem_interior_feasible hI interior, hbd]
State after:
no goals