Theorem: Turanpartition.mod_tplus1 (Turan4/Turanpartition.lean)

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
⊢ a = b ∧ c = d
Tactic:
have mc : c % (t + 1) = c := mod_eq_of_lt (succ_le_succ hc )
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
⊢ a = b ∧ c = d
Tactic:
have md : d % (t + 1) = d := mod_eq_of_lt (succ_le_succ hd)
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Tactic:
rw [add_comm, add_comm _ d] at ht
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Tactic:
have hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1) := add_mul_mod_self_left c (t + 1) a
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
⊢ a = b ∧ c = d
Tactic:
have hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1) := add_mul_mod_self_left d (t + 1) b
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Tactic:
rw [mc,ht] at hmtl
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Tactic:
rw [md,hmtl] at hmtr
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b ∧ c = d

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b ∧ c = d
Tactic:
refine' ⟨_, hmtr⟩
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
rw [hmtr] at ht
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : d + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : d + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
rw [add_right_inj, mul_eq_mul_left_iff] at ht
State after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : a = b ∨ t + 1 = 0
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b

State before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : a = b ∨ t + 1 = 0
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
cases ht with
| inl h => exact h
| inr h => contradiction
State after:
no goals

State before:
case inl
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
h : a = b
⊢ a = b
Tactic:
exact h
State after:
no goals

State before:
case inr
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
h : t + 1 = 0
⊢ a = b
Tactic:
contradiction
State after:
no goals