internlm/Lean-Github huggingface dataset:
Theorem: Partition.bind_le
Proof state before:
case intro.intro
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
b : α
hbp : b ∈ P
h : t ∈ Qs b hbp
⊢ ∃ y ∈ P, t ≤ y
Tactic:
exact ⟨b, hbp, Partition.le_of_mem _ h⟩
Proof state after:
no goals
Theorem: Partition.eq_of_mem_inter
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P : Partition s
x : α
ht : t ∈ P
hu : u ∈ P
hx : x ∈ t ∩ u
hdj : Disjoint t u
⊢ False
Tactic:
simp [hdj.inter_eq] at hx
Proof state after:
no goals
Theorem: Partition.exists_unique_of_mem_set
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
rw [← P.sUnion_eq, mem_sUnion] at hx
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Theorem: Partition.exists_unique_of_mem_set
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
obtain ⟨t, hxt⟩ := hx
Proof state after:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
t : Set α
hxt : t ∈ ↑P ∧ x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Theorem: Partition.exists_unique_of_mem_set
Proof state before:
case intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
t : Set α
hxt : t ∈ ↑P ∧ x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
Tactic:
exact ⟨t, hxt, fun u ⟨huP, hxu⟩ ↦ eq_of_mem_inter huP hxt.1 ⟨hxu, hxt.2⟩⟩
Proof state after:
no goals
Theorem: Partition.partOf_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ P.partOf x ∈ P
Tactic:
obtain ⟨t, ⟨h', h⟩⟩ := P.exists_unique_of_mem_set hx
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ P.partOf x ∈ P
Theorem: Partition.partOf_mem
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ P.partOf x ∈ P
Tactic:
have hrw : {t | t ∈ P ∧ x ∈ t} = {t} := by
  ext t'
  simp only [mem_setOf_eq, mem_singleton_iff]
  exact ⟨h t', by rintro rfl; exact h'⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ P.partOf x ∈ P
Theorem: Partition.partOf_mem
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ P.partOf x ∈ P
Tactic:
rw [partOf, hrw, sUnion_singleton]
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ t ∈ P
Theorem: Partition.partOf_mem
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
hrw : {t | t ∈ P ∧ x ∈ t} = {t}
⊢ t ∈ P
Tactic:
exact h'.1
Proof state after:
no goals
Theorem: Partition.partOf_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
⊢ {t | t ∈ P ∧ x ∈ t} = {t}
Tactic:
ext t'
Proof state after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ {t | t ∈ P ∧ x ∈ t} ↔ t' ∈ {t}
Theorem: Partition.partOf_mem
Proof state before:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ {t | t ∈ P ∧ x ∈ t} ↔ t' ∈ {t}
Tactic:
simp only [mem_setOf_eq, mem_singleton_iff]
Proof state after:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ P ∧ x ∈ t' ↔ t' = t
Theorem: Partition.partOf_mem
Proof state before:
case h
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' ∈ P ∧ x ∈ t' ↔ t' = t
Tactic:
exact ⟨h t', by rintro rfl; exact h'⟩
Proof state after:
no goals
Theorem: Partition.partOf_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t✝ u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t : Set α
h' : t ∈ P ∧ x ∈ t
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t
t' : Set α
⊢ t' = t → t' ∈ P ∧ x ∈ t'
Tactic:
rintro rfl
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t' : Set α
h' : t' ∈ P ∧ x ∈ t'
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t' ∈ P ∧ x ∈ t'
Theorem: Partition.partOf_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
t' : Set α
h' : t' ∈ P ∧ x ∈ t'
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t' ∈ P ∧ x ∈ t'
Tactic:
exact h'
Proof state after:
no goals
Theorem: Partition.partOf_eq_empty
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ s
⊢ P.partOf x = ∅
Tactic:
rw [← P.sUnion_eq] at hx
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ P.partOf x = ∅
Theorem: Partition.partOf_eq_empty
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ P.partOf x = ∅
Tactic:
simp only [partOf, eq_empty_iff_forall_not_mem, mem_sUnion, mem_setOf, not_exists, not_and,
  and_imp]
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ ∀ (x_1 : α), ∀ x_2 ∈ P, x ∈ x_2 → x_1 ∉ x_2
Theorem: Partition.partOf_eq_empty
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∉ ⋃₀ ↑P
⊢ ∀ (x_1 : α), ∀ x_2 ∈ P, x ∈ x_2 → x_1 ∉ x_2
Tactic:
exact fun y t ht hxt _ ↦ hx <| mem_sUnion_of_mem hxt ht
Proof state after:
no goals
Theorem: Partition.mem_partOf
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
⊢ x ∈ P.partOf x
Tactic:
obtain ⟨_, ⟨h, -⟩⟩ := P.exists_unique_of_mem_set hx
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
w✝ : Set α
h : w✝ ∈ P ∧ x ∈ w✝
⊢ x ∈ P.partOf x
Theorem: Partition.mem_partOf
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
hx : x ∈ s
w✝ : Set α
h : w✝ ∈ P ∧ x ∈ w✝
⊢ x ∈ P.partOf x
Tactic:
exact mem_sUnion_of_mem h.2 h
Proof state after:
no goals
Theorem: Partition.eq_partOf_of_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x
Tactic:
have hx : x ∈ s := by
  rw [← P.sUnion_eq]
  exact mem_sUnion_of_mem hxt ht
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
⊢ t = P.partOf x
Theorem: Partition.eq_partOf_of_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
⊢ t = P.partOf x
Tactic:
obtain ⟨t', ⟨-, h⟩⟩ := P.exists_unique_of_mem_set hx
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
t' : Set α
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t = P.partOf x
Theorem: Partition.eq_partOf_of_mem
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
hx : x ∈ s
t' : Set α
h : ∀ (y : Set α), (fun t => t ∈ P ∧ x ∈ t) y → y = t'
⊢ t = P.partOf x
Tactic:
rw [h t ⟨ht, hxt⟩, h (P.partOf x) ⟨P.partOf_mem hx, P.mem_partOf hx⟩]
Proof state after:
no goals
Theorem: Partition.eq_partOf_of_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
Tactic:
rw [← P.sUnion_eq]
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ ⋃₀ ↑P
Theorem: Partition.eq_partOf_of_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x✝ y z : α
s t u : Set α
P✝ : Partition s
x : α
P : Partition s
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ ⋃₀ ↑P
Tactic:
exact mem_sUnion_of_mem hxt ht
Proof state after:
no goals
Theorem: Partition.eqv_class_comm
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
x : α
⊢ {y | r x y} = {y | r y x}
Tactic:
simp_rw [symm_iff_of]
Proof state after:
no goals
Theorem: Partition.rel_iff_eqv_class_eq_right
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
hy : r y y
⊢ r x y ↔ {z | r x z} = {z | r y z}
Tactic:
simp_rw [Set.ext_iff, mem_setOf]
Proof state after:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
hy : r y y
⊢ r x y ↔ ∀ (x_1 : α), r x x_1 ↔ r y x_1
Theorem: Partition.rel_iff_eqv_class_eq_right
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
hy : r y y
⊢ r x y ↔ ∀ (x_1 : α), r x x_1 ↔ r y x_1
Tactic:
refine' ⟨fun hxy z ↦ ⟨fun hxz ↦ trans_of r (symm_of r hxy) hxz,
  fun hyz ↦ trans_of r hxy hyz⟩, fun h ↦ by rwa [h]⟩
