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

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

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

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

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

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

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

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

State before:
α : 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
h : y = f a
hp : p
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Tactic:
left
State after:
case h
α : 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
h : y = f a
hp : p
⊢ y ∈ (Set.map (fun f => f a) f✝).inter (Set.const p)

State before:
case h
α : 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
h : y = f a
hp : p
⊢ y ∈ (Set.map (fun f => f a) f✝).inter (Set.const p)
Tactic:
constructor
State after:
case h.left
α : 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
h : y = f a
hp : p
⊢ y ∈ Set.map (fun f => f a) f✝

case h.right
α : 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
h : y = f a
hp : p
⊢ y ∈ Set.const p

State before:
case h.left
α : 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
h : y = f a
hp : p
⊢ y ∈ Set.map (fun f => f a) f✝
Tactic:
exists f
State after:
case h.left
α : 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
h : y = f a
hp : p
⊢ f ∈ f✝ ∧ (fun f => f a) f = y

State before:
case h.left
α : 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
h : y = f a
hp : p
⊢ f ∈ f✝ ∧ (fun f => f a) f = y
Tactic:
constructor
State after:
case h.left.left
α : 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
h : y = f a
hp : p
⊢ f ∈ f✝

case h.left.right
α : 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
h : y = f a
hp : p
⊢ (fun f => f a) f = y

State before:
case h.left.left
α : 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
h : y = f a
hp : p
⊢ f ∈ f✝
Tactic:
exact hf
State after:
no goals

State before:
case h.left.right
α : 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
h : y = f a
hp : p
⊢ (fun f => f a) f = y
Tactic:
exact h.symm
State after:
no goals

State before:
case h.right
α : 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
h : y = f a
hp : p
⊢ y ∈ Set.const p
Tactic:
exact hp
State after:
no goals

State before:
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
Tactic:
right
State after:
case h
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ f✝.bind fun f => Set.map f s

State before:
case h
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ f✝.bind fun f => Set.map f s
Tactic:
exists f
State after:
case h
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f s) f

State before:
case h
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f s) f
Tactic:
constructor
State after:
case h.left
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ f ∈ f✝

case h.right
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ (fun f => Set.map f s) f

State before:
case h.left
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ f ∈ f✝
Tactic:
exact hf
State after:
no goals

State before:
case h.right
α : 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
x : α
hxs : x ∈ s
h : f x = y
⊢ y ∈ (fun f => Set.map f s) f
Tactic:
exists x
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ y ∈ f✝.bind fun f => Set.map f (s.insertIf a p)
Tactic:
exists f
State after:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f (s.insertIf a p)) f

State before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f (s.insertIf a p)) f
Tactic:
constructor
State after:
case left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f ∈ f✝

case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ y ∈ (fun f => Set.map f (s.insertIf a p)) f

State before:
case left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f ∈ f✝
Tactic:
exact hf
State after:
no goals

State before:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ y ∈ (fun f => Set.map f (s.insertIf a p)) f
Tactic:
exists a
State after:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ s.insertIf a p ∧ f a = y

State before:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ s.insertIf a p ∧ f a = y
Tactic:
constructor
State after:
case right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ s.insertIf a p

case right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f a = y

State before:
case right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ s.insertIf a p
Tactic:
left
State after:
case right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ Set.pureIf a p

State before:
case right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a ∈ Set.pureIf a p
Tactic:
constructor
State after:
case right.left.h.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a = a

case right.left.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ p

State before:
case right.left.h.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ a = a
Tactic:
rfl
State after:
no goals

State before:
case right.left.h.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ p
Tactic:
exact hp
State after:
no goals

State before:
case right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
h : (fun f => f a) f = y
hp : y ∈ Set.const p
⊢ f a = y
Tactic:
exact h
State after:
no goals

State before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).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.insertIf a p)
Tactic:
exists f
State after:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f (s.insertIf a p)) f

State before:
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f ∈ f✝ ∧ y ∈ (fun f => Set.map f (s.insertIf a p)) f
Tactic:
constructor
State after:
case left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f ∈ f✝

case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ (fun f => Set.map f (s.insertIf a p)) f

State before:
case left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f ∈ f✝
Tactic:
exact hf
State after:
no goals

State before:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ (fun f => Set.map f (s.insertIf a p)) f
Tactic:
exists x
State after:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s.insertIf a p ∧ f x = y

State before:
case right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s.insertIf a p ∧ f x = y
Tactic:
constructor
State after:
case right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s.insertIf a p

case right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f x = y

State before:
case right.left
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s.insertIf a p
Tactic:
right
State after:
case right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s

State before:
case right.left.h
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
case right.right
α : Sort u_1
β : Sort u_2
f✝ : Set (α → β)
a : α
p : Prop
s : Set α
y : β
x✝ : y ∈ ((Set.map (fun f => f a) f✝).inter (Set.const p)).union (f✝.bind fun f => Set.map f s)
f : α → β
hf : f ∈ f✝
x : α
hx : x ∈ s
h : f x = y
⊢ f x = y
Tactic:
exact h
State after:
no goals