awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l))
hr :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (node v l r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g (node v l r)))
have node : Eq (α := Functor.Comp G F (Tree γ))
  (node <$> (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) v <*>
      Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l) <*>
    Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
  (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> (node <$> g v <*> traverse g l <*> traverse g r)))
Tactic: rw [traverse, hl, hr, traverse]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l))
hr :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
⊢ Eq (α := Functor.Comp G F (Tree γ))
    (node <$> (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) v <*>
        Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> (node <$> g v <*> traverse g l <*> traverse g r)))
have node : Eq (α := Functor.Comp G F (Tree γ))
  (Functor.Comp.mk
    ((fun (a : β) (x x_1 : Tree β) ↦ node <$> f a <*> traverse f x <*> traverse f x_1) <$> g v <*> traverse g l <*>
      traverse g r))
  (Functor.Comp.mk
    ((fun (a : β) (x x_1 : Tree β) ↦ traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r))
Tactic: simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
t : Tree α
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) t)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g t))
have nil : Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) nil)
  (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g nil))
Tactic: induction t with
  | nil => rw [traverse, traverse, map_pure, traverse]; rfl
  | node v l r hl hr =>
    rw [traverse, hl, hr, traverse]
    simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]
    rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
t : Tree α
nil :
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) Tree.nil)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g Tree.nil))
⊢ Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) t)
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g t))
have node : ∀ (v : α) (l r : Tree α)
  (hl :
    Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) l)
      (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g l)))
  (hr :
    Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) r)
      (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g r))),
  Eq (α := Functor.Comp G F (Tree γ)) (traverse (Functor.Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (node v l r))
    (Functor.Comp.mk ((fun (x : Tree β) ↦ traverse f x) <$> traverse g (node v l r)))
Tactic: induction t with
  | nil => rw [traverse, traverse, map_pure, traverse]; rfl
  | node v l r hl hr =>
    rw [traverse, hl, hr, traverse]
    simp only [Function.comp_def, Function.comp_apply, Functor.Comp.map_mk, Functor.map_map,
      Comp.seq_mk, seq_map_assoc, map_seq]
    rfl
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) nil) (pure (map f nil))
have nil : Eq (α := Id (Tree β)) (pure nil) (pure (map f nil))
Tactic: rw [traverse, map]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
nil : Eq (α := Id (Tree β)) (pure Tree.nil) (pure (map f Tree.nil))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) Tree.nil) (pure (map f Tree.nil))
have nil₁ : Eq.{u_2 + 1} (α := Id (Tree β)) (pure Tree.nil) (pure Tree.nil)
Tactic: rw [traverse, map]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (node v l r)) (pure (map f (node v l r)))
have node : Eq (α := Id (Tree β)) (node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
  (pure (map f (node v l r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₁ : Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₂ : Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₃ : Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₄ : Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₅ : Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₅ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₆ : Eq (α := Id (Tree β)) (Tree.node (f v) <$> pure (map f l) <*> pure (map f r))
  (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₅ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₆ :
  Eq (α := Id (Tree β)) (Tree.node (f v) <$> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₇ : Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l)) <*> pure (map f r)) (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₅ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₆ :
  Eq (α := Id (Tree β)) (Tree.node (f v) <$> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₇ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l)) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₈ : Eq (α := Id (Tree β)) (Tree.node (f v) (map f l) <$> pure (map f r)) (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
v : α
l r : Tree α
hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l))
hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))
node :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (map f (Tree.node v l r)))
node₁ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> traverse (pure ∘ f) l <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₂ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> traverse (pure ∘ f) r)
    (pure (Tree.node (f v) (map f l) (map f r)))
node₃ :
  Eq (α := Id (Tree β)) (Tree.node <$> (pure ∘ f) v <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₄ :
  Eq (α := Id (Tree β)) (Tree.node <$> pure (f v) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₅ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v)) <*> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₆ :
  Eq (α := Id (Tree β)) (Tree.node (f v) <$> pure (map f l) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₇ :
  Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l)) <*> pure (map f r))
    (pure (Tree.node (f v) (map f l) (map f r)))
node₈ :
  Eq (α := Id (Tree β)) (Tree.node (f v) (map f l) <$> pure (map f r)) (pure (Tree.node (f v) (map f l) (map f r)))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) (Tree.node v l r)) (pure (map f (Tree.node v l r)))
