internlm/Lean-Github huggingface dataset:
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
⊢ ↑a = ↑d ∨ ↑a = -↑d
Tactic:
by_contra! H
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ False
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ False
Tactic:
have help : ∀ {a d : ZMod 3}, -d ≠ d → (a ≠ d ∧ a ≠ -d) → a = 0 := by decide
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
⊢ False
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
⊢ False
Tactic:
have ha₀ := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a 3).mp <| help hdd H
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
⊢ False
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
⊢ False
Tactic:
have hb₀ := (ZMod.nat_cast_zmod_eq_zero_iff_dvd b 3).mp <| (help hdd H ▸ hab).symm
Proof state after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
hb₀ : 3 ∣ b
⊢ False
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
hb₀ : 3 ∣ b
⊢ False
Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨3, Nat.prime_three, ha₀, hb₀⟩ hcop
Proof state after:
no goals
Theorem: Weight.eq_or_eq_neg_in_zmod_3
Proof state before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
Tactic:
decide
Proof state after:
no goals
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
δ a b : ℕ
hcop : Nat.Coprime a b
hSle : mem_S_le (3 * δ) ↑a ↑b
⊢ a + b ≤ δ
Tactic:
obtain ⟨_, i₁, i₂, hi₁, hi₂, hSle⟩ := hSle
Proof state after:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * (3 * δ)
hi₂ : 3 * δ < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * i₁ + 3 * i₂ ≤ 2 * (3 * δ)
hi₂ : 3 * δ < 3 * i₂
hSle : ↑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
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * (i₁ + i₂) ≤ 3 * (2 * δ)
hi₂ : 3 * δ < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : 3 * (i₁ + i₂) ≤ 3 * (2 * δ)
hi₂ : 3 * δ < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a + b ≤ δ
Tactic:
replace hi₁ := (mul_le_mul_left (by norm_num)).mp hi₁
Proof state after:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₂ : 3 * δ < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₂ : 3 * δ < 3 * i₂
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
⊢ a + b ≤ δ
Tactic:
replace hi₂ := (mul_lt_mul_left (by norm_num)).mp hi₂
Proof state after:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
⊢ a + b ≤ δ
Tactic:
obtain ⟨x₁, Hx₁⟩ : ∃ x : ℕ, (x : ℤ) = 2 * δ - i₁ - i₂ :=
  ⟨2 * δ - i₁ -i₂, by rw [Nat.sub_sub, Int.sub_sub]; norm_cast⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
⊢ a + b ≤ δ
Tactic:
obtain ⟨x₂, Hx₂, Hx₂'⟩ : ∃ x : ℕ, (x : ℤ) = i₂ - δ ∧ 0 < x :=
  ⟨i₂ - δ, 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 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
⊢ a + b ≤ δ
Tactic:
have hx : x₁ + x₂ ≤ δ := by linarith
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
⊢ a + b ≤ δ
Tactic:
push_cast at hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : ↑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 hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : 3 * (↑a * ↑x₂) = 3 * (↑b * ↑x₁)
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : 3 * (↑a * ↑x₂) = 3 * (↑b * ↑x₁)
⊢ a + b ≤ δ
Tactic:
replace hSle := mul_left_cancel₀ (by norm_num) hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a + b ≤ δ
Tactic:
norm_cast at hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
⊢ a + b ≤ δ
Theorem: Weight.add_le_delta_of_mem_S_le
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
⊢ a + b ≤ δ
Tactic:
have ha : a ≤ x₁
Proof state after:
case ha
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
⊢ a ≤ x₁

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

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

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