internlm/Lean-Github huggingface dataset:
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
⊢ f.seq (s.insert a) = (Set.map (fun f => f a) f).union (f.seq s)
Tactic:
unfold Set.seq
Proof state after:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
⊢ (f.bind fun f => Set.map f (s.insert a)) = (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
⊢ (f.bind fun f => Set.map f (s.insert a)) = (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
⊢ ∀ (x : β),
    (x ∈ f.bind fun f => Set.map f (s.insert a)) ↔ x ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
⊢ ∀ (x : β),
    (x ∈ f.bind fun f => Set.map f (s.insert a)) ↔ x ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Tactic:
intro y
Proof state after:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) ↔ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) ↔ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) → y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s) → y ∈ f.bind fun f => Set.map f (s.insert a)
Theorem: Set.insert_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) → y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
Tactic:
intro ⟨f,hf,h⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (fun f => Set.map f (s.insert a)) f
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (fun f => Set.map f (s.insert a)) f
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
clean at h
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ Set.map f (s.insert a)
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ Set.map f (s.insert a)
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
rw [insert_map] at h
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (Set.map f s).insert (f a)
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (Set.map f s).insert (f a)
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
match h with
| Or.inl h => cases h; left; exists f
| Or.inr ⟨x,hxs,h⟩ => cases h; right; exists f; constructor; assumption; exists x
Proof state after:
no goals
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h✝ : y ∈ (Set.map f s).insert (f a)
h : y ∈ Set.pure (f a)
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
h : f a ∈ (Set.map f s).insert (f a)
⊢ f a ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
h : f a ∈ (Set.map f s).insert (f a)
⊢ f a ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
left
Proof state after:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
h : f a ∈ (Set.map f s).insert (f a)
⊢ f a ∈ Set.map (fun f => f a) f✝
Theorem: Set.insert_seq
Proof state before:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
h : f a ∈ (Set.map f s).insert (f a)
⊢ f a ∈ Set.map (fun f => f a) f✝
Tactic:
exists f
Proof state after:
no goals
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h✝ : y ∈ (Set.map f s).insert (f a)
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
Tactic:
right
Proof state after:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ f✝.bind fun f => Set.map f s
Theorem: Set.insert_seq
Proof state before:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ f✝.bind fun f => Set.map f s
Tactic:
exists f
Proof state after:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f ∈ f✝ ∧ f x ∈ (fun f => Set.map f s) f
Theorem: Set.insert_seq
Proof state before:
case refl.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f ∈ f✝ ∧ f x ∈ (fun f => Set.map f s) f
Tactic:
constructor
Proof state after:
case refl.h.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f ∈ f✝

case refl.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (fun f => Set.map f s) f
Theorem: Set.insert_seq
Proof state before:
case refl.h.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f ∈ f✝

case refl.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (fun f => Set.map f s) f
Tactic:
assumption
Proof state after:
case refl.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (fun f => Set.map f s) f
Theorem: Set.insert_seq
Proof state before:
case refl.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hxs : x ∈ s
h : f x ∈ (Set.map f s).insert (f a)
⊢ f x ∈ (fun f => Set.map f s) f
Tactic:
exists x
Proof state after:
no goals
Theorem: Set.insert_seq
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s) → y ∈ f.bind fun f => Set.map f (s.insert a)
Tactic:
intro
| Or.inl ⟨f,hf,h⟩ => cases h; exists f; constructor; assumption; exists a; constructor; left; rfl; rfl
| Or.inr ⟨f,hf,x,hx,h⟩ => cases h; exists f; constructor; assumption; exists x; constructor; right; assumption; rfl
Proof state after:
no goals
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
x✝ : y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
⊢ y ∈ f✝.bind fun f => Set.map f (s.insert a)
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ f✝.bind fun f => Set.map f (s.insert a)
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ f✝.bind fun f => Set.map f (s.insert a)
Tactic:
exists f
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝ ∧ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝ ∧ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
constructor
Proof state after:
case refl.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝

