Prop3d4

lemma prop3d4 {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S) (hμDCC : μA_DescendingChainCondition μ)(I : {p : ℒ × ℒ // p.1 < p.2}) (hμcvx : ConvexI I μ): (StI μ I).Nonempty := by  classical  let len := prop3d4₀func_len μ I hμDCC  let func:= prop3d4₀func μ I  by_cases h : len = 1  · refine ⟨I.val.2, ⟨le_of_lt I.prop, le_rfl⟩, ne_of_lt I.prop,⟨?_,fun _ hyI _ _ ↦ hyI.2⟩⟩    intro y hyI hy    have h' :=      (congrArg (fun _a ↦ (func (_a - 1)).val = I.val.2) h) ▸ (of_eq_true (eq_self I.val.2))    have h'' : ¬ μA μ ⟨(I.val.1, y), lt_of_le_of_ne hyI.1 hy⟩ > μA μ ⟨(I.val.1, (func (len-1)).val),      prop3d4₀func_defprop3₀ μ I hμDCC (len - 1) <| Nat.sub_one_lt <|      prop3d4₀func_len_nonzero μ I hμDCC⟩        := prop3d4₀func_defprop3 μ I hμDCC y ⟨lt_of_le_of_ne hyI.left hy,h' ▸ hyI.2⟩    simp only [h', Prod.mk.eta, Subtype.coe_eta, gt_iff_lt] at h''    exact h''  · have h₂ : ∀ i : ℕ, i ≤ len -1 → I.val.1 ≠ (func i).val := by      intro i hi      by_contra!      exact (Nat.find_min (prop3d4₀func_fin_len μ I hμDCC) <| Nat.lt_of_le_sub_one        (Nat.zero_lt_of_ne_zero <| prop3d4₀func_len_nonzero μ I hμDCC) hi) this.symm    have h₃ : ∀ i : ℕ, (hi : 1 ≤ i ∧ i ≤ len -1) → (∀ y : ℒ, (hyI : InIntvl I y) →      (hy : I.val.1 ≠ y) → (y < func (i-1) ∧ μA μ ⟨(I.val.1, y), lt_of_le_of_ne hyI.1 hy⟩ ≥      μA μ ⟨(I.val.1, (func i).val), lt_of_le_of_ne (func i).prop.1 <| h₂ i hi.2⟩) →      y ≤ (func i).val) := by      intro i hi y hyI hy hy'      by_contra!      have h₃' : (func i).val < y ⊔ (func i).val ∧ y ⊔ (func i).val ≤ (func (i-1)).val := by        refine ⟨right_lt_sup.2 this, sup_le_iff.2 ⟨le_of_lt hy'.1,?_⟩⟩        have h₃'' : (prop3d4₀func μ I (i - 1)).val > (prop3d4₀func μ I (i - 1 + 1)).val :=          prop3d4₀func_strict_decreasing μ I (i-1) (h₂ (i-1) <| le_trans (le_of_lt <|            Nat.sub_one_lt <| Nat.one_le_iff_ne_zero.1 hi.1) hi.2)        rw [Nat.sub_one_add_one] at h₃''        · apply le_of_lt h₃''        · exact Nat.one_le_iff_ne_zero.1 hi.1      have h₃''' : ∀ (hi' : I.val.1 ≠ (func i).val) (z : ℒ) (hz : (func i).val < z ∧        z ≤ (func (i - 1)).val), ¬ μA μ ⟨(I.val.1, z), lt_of_le_of_lt (func i).prop.1 hz.1⟩ ≥        μA μ ⟨(I.val.1, (func (i - 1 + 1)).val), lt_of_le_of_ne ((func (i - 1 + 1)).prop).1        ((Nat.sub_one_add_one <| Nat.one_le_iff_ne_zero.1 hi.1) ▸ h₂ i hi.2)⟩ :=        fun hi' z hz ↦ prop3d4₀func_defprop2 μ I (i - 1) ( (Nat.sub_one_add_one <|          Nat.one_le_iff_ne_zero.1 hi.1) ▸ h₂ i hi.2) z ((Nat.sub_one_add_one <|          Nat.one_le_iff_ne_zero.1 hi.1) ▸ hz)      simp only [ne_eq, not_false_eq_true, Nat.sub_add_cancel, ge_iff_le, forall_const, hi,        h₂] at h₃'''      exact (h₃''' (y ⊔ func i) h₃') <| inf_eq_right.2 hy'.2 ▸ impl.prop2d8₁I I μ hμcvx y hyI        (func i) (func i).prop I.val.1 ⟨le_rfl,le_of_lt I.prop⟩  ⟨lt_of_le_of_ne hyI.1 hy,        lt_of_le_of_ne (func i).prop.1 <| h₂ i hi.2⟩    have h₄ : ∀ y : ℒ, (hyI : InIntvl I y) → (hy : I.val.1 ≠ y) → μA μ ⟨(I.val.1, y) ,      lt_of_le_of_ne hyI.1 hy⟩ ≥ μA μ ⟨(I.val.1, (func (len - 1)).val) , lt_of_le_of_ne (func      (len - 1)).prop.1 <| h₂ (len - 1) le_rfl⟩ → (∀ i : ℕ, i ≤ len - 1 → y ≤ (func i).val) := by      intro y hyI hy hy' i hi      induction i with      | zero =>        simp only [func,prop3d4₀func]        exact hyI.2      | succ i hi' =>        have hfinal : ∀ j : ℕ, (hj : j ≤ len - 1) → μA μ ⟨(I.val.1, (func (len - 1)).val),          lt_of_le_of_ne ((func (len - 1)).prop).1 (h₂ (len - 1) le_rfl)⟩ ≥ μA μ ⟨(I.val.1, func j),          prop3d4₀func_defprop3₀ μ I hμDCC j <| lt_of_le_of_lt hj <| Nat.sub_one_lt <| ne_of_gt <|          Nat.zero_lt_of_ne_zero <| prop3d4₀func_len_nonzero μ I hμDCC⟩         := by          apply Nat.decreasingInduction          · exact fun k hk hk' ↦  le_of_lt <| lt_of_lt_of_le (prop3d4₀func_defprop1 μ I k <|              ne_of_lt <| prop3d4₀func_defprop3₀ μ I hμDCC (k+1) <| Nat.add_lt_of_lt_sub hk) hk'          · exact le_rfl        have hh : y < func i := by          refine lt_of_le_of_ne (hi' (Nat.le_of_succ_le hi)) ?_          by_contra!          have hhh :=  lt_of_le_of_lt' hy' <| lt_of_le_of_lt' (hfinal (i+1) hi) <|            prop3d4₀func_defprop1 μ I i (ne_of_lt <| prop3d4₀func_defprop3₀ μ I hμDCC (i+1) <|            lt_of_le_of_lt hi <| Nat.sub_one_lt <| ne_of_gt <| Nat.zero_lt_of_ne_zero <|            prop3d4₀func_len_nonzero μ I hμDCC)          simp only [this] at hhh          exact irrefl _ hhh        exact h₃ (i+1) ⟨Nat.le_add_left 1 i,hi⟩ y hyI hy ⟨hh,ge_trans hy' (hfinal (i+1) hi)⟩    use (func (len - 1)).val    constructor    · refine ⟨h₂ (len - 1) le_rfl,⟨?_,fun y hyI hy hy' ↦        (fun y hyI hy h ↦ h₄ y hyI hy h (len - 1) le_rfl) y hyI hy <| ge_of_eq hy'⟩⟩      intro y hyI hy      by_contra!      exact prop3d4₀func_defprop3 μ I hμDCC y ⟨lt_of_le_of_ne hyI.1 hy,        (fun y hyI hy h ↦ h₄ y hyI hy h (len - 1) le_rfl) y hyI hy <| le_of_lt this⟩ this    · exact (func (len - 1)).prop