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

State before:
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
obtain ⟨h₁, h₂⟩ := h
State after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I

State before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
cases' h₁.eq_or_lt with H₁ H₁
State after:
case intro.inl
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ = a * I.b₁
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I

case intro.inr
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I

State before:
case intro.inr
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
cases' h₂.eq_or_lt with H₂ H₂
State after:
case intro.inr.inl
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
H₂ : a * I.b₂ = b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I

case intro.inr.inr
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
H₂ : a * I.b₂ < b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I

State before:
case intro.inr.inr
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
H₂ : a * I.b₂ < b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
exact Or.inr <| Or.inr ⟨H₁, H₂⟩
State after:
no goals

State before:
case intro.inl
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ = a * I.b₁
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
exact Or.inl H₁.symm
State after:
no goals

State before:
case intro.inr.inl
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * I.b₂ ≤ b * I.a₂
H₁ : b * I.a₁ < a * I.b₁
H₂ : a * I.b₂ = b * I.a₂
⊢ a * I.b₁ = b * I.a₁ ∨ a * I.b₂ = b * I.a₂ ∨ mem_interior a b I
Tactic:
exact Or.inr <| Or.inl H₂
State after:
no goals