awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
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

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'
-- Module: Mathlib.Data.Seq.Parallel
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
⊢ a ∈ c

Tactic:
obtain ⟨ac, cs⟩ := this
-- Module: Mathlib.Data.Seq.Parallel
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 ∈ S

Tactic:
obtain ⟨ac, cs⟩ := this
-- Module: Mathlib.Data.Seq.Parallel
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)
ac : a ∈ c
cs : c ∈ S
⊢ C a

Tactic:
apply H _ cs _ ac
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
⊢ parallel S ~> a

Tactic:
fun _ ma' =>
  let ⟨_, cs, ac⟩ := exists_of_mem_parallel ma'
  H _ cs ac

Premises used: Computation.exists_of_mem_parallel, Computation.Promises, _private.0.Computation.parallel_promises.match_1, Eq
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ c.Terminates

Tactic:
haveI := terminates_of_mem ac
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : c.Terminates
⊢ (parallel S).Terminates

Tactic:
haveI := terminates_parallel cs
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this_1 : c.Terminates
this : (parallel S).Terminates
⊢ a ∈ parallel S

Tactic:
mem_of_promises _ (parallel_promises H)

Premises used: Computation.parallel_promises, Computation.mem_of_promises
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this_1 : c.Terminates
this : (parallel S).Terminates
⊢ a ∈ parallel S

Tactic:
exact mem_of_promises _ (parallel_promises H)

Premises used: Computation.parallel_promises, Computation.mem_of_promises
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
H : WSeq.LiftRel Equiv S T
⊢ (∀ s ∈ S, s ~> a) ↔ ∀ t ∈ T, t ~> a

Tactic:
⟨fun h1 _ tT =>
    let ⟨_, sS, se⟩ := WSeq.exists_of_liftRel_right H tT
    (promises_congr se _).1 (h1 _ sS),
    fun h2 _ sS =>
    let ⟨_, tT, se⟩ := WSeq.exists_of_liftRel_left H sS
    (promises_congr se _).2 (h2 _ tT)⟩

Premises used: Iff.mpr, _private.0.Computation.parallel_congr_lem.match_1, Computation.promises_congr, Computation.Promises, _private.0.Computation.parallel_congr_lem.match_2, Iff.intro, Stream'.WSeq.exists_of_liftRel_right, Iff.mp, Stream'.WSeq.exists_of_liftRel_left
-- Module: Mathlib.Data.Seq.Parallel
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 = a'

Tactic:
have aa := parallel_promises h1 h
-- Module: Mathlib.Data.Seq.Parallel
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'
rw : a ∈ parallel T
⊢ a' ∈ parallel T

Tactic:
rw [← aa]
-- Module: Mathlib.Data.Seq.Parallel
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 S

Tactic:
rw [← aa] at h
-- Module: Mathlib.Data.Seq.Parallel
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'
h₁ : a ∈ parallel S
⊢ a = a'

Tactic:
rw [← aa] at h
-- Module: Mathlib.Data.Seq.Parallel
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

Tactic:
let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_left H sS
      let aT := (st _).1 as
      mem_parallel h2 tT aT

Premises used: Computation.exists_of_mem_parallel, Computation.parallel, Membership.mem, Computation.mem_parallel, _private.0.Computation.parallel_empty.match_2, _private.0.Computation.parallel_congr_left.match_1, Iff.mp, Stream'.WSeq.exists_of_liftRel_left
-- Module: Mathlib.Data.Seq.Parallel
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

Tactic:
exact
      let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_left H sS
      let aT := (st _).1 as
      mem_parallel h2 tT aT
-- Module: Mathlib.Data.Seq.Parallel
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 = a'

Tactic:
have aa := parallel_promises h2 h
-- Module: Mathlib.Data.Seq.Parallel
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'
rw : a ∈ parallel S
⊢ a' ∈ parallel S

Tactic:
rw [← aa]
-- Module: Mathlib.Data.Seq.Parallel
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 T

Tactic:
rw [← aa] at h
-- Module: Mathlib.Data.Seq.Parallel
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'
h₁ : a ∈ parallel T
⊢ a = a'

