awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
⊢ sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup (↑P : Set α) ⊓ sSup (↑Q : Set α)

Tactic:
rw [sSup_inf_sSup]

Premises used: sSup_inf_sSup
-- 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
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 :
  LE.le.{u_2} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)
refine_2 :
  LE.le.{u_2} (α := α) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q})
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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 : α
h : Membership.mem (γ := Set α) {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} a
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
ha : a = p ⊓ q
⊢ a ≤ (p, q).1 ⊓ (p, q).2

Tactic:
grind
-- 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
⊢ LE.le.{u_2} (α := α) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2)

Tactic:
exact sSup_le fun a ⟨p, hp, q, hq, ha⟩ ↦ le_iSup₂_of_le (p, q) ⟨hp, hq⟩ <| by grind
-- 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
x_1 : α × α
p q : α
h : (p, q) ∈ (↑P : Set α) ×ˢ (↑Q : Set α)
hp : (p, q).1 ∈ (↑P : Set α)
hq : (p, q).2 ∈ (↑Q : Set α)
⊢ (p, q).1 ⊓ (p, q).2 ≤ p ⊓ q

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
⊢ LE.le.{u_2} (α := α) (⨆ p ∈ (↑P : Set α) ×ˢ (↑Q : Set α), p.1 ⊓ p.2) (sSup {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q})

Tactic:
exact iSup₂_le fun (p, q) ⟨hp, hq⟩ ↦ le_sSup_of_le ⟨p, hp, q, hq, rfl⟩ (by simp)

