internlm/Lean-Github huggingface dataset:
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
⊢ False
Tactic:
have : k₁ = 1 ∨ 2 ≤ k₁ := by rwa [eq_comm, Nat.succ_le, ← le_iff_eq_or_lt]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
⊢ False
Tactic:
have hI₂ := hI.2.2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
⊢ False
Tactic:
have hbd' : 2 * d < s₂ + t₂
Proof state after:
case hbd'
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
⊢ 2 * d < s₂ + t₂

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hbd' : 2 * d < s₂ + t₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.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₂
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₁
this : k₁ = 1 ∨ 2 ≤ k₁
hI₂ : d < I.a₁ + I.a₂ + I.b₁ + I.b₂
hbd' : 2 * d < s₂ + t₂
⊢ False
Tactic:
exact lt_irrefl _ <| hbd'.trans_le hbd
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
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
⊢ False
Tactic:
obtain ⟨δ, rfl⟩ := (ZMod.nat_cast_zmod_eq_zero_iff_dvd d 3).mp hd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
⊢ False
Tactic:
have hs₁t₁ := add_le_delta_of_mem_S_le hcop₁ hSle
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
⊢ False
Tactic:
obtain ⟨hs₁a₁, ht₁b₁⟩ := eq_left_of_add_le hI hcop₁ hmem₁ (by linarith) hne₁
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
⊢ False
Tactic:
obtain ⟨hs₁, ht₂⟩ := le_delta_of_mem_S_ge hcop₂ hSge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
⊢ False
Tactic:
obtain ⟨hs₂a₂, ht₂b₂⟩ := eq_right_of_add_le hI hcop₂ hmem₂ (by linarith) hne₂
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ False
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ False
Tactic:
refine False.elim <| Nat.lt_irrefl (3 * δ) ?_
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ 3 * δ < 3 * δ
Theorem: Weight.condition_of_feasible
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.intro
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ 3 * δ < 3 * δ
Tactic:
calc
  3 * δ < I.a₁ + I.a₂ + I.b₁ + I.b₂     := hI.2.2
  _     = (I.a₁ + I.b₁) + (I.a₂ + I.b₂) := by abel
  _     = (s₁ + t₁) + (s₂ + t₂)         := by symm; congr
  _     ≤ δ + (δ + δ)                   := by gcongr
  _     = _                             := by ring
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
⊢ s₁ + t₁ ≤ 3 * δ
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
⊢ s₂ + t₂ ≤ 3 * δ
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ I.a₁ + I.a₂ + I.b₁ + I.b₂ = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
Tactic:
abel
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ I.a₁ + I.b₁ + (I.a₂ + I.b₂) = s₁ + t₁ + (s₂ + t₂)
Tactic:
symm
Proof state after:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ s₁ + t₁ + (s₂ + t₂) = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ s₁ + t₁ + (s₂ + t₂) = I.a₁ + I.b₁ + (I.a₂ + I.b₂)
Tactic:
congr
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ s₁ + t₁ + (s₂ + t₂) ≤ δ + (δ + δ)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
I : BasicInterval
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
δ : ℕ
inst✝ : NeZero (3 * δ)
hI : feasible (3 * δ) I
hSle : mem_S_le (3 * δ) ↑s₁ ↑t₁
hSge : mem_S_ge (3 * δ) ↑s₂ ↑t₂
hd : ↑(3 * δ) = 0
hs₁t₁ : s₁ + t₁ ≤ δ
hs₁a₁ : s₁ = I.a₁
ht₁b₁ : t₁ = I.b₁
hs₁ : s₂ ≤ δ
ht₂ : t₂ ≤ δ
hs₂a₂ : s₂ = I.a₂
ht₂b₂ : t₂ = I.b₂
⊢ δ + (δ + δ) = 3 * δ
Tactic:
ring
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
⊢ s₁ + t₁ ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd
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₂
⊢ s₂ + t₂ ≤ 2 * d
Tactic:
rcases hyp₂ with ⟨_, H₁, H₂⟩ | ⟨_, H₁, H₂⟩
Proof state after:
case hbd.inl.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

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 / 2
H₂ : t₂ ≤ d / 2
⊢ s₂ + t₂ ≤ 2 * d
Theorem: Weight.condition_of_feasible
Proof state before:
case hbd.inl.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 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 / 2
H₂ : t₂ ≤ d / 2
⊢ 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₂ : t₂ ≤ d / 2
H₁ : s₂ ≤ d
⊢ s₂ + t₂ ≤ 2 * d