Theorem: Weight.add_le_delta_of_mem_S_le (Weights/Dimension2.lean)

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
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 ≤ δ

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₁
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 ≤ δ

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₁
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 ≤ δ

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₂
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 ≤ δ

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⟩
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 ≤ δ

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₂⟩
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 ≤ δ

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
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 ≤ δ

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
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 ≤ δ

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
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 ≤ δ

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
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 ≤ δ

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
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 ≤ δ

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₁
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 ≤ δ

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
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 ≤ δ

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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₂)

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
State after:
no goals

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
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₂ - ↑δ

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
State after:
no goals

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
State after:
no goals

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₂]
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₂ - ↑δ))

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
State after:
no goals

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₁]
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₂))

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
State after:
no goals

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
State after:
no goals

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
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₁

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
State after:
no goals

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
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₁

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
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₁

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 _
State after:
no goals

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₂'
State after:
no goals