α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
⊢ ⊤.parts ⊆ {a}
intro b hb
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then copy (Finpartition.empty α) (_ : ⊥ = a) else indiscrete ha).parts
⊢ b ∈ {a}
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb : b ∈ ⊤.parts
⊢ b ∈ {a}
have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
case inl
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ (copy (Finpartition.empty α) (_ : ⊥ = a)).parts
⊢ b ∈ {a}

case inr
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
hb : b ∈ (if ha : a = ⊥ then copy (Finpartition.empty α) (_ : ⊥ = a) else indiscrete ha).parts
⊢ b ∈ {a}
split_ifs at hb
no goals
case inl
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : a = ⊥
hb : b ∈ (copy (Finpartition.empty α) (_ : ⊥ = a)).parts
⊢ b ∈ {a}
simp only [copy_parts, empty_parts, not_mem_empty] at hb
no goals
case inr
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a✝ : α
P : Finpartition a✝
a : α
inst✝ : Decidable (a = ⊥)
b : α
hb✝ : b ∈ ⊤.parts
h✝ : ¬a = ⊥
hb : b ∈ (indiscrete h✝).parts
⊢ b ∈ {a}
exact hb