awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
x : Seq1 (Seq1 α)
s : Seq (Seq1 (Seq1 α))
cons :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons x s).join.join.destruct,
    (Seq.cons x.join (Seq.map join s)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons x s).join.join.destruct,
    (Seq.map join (Seq.cons x s)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
S : Seq1 (Seq1 α)
SS : Seq (Seq1 (Seq1 α))
obtain :
  ∀ (s : Seq1 α) (S : Seq (Seq1 α)),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (s, S) SS).join.join.destruct,
      (Seq.cons (join (s, S)) (Seq.map join SS)).join.destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons S SS).join.join.destruct,
    (Seq.cons S.join (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
obtain ⟨s, S⟩ := S
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
s : Seq1 α
S : Seq (Seq1 α)
obtain :
  ∀ (x : α) (s : Seq α),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons ((x, s), S) SS).join.join.destruct,
      (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons (s, S) SS).join.join.destruct,
    (Seq.cons (join (s, S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
obtain ⟨x, s⟩ := s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
simp :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, s.append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) (Seq.cons ((x, s), S) SS).join.join.destruct,
    (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
simp only [Seq.join_cons, join_append, destruct_cons]

Premises used: Stream'.Seq.join_append, Stream'.Seq.join_cons, Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
s : Seq α
nil :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, append Seq.nil (S.join.append SS.join.join)),
    (Seq.cons (join ((x, Seq.nil), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False
cons :
  ∀ (x_1 : α) (s : Seq α),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
      some (x, (Seq.cons x_1 s).append (S.join.append SS.join.join)),
      (Seq.cons (join ((x, Seq.cons x_1 s), S)) (Seq.map join SS)).join.destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
    | x, x_2 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, s.append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
simp :
  ∃ (s : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    S.join.append SS.join.join = s.append SS_2.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_2).join
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) some (x, append nil (S.join.append SS.join.join)),
    (Seq.cons (join ((x, nil), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x x_1 : α
s : Seq α
cons :
  ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    Seq.cons x_1 (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
      Seq.cons x_1 (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    some (x, (Seq.cons x_1 s).append (S.join.append SS.join.join)),
    (Seq.cons (join ((x, Seq.cons x_1 s), S)) (Seq.map join SS)).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_2 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ ∃ (s : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    S.join.append SS.join.join = s.append SS_2.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_2).join

Tactic:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ ∃ (s : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    S.join.append SS.join.join = s.append SS_2.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_2).join

Tactic:
exact ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ ∃ (s : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    S.join.append SS.join.join = s.append SS_2.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_2).join

Tactic:
case nil => exact ⟨_, _, rfl, rfl⟩

Premises used: Stream'.Seq.nil
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join

Tactic:
⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩

Premises used: Stream'.Seq.join, And.intro, Stream'.Seq.cons, Exists.intro, Stream'.Seq.append
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
refine_1 : Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join
refine_2 :
  Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) =
    (Seq.cons x (s.append S.join)).append (Seq.map join SS).join
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_2.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_2).join

Tactic:
refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x_1 x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) =
    (Seq.cons x (s.append S.join)).append (Seq.map join SS).join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop) SS.join.join.destruct, (Seq.map join SS).join.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_1 : Seq α) (SS : Seq (Seq1 (Seq1 α))), s = s_1.append SS.join.join ∧ s' = s_1.append (Seq.map join SS).join
  | x, x_1 => False

Tactic:
case nil =>
          cases SS <;> simp
          case cons S SS =>
            obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
            simp only [Seq.join_cons, join_append, destruct_cons]
            cases s <;> simp
            case nil => exact ⟨_, _, rfl, rfl⟩
            case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp

Premises used: Stream'.Seq.join_append, Stream'.Seq.nil, Stream'.Seq.join_cons, Stream'.Seq.destruct_cons, Stream'.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    s.append SS.join.join = s_1.append SS_2.join.join ∧
      s.append (Seq.map join SS).join = s_1.append (Seq.map join SS_2).join

Tactic:
⟨s, SS, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS_1 : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
x : α
s : Seq α
⊢ ∃ (s_1 : Seq α) (SS_2 : Seq (Seq1 (Seq1 α))),
    s.append SS.join.join = s_1.append SS_2.join.join ∧
      s.append (Seq.map join SS).join = s_1.append (Seq.map join SS_2).join

Tactic:
exact ⟨s, SS, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
⊢ BisimO
    (fun (s1 s2 : Seq α) ↦
      ∃ (s : Seq α) (SS : Seq (Seq1 (Seq1 α))), s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    s1.destruct s2.destruct

Tactic:
exact
      match s1, s2, h with
      | _, _, ⟨s, SS, rfl, rfl⟩ => by
        cases s <;> simp
        case nil =>
          cases SS <;> simp
          case cons S SS =>
            obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
            simp only [Seq.join_cons, join_append, destruct_cons]
            cases s <;> simp
            case nil => exact ⟨_, _, rfl, rfl⟩
            case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
        case cons _ s => exact ⟨s, SS, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ (s : Seq α) (SS_1 : Seq (Seq1 (Seq1 α))),
    SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Tactic:
⟨nil, SS, ?_, ?_⟩

Premises used: Stream'.Seq.nil, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
r : SS.join.join = append nil SS.join.join
r₁ : (Seq.map join SS).join = append nil (Seq.map join SS).join
⊢ ∃ (s : Seq α) (SS_1 : Seq (Seq1 (Seq1 α))),
    SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Tactic:
refine ⟨nil, SS, ?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = append nil SS.join.join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ (Seq.map join SS).join = append nil (Seq.map join SS).join

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
obtain : ∀ (a : α) (s : Seq α), (bind (a, s) f).bind g = bind (a, s) fun (x : α) ↦ (f x).bind g
⊢ (s.bind f).bind g = s.bind fun (x : α) ↦ (f x).bind g

Tactic:
obtain ⟨a, s⟩ := s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
simp :
  (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
⊢ (bind (a, s) f).bind g = bind (a, s) fun (x : α) ↦ (f x).bind g

Tactic:
simp only [bind, map_pair, map_join]

Premises used: Stream'.Seq1.bind, Stream'.Seq1.map_join, Stream'.Seq1.map_pair
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
rw :
  (join (map g (f a), Seq.map (map g ∘ f) s)).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)
⊢ (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)

Tactic:
rw [← map_comp]

Premises used: Stream'.Seq.map_comp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
simp : (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join =
    join ((map g (f a)).join, Seq.map (fun (x : α) ↦ (map g (f x)).join) s)

Tactic:
simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

Premises used: rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
rw : (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)

Tactic:
rw [map_comp _ join]

Premises used: Stream'.Seq.map_comp, Stream'.Seq1.join
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
generalize : ∀ (SS : Seq (Seq1 (Seq1 γ))), (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))

Tactic:
generalize Seq.map (map g ∘ f) s = SS

Premises used: Function.comp, Stream'.Seq.map, Stream'.Seq1.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
rcases :
  ∀ (S : Seq (Seq1 γ)) (a : γ) (s : Seq γ), (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)

Tactic:
rcases map g (f a) with ⟨⟨a, s⟩, S⟩

Premises used: Stream'.Seq1.map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)

Tactic:
?_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)

Tactic:
?_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s_1 : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
nil : (join (((a, Seq.nil), S), SS)).join = join (join ((a, Seq.nil), S), Seq.map join SS)
cons :
  ∀ (x : γ) (s_1 : Seq γ),
    (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)
⊢ (join (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)

Tactic:
induction s using recOn with | nil => ?_ | cons x s_1 => ?_

Premises used: Stream'.Seq.nil, Stream'.Seq.recOn, Stream'.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
⊢ (join (((a, nil), nil), SS)).join = join (join ((a, nil), nil), Seq.map join SS)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
?_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
nil :
  ∀ (x_1 : Seq1 γ) (s_2 : Seq (Seq1 γ)),
    (join (((a, Seq.nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, Seq.nil), Seq.cons x_1 s_2), Seq.map join SS)
⊢ (join (((a, Seq.nil), S), SS)).join = join (join ((a, Seq.nil), S), Seq.map join SS)

Tactic:
induction S using recOn with | nil => simp | cons x_1 s_2 => ?_

Premises used: Stream'.Seq.nil, Stream'.Seq.recOn, Stream'.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), nil), SS)).join = join (join ((a, Seq.cons x s_1), nil), Seq.map join SS)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
?_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
cons :
  ∀ (x_1 : Seq1 γ) (s_2 : Seq (Seq1 γ)),
    (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
      join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)

Tactic:
induction S using recOn with | nil => simp | cons x_1 s_2 => ?_

Premises used: Stream'.Seq.nil, Stream'.Seq.recOn, Stream'.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
nil :
  ∀ (x : γ) (t : Seq γ),
    (join (((a, Seq.nil), Seq.cons (x, t) s_2), SS)).join =
      join (join ((a, Seq.nil), Seq.cons (x, t) s_2), Seq.map join SS)
⊢ (join (((a, Seq.nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, Seq.nil), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
obtain ⟨x, t⟩ := x_1
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
nil :
  (join (((a, Seq.nil), Seq.cons (x, Seq.nil) s_2), SS)).join =
    join (join ((a, Seq.nil), Seq.cons (x, Seq.nil) s_2), Seq.map join SS)
nil₁ :
  ∀ (x_1 : γ) (s : Seq γ),
    (join (((a, Seq.nil), Seq.cons (x, Seq.cons x_1 s) s_2), SS)).join =
      join (join ((a, Seq.nil), Seq.cons (x, Seq.cons x_1 s) s_2), Seq.map join SS)
⊢ (join (((a, Seq.nil), Seq.cons (x, t) s_2), SS)).join =
    join (join ((a, Seq.nil), Seq.cons (x, t) s_2), Seq.map join SS)

Tactic:
cases t
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
⊢ (join (((a, nil), Seq.cons (x, nil) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, nil) s_2), Seq.map join SS)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x x_1 : γ
s_1 : Seq γ
⊢ (join (((a, nil), Seq.cons (x, Seq.cons x_1 s_1) s_2), SS)).join =
    join (join ((a, nil), Seq.cons (x, Seq.cons x_1 s_1) s_2), Seq.map join SS)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
cons :
  ∀ (y : γ) (t : Seq γ),
    (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
      join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
obtain ⟨y, t⟩ := x_1