internlm/Lean-Github huggingface dataset:
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 : α → α := 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
Tactic:
refine ⟨RepFun.mk f (fun a ha ↦ by simp [hf, ha]) (fun a ha ↦ ?_) (fun a b hab ↦ ?_), fun a ↦ ?_⟩
Proof state after:
case refine_1
α : 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
a : α
ha : a ∈ s
⊢ P.Rel a (f a)

case refine_2
α : 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
a b : α
hab : P.Rel a b
⊢ f a = f b

case refine_3
α : 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
a : ↑t
⊢ { toFun := f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } ↑a = f₀ a
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_3
α : 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
a : ↑t
⊢ { toFun := f, apply_eq_self_of_not_mem := ⋯, rel_apply_of_mem := ⋯, apply_eq_of_rel := ⋯ } ↑a = f₀ a
Tactic:
change f a = f₀ a
Proof state after:
case refine_3
α : 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
a : ↑t
⊢ f ↑a = f₀ a
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_3
α : 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
a : ↑t
⊢ f ↑a = f₀ a
Tactic:
obtain (ha | ha) := em (a.1 ∈ s)
Proof state after:
case refine_3.inl
α : 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
a : ↑t
ha : ↑a ∈ s
⊢ f ↑a = f₀ a

case refine_3.inr
α : 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
a : ↑t
ha : ↑a ∉ s
⊢ f ↑a = f₀ a
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_3.inr
α : 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
a : ↑t
ha : ↑a ∉ s
⊢ f ↑a = f₀ a
Tactic:
simp [hf, ha, h_not_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 : α → α := 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
a : α
ha : a ∉ s
⊢ f a = a
Tactic:
simp [hf, ha]
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_1
α : 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
a : α
ha : a ∈ s
⊢ P.Rel a (f a)
Tactic:
simp only [hf, exists_prop, ha, ↓reduceDite]
Proof state after:
case refine_1
α : 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
a : α
ha : a ∈ s
⊢ P.Rel a (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯)
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_1
α : 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
a : α
ha : a ∈ s
⊢ P.Rel a (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯)
Tactic:
split_ifs with h
Proof state after:
case pos
α : 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
a : α
ha : a ∈ s
h : ∃ b, P.Rel a ↑b
⊢ P.Rel a (f₀ h.choose)

case neg
α : 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
a : α
ha : a ∈ s
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg
α : 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
a : α
ha : a ∈ s
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Tactic:
push_neg at h
Proof state after:
case neg
α : 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
a : α
ha : a ∈ s
h : ∀ (b : ↑t), ¬P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg
α : 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
a : α
ha : a ∈ s
h : ∀ (b : ↑t), ¬P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)
Tactic:
exact P.rep_rel (P.partOf_mem ha) (P.mem_partOf ha)
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case pos
α : 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
a : α
ha : a ∈ s
h : ∃ b, P.Rel a ↑b
⊢ P.Rel a (f₀ h.choose)
Tactic:
exact h.choose_spec.trans <| h_mem h.choose h.choose_spec.mem_right
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_2
α : 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
a b : α
hab : P.Rel a b
⊢ f a = f b
Tactic:
simp_rw [hf, dif_pos hab.mem_left, dif_pos hab.mem_right]
Proof state after:
case refine_2
α : 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
a b : α
hab : P.Rel a b
⊢ (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯) = if hb : ∃ b_1, P.Rel b ↑b_1 then f₀ hb.choose else P.rep ⋯
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_2
α : 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
a b : α
hab : P.Rel a b
⊢ (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯) = if hb : ∃ b_1, P.Rel b ↑b_1 then f₀ hb.choose else P.rep ⋯
Tactic:
split_ifs with h₁ h₂ h₂
Proof state after:
case pos
α : 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
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = f₀ h₂.choose

case neg
α : 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
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯

case pos
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

case neg
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯
Tactic:
congr
Proof state after:
case neg.e_t
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.partOf a = P.partOf b
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg.e_t
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.partOf a = P.partOf b
Tactic:
rwa [← rel_iff_partOf_eq_partOf _ hab.mem_left hab.mem_right]
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case pos
α : 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
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = f₀ h₂.choose
Tactic:
exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg
α : 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
a b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯
Tactic:
exact False.elim <| h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case pos
α : 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
a b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose
Tactic:
exact False.elim <| h₁ ⟨_, hab.trans h₂.choose_spec⟩
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_3.inl
α : 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
a : ↑t
ha : ↑a ∈ s
⊢ f ↑a = f₀ a
Tactic:
simp only [hf, exists_prop, ha, ↓reduceDite]
Proof state after:
case refine_3.inl
α : 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
a : ↑t
ha : ↑a ∈ s
⊢ (if hb : ∃ b, P.Rel ↑a ↑b then f₀ hb.choose else P.rep ⋯) = f₀ a
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case refine_3.inl
α : 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
a : ↑t
ha : ↑a ∈ s
⊢ (if hb : ∃ b, P.Rel ↑a ↑b then f₀ hb.choose else P.rep ⋯) = f₀ a
Tactic:
split_ifs with h
Proof state after:
case pos
α : 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
a : ↑t
ha : ↑a ∈ s
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a

case neg
α : 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
a : ↑t
ha : ↑a ∈ s
h : ¬∃ b, P.Rel ↑a ↑b
⊢ P.rep ⋯ = f₀ a
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case neg
α : 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
a : ↑t
ha : ↑a ∈ s
h : ¬∃ b, P.Rel ↑a ↑b
⊢ P.rep ⋯ = f₀ a
Tactic:
exact False.elim <| h ⟨a, rel_self_iff_mem.2 ha⟩
Proof state after:
no goals
Theorem: Partition.exists_extend_partial_repFun
Proof state before:
case pos
α : 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
a : ↑t
ha : ↑a ∈ s
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a
Tactic:
exact Eq.symm <| h_eq _ _ h.choose_spec
Proof state after:
no goals