awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i : ι
obtain : ∀ (j : ι) (hj_mem : j ∈ Iic i) (hj_le : ∀ k ∈ Iic i, f k ≤ f j), ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j

Tactic:
obtain ⟨j, hj_mem, hj_le⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩

Premises used: Iff.mpr, le_rfl, Finset.mem_Iic, Finset.exists_max_image, Exists.intro, Finset.Iic
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
⊢ j ≤ i

Tactic:
simp only [Finset.mem_Iic] at hj_mem hj_le

Premises used: Finset.mem_Iic
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
hj_mem₁ : j ≤ i
⊢ ∀ k ≤ i, f k ≤ f j

Tactic:
simp only [Finset.mem_Iic] at hj_mem hj_le

Premises used: Finset.mem_Iic
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
right : (partialSups f : (a : ι) → α) i = f j
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j

Tactic:
use j, hj_mem
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
right : (partialSups f : (a : ι) → α) i ≤ f j
right₁ : f j ≤ (partialSups f : (a : ι) → α) i
⊢ (partialSups f : (a : ι) → α) i = f j

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f : (a : ι) → α) i ≤ f j

Tactic:
partialSups_le _ _ _ fun k hk => hj_le k hk

Premises used: partialSups_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f : (a : ι) → α) i ≤ f j

Tactic:
exact partialSups_le _ _ _ fun k hk => hj_le k hk

Premises used: partialSups_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f : (a : ι) → α) i

Tactic:
le_partialSups_of_le f hj_mem

Premises used: le_partialSups_of_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f : (a : ι) → α) i

Tactic:
exact le_partialSups_of_le f hj_mem