Proof state after:
no goals
Theorem: Partition.rel_iff_eqv_class_eq_right
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
hy : r y y
h : ∀ (x_1 : α), r x x_1 ↔ r y x_1
⊢ r x y
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: Partition.rel_iff_eqv_class_eq_left
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
hx : r x x
⊢ r x y ↔ {z | r x z} = {z | r y z}
Tactic:
rw [symm_iff_of r, rel_iff_eqv_class_eq_right hx, eq_comm]
Proof state after:
no goals
Theorem: Partition.mem_ofRel_iff
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
⊢ t ∈ ofRel r ↔ ∃ x, r x x ∧ t = {y | r x y}
Tactic:
simp_rw [eq_comm (a := t)]
Proof state after:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
⊢ t ∈ ofRel r ↔ ∃ x, r x x ∧ {y | r x y} = t
Theorem: Partition.mem_ofRel_iff
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
⊢ t ∈ ofRel r ↔ ∃ x, r x x ∧ {y | r x y} = t
Tactic:
rfl
Proof state after:
no goals
Theorem: Partition.mem_ofRel'_iff
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
hs : s = {x | r x x}
⊢ t ∈ ofRel' r hs ↔ ∃ x ∈ s, t = {y | r x y}
Tactic:
subst hs
Proof state after:
α : Type u_1
inst✝² : CompleteLattice α
s✝ x y z : α
s t✝ : Set α
a b : α
P : Partition s
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
t : Set α
⊢ t ∈ ofRel' r ⋯ ↔ ∃ x ∈ {x | r x x}, t = {y | r x y}
Theorem: Partition.mem_ofRel'_iff
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝ x y z : α
s t✝ : Set α
a b : α
P : Partition s
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
t : Set α
⊢ t ∈ ofRel' r ⋯ ↔ ∃ x ∈ {x | r x x}, t = {y | r x y}
Tactic:
simp [ofRel', mem_congr_iff, mem_ofRel_iff]
Proof state after:
no goals
Theorem: Partition.class_nonempty
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s t : Set α
ht : t ∈ ofRel r
⊢ t.Nonempty
Tactic:
obtain ⟨x, hx, rfl⟩ := ht
Proof state after:
case intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
x : α
hx : x ∈ {x | r x x}
⊢ ((fun a => {x | r a x}) x).Nonempty
Theorem: Partition.class_nonempty
Proof state before:
case intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
x : α
hx : x ∈ {x | r x x}
⊢ ((fun a => {x | r a x}) x).Nonempty
Tactic:
exact ⟨x, hx⟩
Proof state after:
no goals
Theorem: Partition.Rel.forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
h : P.Rel x y
ht : t ∈ P
⊢ x ∈ t ↔ y ∈ t
Tactic:
obtain ⟨t', ht', hx, hy⟩ := h
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
⊢ x ∈ t ↔ y ∈ t
Theorem: Partition.Rel.forall
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
⊢ x ∈ t ↔ y ∈ t
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]⟩
Proof state after:
no goals
Theorem: Partition.Rel.forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
h : x ∈ t
⊢ y ∈ t
Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hx]
Proof state after:
no goals
Theorem: Partition.Rel.forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
ht : t ∈ P
t' : Set α
ht' : t' ∈ P
hx : x ∈ t'
hy : y ∈ t'
h : y ∈ t
⊢ x ∈ t
Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hy]
Proof state after:
no goals
Theorem: Partition.Rel.mem_left
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
h : P.Rel x y
⊢ x ∈ s
Tactic:
obtain ⟨t, htP, hxt, -⟩ := h
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
Theorem: Partition.Rel.mem_left
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
t : Set α
htP : t ∈ P
hxt : x ∈ t
⊢ x ∈ s
Tactic:
exact subset_of_mem htP hxt
Proof state after:
no goals
Theorem: Partition.rel_iff_partOf_eq_partOf
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
⊢ P.Rel x y ↔ P.partOf x = P.partOf y
Tactic:
refine ⟨fun ⟨t, htP, hxt, hyt⟩ ↦ ?_, fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, ?_⟩⟩
Proof state after:
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ P.partOf x = P.partOf y

