-- Mathlib/Data/Tree/Traversable.lean
lemma comp_traverse
    {F : Type u → Type v} {G : Type v → Type w} [Applicative F] [Applicative G]
    [LawfulApplicative G] {β : Type v} {γ : Type u} (f : β → F γ) (g : α → G β)
    (t : Tree α) : t.traverse (Functor.Comp.mk ∘ (f <$> ·) ∘ g) =
      Functor.Comp.mk ((·.traverse f) <$> (t.traverse g))

Proof state:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) l = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) r = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r)
⊢ traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) (node v l r) =
    Functor.Comp.mk ((fun x => traverse f x) <$> traverse g (node v l r))

Tactic:
rw [traverse, hl, hr, traverse]

Result:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) l = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) r = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) v <*>
        Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r) =
    Functor.Comp.mk ((fun x => traverse f x) <$> (node <$> g v <*> traverse g l <*> traverse g r))

Proof state:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) l = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) r = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) v <*>
        Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r) =
    Functor.Comp.mk ((fun x => traverse f x) <$> (node <$> 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]

Result:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) l = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) r = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r)
⊢ Functor.Comp.mk
      ((fun a x x_1 => 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 => traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r)

Proof state:
case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) nil = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g nil)

Tactic:
rw [traverse, traverse, map_pure, traverse]

Result:
case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))

Proof state:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : Tree α
hl : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) l = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) r = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g r)
⊢ Functor.Comp.mk
      ((fun a x x_1 => 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 => traverse f (node a x x_1)) <$> g v <*> traverse g l <*> traverse g r)

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Functor.Comp.mk (pure (pure nil))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
t : Tree α
⊢ traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) t = Functor.Comp.mk ((fun x => traverse f x) <$> traverse g t)

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

Result:
no goals