Theorem: Set.insert_seq (GMLInit/Data/Set/Insert.lean)

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
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)

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
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)

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
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)

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
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)

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⟩
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)

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
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)

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
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)

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
State after:
no goals

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
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)

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
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✝

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
State after:
no goals

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
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)

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals