internlm/Lean-Github huggingface dataset:
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : (fun x x_1 => x ∘ x_1) g' f' x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hz
Proof state after:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ g.seq (f.seq s)
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ g.seq (f.seq s)
Tactic:
exists g'
Proof state after:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g ∧ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g ∧ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Tactic:
constructor
Proof state after:
case a.mpr.refl.refl.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g

case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g
Tactic:
exact hg'
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Tactic:
exists f' x
Proof state after:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s ∧ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s ∧ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Tactic:
constructor
Proof state after:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s

case a.mpr.refl.refl.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s
Tactic:
exists f'
Proof state after:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f ∧ f' x ∈ (fun f => Set.map f s) f'
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f ∧ f' x ∈ (fun f => Set.map f s) f'
Tactic:
constructor
Proof state after:
case a.mpr.refl.refl.refl.right.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f

case a.mpr.refl.refl.refl.right.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ (fun f => Set.map f s) f'
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f
Tactic:
exact hf'
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ (fun f => Set.map f s) f'
Tactic:
exists x
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl.refl.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.union_empty
Proof state before:
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
⊢ s.union Set.empty = s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
⊢ ∀ (x : α), x ∈ s.union Set.empty ↔ x ∈ s
Theorem: Set.union_empty
Proof state before:
case a
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
⊢ ∀ (x : α), x ∈ s.union Set.empty ↔ x ∈ s
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s.union Set.empty ↔ x ∈ s
Theorem: Set.union_empty
Proof state before:
case a
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s.union Set.empty ↔ x ∈ s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s.union Set.empty → x ∈ s

case a.mpr
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s → x ∈ s.union Set.empty
Theorem: Set.union_empty
Proof state before:
case a.mp
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s.union Set.empty → x ∈ s
Tactic:
intro
| Or.inl _ => assumption
| Or.inr _ => contradiction
Proof state after:
no goals
Theorem: Set.union_empty
Proof state before:
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
x✝ : x ∈ s.union Set.empty
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.union_empty
Proof state before:
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
x✝ : x ∈ s.union Set.empty
h✝ : x ∈ Set.empty
⊢ x ∈ s
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.union_empty
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
⊢ x ∈ s → x ∈ s.union Set.empty
Tactic:
intro h
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s.union Set.empty
Theorem: Set.union_empty
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s.union Set.empty
Tactic:
left
Proof state after:
case a.mpr.h
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s
Theorem: Set.union_empty
Proof state before:
case a.mpr.h
α : Sort u_1
β : ?m.12848
γ : ?m.12851
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.empty_union
Proof state before:
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
⊢ Set.empty.union s = s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
⊢ ∀ (x : α), x ∈ Set.empty.union s ↔ x ∈ s
Theorem: Set.empty_union
Proof state before:
case a
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
⊢ ∀ (x : α), x ∈ Set.empty.union s ↔ x ∈ s
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ Set.empty.union s ↔ x ∈ s
Theorem: Set.empty_union
Proof state before:
case a
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ Set.empty.union s ↔ x ∈ s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ Set.empty.union s → x ∈ s

case a.mpr
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ s → x ∈ Set.empty.union s
Theorem: Set.empty_union
Proof state before:
case a.mp
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ Set.empty.union s → x ∈ s
Tactic:
intro
| Or.inl _ => contradiction
| Or.inr _ => assumption
Proof state after:
no goals
Theorem: Set.empty_union
Proof state before:
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
x✝ : x ∈ Set.empty.union s
h✝ : x ∈ Set.empty
⊢ x ∈ s
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_union
Proof state before:
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
x✝ : x ∈ Set.empty.union s
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.empty_union
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
⊢ x ∈ s → x ∈ Set.empty.union s
Tactic:
intro h
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
h : x ∈ s
⊢ x ∈ Set.empty.union s
Theorem: Set.empty_union
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
h : x ∈ s
⊢ x ∈ Set.empty.union s
Tactic:
right
Proof state after:
case a.mpr.h
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s
Theorem: Set.empty_union
Proof state before:
case a.mpr.h
α : Sort u_1
β : ?m.13016
γ : ?m.13019
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.inter_empty
Proof state before:
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
⊢ s.inter Set.empty = Set.empty
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
⊢ ∀ (x : α), x ∈ s.inter Set.empty ↔ x ∈ Set.empty
Theorem: Set.inter_empty
Proof state before:
case a
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
⊢ ∀ (x : α), x ∈ s.inter Set.empty ↔ x ∈ Set.empty
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ s.inter Set.empty ↔ x ∈ Set.empty
Theorem: Set.inter_empty
Proof state before:
case a
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ s.inter Set.empty ↔ x ∈ Set.empty
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ s.inter Set.empty → x ∈ Set.empty

