-- Mathlib/Order/Disjointed.lean
lemma disjointed_partialSups (f : ι → α) :
    disjointed (partialSups f) = disjointed f

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed (⇑(partialSups f)) i = disjointed f i

Tactic:
have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
  rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
  simp only [funext (partialSups_apply f), sup'_eq_sup]
  rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
  simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f)) i = disjointed f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
classical
ext i
have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
  rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
  simp only [funext (partialSups_apply f), sup'_eq_sup]
  rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
  simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
congr 2 with r
simpa only [mem_biUnion, mem_Iio, mem_Iic] using
  ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f

Tactic:
congr 2 with r

Result:
case h.e_a.e_s.h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
ext i

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed (⇑(partialSups f)) i = disjointed f i

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ disjointed (⇑(partialSups f)) i = disjointed f i

Tactic:
simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f

Proof state:
case h.e_a.e_s.h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i

Tactic:
simpa only [mem_biUnion, mem_Iio, mem_Iic] using
  ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f

Tactic:
rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ≤ (Iio i).sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (partialSups f) i \ (f i \ (Iio i).sup f) = (Iio i).sup f

Tactic:
simp only [funext (partialSups_apply f), sup'_eq_sup]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f

Tactic:
rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (partialSups f) i \ (f i \ (Iio i).sup f) = (Iio i).sup f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ≤ (Iio i).sup f

Tactic:
simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]

Result:
no goals