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

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
hSge : mem_S_ge (3 * δ) ↑a ↑b
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨_, i₁, i₂, hi₀, hi₁, hi₂, hSge⟩ := hSge
State after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * (3 * δ) < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * (3 * δ) < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑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.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hi₁ := (mul_lt_mul_left (by norm_num)).mp hi₁
State after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hi₂ := (mul_le_mul_left (by norm_num)).mp hi₂
State after:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨x₁, Hx₁, Hx₁'⟩ : ∃ x : ℕ, (x : ℤ) = i₁ + i₂ - 2 * δ ∧ 0 < x:=
  ⟨i₁ + i₂ - 2 * δ, by have := hi₁.le; norm_cast, Nat.sub_pos_of_lt hi₁⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
obtain ⟨x₂, Hx₂⟩ : ∃ x : ℕ, (x : ℤ) = δ - i₂ := ⟨δ - i₂, by norm_cast⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hx₁ : x₁ ≤ δ := by linarith
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hx₂ : x₂ ≤ δ := by linarith
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
push_cast at hSge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
rw [(by rw [Hx₂]; ring : (a : ℤ) * (3 * i₂ - 3 * δ) = (-3) * (a * x₂)),
    (by rw [Hx₁]; ring : (b : ℤ) * (2 * (3 * δ) - 3 * i₁ - 3 * i₂) = (-3) * (b * x₁))] at hSge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
replace hSge := mul_left_cancel₀ (by norm_num) hSge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * ↑x₂ = ↑b * ↑x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
norm_cast at hSge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have ha : a ≤ x₁ := Nat.le_of_dvd Hx₁' <| hcop.dvd_of_dvd_mul_left <| Dvd.intro x₂ hSge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
have hb : b ≤ x₂
State after:
case hb
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ b ≤ x₂

case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
hb : b ≤ x₂
⊢ a ≤ δ ∧ b ≤ δ

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
hb : b ≤ x₂
⊢ a ≤ δ ∧ b ≤ δ
Tactic:
exact ⟨ha.trans hx₁, hb.trans hx₂⟩
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ
Tactic:
have := hi₁.le
State after:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
this : 2 * δ ≤ i₁ + i₂
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
this : 2 * δ ≤ i₁ + i₂
⊢ ↑(i₁ + i₂ - 2 * δ) = ↑i₁ + ↑i₂ - 2 * ↑δ
Tactic:
norm_cast
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
⊢ ↑(δ - i₂) = ↑δ - ↑i₂
Tactic:
norm_cast
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
⊢ x₁ ≤ δ
Tactic:
linarith
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ x₂ ≤ δ
Tactic:
linarith
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * ↑x₂)
Tactic:
rw [Hx₂]
State after:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * (↑δ - ↑i₂))

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : ↑a * (3 * ↑i₂ - 3 * ↑δ) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a * (3 * ↑i₂ - 3 * ↑δ) = -3 * (↑a * (↑δ - ↑i₂))
Tactic:
ring
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * ↑x₁)
Tactic:
rw [Hx₁]
State after:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * (↑i₁ + ↑i₂ - 2 * ↑δ))

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑b * (2 * (3 * ↑δ) - 3 * ↑i₁ - 3 * ↑i₂) = -3 * (↑b * (↑i₁ + ↑i₂ - 2 * ↑δ))
Tactic:
ring
State after:
no goals

State before:
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : -3 * (↑a * ↑x₂) = -3 * (↑b * ↑x₁)
⊢ -3 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case hb
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ b ≤ x₂
Tactic:
cases' eq_or_ne x₂ 0 with H H
State after:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ = 0
⊢ b ≤ x₂

case hb.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ ≠ 0
⊢ b ≤ x₂

State before:
case hb.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ ≠ 0
⊢ b ≤ x₂
Tactic:
exact Nat.le_of_dvd (Nat.pos_of_ne_zero H) <| hcop.symm.dvd_of_dvd_mul_left <|
        Dvd.intro x₁ hSge.symm
State after:
no goals

State before:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
hSge : a * x₂ = b * x₁
ha : a ≤ x₁
H : x₂ = 0
⊢ b ≤ x₂
Tactic:
simp only [H, mul_zero, zero_eq_mul] at hSge
State after:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hSge : b = 0 ∨ x₁ = 0
⊢ b ≤ x₂

State before:
case hb.inl
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hSge : b = 0 ∨ x₁ = 0
⊢ b ≤ x₂
Tactic:
rcases hSge with rfl | rfl
State after:
case hb.inl.inl
δ a : ℕ
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hcop : Nat.Coprime a 0
⊢ 0 ≤ x₂

case hb.inl.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₂ : x₂ ≤ δ
H : x₂ = 0
Hx₁ : ↑0 = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < 0
hx₁ : 0 ≤ δ
ha : a ≤ 0
⊢ b ≤ x₂

State before:
case hb.inl.inl
δ a : ℕ
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
hx₂ : x₂ ≤ δ
ha : a ≤ x₁
H : x₂ = 0
hcop : Nat.Coprime a 0
⊢ 0 ≤ x₂
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
case hb.inl.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₂ : x₂ ≤ δ
H : x₂ = 0
Hx₁ : ↑0 = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < 0
hx₁ : 0 ≤ δ
ha : a ≤ 0
⊢ b ≤ x₂
Tactic:
exact False.elim <| Nat.lt_irrefl _ Hx₁'
State after:
no goals