internlm/Lean-Github huggingface dataset:
Theorem: Set.pure_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ (Set.pure a).bind f → y ∈ f a
Tactic:
intro ⟨_, rfl, h⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
h : y ∈ f a
⊢ y ∈ f a
Theorem: Set.pure_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
h : y ∈ f a
⊢ y ∈ f a
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.pure_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ f a → y ∈ (Set.pure a).bind f
Tactic:
intro h
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
h : y ∈ f a
⊢ y ∈ (Set.pure a).bind f
Theorem: Set.pure_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
h : y ∈ f a
⊢ y ∈ (Set.pure a).bind f
Tactic:
refine ⟨a, rfl, h⟩
Proof state after:
no goals
Theorem: Set.pureIf_bind
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ (Set.pureIf a p).bind f = (f a).inter (Set.const p)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pureIf a p).bind f ↔ x ∈ (f a).inter (Set.const p)
Theorem: Set.pureIf_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pureIf a p).bind f ↔ x ∈ (f a).inter (Set.const p)
Tactic:
intro y
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f ↔ y ∈ (f a).inter (Set.const p)
Theorem: Set.pureIf_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f ↔ y ∈ (f a).inter (Set.const p)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f → y ∈ (f a).inter (Set.const p)

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (f a).inter (Set.const p) → y ∈ (Set.pureIf a p).bind f
Theorem: Set.pureIf_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (Set.pureIf a p).bind f → y ∈ (f a).inter (Set.const p)
Tactic:
intro ⟨_, ⟨rfl, hp⟩, h⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
hp : p
h : y ∈ f a
⊢ y ∈ (f a).inter (Set.const p)
Theorem: Set.pureIf_bind
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
hp : p
h : y ∈ f a
⊢ y ∈ (f a).inter (Set.const p)
Tactic:
refine ⟨h, hp⟩
Proof state after:
no goals
Theorem: Set.pureIf_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (f a).inter (Set.const p) → y ∈ (Set.pureIf a p).bind f
Tactic:
intro ⟨h, hp⟩
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
h : y ∈ f a
hp : y ∈ Set.const p
⊢ y ∈ (Set.pureIf a p).bind f
Theorem: Set.pureIf_bind
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
h : y ∈ f a
hp : y ∈ Set.const p
⊢ y ∈ (Set.pureIf a p).bind f
Tactic:
refine ⟨a, ⟨rfl, hp⟩, h⟩
Proof state after:
no goals
Theorem: Set.bind_assoc
Proof state before:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ (s.bind f).bind g = s.bind fun x => (f x).bind g
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ ∀ (x : γ), x ∈ (s.bind f).bind g ↔ x ∈ s.bind fun x => (f x).bind g
Theorem: Set.bind_assoc
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
⊢ ∀ (x : γ), x ∈ (s.bind f).bind g ↔ x ∈ s.bind fun x => (f x).bind g
Tactic:
intro z
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g ↔ z ∈ s.bind fun x => (f x).bind g
Theorem: Set.bind_assoc
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g ↔ z ∈ s.bind fun x => (f x).bind g
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g → z ∈ s.bind fun x => (f x).bind g

