Combine theorem

theorem combine_theorem  {φ : ι ↪ F} {dstar m : ℕ}  (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ i, degs i ≤ dstar)  (δ : ℝ≥0) (hδPos : δ > 0)  (hδLt : δ < (min (1 - (ReedSolomon.sqrtRate dstar φ))                   (1 - (rate (code φ dstar)) - 1 / Fintype.card ι)))  (hProb : Pr_{ let r ← $ᵖ F}[δᵣ((combine φ dstar r fs degs), (code φ dstar)) ≤ δ] >    (m * (dstar + 1) - ∑ i, degs i - 1) * ProximityGap.errorBound δ dstar φ) :    ∃ S : Finset ι, S.card ≥ (1 - δ) * (Fintype.card ι) ∧      ∃ v : Fin m → ι → F, ∀ i,        v i ∈ (code φ (degs i)) ∧          S ⊆ Finset.filter (fun j => v i j = fs i j) Finset.univ    := by  by_cases hempty : Fintype.card ι = 0  · exists ∅    simp only [card_empty, CharP.cast_eq_zero, hempty, mul_zero, ge_iff_le, Std.le_refl,      empty_subset, and_true, true_and]    rw [Fintype.card_eq_zero_iff] at hempty    exists (fun i j => False.elim <| hempty.1 j)    intro i    simp only [code, Submodule.mem_map]    exists 0    simp only [zero_mem, map_zero, true_and]    ext j    exact (False.elim <| hempty.1 j)  · generalize htotal: total_terms dstar degs = total    rw [Fintype.card_eq_zero_iff, not_isEmpty_iff] at hempty    rcases total with _ | total    · rcases m with _ | m      · aesop          (add simp [total_terms, block_size])          (add safe (by exists Finset.univ))      · aesop (add simp [total_terms, block_size])    · have proximity_gap :=        @ProximityGap.correlatedAgreement_affine_curves ι _ _ F _ _ _          (total_terms dstar degs - 1) dstar φ δ (le_of_lt <| by            aesop (add simp [lt_min_iff, ReedSolomon.sqrtRate]))      simp only [ProximityGap.δ_ε_correlatedAgreementCurves] at proximity_gap      specialize proximity_gap          (fun l (x : ι) ↦ (            let i : WithBot (Fin m) :=              Finset.max (univ.filter (block_start dstar degs · ≤ l))            i.elim (0 : F) fun i ↦              let k := l - block_start dstar degs i              fs i x * (φ x) ^ k          ))          (by {            simp only [bind_pure_comp, Functor.map, PMF.bind_apply,              PMF.uniformOfFintype_apply,              tsum_fintype, Function.comp_apply, PMF.pure_apply,              eq_iff_iff, true_iff, mul_ite, mul_one,              mul_zero, gt_iff_lt] at hProb            conv at hProb =>              rhs              rhs              ext x              rw [combine_eq_flat_final φ dstar x]            simp only [bind_pure_comp, Functor.map, PMF.bind_apply,              PMF.uniformOfFintype_apply,              tsum_fintype, Function.comp_apply, PMF.pure_apply,              eq_iff_iff, true_iff, mul_ite, mul_one,              mul_zero, gt_iff_lt]            apply lt_of_le_of_lt              (b := ((↑m : ENNReal) * (↑dstar + 1) - ↑(∑ i, degs i) - 1) *                      ↑(ProximityGap.errorBound δ dstar φ))            · apply mul_le_mul_left              rw [htotal, add_tsub_cancel_right,                  Nat.cast_sum, mul_add, mul_one,                  show (↑m : ENNReal) * ↑dstar                    = ∑ x : Fin m, ↑dstar by simp,                  show (↑m : ENNReal) = ∑ x : Fin m, 1 by simp,                  ←Finset.sum_add_distrib,                  show ∑ x : Fin m, ((↑dstar : ENNReal) + 1) - ∑ x, ↑(degs x)                    = ↑(∑ x : Fin m, (dstar + 1)) - ↑(∑ x, degs x)                      by simp; ring_nf,                  ←ENNReal.natCast_sub,                  ←Finset.sum_tsub_distrib _ (fun x _ ↦                    le_trans (hdegs x) (by omega))]              conv =>                rhs                lhs                rhs                rhs                ext x                rw [Nat.sub_add_comm (hdegs x)]              rw [show ∑ x, (dstar - degs x + 1) = total + 1 by                aesop (add simp [total_terms, block_size])]              simp            · exact lt_of_lt_of_le hProb <| le_of_eq <| by                congr                ext x                congr <;> try (rw [htotal]; omega)                refine (Fin.heq_fun_iff ?_).mpr ?_                · aesop (add safe (by omega))                · aesop      })      simp only [jointAgreement, ge_iff_le, SetLike.mem_coe] at proximity_gap      have proximity_gap :        ∃ S : Finset ι,          ↑(#S) ≥ (1 - δ) * ↑(Fintype.card ι)            ∧ ∃ v : Π i : Fin m, (Fin (block_size dstar degs i) → Polynomial F),                ∀ i j, (v i j).degree < dstar ∧                  ∀ x ∈ S, (v i j).eval (φ x) = (φ x) ^ j.val * (fs i x) := by          obtain ⟨S, hcard, hagr⟩ := proximity_gap          exists S          obtain ⟨v, hagr⟩ := hagr          simp only [ge_iff_le, hcard, true_and]          simp only [code, Submodule.mem_map, forall_and] at hagr          rcases hagr with ⟨hagr1, hagr2⟩          let vaux (i : Fin m) (j : Fin (block_size dstar degs i)) :            Fin (total_terms dstar degs - 1 + 1) :=            ⟨block_start dstar degs i + j.val,            by {            rw [htotal, add_tsub_cancel_right, ←htotal]            simp only [block_start, block_size, total_terms]            rcases i with ⟨i, hi⟩            rcases j with ⟨j, hj⟩            apply lt_of_lt_of_le            · apply Nat.add_lt_add_left (m := dstar - degs ⟨i, hi⟩ + 1)                (by aesop (add simp [block_size]) (add safe (by omega)))            · rw [Finset.sum_equiv                (t := Finset.erase {x : Fin _ | x ≤ ⟨i, hi⟩} ⟨i, hi⟩)                (g := fun x => (dstar - degs x + 1))                (Equiv.refl _)                (by aesop (add safe (by omega)))                (by aesop), Finset.sum_erase_add _ _ (by simp)]              exact Finset.sum_le_sum_of_subset (by simp)          }⟩          simp only [Polynomial.degreeLT, ge_iff_le, Submodule.mem_iInf, LinearMap.mem_ker,            Polynomial.lcoeff_apply, evalOnPoints, LinearMap.coe_mk, AddHom.coe_mk] at hagr1          exists (fun i j => Classical.choose            (hagr1 (vaux i j)))          intro i j          have h_spec := Classical.choose_spec (hagr1 (vaux i j))          constructor          · rw [Polynomial.degree_lt_iff_coeff_zero]            intro m hm            rw [h_spec.1 m hm]          · intro x hx            rw [congrFun h_spec.2 x]            specialize hagr2 (vaux i j) hx            simp only [mem_filter, mem_univ, true_and] at hagr2            rw [hagr2, block_idx_eq_max]            simp only [Option.elim]            rw [add_tsub_cancel_left, mul_comm]      rcases proximity_gap with ⟨S, ⟨hS_card, ⟨v, hv⟩⟩⟩      have master_lemma :=        @master_lemma _ _ _ _ hempty          _ _ _ _ hdegs _          hδLt _ (by aesop) (v := v) (fs := fs)        (by aesop)        (by aesop)      exists S      simp only [ge_iff_le, hS_card, true_and]      have hf : ∀ i, 0 < block_size dstar degs i := by simp [block_size]      exists (fun i => evalOnPoints φ <| v i (⟨0, hf i⟩))      intro i      constructor      · simp only [code, evalOnPoints, LinearMap.coe_mk, AddHom.coe_mk, Submodule.mem_map]        exists (v i ⟨0, hf i⟩)        simp only [Polynomial.degreeLT, ge_iff_le, Submodule.mem_iInf, LinearMap.mem_ker,          Polynomial.lcoeff_apply, and_true]        intro j hj        specialize master_lemma i ⟨0, hf i⟩        simp only [WithBot.coe_zero, add_zero] at master_lemma        rw [Polynomial.degree_lt_iff_coeff_zero] at master_lemma        exact (master_lemma _ hj)      · intro x hx        simp only [evalOnPoints, LinearMap.coe_mk, AddHom.coe_mk, mem_filter, mem_univ, true_and]        specialize (hv i ⟨0, hf i⟩)        have hv := hv.2 x hx        simp only [pow_zero, one_mul] at hv        exact hv