internlm/Lean-Github huggingface dataset:
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd.inr.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
left✝ : ↑s₂ = -↑d
H₂ : t₂ ≤ d / 2
H₁ : s₂ ≤ d
⊢ s₂ + t₂ ≤ 2 * d
Tactic:
replace H₂ := H₂.trans <| Nat.div_le_self d 2
Proof state after:
case hbd.inr.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
left✝ : ↑s₂ = -↑d
H₁ : s₂ ≤ d
H₂ : t₂ ≤ d
⊢ s₂ + t₂ ≤ 2 * d
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd.inr.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
left✝ : ↑s₂ = -↑d
H₁ : s₂ ≤ d
H₂ : t₂ ≤ d
⊢ s₂ + t₂ ≤ 2 * d
Tactic:
linarith only [H₁, H₂]
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ 3 ∣ k₂
Tactic:
rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd]
Proof state after:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ ↑k₂ = 0
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ ↑k₂ = 0
Tactic:
have : k₂ + t₂ * s₁ = s₂ * t₁
Proof state after:
case this
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ k₂ + t₂ * s₁ = s₂ * t₁

case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
this : k₂ + t₂ * s₁ = s₂ * t₁
⊢ ↑k₂ = 0
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
this : k₂ + t₂ * s₁ = s₂ * t₁
⊢ ↑k₂ = 0
Tactic:
reduce_mod_3 this
Proof state after:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
this : ↑k₂ + ↑t₂ * ↑s₁ = ↑s₂ * ↑t₁
H₁✝ : 3 = 0
H₂✝ : 2 = -1
⊢ ↑k₂ = 0
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂'
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
this : ↑k₂ + ↑t₂ * ↑s₁ = ↑s₂ * ↑t₁
H₁✝ : 3 = 0
H₂✝ : 2 = -1
⊢ ↑k₂ = 0
Tactic:
simpa only [hs₁t₁mod3, hs₂t₂mod3, add_left_eq_self] using this
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case this
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ k₂ + t₂ * s₁ = s₂ * t₁
Tactic:
rw [hks₂, hkt₂, hs₁a₁, ht₁b₁, add_mul _ _ I.b₁, mul_assoc _ I.a₂, I.rel]
Proof state after:
case this
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ k₂ + (k₁ * I.b₁ + k₂ * I.b₂) * I.a₁ = k₁ * I.a₁ * I.b₁ + k₂ * (I.a₁ * I.b₂ + 1)
Theorem: Weight.condition_of_feasible
Proof state before:
case this
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
⊢ k₂ + (k₁ * I.b₁ + k₂ * I.b₂) * I.a₁ = k₁ * I.a₁ * I.b₁ + k₂ * (I.a₁ * I.b₂ + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
⊢ 3 ≤ k₂
Tactic:
refine Nat.le_of_dvd ((Nat.eq_zero_or_pos _).resolve_left ?_) hk₂'
Proof state after:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
⊢ ¬k₂ = 0
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
⊢ ¬k₂ = 0
Tactic:
rintro rfl
Proof state after:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hks₂ : s₂ = k₁ * I.a₁ + 0 * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + 0 * I.b₂
hk₂' : 3 ∣ 0
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hks₂ : s₂ = k₁ * I.a₁ + 0 * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + 0 * I.b₂
hk₂' : 3 ∣ 0
⊢ False
Tactic:
rw [hks₂, hkt₂, zero_mul, add_zero, zero_mul, add_zero, Nat.mul_right_comm] at hne₂
Proof state after:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ : ℕ
hne₂ : k₁ * I.b₁ * I.a₁ ≠ k₁ * I.b₁ * I.a₁
hbd : s₂ + t₂ ≤ 2 * d
hks₂ : s₂ = k₁ * I.a₁ + 0 * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + 0 * I.b₂
hk₂' : 3 ∣ 0
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₂
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ : ℕ
hne₂ : k₁ * I.b₁ * I.a₁ ≠ k₁ * I.b₁ * I.a₁
hbd : s₂ + t₂ ≤ 2 * d
hks₂ : s₂ = k₁ * I.a₁ + 0 * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + 0 * I.b₂
hk₂' : 3 ∣ 0
⊢ False
Tactic:
exact hne₂ rfl
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
⊢ 1 ≤ k₁
Tactic:
refine (Nat.eq_zero_or_pos k₁).resolve_left ?_
Proof state after:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
⊢ ¬k₁ = 0
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
⊢ ¬k₁ = 0
Tactic:
rintro rfl
Proof state after:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = 0 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 0 * I.b₁ + k₂ * I.b₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = 0 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 0 * I.b₁ + k₂ * I.b₂
⊢ False
Tactic:
simp only [zero_mul, zero_add] at hks₂ hkt₂
Proof state after:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = k₂ * I.a₂
hkt₂ : t₂ = k₂ * I.b₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = k₂ * I.a₂
hkt₂ : t₂ = k₂ * I.b₂
⊢ False
Tactic:
rw [hks₂, hkt₂] at hcop₂
Proof state after:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hcop₂ : Nat.Coprime (k₂ * I.a₂) (k₂ * I.b₂)
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = k₂ * I.a₂
hkt₂ : t₂ = k₂ * I.b₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case hk₁
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₂ : ℕ
hcop₂ : Nat.Coprime (k₂ * I.a₂) (k₂ * I.b₂)
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hks₂ : s₂ = k₂ * I.a₂
hkt₂ : t₂ = k₂ * I.b₂
⊢ False
Tactic:
linarith only [Nat.eq_one_of_coprime_mul_mul hcop₂, hk₂]
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
hd : ↑d ≠ 0
hs₁t₁mod3 : ↑s₁ = ↑t₁
hyp₁ : ↑s₁ = -↑d ∧ s₁ + t₁ ≤ d ∨ ↑s₁ = ↑d ∧ s₁ + t₁ ≤ d / 2
h' : s₁ + t₁ ≤ d
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₂t₂mod3 : ↑s₂ = ↑t₂
hyp₂ : ↑s₂ = ↑d ∧ s₂ ≤ d ∧ t₂ ≤ d ∨ ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
k₁ k₂ : ℕ
hks₂ : s₂ = k₁ * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = k₁ * I.b₁ + k₂ * I.b₂
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hk₁ : 1 ≤ k₁
⊢ k₁ = 1 ∨ 2 ≤ k₁
Tactic:
rwa [eq_comm, Nat.succ_le, ← le_iff_eq_or_lt]
Proof state after:
no goals