internlm/Lean-Github huggingface dataset:
Theorem: Partition.setOf_rel_self_eq
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
x : α
hx : x ∈ {x | P.Rel x x}
⊢ x ∈ s
Tactic:
obtain ⟨t, ht, hxP, -⟩ := hx
Proof state after:
case refine_1.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 : α
t : Set α
ht : t ∈ P
hxP : x ∈ t
⊢ x ∈ s
Theorem: Partition.setOf_rel_self_eq
Proof state before:
case refine_1.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 : α
t : Set α
ht : t ∈ P
hxP : x ∈ t
⊢ x ∈ s
Tactic:
exact subset_of_mem ht hxP
Proof state after:
no goals
Theorem: Partition.rel_self_iff_mem
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 x ↔ x ∈ s
Tactic:
simp [← P.setOf_rel_self_eq]
Proof state after:
no goals
Theorem: Partition.setOf_rel_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 α
ht : t ∈ P
hx : x ∈ t
y : α
x✝ : y ∈ {y | P.Rel x y}
t' : Set α
ht' : t' ∈ P
hx' : x ∈ t'
hy' : y ∈ t'
⊢ y ∈ t
Tactic:
rwa [P.eq_of_mem_of_mem ht ht' hx hx']
Proof state after:
no goals
Theorem: Partition.setOf_rel_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
x : α
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
by_cases hx : x ∈ s
Proof state after:
case pos
α : 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
⊢ {y | P.Rel x y} = P.partOf x

case neg
α : 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
⊢ {y | P.Rel x y} = P.partOf x
Theorem: Partition.setOf_rel_eq_partOf
Proof state before:
case neg
α : 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
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
rw [partOf_eq_empty _ hx, eq_empty_iff_forall_not_mem]
Proof state after:
case neg
α : 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_1 : α), x_1 ∉ {y | P.Rel x y}
Theorem: Partition.setOf_rel_eq_partOf
Proof state before:
case neg
α : 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_1 : α), x_1 ∉ {y | P.Rel x y}
Tactic:
exact fun y hxy ↦ hx <| Rel.mem_left hxy
Proof state after:
no goals
Theorem: Partition.setOf_rel_eq_partOf
Proof state before:
case pos
α : 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
⊢ {y | P.Rel x y} = P.partOf x
Tactic:
rw [setOf_rel_eq (P.partOf_mem hx) (P.mem_partOf hx)]
Proof state after:
no goals
Theorem: Partition.setOf_rel_mem
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
⊢ {y | P.Rel x y} ∈ P
Tactic:
obtain ⟨t, ⟨ht,hp⟩, -⟩ := P.exists_unique_of_mem_set hx
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
hx : x ∈ s
t : Set α
ht : t ∈ P
hp : x ∈ t
⊢ {y | P.Rel x y} ∈ P
Theorem: Partition.setOf_rel_mem
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
hx : x ∈ s
t : Set α
ht : t ∈ P
hp : x ∈ t
⊢ {y | P.Rel x y} ∈ P
Tactic:
rwa [setOf_rel_eq ht hp]
Proof state after:
no goals
Theorem: Partition.ofRel_rel_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
⊢ ofRel' P.Rel ⋯ = P
Tactic:
ext a
Proof state after:
case hP
α : 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
a : Set α
⊢ a ∈ ofRel' P.Rel ⋯ ↔ a ∈ P
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP
α : 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
a : Set α
⊢ a ∈ ofRel' P.Rel ⋯ ↔ a ∈ P
Tactic:
simp only [mem_ofRel'_iff]
Proof state after:
case hP
α : 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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) ↔ a ∈ P
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP
α : 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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) ↔ a ∈ P
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
Proof state after:
case hP.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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) → a ∈ P

