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

State before:
a b : ℕ
I : BasicInterval
h : mem_interior a b I
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
obtain ⟨k₁, k₂, h₁, h₂⟩ := exists_of_mem (mem_of_mem_interior h)
State after:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : mem_interior a b I
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂

State before:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : mem_interior a b I
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
simp only [mem_interior] at h
State after:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂

State before:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
refine ⟨k₁, k₂, Nat.pos_of_ne_zero ?_, Nat.pos_of_ne_zero ?_, h₁, h₂⟩
State after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ ≠ 0

case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₂ ≠ 0

State before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ ≠ 0
Tactic:
rintro rfl
State after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = 0 * I.a₁ + k₂ * I.a₂
h₂ : b = 0 * I.b₁ + k₂ * I.b₂
⊢ False

State before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = 0 * I.a₁ + k₂ * I.a₂
h₂ : b = 0 * I.b₁ + k₂ * I.b₂
⊢ False
Tactic:
simp only [zero_mul, zero_add] at h₁ h₂
State after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
⊢ False

State before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
⊢ False
Tactic:
replace h := h.2
State after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : a * I.b₂ < b * I.a₂
⊢ False

State before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : a * I.b₂ < b * I.a₂
⊢ False
Tactic:
simp only [h₁, mul_assoc, h₂, mul_comm I.a₂] at h
State after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : k₂ * (I.b₂ * I.a₂) < k₂ * (I.b₂ * I.a₂)
⊢ False

State before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : k₂ * (I.b₂ * I.a₂) < k₂ * (I.b₂ * I.a₂)
⊢ False
Tactic:
exact lt_irrefl _ h
State after:
no goals

State before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₂ ≠ 0
Tactic:
rintro rfl
State after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁ + 0 * I.a₂
h₂ : b = k₁ * I.b₁ + 0 * I.b₂
⊢ False

State before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁ + 0 * I.a₂
h₂ : b = k₁ * I.b₁ + 0 * I.b₂
⊢ False
Tactic:
simp only [zero_mul, add_zero] at h₁ h₂
State after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
⊢ False

State before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
⊢ False
Tactic:
replace h := h.1
State after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : b * I.a₁ < a * I.b₁
⊢ False

State before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : b * I.a₁ < a * I.b₁
⊢ False
Tactic:
simp only [h₁, mul_assoc, h₂, mul_comm I.a₁] at h
State after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : k₁ * (I.b₁ * I.a₁) < k₁ * (I.b₁ * I.a₁)
⊢ False

State before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : k₁ * (I.b₁ * I.a₁) < k₁ * (I.b₁ * I.a₁)
⊢ False
Tactic:
exact lt_irrefl _ h
State after:
no goals