α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥
intro h
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False
refine' P.not_bot_mem (_)
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
rw [h] at hb
no goals
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts
exact hb