awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd parts parts₁ parts₂ parts₃ : c ≤ d
⊢ c ≤ b

Tactic:
rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]

Premises used: Finpartition.disjoint, Set.PairwiseDisjoint.eq_of_le, Finpartition.ne_bot, LE.le.trans
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
pos : ∀ (h : a = ⊥), P ≤ copy (Finpartition.empty α) ⋯
neg : ∀ (h : ¬a = ⊥), P ≤ indiscrete h
⊢ P ≤ if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
x : α
hx : x ∈ P.parts
⊢ ∃ c ∈ (copy (Finpartition.empty α) ⋯).parts, x ≤ c

Tactic:
simpa [h, P.ne_bot hx] using P.le hx

Premises used: Finpartition.ne_bot, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h

Tactic:
fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩

Premises used: Finset.mem_singleton_self, And.intro, Exists.intro, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h

Tactic:
exact fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
⊢ Membership.mem (γ := Finset α) (parts (a := a) (if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha))
    b

Tactic:
have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
hb :
  Membership.mem (γ := Finset α) (parts (a := a) (if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha))
    b
pos : ∀ (h : a = ⊥) (hb : b ∈ (copy (Finpartition.empty α) ⋯).parts), Membership.mem (γ := Finset α) {a} b
neg : ∀ (h : ¬a = ⊥) (hb : b ∈ (indiscrete h).parts), Membership.mem (γ := Finset α) {a} b
⊢ Membership.mem (γ := Finset α) {a} b

Tactic:
split_ifs at hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
h : a = ⊥
hb : b ∈ (copy (Finpartition.empty α) ⋯).parts
⊢ Membership.mem (γ := Finset α) {a} b

Tactic:
simp only [copy_parts, empty_parts, notMem_empty] at hb

Premises used: Finpartition.empty_parts, Finpartition.copy_parts, Finset.notMem_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
h : ¬a = ⊥
hb : b ∈ (indiscrete h).parts
⊢ Membership.mem (γ := Finset α) {a} b

Tactic:
hb

Premises used: Set.Mem, setOf
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
h : ¬a = ⊥
hb : b ∈ (indiscrete h).parts
⊢ Membership.mem (γ := Finset α) {a} b

Tactic:
exact hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
⊢ (↑(parts (a := a) ⊤) : Set α).Subsingleton

Tactic:
Set.subsingleton_of_subset_singleton fun _ hb ↦ mem_singleton.1 <| parts_top_subset _ hb

Premises used: Finset.mem_singleton, Finpartition.parts_top_subset, Iff.mp, Set.subsingleton_of_subset_singleton
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
⊢ Membership.mem (γ := Finset (Finpartition s))
    (image
      (fun (ps : Finset (Finset α)) ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset)
    P

Tactic:
mem_image.mpr ⟨P.parts, ?_, ?_⟩

Premises used: Iff.mpr, Finset.mem_image, Finpartition.parts, And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
refine_1 : P.parts ∈ s.powerset.powerset
refine_2 :
  (if h : P.parts.sup id = s ∧ ⊥ ∉ P.parts ∧ P.parts.SupIndep id then
      { parts := P.parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
    else ⊤) =
    P
⊢ Membership.mem (γ := Finset (Finpartition s))
    (image
      (fun (ps : Finset (Finset α)) ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset)
    P

Tactic:
refine mem_image.mpr ⟨P.parts, ?_, ?_⟩

Premises used: Iff.mpr, Finset.mem_image, Finpartition.parts, And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
refine_1 : P.parts ⊆ s.powerset
⊢ P.parts ∈ s.powerset.powerset

Tactic:
rw [mem_powerset]

Premises used: Finset.mem_powerset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
refine_1 : p ⊆ s
⊢ p ∈ s.powerset

Tactic:
rw [mem_powerset]

Premises used: Finset.mem_powerset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ⊆ s

Tactic:
P.le hp

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ⊆ s

Tactic:
exact P.le hp

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
⊢ (if h : P.parts.sup id = s ∧ ⊥ ∉ P.parts ∧ P.parts.SupIndep id then
      { parts := P.parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
    else ⊤) =
    P

Tactic:
simp [P.supIndep, P.sup_parts, P.bot_notMem, -bot_eq_empty]

Premises used: Finset.bot_eq_empty, Finpartition.supIndep, Finpartition.bot_notMem, Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
by_contra H
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ False

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

Premises used: Finpartition.ne_bot, Iff.mp, Finpartition.le, disjoint_self, Disjoint.mono_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
refine : Disjoint b a
⊢ False

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

Premises used: Finpartition.ne_bot, Iff.mp, Finpartition.le, disjoint_self, Disjoint.mono_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q

Tactic:
grind [h _]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q

Tactic:
have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
⊢ P.parts.sup id ≤ (Q.parts.erase b).sup id

Tactic:
grind [Finset.le_sup, Finset.sup_le_iff]

Premises used: Finset.sup_le_iff, Finset.le_sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
⊢ P.parts.sup id ≤ (Q.parts.erase b).sup id

Tactic:
have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this_1 : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
grw : Disjoint b ((Q.parts.erase b).sup id)
⊢ Disjoint b a

Tactic:
grw [← P.sup_parts, this]

Premises used: Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this_1 : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b ((Q.parts.erase b).sup id)

Tactic:
Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)

Premises used: Finpartition.supIndep, Finset.notMem_erase, Finset.erase_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this_1 : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
this : P.parts.sup id ≤ (Q.parts.erase b).sup id
⊢ Disjoint b ((Q.parts.erase b).sup id)

Tactic:
exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)

Premises used: Finpartition.supIndep, Finset.notMem_erase, Finset.erase_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
by_contra by_contra₁ by_contra₂ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
by_contra₃ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), Disjoint b a
by_contra₄ : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q), Disjoint b a
by_contra₅ :
  ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q)
    (this : P.parts.sup id ≤ (Q.parts.erase b).sup id), Disjoint b a
