-- Mathlib/Order/Partition/Finpartition.lean
theorem exists_le_of_le {a b : α} {P Q : Finpartition a} (h : P ≤ Q) (hb : b ∈ Q.parts) :
    ∃ c ∈ P.parts, c ≤ b

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ Disjoint b a

Tactic:
rw [← P.sup_parts, Finset.disjoint_sup_right]

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ False

Tactic:
refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ Disjoint b a

Proof state:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ Disjoint b (id c)

Tactic:
refine (Q.disjoint hb hd ?_).mono_right hcd

Result:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ≠ d

Proof state:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ≠ d

Tactic:
rintro rfl

Result:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
by_contra H

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)

Tactic:
rintro c hc

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
⊢ Disjoint b (id c)

Proof state:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
hd : b ∈ Q.parts
hcd : c ≤ b
⊢ False

Tactic:
simp only [not_exists, not_and] at H

Result:
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 ∈ P.parts, ¬x ≤ b
⊢ False

Proof state:
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 ∈ P.parts, ¬x ≤ b
⊢ False

Tactic:
exact H _ hc hcd

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
⊢ Disjoint b (id c)

Tactic:
obtain ⟨d, hd, hcd⟩ := h hc

Result:
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 ∈ P.parts, c ≤ b
c : α
hc : c ∈ P.parts
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ Disjoint b (id c)