Prop3d4₀func defprop2

lemma prop3d4₀func_defprop2{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [inst_3 : WellFoundedGT ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S)(I : {p : ℒ × ℒ // p.1 < p.2})(i : ℕ) (hi : I.val.1 ≠ (prop3d4₀func μ I (i + 1)).val) :∀ z : ℒ, (hz : (prop3d4₀func μ I (i+1)).val < z ∧ z ≤ (prop3d4₀func μ I i).val) →    ¬ μA μ ⟨(I.val.1, z),lt_of_le_of_lt (prop3d4₀func μ I (i+1)).prop.1 hz.1⟩ ≥      μA μ ⟨(I.val.1 , (prop3d4₀func μ I (i+1)).val) ,        lt_of_le_of_ne (prop3d4₀func μ I (i+1)).prop.1 hi⟩ := by  intro z hz  simp only [prop3d4₀func, prop3d4₀func_helper μ I i hi]  have hne : (ℒₛ μ I (prop3d4₀func μ I i) <| prop3d4₀func_helper μ I i hi).Nonempty := by    by_contra hcontra    simp only [prop3d4₀func, prop3d4₀func_helper μ I i hi, hcontra] at hi    simp only [↓reduceDIte, ne_eq, not_true_eq_false] at hi  simp only [hne]  by_contra hcontra  have h' : z ∈ (ℒₛ μ I (prop3d4₀func μ I i) <| prop3d4₀func_helper μ I i hi) := by    use ⟨le_of_lt <| lt_of_le_of_lt (prop3d4₀func μ I (i + 1)).prop.1 hz.1,      le_trans hz.2 (prop3d4₀func μ I i).prop.2⟩    have h'' : z < (prop3d4₀func μ I i).val := by      apply lt_of_le_of_ne hz.2      by_contra hcontra'      simp only [hcontra', ↓reduceDIte, ge_iff_le] at hcontra      exact (inst_3.wf.has_min (ℒₛ μ I (prop3d4₀func μ I i) <| prop3d4₀func_helper μ I i hi) hne        ).choose_spec.1.out.choose_spec.choose_spec.not_ge hcontra    use ⟨ne_of_lt <| lt_of_le_of_lt (prop3d4₀func μ I (i+1)).prop.1 hz.1,h''⟩, lt_of_le_of_lt'      hcontra.ge (inst_3.wf.has_min (ℒₛ μ I (prop3d4₀func μ I i) <| prop3d4₀func_helper μ I i hi)      hne).choose_spec.1.out.choose_spec.choose_spec  simp only [prop3d4₀func, prop3d4₀func_helper μ I i hi, hne] at hz  exact (inst_3.wf.has_min (ℒₛ μ I (prop3d4₀func μ I i) <| prop3d4₀func_helper μ I i hi) hne    ).choose_spec.2 z h' hz.1