internlm/Lean-Github huggingface dataset:
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
⊢ 1 * I.b₁ + 3 * I.b₂ ≤ 1 * I.b₁ + k₂ * I.b₂
Tactic:
gcongr
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
⊢ d < s₂ + t₂
Tactic:
linarith
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
⊢ d / 2 + d / 2 ≤ d
Tactic:
rw [← two_mul]
Proof state after:
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
⊢ 2 * (d / 2) ≤ d
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
⊢ 2 * (d / 2) ≤ d
Tactic:
exact Nat.mul_div_le d 2
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
x✝ : ↑s₂ = -↑d ∧ s₂ ≤ d / 2 ∧ t₂ ≤ d / 2
⊢ s₂ + t₂ ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case H₃
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
⊢ ↑s₁ = ↑d
Tactic:
have : (k₂ : ZMod 3) = 0 := (ZMod.nat_cast_zmod_eq_zero_iff_dvd k₂ 3).mpr hk₂'
Proof state after:
case H₃
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
this : ↑k₂ = 0
⊢ ↑s₁ = ↑d
Theorem: Weight.condition_of_feasible
Proof state before:
case H₃
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
this : ↑k₂ = 0
⊢ ↑s₁ = ↑d
Tactic:
reduce_mod_3 hks₂
Proof state after:
case H₃
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
this : ↑k₂ = 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
hks₂ : ↑s₂ = ↑I.a₁ + ↑k₂ * ↑I.a₂
⊢ ↑s₁ = ↑d
Theorem: Weight.condition_of_feasible
Proof state before:
case H₃
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
this : ↑k₂ = 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
hks₂ : ↑s₂ = ↑I.a₁ + ↑k₂ * ↑I.a₂
⊢ ↑s₁ = ↑d
Tactic:
simpa only [H₂, ← hs₁a₁, one_mul, this, zero_mul, add_zero] using hks₂.symm
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case H₄
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
⊢ 2 * (I.a₁ + I.b₁) ≤ d
Tactic:
rw [← hs₁a₁, ← ht₁b₁]
Proof state after:
case H₄
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
⊢ 2 * (s₁ + t₁) ≤ d
Theorem: Weight.condition_of_feasible
Proof state before:
case H₄
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
⊢ 2 * (s₁ + t₁) ≤ d
Tactic:
rcases hyp₁ with ⟨hmod, _⟩ | ⟨_, hle⟩
Proof state after:
case H₄.inl.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
⊢ 2 * (s₁ + t₁) ≤ d

case H₄.inr.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ left✝ : ↑s₁ = ↑d
hle : s₁ + t₁ ≤ d / 2
⊢ 2 * (s₁ + t₁) ≤ d
Theorem: Weight.condition_of_feasible
Proof state before:
case H₄.inl.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
⊢ 2 * (s₁ + t₁) ≤ d
Tactic:
have hch : ringChar (ZMod 3) ≠ 2 := by rw [ZMod.ringChar_zmod_n]; norm_num
Proof state after:
case H₄.inl.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
hch : ringChar (ZMod 3) ≠ 2
⊢ 2 * (s₁ + t₁) ≤ d
Theorem: Weight.condition_of_feasible
Proof state before:
case H₄.inl.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
hch : ringChar (ZMod 3) ≠ 2
⊢ 2 * (s₁ + t₁) ≤ d
Tactic:
exact False.elim <| hd <|
        (Ring.eq_self_iff_eq_zero_of_char_ne_two hch).mp (H₃ ▸ hmod).symm
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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
⊢ ringChar (ZMod 3) ≠ 2
Tactic:
rw [ZMod.ringChar_zmod_n]
Proof state after:
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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
⊢ 3 ≠ 2
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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
hmod : ↑s₁ = -↑d
right✝ : s₁ + t₁ ≤ d
⊢ 3 ≠ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case H₄.inr.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₁
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₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ left✝ : ↑s₁ = ↑d
hle : s₁ + t₁ ≤ d / 2
⊢ 2 * (s₁ + t₁) ≤ d
Tactic:
exact (Nat.mul_le_mul_left 2 hle).trans <| Nat.mul_div_le d 2
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
H₄ : 2 * (I.a₁ + I.b₁) ≤ d
⊢ d < 2 * (I.a₂ + I.b₂)
Tactic:
calc
  d = 2 * d - d                 := by rw [Nat.two_mul, Nat.add_sub_cancel]
  _ ≤ 2 * d - 2 * (I.a₁ + I.b₁) := Nat.sub_le_sub_left H₄ _
  _ < 2 * (I.a₂ + I.b₂)         :=
        Nat.sub_lt_left_of_lt_add (H₄.trans <| Nat.le_mul_of_pos_left _ (zero_lt_two))
                                  (by linarith)
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
H₄ : 2 * (I.a₁ + I.b₁) ≤ d
⊢ d = 2 * d - d
Tactic:
rw [Nat.two_mul, Nat.add_sub_cancel]
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₂ : ℕ
hbd : s₂ + t₂ ≤ 2 * d
hk₂' : 3 ∣ k₂
hk₂ : 3 ≤ k₂
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hks₂ : s₂ = 1 * I.a₁ + k₂ * I.a₂
hkt₂ : t₂ = 1 * I.b₁ + k₂ * I.b₂
hk₁ : 1 ≤ 1
hs₂bd : 1 * I.a₁ + 3 * I.a₂ ≤ s₂
ht₂bd : 1 * I.b₁ + 3 * I.b₂ ≤ t₂
H₁ : d < s₂ + t₂
Hd : d / 2 + d / 2 ≤ d
H₂ : ↑s₂ = ↑d
H₃ : ↑s₁ = ↑d
H₄ : 2 * (I.a₁ + I.b₁) ≤ d
⊢ 2 * d < 2 * (I.a₁ + I.b₁) + 2 * (I.a₂ + I.b₂)
Tactic:
linarith
Proof state after:
no goals