case a.mpr
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ Set.empty → x ∈ s.inter Set.empty
Theorem: Set.inter_empty
Proof state before:
case a.mp
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ s.inter Set.empty → x ∈ Set.empty
Tactic:
intro ⟨_, _⟩
Proof state after:
case a.mp
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
left✝ : x ∈ s
right✝ : x ∈ Set.empty
⊢ x ∈ Set.empty
Theorem: Set.inter_empty
Proof state before:
case a.mp
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
left✝ : x ∈ s
right✝ : x ∈ Set.empty
⊢ x ∈ Set.empty
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.inter_empty
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
⊢ x ∈ Set.empty → x ∈ s.inter Set.empty
Tactic:
intro _
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
a✝ : x ∈ Set.empty
⊢ x ∈ s.inter Set.empty
Theorem: Set.inter_empty
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13185
γ : ?m.13188
s : Set α
x : α
a✝ : x ∈ Set.empty
⊢ x ∈ s.inter Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_inter
Proof state before:
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
⊢ Set.empty.inter s = Set.empty
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
⊢ ∀ (x : α), x ∈ Set.empty.inter s ↔ x ∈ Set.empty
Theorem: Set.empty_inter
Proof state before:
case a
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
⊢ ∀ (x : α), x ∈ Set.empty.inter s ↔ x ∈ Set.empty
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s ↔ x ∈ Set.empty
Theorem: Set.empty_inter
Proof state before:
case a
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s ↔ x ∈ Set.empty
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s → x ∈ Set.empty

case a.mpr
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty → x ∈ Set.empty.inter s
Theorem: Set.empty_inter
Proof state before:
case a.mp
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s → x ∈ Set.empty
Tactic:
intro ⟨_, _⟩
Proof state after:
case a.mp
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
left✝ : x ∈ Set.empty
right✝ : x ∈ s
⊢ x ∈ Set.empty
Theorem: Set.empty_inter
Proof state before:
case a.mp
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
left✝ : x ∈ Set.empty
right✝ : x ∈ s
⊢ x ∈ Set.empty
Tactic:
assumption
Proof state after:
no goals
Theorem: Set.empty_inter
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty → x ∈ Set.empty.inter s
Tactic:
intro _
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
a✝ : x ∈ Set.empty
⊢ x ∈ Set.empty.inter s
Theorem: Set.empty_inter
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
a✝ : x ∈ Set.empty
⊢ x ∈ Set.empty.inter s
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_map
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
⊢ Set.map f Set.empty = Set.empty
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
⊢ ∀ (x : β), x ∈ Set.map f Set.empty ↔ x ∈ Set.empty
Theorem: Set.empty_map
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
⊢ ∀ (x : β), x ∈ Set.map f Set.empty ↔ x ∈ Set.empty
Tactic:
intro x
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.map f Set.empty ↔ x ∈ Set.empty
Theorem: Set.empty_map
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.map f Set.empty ↔ x ∈ Set.empty
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.map f Set.empty → x ∈ Set.empty

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.empty → x ∈ Set.map f Set.empty
Theorem: Set.empty_map
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.map f Set.empty → x ∈ Set.empty
Tactic:
intro ⟨_,_,_⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
w✝ : α
left✝ : w✝ ∈ Set.empty
right✝ : f w✝ = x
⊢ x ∈ Set.empty
Theorem: Set.empty_map
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
w✝ : α
left✝ : w✝ ∈ Set.empty
right✝ : f w✝ = x
⊢ x ∈ Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_map
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
⊢ x ∈ Set.empty → x ∈ Set.map f Set.empty
Tactic:
intro _
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ Set.map f Set.empty
Theorem: Set.empty_map
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13535
f : α → β
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ Set.map f Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_bind
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
⊢ Set.empty.bind f = Set.empty
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
⊢ ∀ (x : β), x ∈ Set.empty.bind f ↔ x ∈ Set.empty
Theorem: Set.empty_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
⊢ ∀ (x : β), x ∈ Set.empty.bind f ↔ x ∈ Set.empty
Tactic:
intro x
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f ↔ x ∈ Set.empty
Theorem: Set.empty_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f ↔ x ∈ Set.empty
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f → x ∈ Set.empty

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty → x ∈ Set.empty.bind f
Theorem: Set.empty_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f → x ∈ Set.empty
Tactic:
intro ⟨_,_,_⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
w✝ : α
left✝ : w✝ ∈ Set.empty
right✝ : x ∈ f w✝
⊢ x ∈ Set.empty
Theorem: Set.empty_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
w✝ : α
left✝ : w✝ ∈ Set.empty
right✝ : x ∈ f w✝
⊢ x ∈ Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty → x ∈ Set.empty.bind f
Tactic:
intro _
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ Set.empty.bind f
Theorem: Set.empty_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ Set.empty.bind f
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_seq
Proof state before:
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
⊢ f.seq Set.empty = Set.empty
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
⊢ ∀ (x : β), x ∈ f.seq Set.empty ↔ x ∈ Set.empty
Theorem: Set.empty_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
⊢ ∀ (x : β), x ∈ f.seq Set.empty ↔ x ∈ Set.empty
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ f.seq Set.empty ↔ x ∈ Set.empty
Theorem: Set.empty_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ f.seq Set.empty ↔ x ∈ Set.empty
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ f.seq Set.empty → x ∈ Set.empty

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ Set.empty → x ∈ f.seq Set.empty
Theorem: Set.empty_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ f.seq Set.empty → x ∈ Set.empty
Tactic:
intro ⟨_, _, (hx : x ∈ Set.empty.map _)⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
w✝ : α → β
left✝ : w✝ ∈ f
hx : x ∈ Set.map w✝ Set.empty
⊢ x ∈ Set.empty
Theorem: Set.empty_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
w✝ : α → β
left✝ : w✝ ∈ f
hx : x ∈ Set.map w✝ Set.empty
⊢ x ∈ Set.empty
Tactic:
rw [empty_map] at hx
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
w✝ : α → β
left✝ : w✝ ∈ f
hx : x ∈ Set.empty
⊢ x ∈ Set.empty
Theorem: Set.empty_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
w✝ : α → β
left✝ : w✝ ∈ f
hx : x ∈ Set.empty
⊢ x ∈ Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.empty_seq
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
⊢ x ∈ Set.empty → x ∈ f.seq Set.empty
Tactic:
intro _
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ f.seq Set.empty
Theorem: Set.empty_seq
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.14047
f : Set (α → β)
x : β
a✝ : x ∈ Set.empty
⊢ x ∈ f.seq Set.empty
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.pure_inter
Proof state before:
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
⊢ (Set.pure a).inter s = Set.pureIf a (a ∈ s)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
⊢ ∀ (x : α), x ∈ (Set.pure a).inter s ↔ x ∈ Set.pureIf a (a ∈ s)
Theorem: Set.pure_inter
Proof state before:
case a
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
⊢ ∀ (x : α), x ∈ (Set.pure a).inter s ↔ x ∈ Set.pureIf a (a ∈ s)
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ (Set.pure a).inter s ↔ x ∈ Set.pureIf a (a ∈ s)
Theorem: Set.pure_inter
Proof state before:
case a
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ (Set.pure a).inter s ↔ x ∈ Set.pureIf a (a ∈ s)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ (Set.pure a).inter s → x ∈ Set.pureIf a (a ∈ s)

