internlm/Lean-Github huggingface dataset:
Theorem: Set.insertIf_seq
Proof 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
Proof 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)
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
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 α
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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
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 α
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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
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 α
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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof 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
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Set.insertIf_seq
Proof 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
Proof state after:
no goals
Theorem: Logic.Relation.TightApartness.eq_iff_not_apart
Proof state before:
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y ↔ ¬r x y
Tactic:
constructor
Proof state after:
case mp
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y → ¬r x y

case mpr
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ ¬r x y → x = y
Theorem: Logic.Relation.TightApartness.eq_iff_not_apart
Proof state before:
case mp
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ x = y → ¬r x y
Tactic:
intro | rfl => irreflexivity
Proof state after:
no goals
Theorem: Logic.Relation.TightApartness.eq_iff_not_apart
Proof state before:
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
x✝ : x = y
⊢ ¬r x x
Tactic:
irreflexivity
Proof state after:
no goals
Theorem: Logic.Relation.TightApartness.eq_iff_not_apart
Proof state before:
case mpr
α✝ : Sort ?u.4458
r✝ : α✝ → α✝ → Prop
α : Sort u_1
r : α → α → Prop
inst✝ : TightApartness r
x y : α
⊢ ¬r x y → x = y
Tactic:
exact TightApartness.tight
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
⊢ unsublist p (⋯ ▸ head) = head
Tactic:
unfold unsublist
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
⊢ (if hh : p x then
      let_fun this := ⋯;
      match ⋯ ▸ ⋯ ▸ head with
      | head => head
      | i.tail => (unsublist p i).tail
    else
      let_fun this := ⋯;
      (unsublist p (this ▸ ⋯ ▸ head)).tail) =
    head
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
⊢ (if hh : p x then
      let_fun this := ⋯;
      match ⋯ ▸ ⋯ ▸ head with
      | head => head
      | i.tail => (unsublist p i).tail
    else
      let_fun this := ⋯;
      (unsublist p (this ▸ ⋯ ▸ head)).tail) =
    head
Tactic:
rw [dif_pos h]
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
⊢ (let_fun this := ⋯;
    match ⋯ ▸ ⋯ ▸ head with
    | head => head
    | i.tail => (unsublist p i).tail) =
    head
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
⊢ (let_fun this := ⋯;
    match ⋯ ▸ ⋯ ▸ head with
    | head => head
    | i.tail => (unsublist p i).tail) =
    head
Tactic:
split
Proof state after:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Theorem: List.Index.unsublist_pos_head
Proof state before:
case h_1
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head

case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Tactic:
next => rfl
Proof state after:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Theorem: List.Index.unsublist_pos_head
Proof state before:
case h_2
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i✝ : (List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = i✝.tail
⊢ (let_fun this := ⋯;
    (unsublist p i✝).tail) =
    head
Tactic:
next i hh => elim_casts at hh; contradiction
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
heq✝ : ⋯ ▸ ⋯ ▸ head = head
⊢ (let_fun this := ⋯;
    head) =
    head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : ⋯ ▸ ⋯ ▸ head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head
Tactic:
elim_casts at hh
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head
Theorem: List.Index.unsublist_pos_head
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
x✝ : (⟨x, h⟩ :: List.sublist p xs).Index
i : (List.sublist p xs).Index
hh : head = i.tail
⊢ (let_fun this := ⋯;
    (unsublist p i).tail) =
    head
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ unsublist p (⋯ ▸ i.tail) = (unsublist p i).tail
Tactic:
simp only [unsublist]
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i.tail with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i.tail)).tail) =
    (unsublist p i).tail
Theorem: List.Index.unsublist_pos_tail
Proof state before:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ (if h_1 : p x then
      match ⋯ ▸ ⋯ ▸ i.tail with
      | head => head
      | i.tail => (unsublist p i).tail
    else (unsublist p (⋯ ▸ ⋯ ▸ i.tail)).tail) =
    (unsublist p i).tail
Tactic:
rw [dif_pos h]
Proof state after:
α : Type u_1
p✝¹ : α → Prop
inst✝² : DecidablePred p✝¹
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h : p x
i : (List.sublist p xs).Index
⊢ (match ⋯ ▸ ⋯ ▸ i.tail with
    | head => head
    | i.tail => (unsublist p i).tail) =
    (unsublist p i).tail