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

Proof state:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x => disjointed f x) = (Iic a).sup f

Tactic:
refine fun x hx ↦ ih x ?_

Result:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) ≤ n

Proof state:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

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

Result:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup f = (Iic i).sup f

Proof state:
case succ
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
rcases lt_or_eq_of_le hi with hn | hn

Result:
case succ.inl
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) < n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Proof state:
case succ.inl
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) < n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
exact ih _ <| Nat.le_of_lt_succ hn

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (Iio i).biUnion Iic = Iio i

Tactic:
ext r

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i

Proof state:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]

Result:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (disjointed f i ⊔ (Iio i).sup fun x => disjointed f x) = (partialSups f) i

Proof state:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) ≤ n

Tactic:
rw [← Nat.lt_add_one_iff, ← hn]

Result:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)

Proof state:
case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
r : ι
hr : r ∈ Iic x
⊢ r ∈ Iio i

Tactic:
simp only [mem_Iic, mem_Iio] at hx hr ⊢

Result:
case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x r : ι
hx : x < i
hr : r ≤ x
⊢ r < i

Proof state:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)

Tactic:
apply lt_of_lt_of_le (b := #(Iic x))

Result:
case succ.inr.hab
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iic x)

case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)