case a.mpr
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ Set.pureIf a (a ∈ s) → x ∈ (Set.pure a).inter s
Theorem: Set.pure_inter
Proof state before:
case a.mp
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ (Set.pure a).inter s → x ∈ Set.pureIf a (a ∈ s)
Tactic:
intro ⟨rfl, hs⟩
Proof state after:
case a.mp
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ Set.pureIf x (x ∈ s)
Theorem: Set.pure_inter
Proof state before:
case a.mp
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ Set.pureIf x (x ∈ s)
Tactic:
refine ⟨rfl, hs⟩
Proof state after:
no goals
Theorem: Set.pure_inter
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
⊢ x ∈ Set.pureIf a (a ∈ s) → x ∈ (Set.pure a).inter s
Tactic:
intro ⟨rfl, hs⟩
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ (Set.pure x).inter s
Theorem: Set.pure_inter
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.14390
γ : ?m.14393
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ (Set.pure x).inter s
Tactic:
refine ⟨rfl, hs⟩
Proof state after:
no goals
Theorem: Set.inter_pure
Proof state before:
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
⊢ s.inter (Set.pure a) = Set.pureIf a (a ∈ s)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.inter (Set.pure a) ↔ x ∈ Set.pureIf a (a ∈ s)
Theorem: Set.inter_pure
Proof state before:
case a
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.inter (Set.pure a) ↔ x ∈ Set.pureIf a (a ∈ s)
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
⊢ x ∈ s.inter (Set.pure a) ↔ x ∈ Set.pureIf a (a ∈ s)
Theorem: Set.inter_pure
Proof state before:
case a
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
⊢ x ∈ s.inter (Set.pure a) ↔ x ∈ Set.pureIf a (a ∈ s)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
⊢ x ∈ s.inter (Set.pure a) → x ∈ Set.pureIf a (a ∈ s)

case a.mpr
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
⊢ x ∈ Set.pureIf a (a ∈ s) → x ∈ s.inter (Set.pure a)
Theorem: Set.inter_pure
Proof state before:
case a.mp
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
⊢ x ∈ s.inter (Set.pure a) → x ∈ Set.pureIf a (a ∈ s)
Tactic:
intro ⟨hs, rfl⟩
Proof state after:
case a.mp
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ Set.pureIf x (x ∈ s)
Theorem: Set.inter_pure
Proof state before:
case a.mp
α : Sort u_1
β : ?m.15184
γ : ?m.15187
a : α
s : Set α
x : α
hs : x ∈ s
⊢ x ∈ Set.pureIf x (x ∈ s)
Tactic:
refine ⟨rfl, hs⟩
Proof state after:
no goals