α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x, x ∈ P.parts ∧ ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d, d ∈ P.parts ∧ ¬d ≤ b ∧ d \ b = c
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ c ∈ (avoid P b).parts ↔ ∃ d, d ∈ P.parts ∧ ¬d ≤ b ∧ d \ b = c
simp only [avoid, ofErase, mem_erase, Ne.def, mem_image, exists_prop, ← exists_and_left,
  @and_left_comm (c ≠ ⊥)]
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
d : α
⊢ d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x, x ∈ P.parts ∧ ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d, d ∈ P.parts ∧ ¬d ≤ b ∧ d \ b = c
refine' exists_congr fun d ↦ and_congr_right' <| and_congr_left _
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
d : α
⊢ d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
rintro rfl
no goals
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b
rw [sdiff_eq_bot_iff]