Premises used: iSup₂_le
-- 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 : a ∈ removeBot {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
obtain : ∀ (p : α) (hp : p ∈ P) (q : α) (hq : q ∈ Q) (h : p ⊓ q ∉ {⊥}), ∃ y ∈ P, p ⊓ q ≤ y
⊢ ∃ y ∈ P, a ≤ y

Tactic:
obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha

Premises used: rfl
-- 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
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
h : p ⊓ q ∉ {⊥}
⊢ ∃ y ∈ P, p ⊓ q ≤ y

Tactic:
grind [inf_le_left]

Premises used: inf_le_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
a : α
ha : a ∈ removeBot {a : α | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
obtain : ∀ (p : α) (hp : p ∈ P) (q : α) (hq : q ∈ Q) (h : p ⊓ q ∉ {⊥}), ∃ y ∈ Q, p ⊓ q ≤ y
⊢ ∃ y ∈ Q, a ≤ y

Tactic:
obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha

Premises used: rfl
-- 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
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
h : p ⊓ q ∉ {⊥}
⊢ ∃ y ∈ Q, p ⊓ q ≤ y

Tactic:
grind [inf_le_right]

Premises used: inf_le_right
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
have : ∀ (q : α) (hq : q ∈ Q ∧ a ≤ q), ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
have ⟨q, hq⟩ := hQ ha
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
have : ∀ (r : α) (hr : r ∈ R ∧ a ≤ r), ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
have ⟨r, hr⟩ := hR ha
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro, Min.min
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
refine_1 : Membership.mem (γ := Set α) {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} (q ⊓ r)
refine_2 : q ⊓ r ∉ {⊥}
refine_3 : a ≤ q ⊓ r
⊢ ∃ y ∈ removeBot {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ Membership.mem (γ := Set α) {a : α | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} (q ⊓ r)

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

Premises used: Partition.ne_bot_of_mem, le_inf_iff
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ q ⊓ r ∉ {⊥}

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

Premises used: Partition.ne_bot_of_mem, le_inf_iff
-- 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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
r : α
hr : r ∈ R ∧ a ≤ r
⊢ a ≤ q ⊓ r

Tactic:
grind [le_inf_iff, P.ne_bot_of_mem ha]

Premises used: Partition.ne_bot_of_mem, le_inf_iff
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_2
inst : Order.Frame α
s a : α
P Q : Partition s
⊢ a ∈ P ⊓ Q ↔ a ≠ ⊥ ∧ ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q

Tactic:
and_comm

Premises used: Set.Mem, Set.diff, setOf, and_comm, Set.singleton
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s : Set α
P : Partition s
⊢ ⋃₀ (↑P : Set (Set α)) = s

Tactic:
P.sSup_eq

Premises used: Set.sUnion, Partition.sSup_eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u t : Set α
P : Partition u
ht : t ∈ P
⊢ t.Nonempty

Tactic:
notMem_singleton_empty.1 <| P.ne_bot_of_mem ht

Premises used: Partition.ne_bot_of_mem, Set.notMem_singleton_empty, Iff.mp
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P : Partition u
⊢ ∅ ∉ P

Tactic:
P.bot_notMem

Premises used: Partition.bot_notMem, Set.Mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u t : Set α
P : Partition u
ht : t ∈ P
⊢ t ⊆ u

Tactic:
P.le_of_mem ht

Premises used: Partition.le_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃ t ∈ P, x ∈ t

Tactic:
⟨fun hx ↦ ?_, fun ⟨t, htP, hxt⟩ ↦ subset_of_mem htP hxt⟩

Premises used: Partition.subset_of_mem, Membership.mem, _private.0.Partition.mem_iff_exists.match_1, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
refine : ∀ (hx : x ∈ u), ∃ t ∈ P, x ∈ t
⊢ x ∈ u ↔ ∃ t ∈ P, x ∈ t

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨t, htP, hxt⟩ ↦ subset_of_mem htP hxt⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
rwa : ∀ (hx : x ∈ ⋃₀ (↑P : Set (Set α))), ∃ t ∈ P, x ∈ t
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hx : ∃ t ∈ (↑P : Set (Set α)), x ∈ t), ∃ t ∈ P, x ∈ t
⊢ ∃ t ∈ P, x ∈ t

Tactic:
rwa [← P.sUnion_eq, mem_sUnion] at hx

Premises used: Partition.sUnion_eq, Set.mem_sUnion
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u s t : Set α
P : Partition u
ht : t ∈ P
hs : s ∈ P
hx : x ∈ t ∩ s
hdj : Disjoint t s
⊢ False

Tactic:
simp [hdj.inter_eq] at hx

Premises used: Disjoint.inter_eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u s t : Set α
P : Partition u
ht : t ∈ P
hus : s ∈ P
hxt : x ∈ t
hxs : x ∈ s
⊢ t = s

Tactic:
eq_of_mem_inter ht hus ⟨hxt, hxs⟩

Premises used: Partition.eq_of_mem_inter, And.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃! t : Set α, t ∈ P ∧ x ∈ t

Tactic:
⟨fun hx ↦ ?_, fun ⟨_, ⟨htP, hxt⟩, _⟩ ↦ subset_of_mem htP hxt⟩

Premises used: Partition.subset_of_mem, Membership.mem, _private.0.Partition.mem_iff_unique.match_1, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
refine : ∀ (hx : x ∈ u), ∃! t : Set α, t ∈ P ∧ x ∈ t
⊢ x ∈ u ↔ ∃! t : Set α, t ∈ P ∧ x ∈ t

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨_, ⟨htP, hxt⟩, _⟩ ↦ subset_of_mem htP hxt⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
⊢ ∃ t ∈ (↑P : Set (Set α)), x ∈ t

Tactic:
rw [← P.sUnion_eq, mem_sUnion] at hx

Premises used: Partition.sUnion_eq, Set.mem_sUnion
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : ∃ t ∈ (↑P : Set (Set α)), x ∈ t
obtain : ∀ (t : Set α) (ht : t ∈ (↑P : Set (Set α))) (hxt : x ∈ t), ∃! t : Set α, t ∈ P ∧ x ∈ t
⊢ ∃! t : Set α, t ∈ P ∧ x ∈ t

Tactic:
obtain ⟨t, ht, hxt⟩ := hx
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
t : Set α
ht : t ∈ (↑P : Set (Set α))
hxt : x ∈ t
⊢ ∃! t : Set α, t ∈ P ∧ x ∈ t

Tactic:
⟨t, ⟨ht, hxt⟩, fun s ⟨hsP, hxs⟩ ↦ P.eq_of_mem_of_mem hsP ht hxs hxt⟩

Premises used: Partition.eq_of_mem_of_mem, ExistsUnique, And.intro, _private.0.Partition.mem_iff_unique.match_2, Exists.intro, Eq
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
t : Set α
ht : t ∈ (↑P : Set (Set α))
hxt : x ∈ t
⊢ ∃! t : Set α, t ∈ P ∧ x ∈ t

Tactic:
exact ⟨t, ⟨ht, hxt⟩, fun s ⟨hsP, hxs⟩ ↦ P.eq_of_mem_of_mem hsP ht hxs hxt⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
⊢ t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S

Tactic:
⟨fun ⟨htsu, htP⟩ ↦ ?_, fun htS ↦ ⟨subset_sUnion_of_mem htS, hSP htS⟩⟩

Premises used: Membership.mem, And.intro, Iff.intro, Set.subset_sUnion_of_mem, _private.0.Partition.subset_sUnion_and_mem_iff_mem.match_1
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
refine : t ⊆ ⋃₀ S ∧ t ∈ P → ∀ (htsu : t ⊆ ⋃₀ S) (htP : t ∈ P), t ∈ S
⊢ t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S

Tactic:
refine ⟨fun ⟨htsu, htP⟩ ↦ ?_, fun htS ↦ ⟨subset_sUnion_of_mem htS, hSP htS⟩⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
obtain : ∀ (x : α) (hxt : x ∈ t), t ∈ S
⊢ t ∈ S

Tactic:
obtain ⟨x, hxt⟩ := nonempty_of_mem htP

Premises used: Partition.nonempty_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
x : α
hxt : x ∈ t
obtain : ∀ (s : Set α) (hsS : s ∈ S) (hxs : x ∈ s), t ∈ S
⊢ t ∈ S

Tactic:
obtain ⟨s, hsS, hxs⟩ := htsu hxt
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
x : α
hxt : x ∈ t
s : Set α
hsS : s ∈ S
hxs : x ∈ s
⊢ t ∈ S

Tactic:
eq_of_mem_of_mem htP (hSP hsS) hxt hxs ▸ hsS

Premises used: Partition.eq_of_mem_of_mem, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ (↑P : Set (Set α))
h : t ⊆ ⋃₀ S ∧ t ∈ P
htsu : t ⊆ ⋃₀ S
htP : t ∈ P
x : α
hxt : x ∈ t
s : Set α
hsS : s ∈ S
hxs : x ∈ s
⊢ t ∈ S

Tactic:
exact eq_of_mem_of_mem htP (hSP hsS) hxt hxs ▸ hsS
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts (s := u)
rw : t ⊆ ⋃₀ S ↔ t ⊆ ⋃₀ S ∧ t ∈ P
⊢ t ⊆ ⋃₀ S ↔ t ∈ S

Tactic:
rw [← subset_sUnion_and_mem_iff_mem hSP]

Premises used: Partition.subset_sUnion_and_mem_iff_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts (s := u)
⊢ t ⊆ ⋃₀ S ↔ t ⊆ ⋃₀ S ∧ t ∈ P

Tactic:
simp [ht]
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u t : Set α
P : Partition u
ht : t ∈ P
⊢ P.rep (u := u) (t := t) ht ∈ t

Tactic:
(P.nonempty_of_mem ht).some_mem

Premises used: Set.Mem, Partition.nonempty_of_mem, Set.Nonempty.some_mem, Partition.rep
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u t : Set α
P : Partition u
ht : t ∈ P
⊢ P.rep (u := u) (t := t) ht ∈ u

Tactic:
P.subset_of_mem ht <| rep_mem ht

Premises used: Partition.rep_mem, Partition.subset_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
⊢ P.Rel (s := u) ≤ Q.Rel (s := u) ↔ P ≤ Q

Tactic:
⟨fun h S hS ↦ ?_, fun h a b ⟨t, ht, ha, hb⟩ ↦ ?_⟩

Premises used: _private.0.Partition.rel_le_iff_le.match_1, Iff.intro, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
refine_1 : ∀ (h : P.Rel (s := u) ≤ Q.Rel (s := u)) (S : Set α) (hS : S ∈ P), ∃ y ∈ Q, S ≤ y
refine_2 :
  ∀ (h : P ≤ Q) (a b : α), P.Rel (s := u) a b → ∀ (t : Set α) (ht : t ∈ P) (ha : a ∈ t) (hb : b ∈ t), Q.Rel (s := u) a b
⊢ P.Rel (s := u) ≤ Q.Rel (s := u) ↔ P ≤ Q

Tactic:
refine ⟨fun h S hS ↦ ?_, fun h a b ⟨t, ht, ha, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
refine_1 : ∀ (x : α) (hxS : x ∈ S), ∃ y ∈ Q, S ≤ y
⊢ ∃ y ∈ Q, S ≤ y

Tactic:
obtain ⟨x, hxS⟩ := nonempty_of_mem hS

Premises used: Partition.nonempty_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
refine_1 : ∀ (T : Set α) (hT : T ∈ Q) (hxT : x ∈ T), ∃ y ∈ Q, S ≤ y
⊢ ∃ y ∈ Q, S ≤ y

Tactic:
obtain ⟨T, hT, hxT, -⟩ := h x x ⟨S, hS, hxS, hxS⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
⊢ ∃ y ∈ Q, S ≤ y

Tactic:
⟨T, hT, fun a haS ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
refine_1 : ∀ (a : α) (haS : a ∈ S), a ∈ T
⊢ ∃ y ∈ Q, S ≤ y

Tactic:
refine ⟨T, hT, fun a haS ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
a : α
haS : a ∈ S
refine_1 : ∀ (T' : Set α) (hT' : T' ∈ Q) (haT' : a ∈ T') (hxT' : x ∈ T'), a ∈ T
⊢ a ∈ T

Tactic:
obtain ⟨T', hT', haT', hxT'⟩ := h a x ⟨S, hS, haS, hxS⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
a : α
haS : a ∈ S
T' : Set α
hT' : T' ∈ Q
haT' : a ∈ T'
hxT' : x ∈ T'
⊢ a ∈ T

Tactic:
eq_of_mem_of_mem hT hT' hxT hxT' ▸ haT'

Premises used: Partition.eq_of_mem_of_mem, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P.Rel (s := u) ≤ Q.Rel (s := u)
S : Set α
hS : S ∈ P
x : α
hxS : x ∈ S
T : Set α
hT : T ∈ Q
hxT : x ∈ T
a : α
haS : a ∈ S
T' : Set α
hT' : T' ∈ Q
haT' : a ∈ T'
hxT' : x ∈ T'
⊢ a ∈ T

Tactic:
exact eq_of_mem_of_mem hT hT' hxT hxT' ▸ haT'
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P ≤ Q
a b : α
h_1 : P.Rel (s := u) a b
t : Set α
ht : t ∈ P
ha : a ∈ t
hb : b ∈ t
refine_2 : ∀ (t' : Set α) (ht' : t' ∈ Q) (htt' : t ≤ t'), Q.Rel (s := u) a b
⊢ Q.Rel (s := u) a b

Tactic:
obtain ⟨t', ht', htt'⟩ := h ht
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
u : Set α
P Q : Partition u
h : P ≤ Q
a b : α
h_1 : P.Rel (s := u) a b
t : Set α
ht : t ∈ P
ha : a ∈ t
hb : b ∈ t
t' : Set α
ht' : t' ∈ Q
htt' : t ≤ t'
w : Set α
left : t' ∈ Q
left₁ : a ∈ t'
right : b ∈ t'
⊢ Q.Rel (s := u) a b

Tactic:
use t', ht', htt' ha, htt' hb
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel (s := u) x y
⊢ ∃ t ∈ P, x ∈ t ∧ y ∈ t

Tactic:
h

Premises used: Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u t : Set α
P : Partition u
h : P.Rel (s := u) x y
ht : t ∈ P
obtain : ∀ (t_1 : Set α) (ht' : t_1 ∈ P) (hx : x ∈ t_1) (hy : y ∈ t_1), x ∈ t ↔ y ∈ t
⊢ x ∈ t ↔ y ∈ t

Tactic:
obtain ⟨t, ht', hx, hy⟩ := h
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u t_1 : Set α
P : Partition u
ht : t_1 ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : x ∈ t_1
rwa rwa₁ rwa₂ rwa₃ : y ∈ t
⊢ y ∈ t_1

Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hx]

Premises used: Partition.eq_of_mem_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u t_1 : Set α
P : Partition u
ht : t_1 ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : y ∈ t_1
rwa rwa₁ rwa₂ rwa₃ : x ∈ t
⊢ x ∈ t_1

Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hy]

Premises used: Partition.eq_of_mem_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u t_1 : Set α
P : Partition u
ht : t_1 ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
⊢ x ∈ t_1 ↔ y ∈ t_1

Tactic:
exact ⟨fun h ↦ by rwa [P.eq_of_mem_of_mem ht ht' h hx],
    fun h ↦ by rwa [P.eq_of_mem_of_mem ht ht' h hy]⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.Rel (s := u) x x ↔ x ∈ u

Tactic:
⟨fun ⟨t, ht, hxP, _⟩ ↦ subset_of_mem ht hxP, fun hx ↦ ?_⟩

Premises used: Partition.subset_of_mem, Membership.mem, _private.0.Partition.rel_rfl_iff.match_1, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
refine : ∀ (hx : x ∈ u), P.Rel (s := u) x x
⊢ P.Rel (s := u) x x ↔ x ∈ u

Tactic:
refine ⟨fun ⟨t, ht, hxP, _⟩ ↦ subset_of_mem ht hxP, fun hx ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
obtain : ∀ (t : Set α) (ht : t ∈ P) (hxt : x ∈ t), P.Rel (s := u) x x
⊢ P.Rel (s := u) x x

Tactic:
obtain ⟨t, ⟨ht, hxt⟩, -⟩ := P.mem_iff_unique.mp hx

Premises used: Iff.mp, Partition.mem_iff_unique
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ P.Rel (s := u) x x

Tactic:
⟨t, ht, hxt, hxt⟩

Premises used: And.intro, Exists.intro, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ P.Rel (s := u) x x

Tactic:
exact ⟨t, ht, hxt, hxt⟩
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
s_1 t_1 x y z : α
S_1 : Set α
S : Set (Set α)
u s t_2 : Set α
a b c : α
P_1 Q P : Partition u
x_1 x_2 x_3 : α
h : P.Rel (s := u) x_1 x_2
h_1 : P.Rel (s := u) x_2 x_3
t : Set α
ht : t ∈ P
ha : x_1 ∈ t
hb : x_2 ∈ t
t' : Set α
ht' : t' ∈ P
hb' : x_2 ∈ t'
hc rwa rwa₁ rwa₂ rwa₃ : x_3 ∈ t'
⊢ x_3 ∈ t

Tactic:
rwa [eq_of_mem_of_mem ht ht' hb hb']

Premises used: Partition.eq_of_mem_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel (s := u) x y
⊢ P.Rel (s := u) y x

Tactic:
symm_of P.Rel h

Premises used: symm_of, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ P.Rel (s := u) x y ↔ P.Rel (s := u) y x

Tactic:
⟨Rel.symm, Rel.symm⟩

Premises used: Partition.Rel.symm, Iff.intro
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y z : α
u : Set α
P : Partition u
hxy : P.Rel (s := u) x y
hyz : P.Rel (s := u) y z
⊢ P.Rel (s := u) x z

Tactic:
trans_of P.Rel hxy hyz

Premises used: trans_of, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel (s := u) x y
obtain : ∀ (t : Set α) (htP : t ∈ P) (hxt : x ∈ t), x ∈ u
⊢ x ∈ u

Tactic:
obtain ⟨t, htP, hxt, -⟩ := h
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ u

Tactic:
subset_of_mem htP hxt

Premises used: Partition.subset_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ u

Tactic:
exact subset_of_mem htP hxt

Premises used: Partition.subset_of_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel (s := u) x y
⊢ y ∈ u

Tactic:
h.symm.left_mem

Premises used: Partition.Rel.symm, Partition.Rel.left_mem
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hx : x ∈ t
⊢ P.Rel (s := u) x (P.rep (u := u) (t := t) ht)

Tactic:
⟨t, ht, hx, P.rep_mem ht⟩

Premises used: Partition.rep_mem, And.intro, Exists.intro, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.partOf (u := u) x ⊆ u

Tactic:
fun _ ⟨_, ht, _, hyt⟩ ↦ subset_of_mem ht hyt

Premises used: Partition.subset_of_mem, Membership.mem, _private.0.Partition.partOf_subset.match_1, Set.Subset
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ x ∈ P.partOf (u := u) y ↔ P.Rel (s := u) y x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Partition.partOf, Partition.Rel
-- Module: Mathlib.Order.Partition.Basic
Goal:
α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
h : ∀ (y : α), y ∈ t ↔ y ∈ P.partOf (u := u) x
⊢ t = P.partOf (u := u) x

Tactic:
ext y