by_contra₆ :
  ∀ (H : ¬∃ c ∈ P.parts, c ≤ b) (this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q)
    (this : P.parts.sup id ≤ (Q.parts.erase b).sup id), Disjoint b ((Q.parts.erase b).sup id)
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
classical
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
  have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]
  grw [← P.sup_parts, this]
  exact Q.supIndep (erase_subset _ _) hb (notMem_erase _ _)

Premises used: Finpartition.ne_bot, Iff.mp, Finpartition.le, disjoint_self, Finpartition.sup_parts, Disjoint.mono_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b

Tactic:
have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
choose :
  ∀ (f : (b : α) → b ∈ Q.parts → α) (hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts)
    (hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b), #Q.parts ≤ #P.parts
⊢ #Q.parts ≤ #P.parts

Tactic:
choose f hP hf using this
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
rw : #Q.parts.attach ≤ #P.parts
⊢ #Q.parts ≤ #P.parts

Tactic:
rw [← card_attach]

Premises used: Finset.card_attach
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts

Tactic:
card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_

Premises used: Finset.card_le_card_of_injOn, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
refine :
  ∀ b ∈ (↑Q.parts.attach : Set ↥Q.parts),
    ∀ c ∈ (↑Q.parts.attach : Set ↥Q.parts),
      ∀ (h : Eq.{u_1 + 1} (α := α) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) b) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) c)),
        b = c
⊢ #Q.parts.attach ≤ #P.parts

Tactic:
refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_

Premises used: Finset.card_le_card_of_injOn
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h_1 : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : ↥Q.parts
h_2 : b ∈ (↑Q.parts.attach : Set ↥Q.parts)
c : ↥Q.parts
h_3 : c ∈ (↑Q.parts.attach : Set ↥Q.parts)
h : Eq.{u_1 + 1} (α := α) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) b) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) c)
⊢ b = c

Tactic:
Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

Premises used: Finpartition.disjoint, Eq.le, Subtype.coe_injective, Set.PairwiseDisjoint.elim, Finpartition.ne_bot, Iff.mp, Disjoint.mono, LE.le.trans, disjoint_self, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P Q : Finpartition a
h_1 : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : ↥Q.parts
h_2 : b ∈ (↑Q.parts.attach : Set ↥Q.parts)
c : ↥Q.parts
h_3 : c ∈ (↑Q.parts.attach : Set ↥Q.parts)
h : Eq.{u_1 + 1} (α := α) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) b) ((fun (b : ↥Q.parts) ↦ f (↑b : α) ⋯) c)
⊢ b = c

Tactic:
exact
    Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

Premises used: Finpartition.disjoint, Eq.le, Subtype.coe_injective, Set.PairwiseDisjoint.elim, Finpartition.ne_bot, Iff.mp, Disjoint.mono, LE.le.trans, disjoint_self, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
⊢ Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))

Tactic:
have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
rw : Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)
rw₁ : ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)
⊢ Disjoint (id i) (t.sup id)

Tactic:
rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]

Premises used: disjoint_subtype_iff, Finset.sup_coe, id, Finset.sup_image, Subtype.val
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
a₁ : image (Subtype.val (p := Pr)) t ⊆ P.parts
a₂ : (↑(id i) : α) ∈ P.parts
a₃ : (↑(id i) : α) ∉ image (Subtype.val (p := Pr)) t
⊢ Disjoint (↑(id i) : α) ((image (Subtype.val (p := Pr)) t).sup id)

Tactic:
apply P.supIndep

Premises used: Finpartition.supIndep
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ image (Subtype.val (p := Pr)) t ⊆ P.parts

Tactic:
simpa [image_subset_iff_subset_preimage] using ht

Premises used: Finset.image_subset_iff_subset_preimage
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ (↑(id i) : α) ∈ P.parts

Tactic:
simpa using hi
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ (↑(id i) : α) ∉ image (Subtype.val (p := Pr)) t

Tactic:
simpa [i.property] using hi'

Premises used: Subtype.property
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)

Tactic:
Prsup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this_1 : Lattice (Subtype Pr) := Subtype.lattice (P := Pr) Prsup Prinf
this_2 : OrderBot (Subtype Pr) := Subtype.orderBot (p := Pr) Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage (Subtype.val (p := Pr)) ⋯
i : Subtype Pr
hi : Membership.mem (γ := Finset (Subtype Pr)) (P.parts.preimage (Subtype.val (p := Pr)) ⋯) i
hi' : i ∉ t
this : Eq.{u_1 + 1} (α := (i : Subtype Pr) → α) (fun (i : Subtype Pr) ↦ (↑(id i) : α)) (id ∘ Subtype.val (p := Pr))
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)

Tactic:
exact Prsup