Prop3d4₀func defprop3

lemma prop3d4₀func_defprop3{ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [inst_3 : WellFoundedGT ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S)(I : {p : ℒ × ℒ // p.1 < p.2}) (hμDCC : μA_DescendingChainCondition μ)(y : ℒ) (hy : I.val.1 < y ∧ y ≤ (prop3d4₀func μ I <| (prop3d4₀func_len μ I hμDCC) - 1).val) :¬ μA μ ⟨(I.val.1,y),hy.1⟩ >  μA μ ⟨(I.val.1 , (prop3d4₀func μ I <| (prop3d4₀func_len μ I hμDCC) - 1).val) ,    prop3d4₀func_defprop3₀ μ I hμDCC ((prop3d4₀func_len μ I hμDCC) - 1) <| Nat.sub_one_lt <|    prop3d4₀func_len_nonzero μ I hμDCC⟩ := by  classical  let len := prop3d4₀func_len μ I hμDCC  by_contra hcontra  by_cases hcases : y < (prop3d4₀func μ I (len - 1)).val  · have h₂ : (prop3d4₀func μ I len).val = I.val.1 := Nat.find_spec (prop3d4₀func_fin_len μ I hμDCC)    have h₃ : ¬ (ℒₛ μ I (prop3d4₀func μ I <| len - 1) (ne_of_lt <| prop3d4₀func_defprop3₀ μ I hμDCC      (len - 1) (Nat.sub_one_lt <| prop3d4₀func_len_nonzero μ I hμDCC))).Nonempty := by      by_contra hcontra'      have triv : len - 1 + 1 = len :=  Nat.sub_one_add_one <| prop3d4₀func_len_nonzero μ I hμDCC      rw [← (triv)] at h₂      simp only [prop3d4₀func, ne_of_lt <| prop3d4₀func_defprop3₀ μ I hμDCC (len - 1)        (Nat.sub_one_lt <| prop3d4₀func_len_nonzero μ I hμDCC)] at h₂      simp only [↓reduceDIte, hcontra'] at h₂      apply (inst_3.wf.has_min (ℒₛ μ I (prop3d4₀func μ I (len-1)) (ne_of_lt <|        prop3d4₀func_defprop3₀ μ I hμDCC (len - 1) (Nat.sub_one_lt <|        prop3d4₀func_len_nonzero μ I hμDCC))) hcontra').choose_spec.1.out.choose_spec.choose.1        h₂.symm    refine h₃ ?_    use y, ⟨le_of_lt hy.1,le_trans hy.2 (prop3d4₀func μ I (prop3d4₀func_len μ I hμDCC - 1)      ).prop.2⟩, ⟨ne_of_lt hy.1,hcases⟩  · simp only [eq_of_le_of_not_lt hy.2 hcases] at hcontra    exact (lt_self_iff_false <| μA μ ⟨(I.val.1 , (prop3d4₀func μ I <| len - 1).val) ,      prop3d4₀func_defprop3₀ μ I hμDCC (len - 1) <| Nat.sub_one_lt <|      prop3d4₀func_len_nonzero μ I hμDCC⟩).1 hcontra