Premises used: le_partialSups_of_le
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s_1 t x y z : α
S : Set α
inst : CompleteLattice α
P Q : Partition s_1
s : α
p p' : Partition s
h : p.parts = p'.parts
mk :
  ∀ (parts : Set α) (sSupIndep' : sSupIndep parts) (bot_notMem' : ⊥ ∉ parts) (sSup_eq' : sSup parts = s)
    (h :
      { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' :
            Partition s }.parts =
        p'.parts),
    { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } = p'
⊢ p = p'

Tactic:
cases p
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s_1 t x y z : α
S : Set α
inst : CompleteLattice α
P Q : Partition s_1
s : α
p' : Partition s
parts : Set α
sSupIndep' : sSupIndep parts
bot_notMem' : ⊥ ∉ parts
sSup_eq' : sSup parts = s
h :
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s }.parts =
    p'.parts
mk :
  ∀ (parts_1 : Set α) (sSupIndep'_1 : sSupIndep parts_1) (bot_notMem'_1 : ⊥ ∉ parts_1) (sSup_eq'_1 : sSup parts_1 = s)
    (h :
      { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' :
            Partition s }.parts =
        { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 :
            Partition s }.parts),
    { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } =
      { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 }
⊢ { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } = p'

Tactic:
cases p'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s_1 t x y z : α
S : Set α
inst : CompleteLattice α
P Q : Partition s_1
s : α
parts : Set α
sSupIndep' : sSupIndep parts
bot_notMem' : ⊥ ∉ parts
sSup_eq' : sSup parts = s
parts_1 : Set α
sSupIndep'_1 : sSupIndep parts_1
bot_notMem'_1 : ⊥ ∉ parts_1
sSup_eq'_1 : sSup parts_1 = s
h :
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s }.parts =
    { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 :
        Partition s }.parts
⊢ { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } =
    { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 }

Tactic:
simpa using h
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ P.parts = (↑P : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P Q : Partition s
hP : ∀ (x : α), x ∈ P ↔ x ∈ Q
⊢ P = Q

Tactic:
SetLike.ext hP

Premises used: SetLike.ext
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ _root_.sSupIndep (↑P : Set α)

Tactic:
P.sSupIndep'

Premises used: Partition.sSupIndep'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x y : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
hy : y ∈ P
hxy : x ≠ y
⊢ Disjoint x y

Tactic:
P.sSupIndep.pairwiseDisjoint hx hy hxy

Premises used: sSupIndep.pairwiseDisjoint, Partition.sSupIndep
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ (↑P : Set α).PairwiseDisjoint id

Tactic:
P.sSupIndep'.pairwiseDisjoint

Premises used: Partition.sSupIndep', sSupIndep.pairwiseDisjoint
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x y : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
hy : y ∈ P
⊢ x = y ∨ Disjoint x y

Tactic:
or_iff_not_imp_left.mpr (P.disjoint hx hy)

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Partition.disjoint
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x y : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
hy : y ∈ P
hxy : ¬Disjoint x y
⊢ x = y

Tactic:
(P.eq_or_disjoint hx hy).resolve_right hxy

Premises used: Partition.eq_or_disjoint, Or.resolve_right
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ sSup (↑P : Set α) = s

Tactic:
P.sSup_eq'

Premises used: Partition.sSup_eq'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ x ∈ P, x) (⨆ a ∈ (↑P : Set α), a)
⊢ ⨆ x ∈ P, x = s

Tactic:
simp_rw [← P.sSup_eq, sSup_eq_iSup]

Premises used: sSup_eq_iSup, Partition.sSup_eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ P, x) (⨆ a ∈ (↑P : Set α), a)

Tactic:
rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
⊢ x ≤ s

Tactic:
(le_sSup hx).trans_eq P.sSup_eq

Premises used: LE.le.trans_eq, le_sSup, Partition.sSup_eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
hs : s ≠ ⊥
hP : (↑P : Set α) = ∅
⊢ False

Tactic:
simp [← P.sSup_eq, hP, sSup_empty] at hs

Premises used: sSup_empty, Partition.sSup_eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ ⊥ ∉ P

Tactic:
P.bot_notMem'

Premises used: Set.Mem, Partition.bot_notMem'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
⊢ x ≠ ⊥

Tactic:
fun h ↦ P.bot_notMem <| h ▸ hx

Premises used: Partition.bot_notMem, Eq.rec, Not
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P : Partition s
hx : x ∈ P
⊢ ⊥ < x

Tactic:
bot_lt_iff_ne_bot.2 <| P.ne_bot_of_mem hx

Premises used: Iff.mpr, Partition.ne_bot_of_mem, bot_lt_iff_ne_bot
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x : α
inst : CompleteLattice α
P : Partition s
hst : s = t
⊢ x ∈ P.copy hst ↔ x ∈ P

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q : Partition s
P : Set α
indep : _root_.sSupIndep P
sSup_eq : sSup P = s
⊢ ⊥ ∉ P \ {⊥}

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q : Partition s
P : Set α
indep : _root_.sSupIndep P
sSup_eq : sSup P = s
⊢ sSup (P \ {⊥}) = s

Tactic:
simp [← sSup_eq]
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P : Set α
indep : _root_.sSupIndep P
sSup_eq : sSup P = s
⊢ x ∈ removeBot P indep sSup_eq ↔ x ∈ P ∧ x ≠ ⊥

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
P : Partition (α := α) ⊥
x : α
hxP : x ∈ P
⊢ ⊥ ∈ P

Tactic:
obtain rfl := le_bot_iff.mp <| P.le_of_mem hxP

Premises used: le_bot_iff, Partition.le_of_mem, Iff.mp, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
P : Partition (α := α) ⊥
hxP : ⊥ ∈ P
⊢ False

Tactic:
P.bot_notMem hxP

Premises used: Partition.bot_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
P : Partition (α := α) ⊥
hxP : ⊥ ∈ P
⊢ False

Tactic:
exact P.bot_notMem hxP

Premises used: Partition.bot_notMem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q : Partition s
P : Partition (α := α) ⊥
hP : ∀ (x : α), x ∈ P ↔ Membership.mem (γ := Partition (α := α) ⊥) (removeBot ∅ ⋯ ⋯) x
⊢ P = removeBot ∅ ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q : Partition s
P : Partition (α := α) ⊥
x_1 : α
⊢ x_1 ∈ P ↔ Membership.mem (γ := Partition (α := α) ⊥) (removeBot ∅ ⋯ ⋯) x_1

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
inst : CompleteLattice α
P : Partition (α := α) ⊥
hxP : x ∈ P
⊢ False

Tactic:
P.notMem_of_bot _ hxP

Premises used: Partition.notMem_of_bot
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
inst : CompleteLattice α
P : Partition (α := α) ⊥
hxP : x ∈ P
⊢ False

Tactic:
exact P.notMem_of_bot _ hxP

Premises used: Partition.notMem_of_bot
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
obtain : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), ∃ y ∈ R, x ≤ y
⊢ ∃ y ∈ R, x ≤ y

