awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P : Finpartition a
parts : Finset α
subset : parts ⊆ P.parts
sup_parts : parts.sup id = b
X : Type u_2
inst_2 : AddCommMonoid X
f : α → X
hf : ∀ p ∈ P.parts, p ∉ parts → f p = 0
⊢ Eq.{u_2 + 1} (α := X) (∑ p ∈ (P.ofSubset subset sup_parts).parts, f p) (∑ p ∈ P.parts, f p)

Tactic:
Finset.sum_subset subset hf

Premises used: Finset.sum_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : u ⊆ Finset.map (↑e : α ≃ β).toEmbedding P.parts
x : β
hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
rw :
  ∀ (hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts) (x : β)
    (hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts) (hbu : x ∉ u) (x_2 : β) (hx : x_2 ≤ id x)
    (hxu : x_2 ≤ u.sup id), x_2 ≤ ⊥
⊢ x_1 ≤ ⊥

Tactic:
rw [← map_symm_subset] at hu

Premises used: Finset.map_symm_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
⊢ Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)

Tactic:
simp only [mem_map_equiv] at hb

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ (((↑e : α ≃ β).symm : (a : β) → α) x : α) ∉ Finset.map (↑e : α ≃ β).symm.toEmbedding u

Tactic:
simp [hbu]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
refine_2 : ∀ (this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) (⊥ : α)), x_1 ≤ ⊥
refine_1 : (e.symm : (a : β) → α) x_1 ≤ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id
⊢ x_1 ≤ ⊥

Tactic:
have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) (⊥ : α)
⊢ LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) ((e.symm : (a : β) → α) ⊥ : α)

Tactic:
rw [← e.symm.map_bot] at this

Premises used: OrderIso.symm, OrderIso.map_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) ((e.symm : (a : β) → α) ⊥ : α)
⊢ x_1 ≤ ⊥

Tactic:
e.symm.map_rel_iff.mp this

Premises used: OrderIso.symm, RelIso.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) ((e.symm : (a : β) → α) ⊥ : α)
⊢ x_1 ≤ ⊥

Tactic:
exact e.symm.map_rel_iff.mp this

Premises used: OrderIso.symm, RelIso.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) ((e.symm : (a : β) → α) (u.sup id) : α)

Tactic:
e.symm.map_rel_iff.mpr hxu

