internlm/Lean-Github huggingface dataset:
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
have hx : x₁ + x₂ ≤ d := by linarith
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
rw [(by rw [Hx₂] : (a : ℤ) * (3 * i₂ - d) = a * x₂),
    (by rw [Hx₁] : (b : ℤ) * (2 * d - 3 * i₁ - 3 * i₂) = b * x₁)] at hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
hSle : ↑a * ↑x₂ = ↑b * ↑x₁
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
hSle : ↑a * ↑x₂ = ↑b * ↑x₁
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
norm_cast at hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
hSle : a * x₂ = b * x₁
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
hSle : a * x₂ = b * x₁
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
obtain ⟨m, hm₁, hm₂⟩ :=  Nat.proportional_of_mul_eq_mul_of_coprime hSle hcop
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
hSle : a * x₂ = b * x₁
m : ℕ
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
hSle : a * x₂ = b * x₁
m : ℕ
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
rw [hm₁, hm₂, ← mul_add] at hx
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
have hm₀ : 0 < m :=
  (Nat.eq_zero_or_pos m).resolve_left (by rintro rfl; linarith only [Hx₂', hm₂])
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
rcases eq_or_eq_neg_in_zmod_3 hd hcop hab with had | had
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
⊢ ↑(2 * d - 3 * i₁ - 3 * i₂) = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
Tactic:
rw [Nat.sub_sub, Int.sub_sub]
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
⊢ ↑(2 * d - (3 * i₁ + 3 * i₂)) = 2 * ↑d - (3 * ↑i₁ + 3 * ↑i₂)
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
⊢ ↑(2 * d - (3 * i₁ + 3 * i₂)) = 2 * ↑d - (3 * ↑i₁ + 3 * ↑i₂)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
⊢ ↑(3 * i₂ - d) = 3 * ↑i₂ - ↑d
Tactic:
have := hi₂.le
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
this : d ≤ 3 * i₂
⊢ ↑(3 * i₂ - d) = 3 * ↑i₂ - ↑d
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
this : d ≤ 3 * i₂
⊢ ↑(3 * i₂ - d) = 3 * ↑i₂ - ↑d
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
⊢ x₁ + x₂ ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑a * (3 * ↑i₂ - ↑d) = ↑a * ↑x₂
Tactic:
rw [Hx₂]
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
hSle : ↑a * ↑x₂ = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ d
⊢ ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂) = ↑b * ↑x₁
Tactic:
rw [Hx₁]
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ¬m = 0
Tactic:
rintro rfl
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
hx : 0 * (a + b) ≤ d
hm₁ : x₁ = 0 * a
hm₂ : x₂ = 0 * b
⊢ False
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
hx : 0 * (a + b) ≤ d
hm₁ : x₁ = 0 * a
hm₂ : x₂ = 0 * b
⊢ False
Tactic:
linarith only [Hx₂', hm₂]
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
refine Or.inr ⟨had, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ a + b ≤ d / 2
Tactic:
have hm : 2 ≤ m
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ 2 ≤ m

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
hm : 2 ≤ m
⊢ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
hm : 2 ≤ m
⊢ a + b ≤ d / 2
Tactic:
have : (a + b : ℤ) * 2 ≤ d := by
  exact_mod_cast mul_comm 2 _ ▸ (Nat.mul_le_mul_right (a + b) hm).trans hx
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
hm : 2 ≤ m
this : (↑a + ↑b) * 2 ≤ ↑d
⊢ a + b ≤ d / 2
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
hm : 2 ≤ m
this : (↑a + ↑b) * 2 ≤ ↑d
⊢ a + b ≤ d / 2
Tactic:
exact Nat.le_div_two_iff_mul_two_le.mpr this
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ 2 ≤ m
Tactic:
by_contra! H
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
H : m < 2
⊢ False
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
H : m < 2
⊢ False
Tactic:
obtain rfl : m = 1 := by linarith
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
⊢ False
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
⊢ False
Tactic:
have hx₁' : (x₁ : ZMod 3) = -d := by reduce_mod_3 Hx₁
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : ↑x₁ = -↑d
⊢ False
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : ↑x₁ = -↑d
⊢ False
Tactic:
rw [hm₁, one_mul, had, eq_comm] at hx₁'
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : -↑d = ↑d
⊢ False
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : -↑d = ↑d
⊢ False
Tactic:
exact not_eq_neg_self hd hx₁'
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
H : m < 2
⊢ m = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
had : ↑a = ↑d
hx : 1 * (a + b) ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
⊢ ↑x₁ = -↑d
Tactic:
reduce_mod_3 Hx₁
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
hm : 2 ≤ m
⊢ (↑a + ↑b) * 2 ≤ ↑d
Tactic:
exact_mod_cast mul_comm 2 _ ▸ (Nat.mul_le_mul_right (a + b) hm).trans hx
Proof state after:
no goals
Theorem: Weight.add_le_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * d
hi₂ : d < 3 * i₂
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = 3 * ↑i₂ - ↑d
Hx₂' : 0 < x₂
hSle : a * x₂ = b * x₁
m : ℕ
hx : m * (a + b) ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
⊢ ↑a = -↑d ∧ a + b ≤ d ∨ ↑a = ↑d ∧ a + b ≤ d / 2
Tactic:
exact Or.inl ⟨had, (Nat.le_mul_of_pos_left _ hm₀).trans hx⟩
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
hSge : mem_S_ge (3 * δ) ↑a ↑b
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨_, i₁, i₂, hi₀, hi₁, hi₂, hSge⟩ := hSge
Proof state after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * (3 * δ) < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * (3 * δ) < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
rw [← mul_add, ← mul_assoc, mul_comm 2, mul_assoc] at hi₁
Proof state after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hi₁ := (mul_lt_mul_left (by norm_num)).mp hi₁
Proof state after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hi₂ := (mul_le_mul_left (by norm_num)).mp hi₂
Proof state after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