simpa only [H₂, ← hs₁a₁, one_mul, this, zero_mul, add_zero] using hks₂.symm
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
no goals