Tactic:
rw [← aa] at h
-- Module: Mathlib.Data.Seq.Parallel
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

Tactic:
let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_right H sS
      let aT := (st _).2 as
      mem_parallel h1 tT aT

Premises used: Iff.mpr, Computation.exists_of_mem_parallel, Computation.parallel, Membership.mem, Computation.mem_parallel, _private.0.Computation.parallel_empty.match_2, _private.0.Computation.parallel_congr_left.match_2, Stream'.WSeq.exists_of_liftRel_right
-- Module: Mathlib.Data.Seq.Parallel
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

Tactic:
exact
      let ⟨s, sS, as⟩ := exists_of_mem_parallel h
      let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_right H sS
      let aT := (st _).2 as
      mem_parallel h1 tT aT
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S T : WSeq (Computation α)
a : α
h2 : ∀ t ∈ T, t ~> a
H : WSeq.LiftRel Equiv S T
⊢ parallel S ~ parallel T

Tactic:
parallel_congr_left ((parallel_congr_lem H).2 h2) H

Premises used: Iff.mpr, Computation.parallel_congr_left, Computation.parallel_congr_lem
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ accumulate s x = ⋃ (y : α), ⋃ (_ : y ≤ x), s y

Tactic:
rfl

Premises used: Set.accumulate, rfl
-- Module: Mathlib.Data.Set.Accumulate
Goal:
β : Type u_2
s : ℕ → Set β
n : ℕ
simp_rw : accumulate s n = ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k
⊢ accumulate s n = ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s k

Tactic:
simp_rw [Nat.lt_add_one_iff, accumulate]

Premises used: Nat.lt_add_one_iff, Set.accumulate
-- Module: Mathlib.Data.Set.Accumulate
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
simp_rw₁ : (∃ (i : α) (_ : i ≤ x), z ∈ s i) ↔ ∃ y ≤ x, z ∈ s y
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

Premises used: exists_prop, Set.mem_iUnion₂, Set.accumulate_def
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ s x ⊆ accumulate s x

Tactic:
fun _ => mem_biUnion le_rfl

Premises used: le_rfl, Set.Mem, Set.mem_biUnion, Set.Subset, Set.accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : LE α
x : α
⊢ accumulate s x ⊆ ⋃ (i : α), s i

Tactic:
(biUnion_subset_biUnion_left (subset_univ _)).trans_eq (biUnion_univ _)

Premises used: LE.le.trans_eq, Set.Mem, Set.subset_univ, Set.biUnion_univ, Set.accumulate, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Monotone (accumulate s)

Tactic:
fun _ _ hxy =>
  biUnion_subset_biUnion_left fun _ hz => le_trans hz hxy

Premises used: Set.Mem, Monotone, Set.accumulate, Set.biUnion_subset_biUnion_left, le_trans
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x y : α
h : x ≤ y
⊢ accumulate s x ⊆ accumulate s y

Tactic:
monotone_accumulate h

Premises used: Set.monotone_accumulate
-- Module: Mathlib.Data.Set.Accumulate
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)
h₂ : Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y)
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)

Tactic:
iUnion₂_subset fun y hy => monotone_accumulate hy

Premises used: Set.iUnion₂_subset, Set.monotone_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y) (⋃ (y : α), ⋃ (_ : y ≤ x), s y)

Tactic:
exact iUnion₂_subset fun y hy => monotone_accumulate hy

Premises used: Set.iUnion₂_subset, Set.monotone_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y)

Tactic:
iUnion₂_mono fun y _ => subset_accumulate

Premises used: Set.iUnion₂_mono, Set.subset_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
x : α
⊢ Subset.{u_2} (α := Set β) (⋃ (y : α), ⋃ (_ : y ≤ x), s y) (⋃ (y : α), ⋃ (_ : y ≤ x), accumulate s y)

Tactic:
exact iUnion₂_mono fun y _ => subset_accumulate

Premises used: Set.iUnion₂_mono, Set.subset_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : Subset.{u_2} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)
h₂ : Subset.{u_2} (α := Set β) (⋃ (x : α), s x) (⋃ (x : α), accumulate s x)
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
h₁ : ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ (i : α), x ∈ s i
⊢ Subset.{u_2} (α := Set β) (⋃ (x : α), accumulate s x) (⋃ (x : α), s x)

Tactic:
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]

Premises used: Set.subset_def, Set.mem_iUnion, Set.mem_accumulate, exists_imp
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
z : β
x x' : α
h₁ : x' ≤ x → ∀ (hz : z ∈ s x'), ∃ (i : α), z ∈ s i
⊢ x' ≤ x ∧ z ∈ s x' → ∃ (i : α), z ∈ s i

Tactic:
⟨_, hz⟩
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
z : β
x x' : α
left : x' ≤ x
hz : z ∈ s x'
⊢ ∃ (i : α), z ∈ s i

Tactic:
⟨x', hz⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
z : β
x x' : α
left : x' ≤ x
hz : z ∈ s x'
⊢ ∃ (i : α), z ∈ s i

Tactic:
exact ⟨x', hz⟩
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Subset.{u_2} (α := Set β) (⋃ (x : α), s x) (⋃ (x : α), accumulate s x)

Tactic:
iUnion_mono fun i => subset_accumulate

Premises used: Set.iUnion_mono, Set.subset_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
⊢ Subset.{u_2} (α := Set β) (⋃ (x : α), s x) (⋃ (x : α), accumulate s x)

Tactic:
exact iUnion_mono fun i => subset_accumulate

Premises used: Set.iUnion_mono, Set.subset_accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
s : α → Set β
⊢ accumulate s ⊥ = s ⊥

Tactic:
simp [Set.accumulate_def]

Premises used: Set.accumulate_def
-- Module: Mathlib.Data.Set.Accumulate
Goal:
β : Type u_2
s : ℕ → Set β
⊢ accumulate s 0 = s 0

Tactic:
simp [accumulate_def]

Premises used: Set.accumulate_def
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
apply : ∀ (x : β) (hx : x ∈ accumulate s i), x ∉ s j
⊢ Disjoint (accumulate s i) (s j)

Tactic:
apply disjoint_left.2 (fun x hx ↦ ?_)

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : x ∈ accumulate s i
⊢ ∃ i_1 ≤ i, x ∈ s i_1

Tactic:
simp only [accumulate, mem_iUnion, exists_prop] at hx

Premises used: Set.mem_iUnion, exists_prop, Set.accumulate
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
hx : ∃ i_1 ≤ i, x ∈ s i_1
rcases : ∀ (k : α) (hk : k ≤ i) (hx : x ∈ s k), x ∉ s j
⊢ x ∉ s j

Tactic:
rcases hx with ⟨k, hk, hx⟩
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j

Tactic:
disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Premises used: Set.disjoint_left, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
β : Type u_2
s : α → Set β
inst : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j

Tactic:
exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Premises used: Set.disjoint_left, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ accumulate u (n + 1) = accumulate u n ∪ u (n + 1)

Tactic:
biUnion_le_succ u n

Premises used: Set.accumulate, Set.biUnion_le_succ
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
f : ℕ → Set α
h : ∀ (n : ℕ) (x : α), Membership.mem (γ := Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α) x ↔ x ∈ accumulate f n
⊢ (⇑(partialSups f) : (a : ℕ) → Set α) = accumulate f

Tactic:
ext n
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
x : α
⊢ Membership.mem (γ := Set α) ((partialSups f : (a : ℕ) → Set α) n : Set α) x ↔ x ∈ accumulate f n

Tactic:
simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff]

Premises used: partialSups_eq_sup_range, Set.accumulate, Nat.lt_succ_iff
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : accumulate s 0 ⊆ s 0
⊢ ∃ (m : ℕ), accumulate s 0 ⊆ s m

Tactic:
use 0
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ accumulate s 0 ⊆ s 0

Tactic:
simp [accumulate_def]

Premises used: Set.accumulate_def
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n : ℕ
hn : ∃ (m : ℕ), accumulate s n ⊆ s m
succ : ∀ (m : ℕ) (hm : accumulate s n ⊆ s m), ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
⊢ ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m