case hP.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
a : Set α
h : a ∈ P
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP.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
a : Set α
h : a ∈ P
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Tactic:
obtain ⟨x, hx⟩ := P.nonempty_of_mem h
Proof state after:
case hP.refine_2.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
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP.refine_2.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
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ ∃ x ∈ s, a = {y | P.Rel x y}
Tactic:
exact ⟨x, (P.subset_of_mem h) hx, by rwa [setOf_rel_eq _ hx]⟩
Proof state after:
no goals
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP.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
a : Set α
⊢ (∃ x ∈ s, a = {y | P.Rel x y}) → a ∈ P
Tactic:
rintro ⟨x,hx, rfl⟩
Proof state after:
case hP.refine_1.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
⊢ {y | P.Rel x y} ∈ P
Theorem: Partition.ofRel_rel_eq
Proof state before:
case hP.refine_1.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
⊢ {y | P.Rel x y} ∈ P
Tactic:
exact setOf_rel_mem _ hx
Proof state after:
no goals
Theorem: Partition.ofRel_rel_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
a : Set α
h : a ∈ P
x : α
hx : x ∈ a
⊢ a = {y | P.Rel x y}
Tactic:
rwa [setOf_rel_eq _ hx]
Proof state after:
no goals
Theorem: Partition.rel_ofRel_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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
⊢ (ofRel r).Rel = r
Tactic:
ext a b
Proof state after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (ofRel r).Rel a b ↔ r a b
Theorem: Partition.rel_ofRel_eq
Proof state before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (ofRel r).Rel a b ↔ r a b
Tactic:
simp only [Rel, mem_ofRel_iff]
Proof state after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) ↔ r a b
Theorem: Partition.rel_ofRel_eq
Proof state before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) ↔ r a b
Tactic:
refine ⟨?_, fun h ↦ ⟨_, ⟨a, refl_of_rel r h, rfl⟩, refl_of_rel r h, h⟩⟩
Proof state after:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) → r a b
Theorem: Partition.rel_ofRel_eq
Proof state before:
case h.h.a
α : 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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b : α
⊢ (∃ t, (∃ x, r x x ∧ t = {y | r x y}) ∧ a ∈ t ∧ b ∈ t) → r a b
Tactic:
rintro ⟨_, ⟨x, -, rfl⟩, ha, hb⟩
Proof state after:
case h.h.a.intro.intro.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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b x : α
ha : a ∈ {y | r x y}
hb : b ∈ {y | r x y}
⊢ r a b
Theorem: Partition.rel_ofRel_eq
Proof state before:
case h.h.a.intro.intro.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 α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsSymm α r
a b x : α
ha : a ∈ {y | r x y}
hb : b ∈ {y | r x y}
⊢ r a b
Tactic:
exact trans_of r (symm_of r ha) hb
Proof state after:
no goals
Theorem: Partition.eq_of_rel_iff_rel
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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P = P'
Tactic:
rw [← ofRel_rel_eq P, ← ofRel_rel_eq P']
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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ ofRel' P.Rel ⋯ = ofRel' P'.Rel ⋯
Theorem: Partition.eq_of_rel_iff_rel
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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ ofRel' P.Rel ⋯ = ofRel' P'.Rel ⋯
Tactic:
congr
Proof state after:
case e_r
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P.Rel = P'.Rel
Theorem: Partition.eq_of_rel_iff_rel
Proof state before:
case e_r
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
⊢ P.Rel = P'.Rel
Tactic:
ext
Proof state after:
case e_r.h.h.a
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
x✝¹ x✝ : α
⊢ P.Rel x✝¹ x✝ ↔ P'.Rel x✝¹ x✝
Theorem: Partition.eq_of_rel_iff_rel
Proof state before:
case e_r.h.h.a
α : 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 P' : Partition s
h : ∀ (x y : α), P.Rel x y ↔ P'.Rel x y
x✝¹ x✝ : α
⊢ P.Rel x✝¹ x✝ ↔ P'.Rel x✝¹ x✝
Tactic:
exact h _ _
Proof state after:
no goals
Theorem: Partition.discrete.rel_iff_eq
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z : α
s : Set α
a b : α
⊢ (Partition.discrete s).Rel a b ↔ a = b ∧ a ∈ s
Tactic:
simp only [Partition.discrete, ofRel', rel_congr, rel_ofRel_eq]
Proof state after:
no goals
Theorem: Partition.discrete.rel_iff_eq_of_mem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z : α
s : Set α
a b : α
ha : a ∈ s
⊢ (Partition.discrete s).Rel a b ↔ a = b
Tactic:
rw [discrete.rel_iff_eq, and_iff_left ha]
Proof state after:
no goals
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel a b
Tactic:
refine (f.rel_apply ha).trans ?_
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel (f a) b
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel (f a) b
Tactic:
rw [hab, P.rel_comm]
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel b (f b)
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
⊢ P.Rel b (f b)
Tactic:
refine f.rel_apply <| by_contra fun hb ↦ ?_
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
hb : b ∉ s
⊢ False
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = f b
hb : b ∉ s
⊢ False
Tactic:
rw [f.apply_of_not_mem hb] at hab
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : b ∉ s
⊢ False
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : b ∉ s
⊢ False
Tactic:
rw [← hab] at hb
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : f a ∉ s
⊢ False
Theorem: Partition.RepFun.rel_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
ha : a ∈ s
hab : f a = b
hb : f a ∉ s
⊢ False
Tactic:
exact hb <| f.apply_mem ha
Proof state after:
no goals
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
⊢ P.Rel a b
Tactic:
obtain (ha | ha) := em (a ∈ s)
Proof state after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∈ s
⊢ P.Rel a b

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∈ s
⊢ P.Rel a b

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Tactic:
exact f.rel_of_apply_eq_apply ha hab
Proof state after:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
⊢ P.Rel a b
Tactic:
obtain (hb | hb) := em (b ∈ s)
Proof state after:
case inr.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∈ s
⊢ P.Rel a b

case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
case inr.inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∈ s
⊢ P.Rel a b

case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Tactic:
exact (f.rel_of_apply_eq_apply hb hab.symm).symm
Proof state after:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : f a = f b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Tactic:
rw [f.apply_of_not_mem ha, f.apply_of_not_mem hb] at hab
Proof state after:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : a = b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Theorem: Partition.RepFun.rel_of_ne_of_apply_eq_apply
Proof state before:
case inr.inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
hne : a ≠ b
hab : a = b
ha : a ∉ s
hb : b ∉ s
⊢ P.Rel a b
Tactic:
contradiction
Proof state after:
no goals
Theorem: Partition.RepFun.idem
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
⊢ f (f a) = f a
Tactic:
obtain (ha | ha) := em (a ∈ s)
Proof state after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f (f a) = f a

case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∉ s
⊢ f (f a) = f a
Theorem: Partition.RepFun.idem
Proof state before:
case inr
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∉ s
⊢ f (f a) = f a
Tactic:
simp_rw [f.apply_of_not_mem ha]
Proof state after:
no goals
Theorem: Partition.RepFun.idem
Proof state before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f (f a) = f a
Tactic:
rw [eq_comm, f.apply_eq_apply_iff_rel ha]
Proof state after:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ P.Rel a (f a)
Theorem: Partition.RepFun.idem
Proof state before:
case inl
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ P.Rel a (f a)
Tactic:
exact f.rel_apply ha
Proof state after:
no goals
Theorem: Partition.RepFun.image_subset_self
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P : Partition s
f : P.RepFun
⊢ ⇑f '' s ⊆ s
Tactic:
rintro _ ⟨a,ha,rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f a ∈ s
Theorem: Partition.RepFun.image_subset_self
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a✝ b : α
s : Set α
P : Partition s
f : P.RepFun
a : α
ha : a ∈ s
⊢ f a ∈ s
Tactic:
exact f.apply_mem ha
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
f₀ : ↑t → α
h_not_mem : ∀ (x : ↑t), ↑x ∉ s → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ s → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
⊢ ∃ f, ∀ (x : ↑t), f ↑x = f₀ x
Tactic:
set f : α → α := fun a ↦ if ha : a ∈ s then
  (if hb : ∃ b : t, P.Rel a b then f₀ hb.choose else P.rep (P.partOf_mem ha)) else a with hf
Proof state after:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z a b : α
s : Set α
P✝ P : Partition s
t : Set α
f₀ : ↑t → α
h_not_mem : ∀ (x : ↑t), ↑x ∉ s → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ s → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a => if ha : a ∈ s then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hf : f = fun a => if ha : a ∈ s then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
⊢ ∃ f, ∀ (x : ↑t), f ↑x = f₀ x