case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
h : P.partOf x = P.partOf y
⊢ y ∈ P.partOf x
Theorem: Partition.rel_iff_partOf_eq_partOf
Proof state before:
case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
h : P.partOf x = P.partOf y
⊢ y ∈ P.partOf x
Tactic:
rw [h]
Proof state after:
case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
h : P.partOf x = P.partOf y
⊢ y ∈ P.partOf y
Theorem: Partition.rel_iff_partOf_eq_partOf
Proof state before:
case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
h : P.partOf x = P.partOf y
⊢ y ∈ P.partOf y
Tactic:
exact mem_partOf P hy
Proof state after:
no goals
Theorem: Partition.rel_iff_partOf_eq_partOf
Proof state before:
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ P.partOf x = P.partOf y
Tactic:
rw [eq_partOf_of_mem (P.partOf_mem hx)]
Proof state after:
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ P.partOf x
Theorem: Partition.rel_iff_partOf_eq_partOf
Proof state before:
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
hy : y ∈ s
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ P.partOf x
Tactic:
rwa [← eq_partOf_of_mem htP hxt]
Proof state after:
no goals
Theorem: Partition.rel_iff_forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
⊢ P.Rel x y ↔ x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
Tactic:
refine ⟨fun h ↦ ⟨h.mem_left, fun _ ↦ h.forall⟩,
  fun ⟨hxs, h⟩ ↦ ⟨P.partOf x, P.partOf_mem hxs, P.mem_partOf hxs, ?_⟩⟩
Proof state after:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ y ∈ P.partOf x
Theorem: Partition.rel_iff_forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ y ∈ P.partOf x
Tactic:
rw [← h _ (P.partOf_mem hxs)]
Proof state after:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ x ∈ P.partOf x
Theorem: Partition.rel_iff_forall
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x✝ : x ∈ s ∧ ∀ t ∈ P, x ∈ t ↔ y ∈ t
hxs : x ∈ s
h : ∀ t ∈ P, x ∈ t ↔ y ∈ t
⊢ x ∈ P.partOf x
Tactic:
exact P.mem_partOf hxs
Proof state after:
no goals
Theorem: Partition.setOf_rel_self_eq
Proof state before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
⊢ {x | P.Rel x x} = s
Tactic:
refine subset_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)
Proof state after:
case refine_1
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x : α
hx : x ∈ {x | P.Rel x x}
⊢ x ∈ s

case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x : α
hx : x ∈ s
⊢ x ∈ {x | P.Rel x x}
Theorem: Partition.setOf_rel_self_eq
Proof state before:
case refine_2
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x : α
hx : x ∈ s
⊢ x ∈ {x | P.Rel x x}
Tactic:
obtain ⟨t, ⟨ht, hxt⟩, -⟩ := P.exists_unique_of_mem_set hx
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ {x | P.Rel x x}
Theorem: Partition.setOf_rel_self_eq
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x✝ y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
x : α
hx : x ∈ s
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ x ∈ {x | P.Rel x x}
Tactic:
exact ⟨t, ht, hxt, hxt⟩
Proof state after:
no goals