Premises used: Iff.mpr, OrderIso.symm, RelIso.map_rel_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
h : (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id = (e.symm : (a : β) → α) (u.sup id)
⊢ (e.symm : (a : β) → α) x_1 ≤ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id

Tactic:
convert! e.symm.map_rel_iff.mpr hxu

Premises used: Iff.mpr, OrderIso.symm, RelIso.map_rel_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
h :
  Eq.{u_1 + 1} (α := α) (u.sup (id ∘ (⇑(↑e : α ≃ β).symm.toEmbedding : (a : β) → α)))
    (u.sup ((⇑e.symm : (a : β) → α) ∘ id))
⊢ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id = (e.symm : (a : β) → α) (u.sup id)

Tactic:
rw [map_finset_sup, sup_map]

Premises used: Finset.sup_map, map_finset_sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ Eq.{u_1 + 1} (α := α) (u.sup (id ∘ (⇑(↑e : α ≃ β).symm.toEmbedding : (a : β) → α)))
    (u.sup ((⇑e.symm : (a : β) → α) ∘ id))

Tactic:
rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ (Finset.map (↑e : α ≃ β).toEmbedding P.parts).sup id = (e : (a : α) → β) a

Tactic:
simp [← P.sup_parts]

Premises used: Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
rw : (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) ∉ P.parts
⊢ ⊥ ∉ Finset.map (↑e : α ≃ β).toEmbedding P.parts

Tactic:
rw [mem_map_equiv]

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ ⊥ ∉ P.parts

Tactic:
P.bot_notMem

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
h : Eq.{u_1 + 1} (α := α) (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) (⊥ : α)
⊢ (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) ∉ P.parts

Tactic:
convert! P.bot_notMem

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ Eq.{u_1 + 1} (α := α) (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) (⊥ : α)

Tactic:
e.symm.map_bot

Premises used: OrderIso.symm, OrderIso.map_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ Eq.{u_1 + 1} (α := α) (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) (⊥ : α)

Tactic:
exact e.symm.map_bot

Premises used: OrderIso.symm, OrderIso.map_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ parts (map e P) = Finset.map (↑e : α ≃ β).toEmbedding P.parts

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
⊢ Eq (α := Finpartition (α := α) ⊥) default (Finpartition.empty α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≤ a

Tactic:
(le_sup hb).trans P.sup_parts.le

Premises used: Eq.le, LE.le.trans, Finpartition.sup_parts, Finset.le_sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False

Tactic:
P.bot_notMem (?_)

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
refine : ⊥ ∈ P.parts
⊢ False

Tactic:
refine P.bot_notMem (?_)

Premises used: Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Tactic:
rw [h] at hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
hb₁ : ⊥ ∈ P.parts
⊢ b = ⊥

Tactic:
rw [h] at hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Tactic:
hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Tactic:
exact hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ (↑P.parts : Set α).PairwiseDisjoint id

Tactic:
P.supIndep.pairwiseDisjoint

Premises used: Finset.SupIndep.pairwiseDisjoint, Finpartition.supIndep
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
simp_rw : P.parts = ∅ ↔ P.parts.sup id = ⊥
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
simp_rw [← P.sup_parts]

Premises used: Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥

Tactic:
⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩

Premises used: Iff.mpr, Finset.eq_empty_iff_forall_notMem, Iff.intro, Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
refine_1 : ∀ (h : P.parts = ∅), P.parts.sup id = ⊥
refine_2 : ∀ (h : P.parts.sup id = ⊥) (b : α) (hb : b ∈ P.parts), ⊥ ∈ P.parts
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
refine_1 : Eq.{u_1 + 1} (α := α) (sup ∅ id) ⊥
⊢ P.parts.sup id = ⊥

Tactic:
rw [h]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ Eq.{u_1 + 1} (α := α) (sup ∅ id) ⊥

Tactic:
Finset.sup_empty

Premises used: Finset.sup_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ Eq.{u_1 + 1} (α := α) (sup ∅ id) ⊥

Tactic:
exact Finset.sup_empty

Premises used: Finset.sup_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
refine_2 refine_2₁ refine_2₂ refine_2₃ : id b ∈ P.parts
⊢ ⊥ ∈ P.parts

Tactic:
rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]

Premises used: le_bot_iff, Eq.le, Iff.mp, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
contrapose! : P.parts = ∅ ↔ a = ⊥
⊢ P.parts.Nonempty ↔ a ≠ ⊥

Tactic:
contrapose!
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
parts_eq_empty_iff

Premises used: Finpartition.parts_eq_empty_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
exact parts_eq_empty_iff

Premises used: Finpartition.parts_eq_empty_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
ha : a ≠ ⊥
⊢ P.parts.Nonempty

Tactic:
parts_nonempty_iff.2 ha

Premises used: Iff.mpr, Finpartition.parts_nonempty_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
P : Finpartition (α := α) ⊥
parts : ∀ (a : α), a ∈ P.parts ↔ Membership.mem (γ := Finset α) (Finpartition.parts (a := ⊥) default) a
⊢ P = default

Tactic:
ext a
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a_1 : α
P_1 : Finpartition a_1
P : Finpartition (α := α) ⊥
a : α
⊢ a ∈ P.parts ↔ Membership.mem (γ := Finset α) (parts (a := ⊥) default) a

Tactic:
iff_of_false (fun h ↦ P.ne_bot h <| le_bot_iff.1 <| P.le h) (notMem_empty a)

Premises used: le_bot_iff, iff_of_false, Finset.notMem_empty, Finpartition.ne_bot, Iff.mp, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a_1 : α
P_1 : Finpartition a_1
P : Finpartition (α := α) ⊥
a : α
⊢ a ∈ P.parts ↔ Membership.mem (γ := Finset α) (parts (a := ⊥) default) a

Tactic:
exact iff_of_false (fun h ↦ P.ne_bot h <| le_bot_iff.1 <| P.le h) (notMem_empty a)

Premises used: le_bot_iff, iff_of_false, Finset.notMem_empty, Finpartition.ne_bot, Iff.mp, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
pos : ∀ (h : a = ⊥), Nonempty.{u_1 + 1} (Finpartition a)
neg : ∀ (h : ¬a = ⊥), Nonempty.{u_1 + 1} (Finpartition a)
⊢ Nonempty.{u_1 + 1} (Finpartition a)

Tactic:
by_cases h : a = ⊥
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
pos : Nonempty.{u_1 + 1} (Finpartition (α := α) ⊥)
⊢ Nonempty.{u_1 + 1} (Finpartition a)

Tactic:
rw [h]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty.{u_1 + 1} (Finpartition (α := α) ⊥)

Tactic:
⟨Finpartition.empty α⟩

Premises used: Nonempty.intro, Finpartition.empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty.{u_1 + 1} (Finpartition (α := α) ⊥)

Tactic:
exact ⟨Finpartition.empty α⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : ¬a = ⊥
⊢ Nonempty.{u_1 + 1} (Finpartition a)

Tactic:
⟨Finpartition.indiscrete h⟩

Premises used: Nonempty.intro, Finpartition.indiscrete
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : ¬a = ⊥
⊢ Nonempty.{u_1 + 1} (Finpartition a)

Tactic:
exact ⟨Finpartition.indiscrete h⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ ∀ b ∈ P.parts, b = a

Tactic:
have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦
      (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
parts : ∀ (b : α), b ∈ P.parts ↔ b ∈ (indiscrete ⋯).parts
⊢ P = indiscrete ⋯

Tactic:
ext b
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
b : α
⊢ b ∈ P.parts ↔ b ∈ (indiscrete ⋯).parts

Tactic:
Iff.trans ⟨h b, ?_⟩ mem_singleton.symm

Premises used: Finset.mem_singleton, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
b : α
parts : b = a → b ∈ P.parts
⊢ b ∈ P.parts ↔ b ∈ (indiscrete ⋯).parts

Tactic:
refine Iff.trans ⟨h b, ?_⟩ mem_singleton.symm

Premises used: Finset.mem_singleton, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
b : α
P_1 : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
parts : ∀ (c : α) (hc : c ∈ P.parts), b ∈ P.parts
⊢ b ∈ P.parts

Tactic:
obtain ⟨c, hc⟩ := P.parts_nonempty ha.1

Premises used: And.left, Finpartition.parts_nonempty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
b : α
P_1 : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
c : α
hc parts : c ∈ P.parts
⊢ b ∈ P.parts

Tactic:
simp_rw [← h c hc]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
b : α
P_1 : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
c : α
hc : c ∈ P.parts
⊢ c ∈ P.parts

Tactic:
hc
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
b : α
P_1 : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
c : α
hc : c ∈ P.parts
⊢ c ∈ P.parts

Tactic:
exact hc
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
obtain : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), ∃ c ∈ R.parts, b ≤ c
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
obtain : ∀ (d : α) (hd : d ∈ R.parts) (hcd : c ≤ d), ∃ c ∈ R.parts, b ≤ c
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
obtain ⟨d, hd, hcd⟩ := hQR hc
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hcd : c ≤ d
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
⟨d, hd, hbc.trans hcd⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ R.parts
hcd : c ≤ d
⊢ ∃ c ∈ R.parts, b ≤ c

Tactic:
exact ⟨d, hd, hbc.trans hcd⟩
-- 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
parts : ∀ (b : α), b ∈ P.parts ↔ b ∈ Q.parts
⊢ P = Q

Tactic:
ext b
-- 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 : α
⊢ b ∈ P.parts ↔ b ∈ Q.parts

Tactic:
⟨fun hb ↦ ?_, fun hb ↦ ?_⟩

Premises used: Iff.intro
-- 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 : α
parts : ∀ (hb : b ∈ P.parts), b ∈ Q.parts
parts₁ : ∀ (hb : b ∈ Q.parts), b ∈ P.parts
⊢ b ∈ P.parts ↔ b ∈ Q.parts

Tactic:
refine ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩
-- 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 ∈ P.parts
parts : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), b ∈ Q.parts
⊢ b ∈ Q.parts