case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ (z ∈ s.bind fun x => (f x).bind g) → z ∈ (s.bind f).bind g
Theorem: Set.bind_assoc
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ z ∈ (s.bind f).bind g → z ∈ s.bind fun x => (f x).bind g
Tactic:
intro ⟨y, ⟨x, hx, hy⟩, hz⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
y : β
x : α
hx : x ∈ s
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ s.bind fun x => (f x).bind g
Theorem: Set.bind_assoc
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
y : β
x : α
hx : x ∈ s
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ s.bind fun x => (f x).bind g
Tactic:
refine ⟨x, hx, ⟨y, hy, hz⟩⟩
Proof state after:
no goals
Theorem: Set.bind_assoc
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
⊢ (z ∈ s.bind fun x => (f x).bind g) → z ∈ (s.bind f).bind g
Tactic:
intro ⟨x, hx, ⟨y, hy, hz⟩⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ (s.bind f).bind g
Theorem: Set.bind_assoc
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : α → Set β
g : β → Set γ
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ f x
hz : z ∈ g y
⊢ z ∈ (s.bind f).bind g
Tactic:
refine ⟨y, ⟨x, hx, hy⟩, hz⟩
Proof state after:
no goals
Theorem: Set.bind_comm
Proof state before:
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
⊢ (s.bind fun x => t.bind fun x_1 => f x x_1) = t.bind fun y => s.bind fun x => f x y
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
⊢ ∀ (x : γ), (x ∈ s.bind fun x => t.bind fun x_1 => f x x_1) ↔ x ∈ t.bind fun y => s.bind fun x => f x y
Theorem: Set.bind_comm
Proof state before:
case a
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
⊢ ∀ (x : γ), (x ∈ s.bind fun x => t.bind fun x_1 => f x x_1) ↔ x ∈ t.bind fun y => s.bind fun x => f x y
Tactic:
intro z
Proof state after:
case a
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ s.bind fun x => t.bind fun x_1 => f x x_1) ↔ z ∈ t.bind fun y => s.bind fun x => f x y
Theorem: Set.bind_comm
Proof state before:
case a
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ s.bind fun x => t.bind fun x_1 => f x x_1) ↔ z ∈ t.bind fun y => s.bind fun x => f x y
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ s.bind fun x => t.bind fun x_1 => f x x_1) → z ∈ t.bind fun y => s.bind fun x => f x y

case a.mpr
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ t.bind fun y => s.bind fun x => f x y) → z ∈ s.bind fun x => t.bind fun x_1 => f x x_1
Theorem: Set.bind_comm
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ s.bind fun x => t.bind fun x_1 => f x x_1) → z ∈ t.bind fun y => s.bind fun x => f x y
Tactic:
intro ⟨x, hx, ⟨y, hy, hz⟩⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ t
hz : z ∈ (fun x_1 => f x x_1) y
⊢ z ∈ t.bind fun y => s.bind fun x => f x y
Theorem: Set.bind_comm
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
x : α
hx : x ∈ s
y : β
hy : y ∈ t
hz : z ∈ (fun x_1 => f x x_1) y
⊢ z ∈ t.bind fun y => s.bind fun x => f x y
Tactic:
refine ⟨y, hy, ⟨x, hx, hz⟩⟩
Proof state after:
no goals
Theorem: Set.bind_comm
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
⊢ (z ∈ t.bind fun y => s.bind fun x => f x y) → z ∈ s.bind fun x => t.bind fun x_1 => f x x_1
Tactic:
intro ⟨y, hy, ⟨x, hx, hz⟩⟩
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hz : z ∈ (fun x => f x y) x
⊢ z ∈ s.bind fun x => t.bind fun x_1 => f x x_1
Theorem: Set.bind_comm
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_3
γ : Sort u_1
f : α → β → Set γ
s : Set α
t : Set β
z : γ
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hz : z ∈ (fun x => f x y) x
⊢ z ∈ s.bind fun x => t.bind fun x_1 => f x x_1
Tactic:
refine ⟨x, hx, ⟨y, hy, hz⟩⟩
Proof state after:
no goals
Theorem: Set.bind_pure_comp
Proof state before:
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
⊢ (s.bind fun x => Set.pure (f x)) = Set.map f s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
⊢ ∀ (x : β), (x ∈ s.bind fun x => Set.pure (f x)) ↔ x ∈ Set.map f s
Theorem: Set.bind_pure_comp
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
⊢ ∀ (x : β), (x ∈ s.bind fun x => Set.pure (f x)) ↔ x ∈ Set.map f s
Tactic:
intro y
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) ↔ y ∈ Set.map f s
Theorem: Set.bind_pure_comp
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) ↔ y ∈ Set.map f s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) → y ∈ Set.map f s

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ s.bind fun x => Set.pure (f x)
Theorem: Set.bind_pure_comp
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) → y ∈ Set.map f s
Tactic:
intro ⟨x, hx, (h : y = f x)⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : y = f x
⊢ y ∈ Set.map f s
Theorem: Set.bind_pure_comp
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : y = f x
⊢ y ∈ Set.map f s
Tactic:
refine ⟨x, hx, h.symm⟩
Proof state after:
no goals
Theorem: Set.bind_pure_comp
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ s.bind fun x => Set.pure (f x)
Tactic:
intro ⟨x, hx, h⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ s.bind fun x => Set.pure (f x)
Theorem: Set.bind_pure_comp
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ s.bind fun x => Set.pure (f x)
Tactic:
refine ⟨x, hx, h.symm⟩
Proof state after:
no goals
Theorem: Set.pure_seq
Proof state before:
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
⊢ (Set.pure f).seq s = Set.map f s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
⊢ ∀ (x : β), x ∈ (Set.pure f).seq s ↔ x ∈ Set.map f s
Theorem: Set.pure_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
⊢ ∀ (x : β), x ∈ (Set.pure f).seq s ↔ x ∈ Set.map f s
Tactic:
intro y
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ (Set.pure f).seq s ↔ y ∈ Set.map f s
Theorem: Set.pure_seq
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ (Set.pure f).seq s ↔ y ∈ Set.map f s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ (Set.pure f).seq s → y ∈ Set.map f s

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ (Set.pure f).seq s
Theorem: Set.pure_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ (Set.pure f).seq s → y ∈ Set.map f s
Tactic:
intro ⟨_, rfl, h⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
h : y ∈ (fun f => Set.map f s) f
⊢ y ∈ Set.map f s
Theorem: Set.pure_seq
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
h : y ∈ (fun f => Set.map f s) f
⊢ y ∈ Set.map f s
Tactic:
exact h
Proof state after:
no goals
Theorem: Set.pure_seq
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ (Set.pure f).seq s
Tactic:
intro ⟨x, hx, h⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ (Set.pure f).seq s
Theorem: Set.pure_seq
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ (Set.pure f).seq s
Tactic:
refine ⟨f, rfl, ⟨x, hx, h⟩⟩
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
⊢ g.seq (f.seq s) = ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
⊢ ∀ (x : γ), x ∈ g.seq (f.seq s) ↔ x ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Theorem: Set.seq_assoc
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
⊢ ∀ (x : γ), x ∈ g.seq (f.seq s) ↔ x ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
intro z
Proof state after:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ g.seq (f.seq s) ↔ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Theorem: Set.seq_assoc
Proof state before:
case a
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ g.seq (f.seq s) ↔ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ g.seq (f.seq s) → z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s

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

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

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

case a.mp.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') x = g' y
Theorem: Set.seq_assoc
Proof state before:
case a.mp.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ x ∈ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
case a.mp.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') x = g' y
Tactic:
cases hy
Proof state after:
case a.mp.refl.right.right.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' ∘ f') x = g' (f' x)
Theorem: Set.seq_assoc
Proof state before:
case a.mp.refl.right.right.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' ∘ f') x = g' (f' x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.seq_assoc
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s → z ∈ g.seq (f.seq s)
Tactic:
intro ⟨gof,⟨go,⟨g',hg',hgo⟩,⟨f',hf',hgof'⟩⟩,⟨x,hx,hz⟩⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
gof : α → γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
hgof' : go f' = gof
x : α
hx : x ∈ s
hz : gof x = z
⊢ z ∈ g.seq (f.seq s)
Theorem: Set.seq_assoc
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
gof : α → γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
hgof' : go f' = gof
x : α
hx : x ∈ s
hz : gof x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hgof'
Proof state after:
case a.mpr.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : go f' x = z
⊢ z ∈ g.seq (f.seq s)
Theorem: Set.seq_assoc
Proof state before:
case a.mpr.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : go f' x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hgo
Proof state after:
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)