MeasureTheory.SimpleFunc.Antitone.support_eq

lemma Antitone.support_eq [ConditionallyCompleteLinearOrderBot α] [AddMonoid β] [LinearOrder β] [CanonicallyOrderedAdd β] [OrderBot β]  {f : α → β} (hf : Antitone f) :    f.support = if (BddAbove f.support) then                  if (sSup f.support ∈ f.support)                    then Set.Iic (sSup f.support)                  else Set.Iio (sSup f.support)                else Set.univ    := by  ext x  simp only [Function.mem_support, ne_eq, ite_not]  split_ifs with h h'  · contrapose    simp only [mem_Iio, not_lt]    constructor    · intro h''      apply csSup_le'      rw [mem_upperBounds]      intro y hy      contrapose! hy      simp only [Function.mem_support, ne_eq, Decidable.not_not]      rw [← bot_eq_zero', ← le_bot_iff]      convert (hf hy.le).trans_eq h''      exact bot_eq_zero'    · intro h''      rw [← bot_eq_zero', ← le_bot_iff]      convert (hf h'').trans_eq h'      exact bot_eq_zero'  · contrapose    simp only [mem_Iic, not_le]    constructor    · intro h''      apply lt_of_le_of_ne      · apply csSup_le'        rw [mem_upperBounds]        intro y hy        contrapose! hy        simp only [Function.mem_support, ne_eq, Decidable.not_not]        rw [← bot_eq_zero', ← le_bot_iff]        convert (hf hy.le).trans_eq h''        exact bot_eq_zero'      · contrapose! h'        rwa [h']    · intro h''      contrapose! h''      rw [le_csSup_iff' h]      intro y hy      rw [mem_upperBounds] at hy      apply hy      simpa  · simp only [mem_univ, iff_true]    contrapose! h    use x    intro y hy    rw [Function.mem_support, ← bot_eq_zero', ← bot_lt_iff_ne_bot, bot_eq_zero'] at hy    have := h.trans_lt hy    contrapose! this    exact hf this.le