have node₉ : Eq (α := Id (Tree β)) (pure (Tree.node (f v) (map f l) (map f r))) (pure (Tree.node (f v) (map f l) (map f r)))
Tactic: rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) t) (pure (map f t))
have nil : Eq (α := Id (Tree β)) (traverse (pure ∘ f) nil) (pure (map f nil))
Tactic: induction t with
  | nil => rw [traverse, map]
  | node v l r hl hr =>
    rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : Tree α
nil : Eq (α := Id (Tree β)) (traverse (pure ∘ f) Tree.nil) (pure (map f Tree.nil))
⊢ Eq (α := Id (Tree β)) (traverse (pure ∘ f) t) (pure (map f t))
have node : ∀ (v : α) (l r : Tree α) (hl : Eq (α := Id (Tree β)) (traverse (pure ∘ f) l) (pure (map f l)))
  (hr : Eq (α := Id (Tree β)) (traverse (pure ∘ f) r) (pure (map f r))),
  Eq (α := Id (Tree β)) (traverse (pure ∘ f) (node v l r)) (pure (map f (node v l r)))
Tactic: induction t with
  | nil => rw [traverse, map]
  | node v l r hl hr =>
    rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq,
      map_pure]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
⊢ (fun {α : Type u} ↦ η.app α) (traverse f nil) = traverse (η.app β ∘ f) nil
have nil : (fun {α : Type u} ↦ η.app α) (pure nil) = traverse (η.app β ∘ f) nil
Tactic: rw [traverse, traverse, η.preserves_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
nil : (fun {α : Type u} ↦ η.app α) (pure Tree.nil) = traverse (η.app β ∘ f) Tree.nil
⊢ (fun {α : Type u} ↦ η.app α) (traverse f Tree.nil) = traverse (η.app β ∘ f) Tree.nil
have nil₁ : Eq.{u_4 + 1} (α := G (Tree β)) ((fun {α : Type u} ↦ η.app α) (pure Tree.nil)) (pure Tree.nil)
Tactic: rw [traverse, traverse, η.preserves_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
nil : (fun {α : Type u} ↦ η.app α) (pure Tree.nil) = traverse (η.app β ∘ f) Tree.nil
nil₁ : Eq.{u_4 + 1} (α := G (Tree β)) ((fun {α : Type u} ↦ η.app α) (pure Tree.nil)) (pure Tree.nil)
⊢ (fun {α : Type u} ↦ η.app α) (traverse f Tree.nil) = traverse (η.app β ∘ f) Tree.nil
have nil₂ : Eq.{u_4 + 1} (α := G (Tree β)) (pure Tree.nil) (pure Tree.nil)
Tactic: rw [traverse, traverse, η.preserves_pure]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (node v l r)) = traverse (η.app β ∘ f) (node v l r)
have node : (fun {α : Type u} ↦ η.app α) (node <$> f v <*> traverse f l <*> traverse f r) = traverse (η.app β ∘ f) (node v l r)
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Tree.Traversable (goal)
Goal:
α : Type u_1
F : Type u → Type u_3
G : Type u → Type u_4
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
η : ApplicativeTransformation F G
β : Type u
f : α → F β
v : α
l r : Tree α
hl : (fun {α : Type u} ↦ η.app α) (traverse f l) = traverse (η.app β ∘ f) l
hr : (fun {α : Type u} ↦ η.app α) (traverse f r) = traverse (η.app β ∘ f) r
node :
  (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
    traverse (η.app β ∘ f) (Tree.node v l r)
⊢ (fun {α : Type u} ↦ η.app α) (traverse f (Tree.node v l r)) = traverse (η.app β ∘ f) (Tree.node v l r)
have node₁ : (fun {α : Type u} ↦ η.app α) (Tree.node <$> f v <*> traverse f l <*> traverse f r) =
  Tree.node <$> (η.app β ∘ f) v <*> traverse (η.app β ∘ f) l <*> traverse (η.app β ∘ f) r
Tactic: rw [traverse, traverse, η.preserves_seq, η.preserves_seq, η.preserves_map, hl, hr,
      Function.comp_apply]