Tactic:
obtain ⟨c, hc, hbc⟩ := hPQ hb
-- 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 ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
parts : ∀ (d : α) (hd : d ∈ P.parts) (hcd : c ≤ d), b ∈ Q.parts
⊢ b ∈ Q.parts

Tactic:
obtain ⟨d, hd, hcd⟩ := hQP hc
-- 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 ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
parts : c ≤ b
⊢ b ∈ Q.parts

Tactic:
rwa [hbc.antisymm]

Premises used: LE.le.antisymm
-- 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 ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd parts parts₁ parts₂ parts₃ : c ≤ d
⊢ c ≤ b

Tactic:
rwa [P.disjoint.eq_of_le hb hd (P.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 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
parts : ∀ (c : α) (hc : c ∈ P.parts) (hbc : b ≤ c), b ∈ P.parts
⊢ b ∈ P.parts

Tactic:
obtain ⟨c, hc, hbc⟩ := hQP hb
-- 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
parts : ∀ (d : α) (hd : d ∈ Q.parts) (hcd : c ≤ d), b ∈ P.parts
⊢ b ∈ P.parts

Tactic:
obtain ⟨d, hd, hcd⟩ := hPQ hc
-- 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 : c ≤ d
parts : c ≤ b
⊢ b ∈ P.parts

Tactic:
rwa [hbc.antisymm]

Premises used: LE.le.antisymm