dyadic_property

lemma dyadic_property {l : ℤ} (hl : -S ≤ l) {k : ℤ} (hl_k : l ≤ k) :    (hk : -S ≤ k) → ∀ (y : Yk X k), ∀ (y' : Yk X l),    ¬ Disjoint (I3 hl y') (I3 hk y) → I3 hl y' ⊆ I3 hk y := by  simp_rw [not_disjoint_iff, forall_exists_index, and_imp]  intro hk y y' x hxl hxk  by_cases hk_l : k = l  · subst hk_l    apply Eq.le (congr_heq _ _)    · congr    simp only [heq_eq_eq]    exact I3_prop_1 hk (And.intro hxl hxk)  · have : l < k := lt_of_le_of_ne hl_k fun a ↦ hk_l (id a.symm)    have hk_not_neg_s : ¬ k = -S := by linarith    have : x ∈ ⋃ (y'' : Yk X (k - 1)), I3 (I_induction_proof hk hk_not_neg_s) y'' :=      cover_by_cubes (I_induction_proof hk hk_not_neg_s) (by linarith) hk y hxk    simp only [mem_iUnion] at this    obtain ⟨y'', hy''⟩ := this    have : l + (-l + (k - 1)).toNat < k := by      rw [Int.toNat_of_nonneg (by linarith)]      linarith    have : I3 hl y' ⊆ I3 (I_induction_proof hk hk_not_neg_s) y'' := by      apply dyadic_property hl (by linarith) (I_induction_proof hk hk_not_neg_s)      rw [not_disjoint_iff]      use x    apply this.trans    by_cases hx_mem_Xk : x ∈ Xk hk    · have hx_i1: x ∈ I1 hk y := by        rw [I3] at hxk        push _ ∈ _ at hxk        simp only [not_or, not_exists] at hxk        rw [not_iff_false_intro hx_mem_Xk,false_and,and_false,or_false] at hxk        exact hxk      rw [I1] at hx_i1      rw [dif_neg hk_not_neg_s] at hx_i1      push _ ∈ _ at hx_i1      obtain ⟨u, hu, hu'⟩ := hx_i1      have hxy'' : x ∈ I3 _ y'' := this hxl      have : y'' = u := by        apply I3_prop_1        use hxy''      subst this      apply Subset.trans _ (I1_subset_I3 _ _)      rw [I1,dif_neg hk_not_neg_s]      intro x' hx'      push _ ∈ _      use y''    · have hx_notMem_i1 (y_1 : Yk X k) : x ∉ I1 hk y_1 := by        rw [Xk] at hx_mem_Xk        simp only [mem_iUnion, not_exists] at hx_mem_Xk        exact hx_mem_Xk y_1      have hx_mem_i2_and : x ∈ I2 hk y ∧ ∀ u < y, x ∉ I3 hk u:= by        rw [I3] at hxk        push _ ∈ _ at hxk        simp only [not_or, not_exists] at hxk        rw [iff_false_intro (hx_notMem_i1 y), iff_true_intro hx_mem_Xk, false_or, true_and] at hxk        exact hxk      have hx_mem_i2 := hx_mem_i2_and.left      have hx_notMem_i3_u := hx_mem_i2_and.right      have hx_notMem_i2_u: ∀ u < y, x ∉ I2 hk u := by        intro u hu        specialize hx_notMem_i3_u u hu        rw [I3] at hx_notMem_i3_u        push _ ∈ _ at hx_notMem_i3_u        -- xxx: can push_neg help here?        simp only [not_or, not_exists, not_and, not_forall, not_not] at hx_notMem_i3_u        rw [iff_true_intro (hx_notMem_i1 u),iff_true_intro hx_mem_Xk] at hx_notMem_i3_u        rw [true_and,true_implies] at hx_notMem_i3_u        intro h        obtain ⟨v, hv, hv'⟩ := hx_notMem_i3_u h        exact hx_mem_i2_and.right v (hv.trans hu) hv'      rw [I2, dif_neg hk_not_neg_s] at hx_mem_i2      push _ ∈ _ at hx_mem_i2      obtain ⟨u, hu, hxu⟩ := hx_mem_i2      obtain rfl : y'' = u := by        apply I3_prop_1 (I_induction_proof hk hk_not_neg_s)        use hy''      have : I3 (I_induction_proof hk hk_not_neg_s) y'' ∩ Xk hk = ∅ := by        ext x'        push _ ∈ _; simp only [iff_false, not_and]        intro hx_i3' hx_xk'        apply hx_mem_Xk        rw [Xk] at hx_xk' ⊢        simp only [mem_iUnion] at hx_xk' ⊢        obtain ⟨u, hu⟩ := hx_xk'        use u        rw [I1,dif_neg hk_not_neg_s] at hu ⊢        push _ ∈ _ at hu ⊢        obtain ⟨u', hu', hu''⟩ := hu        use u', hu'        obtain rfl : u' = y'' := I3_prop_1 (I_induction_proof hk hk_not_neg_s) (And.intro hu'' hx_i3')        exact hxu      intro x' hx'      rw [I3]      have hx_not_xk : x' ∉ Xk hk := by        intro hcontra        have : x' ∈ (∅ : Set X) := by          rw [← this]          exact mem_inter hx' hcontra        exact this      push _ ∈ _      simp only [exists_prop, not_or, not_exists, not_and, iff_true_intro hx_not_xk, true_and]      right      constructor      · rw [I2, dif_neg hk_not_neg_s]        push _ ∈ _        use y''      intro u hu      have hx_not_i1' : x' ∉ I1 hk u := by        intro hx_i1'        apply hx_not_xk        rw [Xk]        simp only [mem_iUnion]        use u      rw [I3]      push _ ∈ _      simp only [exists_prop, not_or, not_exists, not_and, not_forall]      rw [iff_true_intro hx_not_xk, iff_true_intro hx_not_i1', true_and, true_implies]      intro hx_i2'      by_contra      apply hx_notMem_i2_u u hu      rw [I2, dif_neg hk_not_neg_s] at hx_i2' ⊢      push _ ∈ _ at hx_i2' ⊢      obtain ⟨z,hz,hz'⟩ := hx_i2'      use z, hz      suffices z = y'' by        subst this        exact hy''      apply I3_prop_1 (I_induction_proof hk hk_not_neg_s)      exact mem_inter hz' hx'  termination_by ((-l + k).toNat)