α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ False
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c, c ∈ P.parts ∧ c ≤ b
by_contra H
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ Disjoint b a
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ False
refine' Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) _)
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ ∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ Disjoint b a
rw [← P.supParts, Finset.disjoint_sup_right]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
⊢ Disjoint b (id c)
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
⊢ ∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)
rintro c hc
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ Disjoint b (id c)
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
⊢ Disjoint b (id c)
obtain ⟨d, hd, hcd⟩ := h hc
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ≠ d
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ Disjoint b (id c)
refine' (Q.disjoint hb hd _).mono_right hcd
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
⊢ False
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ≠ d
rintro rfl
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
H : ∀ (x : α), x ∈ P.parts → ¬x ≤ b
⊢ False
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c, c ∈ P.parts ∧ c ≤ b
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
⊢ False
simp only [not_exists, not_and] at H
no goals
case intro.intro
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
H : ∀ (x : α), x ∈ P.parts → ¬x ≤ b
⊢ False
exact H _ hc hcd