awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.join.join.destruct.destruct (map join SS).join.destruct.destruct
have nil : LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
  (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
  (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
  (Computation.destruct (destruct (join (join nil)))) (Computation.destruct (destruct (join (map join nil))))
Tactic: induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
Cleared hypotheses: SS
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (Computation.destruct (destruct (join (join WSeq.nil))))
    (Computation.destruct (destruct (join (map join WSeq.nil))))
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.join.join.destruct.destruct (map join SS).join.destruct.destruct
have nil₁ : ∀ (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct
Tactic: induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
Cleared hypotheses: SS
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (Computation.destruct (destruct (join (join WSeq.nil))))
    (Computation.destruct (destruct (join (map join WSeq.nil))))
nil₁ :
  ∀ (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.join.join.destruct.destruct (map join SS).join.destruct.destruct
have nil₂ : ∀ (SS : WSeq (WSeq (WSeq α))),
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.think.join.join.destruct.destruct (map join SS.think).join.destruct.destruct
Tactic: induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
Cleared hypotheses: SS
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append nil (S.think.append SS.join).join).destruct.destruct
    (append nil (S.think.join.append (map join SS).join)).destruct.destruct
have nil : (append nil (S.think.append SS.join).join).destruct.tail = (append nil (S.append SS.join).join).destruct
Tactic: refine ⟨nil, S, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
nil : (append WSeq.nil (S.think.append SS.join).join).destruct.tail = (append WSeq.nil (S.append SS.join).join).destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (S.think.append SS.join).join).destruct.destruct
    (append WSeq.nil (S.think.join.append (map join SS).join)).destruct.destruct
have nil₁ : (append WSeq.nil (S.think.join.append (map join SS).join)).destruct.tail =
  (append WSeq.nil (S.join.append (map join SS).join)).destruct
Tactic: refine ⟨nil, S, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append nil (S.append SS.join).join).destruct.destruct
    (append nil (S.join.append (map join SS).join)).destruct.destruct
have nil : LiftRelAux
  (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
  (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
  (append nil (append nil SS.join).join).destruct.destruct
  (append nil (append (join nil) (map join SS).join)).destruct.destruct
Tactic: induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (append WSeq.nil SS.join).join).destruct.destruct
    (append WSeq.nil (append (join WSeq.nil) (map join SS).join)).destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (S.append SS.join).join).destruct.destruct
    (append WSeq.nil (S.join.append (map join SS).join)).destruct.destruct
have nil₁ : ∀ (s : WSeq α) (S : WSeq (WSeq α)),
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil ((cons s S).append SS.join).join).destruct.destruct
    (append WSeq.nil ((cons s S).join.append (map join SS).join)).destruct.destruct
Tactic: induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct
have nil : LiftRelAux
  (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
  (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
      c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
  (append nil (S.append SS.join).join).destruct.destruct
  (append nil (S.join.append (map join SS).join)).destruct.destruct
Tactic: induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (S.append SS.join).join).destruct.destruct
    (append WSeq.nil (S.join.append (map join SS).join)).destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct
have cons : ∀ (a : α) (s : WSeq α),
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    ((cons a s).append (S.append SS.join).join).destruct.destruct
    ((cons a s).append (S.join.append (map join SS).join)).destruct.destruct
Tactic: induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind ((fun (y : WSeq β) ↦ y.bind g) ∘ f)
have simp : (map (map g) (map f s)).join.join ~ʷ join (map ((fun (y : WSeq β) ↦ (map g y).join) ∘ f) s)
Tactic: simp only [bind, map_join]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g) (map f s)).join.join ~ʷ join (map ((fun (y : WSeq β) ↦ (map g y).join) ∘ f) s)
have rw : (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join
Tactic: rw [← map_comp f (map g), ← Function.comp_def, comp_assoc, map_comp (map g ∘ f) join s]
-- Lean 4 proof step from Mathlib.Data.ZMod.Aut (goal)
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
have rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
Tactic: rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Aut (goal)
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
have rw₁ : HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) ((f : (a : ZMod n) → ZMod n) 1) =
  (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
Tactic: rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Aut (goal)
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
rw₁ :
  HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
have rw₂ : HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast ((f : (a : ZMod n) → ZMod n) 1) =
  (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
Tactic: rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Aut (goal)
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
rw₁ :
  HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
rw₂ :
  HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
have rw₃ : Eq (α := ZMod n) ((f : (a : ZMod n) → ZMod n) (HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast 1) : ZMod n)
  ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n) : ZMod n)
Tactic: rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Aut (goal)
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
rw₁ :
  HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
rw₂ :
  HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
rw₃ :
  Eq (α := ZMod n) ((f : (a : ZMod n) → ZMod n) (HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast 1) : ZMod n)
    ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n) : ZMod n)
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
have rw₄ : Eq (α := ZMod n) ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)) ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n))
Tactic: rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ a.val < n
have zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), a.val < 0
Tactic: cases n
Cleared hypotheses: n, inst, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), a.val < 0
⊢ a.val < n
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), a.val < n + 1
Tactic: cases n
Cleared hypotheses: n, inst, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
⊢ val (n := n) (↑a : ZMod n) = a % n
have zero : val (n := 0) (↑a : ZMod 0) = a % 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n a : ℕ
zero : val (n := 0) (↑a : ZMod 0) = a % 0
⊢ val (n := n) (↑a : ZMod n) = a % n
have succ : ∀ (n : ℕ), val (n := n + 1) (↑a : ZMod (n + 1)) = a % (n + 1)
Tactic: cases n
Cleared hypotheses: n