-- Mathlib/Order/Disjointed.lean
/-- Note this lemma does not require `¬IsMax i`, unlike `disjointed_succ`. -/
lemma Monotone.disjointed_succ_sup {f : ι → α} (hf : Monotone f) (i : ι) :
    disjointed f (succ i) ⊔ f i = f (succ i)

Proof state:
case pos
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
simpa only [succ_eq_iff_isMax.mpr h, sup_eq_right] using disjointed_le f i

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
a✝ : ι
⊢ a✝ ∈ Iio (succ i) ↔ a✝ ∈ Iic i

Tactic:
simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
by_cases h : IsMax i

Result:
case pos
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Proof state:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)

Tactic:
rw [this, ← sup'_eq_sup, ← partialSups_apply, hf.partialSups_eq,
  sdiff_sup_cancel <| hf <| le_succ i]

Result:
no goals

Proof state:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)

Tactic:
have : Iio (succ i) = Iic i := by
  ext
  simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]

Result:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ Iio (succ i) = Iic i

Tactic:
ext

Result:
case h
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
a✝ : ι
⊢ a✝ ∈ Iio (succ i) ↔ a✝ ∈ Iic i

Proof state:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
rw [disjointed_apply]

Result:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)