Tactic:
obtain ⟨m, hm⟩ := hn
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
succ :
  ∀ (k : ℕ) (hk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s m) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s (n + 1)) (s k)),
    ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
⊢ ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m

Tactic:
obtain ⟨k, hk⟩ := hd m (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
simp : accumulate s n ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s (n + 1) ⊆ s k

Tactic:
simp
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s n ⊆ s k ∧ s (n + 1) ⊆ s k

Tactic:
grind
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m

Tactic:
exact ⟨k, by simp; grind⟩
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
n : ℕ
zero : ∃ (m : ℕ), accumulate s 0 ⊆ s m
succ : ∀ (n : ℕ) (hn : ∃ (m : ℕ), accumulate s n ⊆ s m), ∃ (m : ℕ), accumulate s (n + 1) ⊆ s m
⊢ ∃ (m : ℕ), accumulate s n ⊆ s m

Tactic:
induction n with
  | zero => use 0; simp [accumulate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    simp at hk
    exact ⟨k, by simp; grind⟩

Premises used: Set.accumulate_def
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
⊢ Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (accumulate s)

Tactic:
monotone_accumulate.directed_le

Premises used: Set.monotone_accumulate, Monotone.directed_le
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
⊢ (∃ (n : ℕ), accumulate s n = univ) ↔ ∃ (n : ℕ), s n = univ

Tactic:
⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩

Premises used: _private.0.Set.exists_accumulate_eq_univ_iff_of_directed.match_1, Set.subset_univ, Set.univ, Exists, subset_antisymm, Eq.le, Set.accumulate, Iff.intro, Exists.intro, Set.subset_accumulate, LE.le.trans, Eq.symm, Eq
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
refine : (∃ (n : ℕ), accumulate s n = univ) → ∃ (n : ℕ), s n = univ
⊢ (∃ (n : ℕ), accumulate s n = univ) ↔ ∃ (n : ℕ), s n = univ

Tactic:
refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n,
    subset_antisymm (subset_univ _) (hn.symm.le.trans subset_accumulate)⟩⟩
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
contrapose! : (∀ (n : ℕ), s n ≠ univ) → ∀ (n : ℕ), accumulate s n ≠ univ
⊢ (∃ (n : ℕ), accumulate s n = univ) → ∃ (n : ℕ), s n = univ

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n : ℕ
obtain : ∀ (m : ℕ) (hm : accumulate s n ⊆ s m), accumulate s n ≠ univ
⊢ accumulate s n ≠ univ

Tactic:
obtain ⟨m, hm⟩ := exists_subset_accumulate_of_directed hd n

Premises used: Set.exists_subset_accumulate_of_directed
-- Module: Mathlib.Data.Set.Accumulate
Goal:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
h : ∀ (n : ℕ), s n ≠ univ
n m : ℕ
hm : accumulate s n ⊆ s m
⊢ accumulate s n ≠ univ

Tactic:
grind
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Injective (α := Set α) Membership.mem

Tactic:
injective_id

Premises used: Set.Mem, Function.injective_id, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Surjective (α := Set α) Membership.mem

Tactic:
surjective_id

Premises used: Set.Mem, Function.surjective_id, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Bijective (α := Set α) Membership.mem

Tactic:
bijective_id

Premises used: Function.bijective_id, Set.Mem, Set
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) ⊤ univ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) ⊥ ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α → Set α → Set α) (fun (x1 x2 : Set α) ↦ x1 ⊔ x2) fun (x1 x2 : Set α) ↦ x1 ∪ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α → Set α → Set α) (fun (x1 x2 : Set α) ↦ x1 ⊓ x2) fun (x1 x2 : Set α) ↦ x1 ∩ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α → Set α → Prop) (fun (x1 x2 : Set α) ↦ x1 ≤ x2) fun (x1 x2 : Set α) ↦ x1 ⊆ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α → Set α → Prop) (fun (x1 x2 : Set α) ↦ x1 < x2) fun (x1 x2 : Set α) ↦ x1 ⊂ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s ≤ t ↔ s ⊆ t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
⊢ s < t ↔ s ⊂ t

Tactic:
Iff.rfl

Premises used: Iff.rfl