Tactic:
obtain ⟨y, hy, hxy⟩ := hPQ hxP
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
obtain : ∀ (z : α) (hz : z ∈ R) (hyz : y ≤ z), ∃ y ∈ R, x ≤ y
⊢ ∃ y ∈ R, x ≤ y

Tactic:
obtain ⟨z, hz, hyz⟩ := hQR hy
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z_1 : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
hz : z ∈ R
hyz : y ≤ z
⊢ ∃ y ∈ R, x ≤ y

Tactic:
⟨z, hz, hxy.trans hyz⟩

Premises used: And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z_1 : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
hz : z ∈ R
hyz : y ≤ z
⊢ ∃ y ∈ R, x ≤ y

Tactic:
exact ⟨z, hz, hxy.trans hyz⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
⊢ P = Q

Tactic:
Partition.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Partition.ext, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
refine_1 : ∀ (x : α) (h : x ∈ P), x ∈ Q
refine_2 : ∀ (x : α) (h : x ∈ Q), x ∈ P
⊢ P = Q

Tactic:
refine Partition.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Partition.ext, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
refine_1 : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), x ∈ Q
⊢ x ∈ Q

Tactic:
obtain ⟨y, hy, hxy⟩ := hp h
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
refine_1 : ∀ (x' : α) (hx' : x' ∈ P) (hyx' : y ≤ x'), x ∈ Q
⊢ x ∈ Q

Tactic:
obtain ⟨x', hx', hyx'⟩ := hq hy
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
x' : α
hx' : x' ∈ P
hyx' : y ≤ x'
⊢ x ∈ P

Tactic:
obtain rfl := P.pairwiseDisjoint.eq_of_le h hx' (P.ne_bot_of_mem h) (hxy.trans hyx')

Premises used: Partition.ne_bot_of_mem, Partition.pairwiseDisjoint, Set.PairwiseDisjoint.eq_of_le, LE.le.trans, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
x' : α
hx' : x' ∈ P
hyx' : y ≤ x'
hx'₁ : x ∈ P
⊢ y ≤ x

Tactic:
obtain rfl := P.pairwiseDisjoint.eq_of_le h hx' (P.ne_bot_of_mem h) (hxy.trans hyx')

Premises used: Partition.ne_bot_of_mem, Partition.pairwiseDisjoint, Set.PairwiseDisjoint.eq_of_le, LE.le.trans, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
hx' : x ∈ P
hyx' : y ≤ x
refine_1 refine_1₁ refine_1₂ refine_1₃ : y ∈ Q
⊢ x ∈ Q

Tactic:
rwa [hxy.antisymm hyx']

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
refine_2 : ∀ (y : α) (hy : y ∈ P) (hxy : x ≤ y), x ∈ P
⊢ x ∈ P

Tactic:
obtain ⟨y, hy, hxy⟩ := hq h
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
refine_2 : ∀ (x' : α) (hx' : x' ∈ Q) (hyx' : y ≤ x'), x ∈ P
⊢ x ∈ P

Tactic:
obtain ⟨x', hx', hyx'⟩ := hp hy
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
x' : α
hx' : x' ∈ Q
hyx' : y ≤ x'
⊢ x ∈ Q

Tactic:
obtain rfl := Q.pairwiseDisjoint.eq_of_le h hx' (Q.ne_bot_of_mem h) (hxy.trans hyx')

Premises used: Partition.ne_bot_of_mem, Partition.pairwiseDisjoint, Set.PairwiseDisjoint.eq_of_le, LE.le.trans, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
x' : α
hx' : x' ∈ Q
hyx' : y ≤ x'
hx'₁ : x ∈ Q
⊢ y ≤ x

Tactic:
obtain rfl := Q.pairwiseDisjoint.eq_of_le h hx' (Q.ne_bot_of_mem h) (hxy.trans hyx')

Premises used: Partition.ne_bot_of_mem, Partition.pairwiseDisjoint, Set.PairwiseDisjoint.eq_of_le, LE.le.trans, rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
hx' : x ∈ Q
hyx' : y ≤ x
refine_2 refine_2₁ refine_2₂ refine_2₃ : y ∈ P
⊢ x ∈ P

