internlm/Lean-Github huggingface dataset:
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 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨x₁, Hx₁, Hx₁'⟩ : ∃ x : ℕ, (x : ℤ) = i₁ + i₂ - 2 * δ ∧ 0 < x:=
  ⟨i₁ + i₂ - 2 * δ, by have := hi₁.le; norm_cast, Nat.sub_pos_of_lt hi₁⟩
Proof state after:
case intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨x₂, Hx₂⟩ : ∃ x : ℕ, (x : ℤ) = δ - i₂ := ⟨δ - i₂, by norm_cast⟩
Proof state after:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hx₁ : x₁ ≤ δ := by linarith
Proof state after:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hx₂ : x₂ ≤ δ := by linarith
Proof state after:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
push_cast at hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
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.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
rw [(by rw [Hx₂]; ring : (a : ℤ) * (3 * i₂ - 3 * δ) = (-3) * (a * x₂)),
    (by rw [Hx₁]; ring : (b : ℤ) * (2 * (3 * δ) - 3 * i₁ - 3 * i₂) = (-3) * (b * x₁))] at hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hSge := mul_left_cancel₀ (by norm_num) hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
norm_cast at hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have ha : a ≤ x₁ := Nat.le_of_dvd Hx₁' <| hcop.dvd_of_dvd_mul_left <| Dvd.intro x₂ hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hb : b ≤ x₂
Proof state after:
case hb
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ b ≤ x₂

case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
hb : b ≤ x₂
⊢ a ≤ δ ∧ b ≤ δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
hb : b ≤ x₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
exact ⟨ha.trans hx₁, hb.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
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₂)
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂ ≤ δ
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ
Tactic:
have := hi₁.le
Proof state after:
δ 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₂ ≤ δ
this : 2 * δ ≤ i₁ + i₂
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂ ≤ δ
this : 2 * δ ≤ i₁ + i₂
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ ↑(δ - i₂) = ↑δ - ↑i₂
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ x₁ ≤ δ
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ 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₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ x₂ ≤ δ
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * ↑x₂)
Tactic:
rw [Hx₂]
Proof state after:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * (↑δ - ↑i₂))
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * (↑δ - ↑i₂))
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * ↑x₁)
Tactic:
rw [Hx₁]
Proof state after:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * (↑i₁ + ↑i₂ - 2 * ↑δ))
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * (↑i₁ + ↑i₂ - 2 * ↑δ))
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ -3 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ b ≤ x₂
Tactic:
cases' eq_or_ne x₂ 0 with H H
Proof state after:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ = 0
⊢ b ≤ x₂

case hb.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ ≠ 0
⊢ b ≤ x₂
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ ≠ 0
⊢ b ≤ x₂
Tactic:
exact Nat.le_of_dvd (Nat.pos_of_ne_zero H) <| hcop.symm.dvd_of_dvd_mul_left <|
        Dvd.intro x₁ hSge.symm
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ = 0
⊢ b ≤ x₂
Tactic:
simp only [H, mul_zero, zero_eq_mul] at hSge
Proof state after:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hSge : b = 0 ∨ x₁ = 0
⊢ b ≤ x₂
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hSge : b = 0 ∨ x₁ = 0
⊢ b ≤ x₂
Tactic:
rcases hSge with rfl | rfl
Proof state after:
case hb.inl.inl
δ a : ℕ
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hcop : Nat.Coprime a 0
⊢ 0 ≤ x₂

case hb.inl.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₂ : x₂ ≤ δ
H : x₂ = 0
Hx₁ : ↑0 = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < 0
hx₁ : 0 ≤ δ
ha : a ≤ 0
⊢ b ≤ x₂
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb.inl.inl
δ a : ℕ
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hcop : Nat.Coprime a 0
⊢ 0 ≤ x₂
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Weight.le_delta_of_mem_S_ge
Proof state before:
case hb.inl.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₂ : x₂ ≤ δ
H : x₂ = 0
Hx₁ : ↑0 = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < 0
hx₁ : 0 ≤ δ
ha : a ≤ 0
⊢ b ≤ x₂
Tactic:
exact False.elim <| Nat.lt_irrefl _ Hx₁'
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
hSge : mem_S_ge d ↑a ↑b
⊢ ↑a = ↑b ∧ (↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2)
Tactic:
obtain ⟨_, i₁, i₂, hi₀, hi₁, hi₂, hSge⟩ := hSge
Proof state after:
case 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
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a = ↑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
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₂)
⊢ ↑a = ↑b ∧ (↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2)
Tactic:
have hab := eq_mod_3_of_rel hd hSge
Proof state after:
case 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
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑b
⊢ ↑a = ↑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
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
⊢ ↑a = ↑b ∧ (↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2)
Tactic:
refine ⟨hab, ?_⟩
Proof state after:
case 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
hSge : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
hab : ↑a = ↑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
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
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
obtain ⟨x₁, Hx₁, Hx₁'⟩ : ∃ x : ℕ, (x : ℤ) = 3 * i₁ + 3 * i₂ - 2 * d ∧ 0 < x :=
  ⟨3 * i₁ + 3 * i₂ - 2 * d, by have := hi₁.le; norm_cast, Nat.sub_pos_of_lt hi₁⟩
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 < ↑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₁
⊢ ↑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
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₁
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
obtain ⟨x₂, Hx₂⟩ : ∃ x : ℕ, (x : ℤ) = d - 3 * i₂ := ⟨d - 3 * i₂, by norm_cast⟩
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
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₂
⊢ ↑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
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₂
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
have hx₁ : x₁ ≤ d := by linarith
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
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
⊢ ↑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
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
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2
Tactic:
have hx₂ : x₂ ≤ d := by linarith
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
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
hx₂ : x₂ ≤ d
⊢ ↑a = ↑d ∧ a ≤ d ∧ b ≤ d ∨ ↑a = -↑d ∧ a ≤ d / 2 ∧ b ≤ d / 2