internlm/Lean-Github huggingface dataset:
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
rw [(by rw [Hx₂]; ring : -((a : ℤ) * (3 * i₂ - d)) = a * x₂),
    (by rw [Hx₁]; ring : -((b : ℤ) * (2 * d - 3 * i₁ - 3 * i₂)) = b * x₁)] at hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
norm_cast at hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
obtain ⟨m, hm₁, hm₂⟩ := Nat.proportional_of_mul_eq_mul_of_coprime hSge hcop
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
m : ℕ
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
m : ℕ
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
rw [hm₁] at hx₁
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
m : ℕ
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₂ : x₂ ≤ d
hSge : a * x₂ = b * x₁
m : ℕ
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
rw [hm₂] at hx₂
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ 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.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ 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.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
⊢ ↑(3 * i₁ + 3 * i₂ - 2 * d) = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Tactic:
have := hi₁.le
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
this : 2 * d ≤ 3 * i₁ + 3 * i₂
⊢ ↑(3 * i₁ + 3 * i₂ - 2 * d) = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
this : 2 * d ≤ 3 * i₁ + 3 * i₂
⊢ ↑(3 * i₁ + 3 * i₂ - 2 * d) = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
⊢ ↑(d - 3 * i₂) = ↑d - 3 * ↑i₂
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
⊢ x₁ ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
⊢ x₂ ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑a * (3 * ↑i₂ - ↑d)) = ↑a * ↑x₂
Tactic:
rw [Hx₂]
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑a * (3 * ↑i₂ - ↑d)) = ↑a * (↑d - 3 * ↑i₂)
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑a * (3 * ↑i₂ - ↑d)) = ↑a * (↑d - 3 * ↑i₂)
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : ↑a * ↑x₂ = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)) = ↑b * ↑x₁
Tactic:
rw [Hx₁]
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : ↑a * ↑x₂ = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)) = ↑b * (3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d)
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : ↑a * ↑x₂ = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)) = ↑b * (3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d)
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ 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 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
hx₂ : 0 * b ≤ d
hx₁ : 0 * a ≤ d
hm₁ : x₁ = 0 * a
hm₂ : x₂ = 0 * b
⊢ False
Theorem: Weight.le_of_mem_S_ge
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
hx₂ : 0 * b ≤ d
hx₁ : 0 * a ≤ d
hm₁ : x₁ = 0 * a
hm₂ : x₂ = 0 * b
⊢ False
Tactic:
linarith only [Hx₁', hm₁]
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
exact Or.inl ⟨had, (Nat.le_mul_of_pos_left _ hm₀).trans hx₁,
                   (Nat.le_mul_of_pos_left _ hm₀).trans hx₂⟩
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ 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 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ 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.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
have Ha : (a : ℤ) * 2 ≤ d
Proof state after:
case Ha
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
⊢ ↑a * 2 ≤ ↑d

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
Ha : ↑a * 2 ≤ ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
Ha : ↑a * 2 ≤ ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
have Hb : (b : ℤ) * 2 ≤ d
Proof state after:
case Hb
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
Ha : ↑a * 2 ≤ ↑d
⊢ ↑b * 2 ≤ ↑d

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
Ha : ↑a * 2 ≤ ↑d
Hb : ↑b * 2 ≤ ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
hm : 2 ≤ m
Ha : ↑a * 2 ≤ ↑d
Hb : ↑b * 2 ≤ ↑d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
exact Or.inr ⟨had, Nat.le_div_two_iff_mul_two_le.mpr Ha, Nat.le_div_two_iff_mul_two_le.mpr Hb⟩
Proof state after:
no goals
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ 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 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ d
hm₁ : x₁ = m * a
hm₂ : x₂ = m * b
hm₀ : 0 < m
had : ↑a = -↑d
H : m < 2
⊢ False
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
m : ℕ
hx₂ : m * b ≤ d
hx₁ : m * a ≤ 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 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
⊢ False
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ 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 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : ↑x₁ = ↑d
⊢ False
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ 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] at hx₁'
Proof state after:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ d
hm₁ : x₁ = 1 * a
hm₂ : x₂ = 1 * b
hm₀ : 0 < 1
H : 1 < 2
hx₁' : -↑d = ↑d
⊢ False
Theorem: Weight.le_of_mem_S_ge
Proof state before:
case hm
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hSge : a * x₂ = b * x₁
had : ↑a = -↑d
hx₂ : 1 * b ≤ d
hx₁ : 1 * a ≤ 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