Tactic:
rwa [hxy.antisymm hyx']

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P Q : Partition s
⊢ P ≤ Q ↔ ∀ x ∈ P, ∃ y ∈ Q, x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
⊢ ∃ y ∈ Q, x ≤ y

Tactic:
h hx
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
obtain : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), ∃! y : α, y ∈ Q ∧ x ≤ y
⊢ ∃! y : α, y ∈ Q ∧ x ≤ y

Tactic:
obtain ⟨y, hy, hxy⟩ := h hx
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ ∃! y : α, y ∈ Q ∧ x ≤ y

Tactic:
⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ ↦ Q.eq_of_not_disjoint hz hy ?_⟩

Premises used: _private.0.Partition.existsUnique_of_mem_le.match_1, Partition.eq_of_not_disjoint, ExistsUnique, And.intro, Exists.intro, Eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
refine : ∀ (z : α), (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z → ∀ (hz : z ∈ Q) (hxz : x ≤ z), ¬Disjoint z y
⊢ ∃! y : α, y ∈ Q ∧ x ≤ y

Tactic:
refine ⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ ↦ Q.eq_of_not_disjoint hz hy ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
⊢ x ≠ ⊥

Tactic:
have := P.ne_bot_of_mem hx
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : x ≠ ⊥
contrapose : ∀ (this : Disjoint z y), x = ⊥
⊢ ¬Disjoint z y

Tactic:
contrapose this
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : Disjoint z y
⊢ x = ⊥

Tactic:
le_bot_iff.mp (this hxz hxy)

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s x : α
inst : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
h_1 : (fun (y : α) ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : Disjoint z y
⊢ x = ⊥

Tactic:
exact le_bot_iff.mp (this hxz hxy)

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q P : Partition s
x : α
hxP : x ∈ P
⊢ ∃ (y : α), Membership.mem (γ := Partition s) (removeBot {s} ⋯ ⋯) y ∧ x ≤ y

Tactic:
simp [P.ne_bot_of_mem' hxP, P.le_of_mem hxP]

Premises used: Partition.le_of_mem, Partition.ne_bot_of_mem'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
⊢ Eq (α := Partition s) ⊤ (removeBot {s} ⋯ ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
hs : s ≠ ⊥
⊢ (↑⊤ : Set α) = {s}

Tactic:
simpa [top_def]

Premises used: Partition.top_def
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
a : α
rw : Membership.mem (γ := Partition s) (removeBot {s} ⋯ ⋯) a ↔ a = s ∧ a ≠ ⊥
rw₁ : Membership.mem (γ := Set α) {s} a ∧ a ≠ ⊥ ↔ a = s ∧ a ≠ ⊥
rw₂ rw₃ : a = s ∧ a ≠ ⊥ ↔ a = s ∧ a ≠ ⊥
⊢ Membership.mem (γ := Partition s) ⊤ a ↔ a = s ∧ a ≠ ⊥

Tactic:
rw [top_def, mem_removeBot, mem_singleton_iff]

Premises used: Partition.top_def, Set.mem_singleton_iff, Partition.mem_removeBot
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
⊢ (↑⊤ : Set α) ⊆ {s}

Tactic:
simp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
rw : PairwiseDisjoint.{u_2, u_2} (α := α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} id
⊢ _root_.sSupIndep.{u_2} (α := α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}

Tactic:
rw [sSupIndep_iff_pairwiseDisjoint]

Premises used: sSupIndep_iff_pairwiseDisjoint
-- Module: Mathlib.Order.Partition.Basic
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
a : α
ha : Membership.mem (γ := Set α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} a
a' : α
ha' : Membership.mem (γ := Set α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} a'
h : a ≠ a'
⊢ Function.onFun Disjoint id a a'

Tactic:
grind [Partition.eq_or_disjoint, Disjoint.inf_left, Disjoint.inf_left']

Premises used: Partition.eq_or_disjoint, Disjoint.inf_left', Disjoint.inf_left
-- Module: Mathlib.Order.Partition.Basic
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
this : sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup (↑P : Set α) ⊓ sSup (↑Q : Set α)
⊢ sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
simpa
-- Module: Mathlib.Order.Partition.Basic
Goal:
α_1 : Type u_1
s_1 t x y z : α_1
S : Set α_1
inst : CompleteLattice α_1
P_1 Q_1 : Partition s_1
α : Type u_2
inst_1 : Order.Frame α
s : α
P Q : Partition s
suffices : sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup (↑P : Set α) ⊓ sSup (↑Q : Set α)
⊢ sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
suffices sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup P ⊓ sSup Q by simpa