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

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

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

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, ?_⟩
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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, ?_⟩
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

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

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

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

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

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

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

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

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

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

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

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

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