case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝

case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
assumption
Proof state after:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ (fun f => f a) f ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
exists a
Proof state after:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ s.insert a ∧ f a = (fun f => f a) f
Theorem: Set.insert_seq
Proof state before:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ s.insert a ∧ f a = (fun f => f a) f
Tactic:
constructor
Proof state after:
case refl.right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ s.insert a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Theorem: Set.insert_seq
Proof state before:
case refl.right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ s.insert a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Tactic:
left
Proof state after:
case refl.right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ Set.pure a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Theorem: Set.insert_seq
Proof state before:
case refl.right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ a ∈ Set.pure a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Tactic:
rfl
Proof state after:
case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Theorem: Set.insert_seq
Proof state before:
case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x✝ : (fun f => f a) f ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f a = (fun f => f a) f
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.insert_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
y : β
x✝ : y ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f✝.bind fun f => Set.map f (s.insert a)
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ f✝.bind fun f => Set.map f (s.insert a)
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ f✝.bind fun f => Set.map f (s.insert a)
Tactic:
exists f
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝ ∧ f x ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝ ∧ f x ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
constructor
Proof state after:
case refl.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝

case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f ∈ f✝

case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
assumption
Proof state after:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ (fun f => Set.map f (s.insert a)) f
Theorem: Set.insert_seq
Proof state before:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x ∈ (fun f => Set.map f (s.insert a)) f
Tactic:
exists x
Proof state after:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s.insert a ∧ f x = f x
Theorem: Set.insert_seq
Proof state before:
case refl.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s.insert a ∧ f x = f x
Tactic:
constructor
Proof state after:
case refl.right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s.insert a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Theorem: Set.insert_seq
Proof state before:
case refl.right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s.insert a

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Tactic:
right
Proof state after:
case refl.right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Theorem: Set.insert_seq
Proof state before:
case refl.right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ x ∈ s

case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Tactic:
assumption
Proof state after:
case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Theorem: Set.insert_seq
Proof state before:
case refl.right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
s : Set α
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
x✝ : f x ∈ (Set.map (fun f => f a) f✝).union (f✝.bind fun f => Set.map f s)
⊢ f x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
⊢ f.seq (s.insertIf a p) = ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.seq s)
Tactic:
unfold Set.seq
Proof state after:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
⊢ (f.bind fun f => Set.map f (s.insertIf a p)) =
    ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Theorem: Set.insertIf_seq
Proof state before:
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
⊢ (f.bind fun f => Set.map f (s.insertIf a p)) =
    ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
⊢ ∀ (x : β),
    (x ∈ f.bind fun f => Set.map f (s.insertIf a p)) ↔
      x ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Theorem: Set.insertIf_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
⊢ ∀ (x : β),
    (x ∈ f.bind fun f => Set.map f (s.insertIf a p)) ↔
      x ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Tactic:
intro y
Proof state after:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insertIf a p)) ↔
    y ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Theorem: Set.insertIf_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insertIf a p)) ↔
    y ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insertIf a p)) →
    y ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
y : β
⊢ y ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s) →
    y ∈ f.bind fun f => Set.map f (s.insertIf a p)
Theorem: Set.insertIf_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
p : Prop
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insertIf a p)) →
    y ∈ ((Set.map (fun f => f a) f).inter (Set.const p)).union (f.bind fun f => Set.map f s)
Tactic:
intro ⟨f,hf,h⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (fun f => Set.map f (s.insertIf a p)) f
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insertIf_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (fun f => Set.map f (s.insertIf a p)) f
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Tactic:
clean at h
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ Set.map f (s.insertIf a p)
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Theorem: Set.insertIf_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ Set.map f (s.insertIf a p)
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Tactic:
rw [insertIf_map] at h
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
f : α → β
hf : f ∈ f✝
h : y ∈ (Set.map f s).insertIf (f a) p
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)