internlm/Lean-Github huggingface dataset:
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ w j = w1 n j
Tactic:
refine ((Finset.sum_eq_sum_iff_of_le (fun k _ ↦ hc₁ k)).mp ?_ j (Finset.mem_univ j)).symm
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Tactic:
rw [Weight.sum] at hn
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = ∑ i : Fin (Nat.succ n), w i
Tactic:
rw [hn]
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = n
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : ∑ j : Fin (Nat.succ n), w j = n
⊢ ∑ i : Fin (Nat.succ n), w1 n i = n
Tactic:
exact sum_w1 n
Proof state after:
no goals
Theorem: Weight.w1_unique
Proof state before:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = 1
Tactic:
conv_rhs => rw [← E_w1 n]
Proof state after:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = E (w1 n)
Theorem: Weight.w1_unique
Proof state before:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = E (w1 n)
Tactic:
exact E_dom_eq hw (w1_zero n) h₂ h₁
Proof state after:
no goals
Theorem: Weight.BasicInterval.rel
Proof state before:
⊢ base.a₂ * base.b₁ = base.a₁ * base.b₂ + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Weight.BasicInterval.rel
Proof state before:
I' : BasicInterval
⊢ (left I').a₂ * (left I').b₁ = (left I').a₁ * (left I').b₂ + 1
Tactic:
simp [add_mul, mul_add, I'.rel, add_assoc]
Proof state after:
no goals
Theorem: Weight.BasicInterval.rel
Proof state before:
I' : BasicInterval
⊢ (right I').a₂ * (right I').b₁ = (right I').a₁ * (right I').b₂ + 1
Tactic:
simp [add_mul, mul_add, I'.rel, add_assoc, add_comm]
Proof state after:
no goals
Theorem: Weight.BasicInterval.b₁_pos
Proof state before:
⊢ 0 < base.b₁
Tactic:
simp
Proof state after:
no goals
Theorem: Weight.BasicInterval.b₁_pos
Proof state before:
I' : BasicInterval
⊢ 0 < (left I').b₁
Tactic:
simp [I'.b₁_pos]
Proof state after:
no goals
Theorem: Weight.BasicInterval.b₁_pos
Proof state before:
I' : BasicInterval
⊢ 0 < (right I').b₁
Tactic:
simp [I'.b₁_pos]
Proof state after:
no goals
Theorem: Weight.BasicInterval.a₂_pos
Proof state before:
⊢ 0 < base.a₂
Tactic:
simp
Proof state after:
no goals
Theorem: Weight.BasicInterval.a₂_pos
Proof state before:
I' : BasicInterval
⊢ 0 < (left I').a₂
Tactic:
simp [I'.a₂_pos]
Proof state after:
no goals
Theorem: Weight.BasicInterval.a₂_pos
Proof state before:
I' : BasicInterval
⊢ 0 < (right I').a₂
Tactic:
simp [I'.a₂_pos]
Proof state after:
no goals
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
⊢ Nat.Coprime (I.a₂ * I.b₁) (I.a₁ * I.b₂)
Tactic:
rw [Nat.Coprime, Nat.gcd_eq_iff]
Proof state after:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
Tactic:
simp? says simp only [isUnit_one, IsUnit.dvd, Nat.isUnit_iff, Nat.dvd_one, true_and]
Proof state after:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1
Tactic:
intros c h₁ h₂
Proof state after:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₂ * I.b₁
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₂ * I.b₁
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Tactic:
rw [I.rel] at h₁
Proof state after:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₁ * I.b₂ + 1
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
c : ℕ
h₁ : c ∣ I.a₁ * I.b₂ + 1
h₂ : c ∣ I.a₁ * I.b₂
⊢ c = 1
Tactic:
exact Nat.dvd_one.mp <| (Nat.dvd_add_right h₂).mp h₁
Proof state after:
no goals
Theorem: Weight.BasicInterval.coprime
Proof state before:
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
Tactic:
simp only [isUnit_one, IsUnit.dvd, Nat.isUnit_iff, Nat.dvd_one, true_and]
Proof state after:
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1
Theorem: Weight.BasicInterval.mem_of_proportional
Proof state before:
I : BasicInterval
a b g : ℕ
hg : 0 < g
h : mem (a * g) (b * g) I
⊢ mem a b I
Tactic:
obtain ⟨h₁, h₂⟩ := h
Proof state after:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : b * g * I.a₁ ≤ a * g * I.b₁
h₂ : a * g * I.b₂ ≤ b * g * I.a₂
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_proportional
Proof state before:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : b * g * I.a₁ ≤ a * g * I.b₁
h₂ : a * g * I.b₂ ≤ b * g * I.a₂
⊢ mem a b I
Tactic:
simp_rw [mul_comm _ g, mul_assoc] at h₁ h₂
Proof state after:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : g * (b * I.a₁) ≤ g * (a * I.b₁)
h₂ : g * (a * I.b₂) ≤ g * (b * I.a₂)
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_proportional
Proof state before:
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : g * (b * I.a₁) ≤ g * (a * I.b₁)
h₂ : g * (a * I.b₂) ≤ g * (b * I.a₂)
⊢ mem a b I
Tactic:
exact ⟨Nat.le_of_mul_le_mul_left h₁ hg, Nat.le_of_mul_le_mul_left h₂ hg⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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
Proof 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
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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₁
Proof 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
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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₂
Proof 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
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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₂⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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
Proof state after:
no goals
Theorem: Weight.BasicInterval.eq_or_eq_or_mem_interior_of_mem
Proof 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₂
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_of_mem_interior
Proof state before:
a b : ℕ
I : BasicInterval
h : mem_interior a b I
⊢ mem a b I
Tactic:
simp only [mem, mem_interior] at h ⊢
Proof state after:
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
Theorem: Weight.BasicInterval.mem_of_mem_interior
Proof state before:
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_base
Proof state before:
a b : ℕ
⊢ mem a b base
Tactic:
simp [mem]
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_of_mem_left
Proof state before:
a b : ℕ
I : BasicInterval
h : mem a b (left I)
⊢ mem a b I
Tactic:
obtain ⟨h₁, h₂⟩ := h
Proof state after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_mem_left
Proof state before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ mem a b I
Tactic:
simp at h₁ h₂
Proof state after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_mem_left
Proof state before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
⊢ mem a b I
Tactic:
exact ⟨h₁, by linarith⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_of_mem_left
Proof state before:
a b : ℕ
I : BasicInterval
h₁ : b * I.a₁ ≤ a * I.b₁
h₂ : a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
⊢ a * I.b₂ ≤ b * I.a₂
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_of_mem_right
Proof state before:
a b : ℕ
I : BasicInterval
h : mem a b (right I)
⊢ mem a b I
Tactic:
obtain ⟨h₁, h₂⟩ := h
Proof state after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
h₂ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_mem_right
Proof state before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
h₂ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ mem a b I
Tactic:
simp at h₁ h₂
Proof state after:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ mem a b I
Theorem: Weight.BasicInterval.mem_of_mem_right
Proof state before:
case intro
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ mem a b I
Tactic:
exact ⟨by linarith, h₂⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_of_mem_right
Proof state before:
a b : ℕ
I : BasicInterval
h₁ : b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂)
h₂ : a * I.b₂ ≤ b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
by_cases hl : mem a b I.left
Proof state after:
case pos
a b : ℕ
I : BasicInterval
h : mem a b I
hl : mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)

case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case pos
a b : ℕ
I : BasicInterval
h : mem a b I
hl : mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
exact Or.inl hl
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case neg
a b : ℕ
I : BasicInterval
h : mem a b I
hl : ¬mem a b (left I)
⊢ mem a b (left I) ∨ mem a b (right I)
Tactic:
unfold mem at h hl ⊢
Proof state after:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬(b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂)
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬(b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂)
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Tactic:
rw [@not_and_or] at hl
Proof state after:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬b * (left I).a₁ ≤ a * (left I).b₁ ∨ ¬a * (left I).b₂ ≤ b * (left I).a₂
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case neg
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : ¬b * (left I).a₁ ≤ a * (left I).b₁ ∨ ¬a * (left I).b₂ ≤ b * (left I).a₂
⊢ b * (left I).a₁ ≤ a * (left I).b₁ ∧ a * (left I).b₂ ≤ b * (left I).a₂ ∨
    b * (right I).a₁ ≤ a * (right I).b₁ ∧ a * (right I).b₂ ≤ b * (right I).a₂
Tactic:
cases' hl with hl hl <;> push_neg at hl <;> simp at hl ⊢
Proof state after:
case neg.inl
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂

case neg.inr
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : b * (I.a₁ + I.a₂) < a * (I.b₁ + I.b₂)
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case neg.inl
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
exact Or.inl ⟨h.1, by linarith⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : a * I.b₁ < b * I.a₁
⊢ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂)
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.mem_left_or_mem_right
Proof state before:
case neg.inr
a b : ℕ
I : BasicInterval
h : b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂
hl : b * (I.a₁ + I.a₂) < a * (I.b₁ + I.b₂)
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * (I.b₁ + I.b₂) ≤ b * (I.a₁ + I.a₂) ∨
    b * (I.a₁ + I.a₂) ≤ a * (I.b₁ + I.b₂) ∧ a * I.b₂ ≤ b * I.a₂
Tactic:
refine Or.inr ⟨hl.le, h.2⟩
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
induction I with
| base       => simp
| left I ih  =>
  obtain ⟨k₁', k₂, H₁, H₂⟩ := ih (mem_of_mem_left I h)
  simp only [left_a₁, left_a₂, left_b₁, left_b₂]
  have ⟨k₁, hk⟩ : ∃ k, k₁' = k + k₂ := by
    rw [← le_iff_exists_add']
    obtain ⟨_, h₂⟩ := h
    simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] at h₂
    have rel := I.rel
    zify at h₂ rel ⊢
    rw [← sub_nonneg] at h₂ ⊢
    convert h₂ using 1
    linear_combination (k₂ - k₁') * rel
    done
  rw [hk] at H₁ H₂
  refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
  done
| right I ih =>
  obtain ⟨k₁, k₂', H₁, H₂⟩ := ih (mem_of_mem_right I h)
  simp only [right_a₁, right_a₂, right_b₁, right_b₂]
  have ⟨k₂, hk⟩ : ∃ k, k₂' = k + k₁ := by
    rw [← le_iff_exists_add']
    obtain ⟨h₁, _⟩ := h
    simp only [H₂, right_a₁, mul_add, add_mul, H₁, right_b₁] at h₁
    have rel := I.rel
    zify at h₁ rel ⊢
    rw [← sub_nonneg] at h₁ ⊢
    convert h₁ using 1
    linear_combination (k₁ - k₂') * rel
    done
  rw [hk] at H₁ H₂
  refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
  done
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case base
a b : ℕ
h : mem a b base
⊢ ∃ k₁ k₂, a = k₁ * base.a₁ + k₂ * base.a₂ ∧ b = k₁ * base.b₁ + k₂ * base.b₂
Tactic:
simp
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case left
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
⊢ ∃ k₁ k₂, a = k₁ * (left I).a₁ + k₂ * (left I).a₂ ∧ b = k₁ * (left I).b₁ + k₂ * (left I).b₂
Tactic:
obtain ⟨k₁', k₂, H₁, H₂⟩ := ih (mem_of_mem_left I h)
Proof state after:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (left I).a₁ + k₂ * (left I).a₂ ∧ b = k₁ * (left I).b₁ + k₂ * (left I).b₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (left I).a₁ + k₂ * (left I).a₂ ∧ b = k₁ * (left I).b₁ + k₂ * (left I).b₂
Tactic:
simp only [left_a₁, left_a₂, left_b₁, left_b₂]
Proof state after:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Tactic:
have ⟨k₁, hk⟩ : ∃ k, k₁' = k + k₂ := by
  rw [← le_iff_exists_add']
  obtain ⟨_, h₂⟩ := h
  simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] at h₂
  have rel := I.rel
  zify at h₂ rel ⊢
  rw [← sub_nonneg] at h₂ ⊢
  convert h₂ using 1
  linear_combination (k₂ - k₁') * rel
  done
Proof state after:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
k₁ : ℕ
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
k₁ : ℕ
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Tactic:
rw [hk] at H₁ H₂
Proof state after:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ k₁ : ℕ
H₂ : b = (k₁ + k₂) * I.b₁ + k₂ * I.b₂
H₁ : a = (k₁ + k₂) * I.a₁ + k₂ * I.a₂
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ k₁ : ℕ
H₂ : b = (k₁ + k₂) * I.b₁ + k₂ * I.b₂
H₁ : a = (k₁ + k₂) * I.a₁ + k₂ * I.a₂
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Tactic:
refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k, k₁' = k + k₂
Tactic:
rw [← le_iff_exists_add']
Proof state after:
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ k₂ ≤ k₁'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ k₂ ≤ k₁'
Tactic:
obtain ⟨_, h₂⟩ := h
Proof state after:
case intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ k₂ ≤ k₁'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ k₂ ≤ k₁'
Tactic:
simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] at h₂
Proof state after:
case intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  k₁' * I.a₁ * I.b₁ + k₂ * I.a₂ * I.b₁ + (k₁' * I.a₁ * I.b₂ + k₂ * I.a₂ * I.b₂) ≤
    k₁' * I.b₁ * I.a₁ + k₂ * I.b₂ * I.a₁ + (k₁' * I.b₁ * I.a₂ + k₂ * I.b₂ * I.a₂)
⊢ k₂ ≤ k₁'