Lean4
theorem isProperSemilinearSet [IsCancelAdd M] (hs : IsLinearSet s) : IsProperSemilinearSet s := by
classical
rw [isLinearSet_iff] at hs
rcases hs with ⟨a, t, rfl⟩
induction hn : t.card using Nat.strong_induction_on generalizing a t with
| _ n ih
subst hn
by_cases hindep : LinearIndepOn ℕ id (t : Set M)
· exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
rw [not_linearIndepOn_finset_iffₒₛ] at hindep
rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
simp only [Function.id_def] at heq
convert_to
IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
· ext x
simp only [mem_vadd_set, SetLike.mem_coe]
constructor
· rintro ⟨y, hy, rfl⟩
rw [mem_closure_finset] at hy
rcases hy with ⟨g, -, rfl⟩
induction hn : g i using Nat.strong_induction_on generalizing g with
| _ n ih'
subst hn
by_cases hfg : ∀ j ∈ t', f j ≤ g j
· convert
ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi)) (fun j => if j ∈ t' then g j - f j else g j + f j)
(by simp [hi]) using
1
conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm, ite_smul,
Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht', Finset.filter_notMem_eq_sdiff,
add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc, add_right_comm, ← Finset.sum_add_distrib]
congr! 2 with j hj
rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
· push_neg at hfg
rcases hfg with ⟨j, hj, hgj⟩
simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
refine
⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k, sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
· simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
rintro ⟨j, hj, k, hk, y, hy, rfl⟩
refine ⟨k • j + y, add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _) ((closure_mono (t.erase_subset j)) hy), ?_⟩
rw [add_assoc]
·
exact
.biUnion_finset fun j hj =>
.biUnion_finset fun k hk => ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl
