awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
⊢ C a
have this₁ : (parallel T).Terminates
Tactic: haveI : Terminates (parallel T) := (terminates_map_iff _ _).1 ⟨⟨_, h'⟩⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
⊢ C a
have rcases : (a' : α) → (c : Computation α) → (e : (parallel T).get = (a', c)) → C a
Tactic: rcases e : get (parallel T) with ⟨a', c⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
⊢ a ∈ c ∧ c ∈ S
have rcases : ∀ (d : α × Computation α) (dT : d ∈ parallel T) (cd : d.1 = a), a ∈ c ∧ c ∈ S
Tactic: rcases exists_of_mem_map h' with ⟨d, dT, cd⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
d : α × Computation α
dT : d ∈ parallel T
cd : d.1 = a
⊢ a ∈ c ∧ c ∈ S
have e₁ : d = (a', c)
Tactic: rw [get_eq_of_mem _ dT] at e
Cleared hypotheses: e, dT, cd
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
d : α × Computation α
e : d = (a', c)
dT : d ∈ parallel T
cd : d.1 = a
⊢ a ∈ c ∧ c ∈ S
have dT₁ : (a', c) ∈ parallel T
Tactic: cases e
Cleared hypotheses: d, e, dT, cd
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
d : α × Computation α
e : d = (a', c)
dT : d ∈ parallel T
cd : d.1 = a
dT₁ : (a', c) ∈ parallel T
⊢ a ∈ c ∧ c ∈ S
have cd₁ : (a', c).1 = a
Tactic: cases e
Cleared hypotheses: d, e, dT, cd
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
dT : (a', c) ∈ parallel T
cd : a' = a
⊢ a ∈ c ∧ c ∈ S
have dT₁ : (a, c) ∈ parallel T
Tactic: cases cd
Cleared hypotheses: a', dT, cd
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
⊢ a ∈ c ∧ c ∈ S
have refl : ∀ (d' : Computation (α × Computation α)) (dT' : d' ∈ T) (ad' : (a, c) ∈ d'), a ∈ c ∧ c ∈ S
Tactic: rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
⊢ a ∈ c ∧ c ∈ S
have refl : ∀ (c' : Computation α) (cs' : c' ∈ S) (e' : map (fun (a : α) ↦ (a, c')) c' = d'), a ∈ c ∧ c ∈ S
Tactic: rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
⊢ a ∈ c ∧ c ∈ S
have ad'₁ : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
Tactic: rw [← e'] at ad'
Cleared hypotheses: ad', cs', e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
⊢ a ∈ c ∧ c ∈ S
have refl : ∀ (a' : α) (ac' : a' ∈ c') (e' : (a', c') = (a, c)), a ∈ c ∧ c ∈ S
Tactic: rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e'_1 : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
e' : (a', c') = (a, c)
⊢ a ∈ c ∧ c ∈ S
have i1 : a' = a
Tactic: injection e' with i1 i2
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e'_1 : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
e' : (a', c') = (a, c)
i1 : a' = a
⊢ a ∈ c ∧ c ∈ S
have i2 : c' = c
Tactic: injection e' with i1 i2
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c ∧ c ∈ S
have refl : a ∈ c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
refl : a ∈ c
⊢ a ∈ c ∧ c ∈ S
have refl₁ : c ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c
have refl : ∀ (ac' : a ∈ c') (i1 : a' = a) (i2 : c' = c), a ∈ c
Tactic: rwa [i1, i2] at ac'
Cleared hypotheses: ac', i1, i2
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
refl : ∀ (ac' : a ∈ c') (i1 : a' = a) (i2 : c' = c), a ∈ c
⊢ a ∈ c
have refl₁ : ∀ (ac' : a ∈ c) (i1 : a' = a) (i2 : c' = c), a ∈ c
Tactic: rwa [i1, i2] at ac'
Cleared hypotheses: ac', i1, i2
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ c ∈ S
have refl : ∀ (cs' : c ∈ S) (e' : map (fun (a : α) ↦ (a, c')) c' = d') (a' : α) (ac' : a' ∈ c') (i1 : a' = a) (i2 : c' = c), c ∈ S
Tactic: rwa [i2] at cs'
Cleared hypotheses: cs', e', a', ac', i1, i2
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
⊢ C a
have this₁ : a ∈ c ∧ c ∈ S
Tactic: have : a ∈ c ∧ c ∈ S := by
    rcases exists_of_mem_map h' with ⟨d, dT, cd⟩
    rw [get_eq_of_mem _ dT] at e
    cases e
    dsimp at cd
    cases cd
    rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩
    rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩
    rw [← e'] at ad'
    rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩
    injection e' with i1 i2
    constructor
    · rwa [i1, i2] at ac'
    · rwa [i2] at cs'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this_2 : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
this : a ∈ c ∧ c ∈ S
⊢ C a
have ac : a ∈ c
Tactic: obtain ⟨ac, cs⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this_2 : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
this : a ∈ c ∧ c ∈ S
ac : a ∈ c
⊢ C a
have cs : c ∈ S
Tactic: obtain ⟨ac, cs⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S
have this : c.Terminates
Tactic: haveI := terminates_of_mem ac
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : c.Terminates
⊢ a ∈ parallel S
have this₁ : (parallel S).Terminates
Tactic: haveI := terminates_parallel cs
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel S
⊢ a' ∈ parallel T
have aa : a = a'
Tactic: have aa := parallel_promises h1 h
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T
have rw : a ∈ parallel T
Tactic: rw [← aa]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
have h₁ : a ∈ parallel S
Tactic: rw [← aa] at h
Cleared hypotheses: h, aa
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel T
⊢ a' ∈ parallel S
have aa : a = a'
Tactic: have aa := parallel_promises h2 h
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S
have rw : a ∈ parallel S
Tactic: rw [← aa]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h1 : ∀ s ∈ S, s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ t ∈ T, t ~> a := ⋯
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
have h₁ : a ∈ parallel T
Tactic: rw [← aa] at h
Cleared hypotheses: h, aa
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
β : Type u_2
s : ℕ → Set β
n : ℕ
⊢ accumulate s n = ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s k
have simp_rw : accumulate s n = ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k
Tactic: simp_rw [Nat.lt_add_one_iff, accumulate]
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y
have simp_rw : Membership.mem (γ := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) z ↔ ∃ y ≤ x, z ∈ s y
Tactic: simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
z : β
simp_rw : Membership.mem (γ := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) z ↔ ∃ y ≤ x, z ∈ s y
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y
have simp_rw₁ : (∃ (i : α) (_ : i ≤ x), z ∈ s i) ↔ ∃ y ≤ x, z ∈ s y
Tactic: simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)
have h₁ : Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
h₁ : Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)
have h₂ : Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
have h₁ : Subset.{u_2} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : Subset.{u_2} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
have h₂ : Subset.{u_2} (α := Set β) (⋃ (x : α), s x) (⋃ (x : α), accumulate s x)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Subset.{u_2} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
have h₁ : ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ (i : α), x ∈ s i
Tactic: simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
-- Lean 4 proof step from Mathlib.Data.Set.Accumulate (goal)
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
z : β
x x' : α
⊢ x' ≤ x ∧ z ∈ s x' → ∃ (i : α), z ∈ s i
have h₁ : x' ≤ x → ∀ (hz : z ∈ s x'), ∃ (i : α), z ∈ s i
Tactic: ⟨_, hz⟩