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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
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 < ↑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
⊢ ↑x₁ = ↑d
Tactic:
reduce_mod_3 Hx₁
State after:
no goals

State before:
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
Tactic:
exact_mod_cast mul_comm 2 a ▸ (Nat.mul_le_mul_right a hm).trans hx₁
State after:
no goals

State before:
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
Tactic:
exact_mod_cast mul_comm 2 b ▸ (Nat.mul_le_mul_right b hm).trans hx₂
State after:
no goals