awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t' α
rw :
  Eq (α := Id (t' α))
    (map (α := t α) (⇑(eqv α) : (a : t α) → t' α) (traverse pure (((eqv α).symm : (a : t' α) → t α) x))) (pure x)
⊢ Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
have rw₁ : Eq (α := Id (t' α))
  (map (α := t α) ((⇑(eqv α) : (a : t α) → t' α) : (a : t α) → t' α)
    (pure (((eqv α).symm : (a : t' α) → t α) x) : Id (t α)))
  (pure x)
Tactic: rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t' α
rw :
  Eq (α := Id (t' α))
    (map (α := t α) (⇑(eqv α) : (a : t α) → t' α) (traverse pure (((eqv α).symm : (a : t' α) → t α) x))) (pure x)
rw₁ :
  Eq (α := Id (t' α))
    (map (α := t α) ((⇑(eqv α) : (a : t α) → t' α) : (a : t α) → t' α)
      (pure (((eqv α).symm : (a : t' α) → t α) x) : Id (t α)))
    (pure x)
⊢ Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
have rw₂ : Eq (α := Id (t' α)) (pure ((eqv α : (a : t α) → t' α) (((eqv α).symm : (a : t' α) → t α) x : t α)) : Id (t' α))
  (pure x : Id (t' α))
Tactic: rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t' α
rw :
  Eq (α := Id (t' α))
    (map (α := t α) (⇑(eqv α) : (a : t α) → t' α) (traverse pure (((eqv α).symm : (a : t' α) → t α) x))) (pure x)
rw₁ :
  Eq (α := Id (t' α))
    (map (α := t α) ((⇑(eqv α) : (a : t α) → t' α) : (a : t α) → t' α)
      (pure (((eqv α).symm : (a : t' α) → t α) x) : Id (t α)))
    (pure x)
rw₂ :
  Eq (α := Id (t' α)) (pure ((eqv α : (a : t α) → t' α) (((eqv α).symm : (a : t' α) → t α) x : t α)) : Id (t' α))
    (pure x : Id (t' α))
⊢ Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
have rw₃ : Eq (α := Id (t' α)) (pure x) (pure x)
Tactic: rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α β : Type u
f : α → β
x : t' α
⊢ Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ f) x) (pure (Equiv.map eqv f x))
have simp : Eq (α := Id (t' β)) (map (α := t β) (⇑(eqv β) : (a : t β) → t' β) (pure (f <$> ((eqv α).symm : (a : t' α) → t α) x)))
  (pure (Equiv.map eqv f x))
Tactic: simp only [Equiv.traverse, traverse_eq_map_id]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : Applicative G
inst_4 : LawfulApplicative F
inst_5 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
have rw : Comp.mk
    ((fun (x : F (t γ)) ↦ (⇑(eqv γ) : (a : t γ) → t' γ) <$> x) <$>
      traverse f <$> traverse g (((eqv α).symm : (a : t' α) → t α) x)) =
  Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
Tactic: rw [traverse_def, comp_traverse, Comp.map_mk]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α : Type u
x : t' α
⊢ Eq (α := Id (t' α)) (traverse pure x) (pure x)
have rw : Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
Tactic: rw [h₂, Equiv.id_traverse]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α : Type u
x : t' α
rw : Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
⊢ Eq (α := Id (t' α)) (traverse pure x) (pure x)
have rw₁ : Eq (α := Id (t' α)) (pure x) (pure x)
Tactic: rw [h₂, Equiv.id_traverse]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
⊢ traverse (Comp.mk ∘ map x ∘ x_1) x_2 = Comp.mk (traverse x <$> traverse x_1 x_2)
have rw : Comp.mk (Equiv.traverse eqv x <$> Equiv.traverse eqv x_1 x_2) = Comp.mk (Equiv.traverse eqv x <$> traverse x_1 x_2)
Tactic: rw [h₂, Equiv.comp_traverse, h₂]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
⊢ Comp.mk (Equiv.traverse eqv x <$> Equiv.traverse eqv x_1 x_2) = Comp.mk (Equiv.traverse eqv x <$> traverse x_1 x_2)
have e_x : Equiv.traverse eqv x_1 x_2 = traverse x_1 x_2
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
α β γ : Type u
x : β → F γ
x_1 : α → G β
x_2 : t' α
⊢ Equiv.traverse eqv x_1 x_2 = traverse x_1 x_2
have e_x : Equiv.traverse eqv x_1 x_2 = Equiv.traverse eqv x_1 x_2
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α β : Type u
x : α → β
x_1 : t' α
⊢ Eq (α := Id (t' β)) (traverse (pure ∘ x) x_1) (pure (x <$> x_1))
have rw : Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ x) x_1) (pure (x <$> x_1))
Tactic: rw [h₂, Equiv.traverse_eq_map_id, h₀]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α β : Type u
x : α → β
x_1 : t' α
rw : Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ x) x_1) (pure (x <$> x_1))
⊢ Eq (α := Id (t' β)) (traverse (pure ∘ x) x_1) (pure (x <$> x_1))
have rw₁ : Eq (α := Id (t' β)) (pure (Equiv.map eqv x x_1)) (pure (x <$> x_1))
Tactic: rw [h₂, Equiv.traverse_eq_map_id, h₀]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_3 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α β : Type u
x : α → β
x_1 : t' α
rw : Eq (α := Id (t' β)) (Equiv.traverse eqv (pure ∘ x) x_1) (pure (x <$> x_1))
rw₁ : Eq (α := Id (t' β)) (pure (Equiv.map eqv x x_1)) (pure (x <$> x_1))
⊢ Eq (α := Id (t' β)) (traverse (pure ∘ x) x_1) (pure (x <$> x_1))
have rw₂ : Eq (α := Id (t' β)) (pure (Equiv.map eqv x x_1)) (pure (Equiv.map eqv x x_1))
Tactic: rw [h₂, Equiv.traverse_eq_map_id, h₀]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
x : ApplicativeTransformation F G
x_1 x_2 : Type u
x_3 : x_1 → F x_2
x_4 : t' x_1
⊢ Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (traverse x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
have rw : Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (Equiv.traverse eqv x_3 x_4))
  (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
Tactic: rw [h₂, Equiv.naturality, h₂]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
x : ApplicativeTransformation F G
x_1 x_2 : Type u
x_3 : x_1 → F x_2
x_4 : t' x_1
rw :
  Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (Equiv.traverse eqv x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
⊢ Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (traverse x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
have rw₁ : Eq (α := G (t' x_2)) (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
  (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
Tactic: rw [h₂, Equiv.naturality, h₂]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst_7 : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F G : Type u → Type u
inst_3 : Applicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative F
inst_6 : LawfulApplicative G
x : ApplicativeTransformation F G
x_1 x_2 : Type u
x_3 : x_1 → F x_2
x_4 : t' x_1
rw :
  Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (Equiv.traverse eqv x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
rw₁ :
  Eq (α := G (t' x_2)) (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
⊢ Eq (α := G (t' x_2)) ((fun {α : Type u} ↦ x.app α) (traverse x_3 x_4))
    (traverse ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
have rw₂ : Eq (α := G (t' x_2)) (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
  (Equiv.traverse eqv ((fun {α : Type u} ↦ x.app α) ∘ x_3) x_4)
Tactic: rw [h₂, Equiv.naturality, h₂]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α : Type u_1
x : Option α
⊢ Eq (α := Id (Option α)) (Option.traverse pure x) (pure x)
have none : Eq.{u_1 + 1} (α := Id (Option α)) (Option.traverse pure none) (pure none)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α : Type u_1
x : Option α
none : Eq.{u_1 + 1} (α := Id (Option α)) (Option.traverse pure Option.none) (pure Option.none)
⊢ Eq (α := Id (Option α)) (Option.traverse pure x) (pure x)
have some : ∀ (val : α), Eq (α := Id (Option α)) (Option.traverse pure (some val)) (pure (some val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)
have none : Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) none = Comp.mk (Option.traverse f <$> Option.traverse g none)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
none :
  Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) Option.none =
    Comp.mk (Option.traverse f <$> Option.traverse g Option.none)
⊢ Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)
have some : ∀ (val : α),
  Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (some val) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) none =
    Comp.mk (Option.traverse f <$> Option.traverse g none)
have none : Eq.{u + 1} (α := Comp G F (Option γ)) (pure none) (Comp.mk (pure (pure none)))
Tactic: simp [Option.traverse, Option.mapM, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α β : Type u_1
f : α → β
x : Option α
⊢ Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) x) (pure (f <$> x))
have none : Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) none) (pure (f <$> none))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α β : Type u_1
f : α → β
x : Option α
none : Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) Option.none) (pure (f <$> Option.none))
⊢ Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) x) (pure (f <$> x))
have some : ∀ (val : α), Eq (α := Id (Option β)) (Option.traverse (pure ∘ f) (some val)) (pure (f <$> some val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
η : ApplicativeTransformation F G
inst_3 : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f x))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have none : Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f none))
  (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) none)
Tactic: rcases x with - | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
η : ApplicativeTransformation F G
inst_3 : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
none :
  Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f Option.none))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) Option.none)
⊢ Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f x))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have some : ∀ (x : α),
  Eq (α := G (Option β)) ((fun {α : Type u} ↦ η.app α) (Option.traverse f (some x)))
    (Option.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (some x))
Tactic: rcases x with - | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α : Type u_1
xs : List α
⊢ Eq (α := Id (List α)) (List.traverse pure xs) (pure xs)
have nil : Eq.{u_1 + 1} (α := Id (List α)) (List.traverse pure []) (pure [])
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := Id (List α)) (List.traverse pure []) (pure [])
⊢ Eq (α := Id (List α)) (List.traverse pure xs) (pure xs)
have cons : ∀ (head : α) (tail : List α),
  Eq (α := Id (List α)) (List.traverse pure tail) (pure tail) →
    Eq (α := Id (List α)) (List.traverse pure (head :: tail)) (pure (head :: tail))
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)
have nil : List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
nil : List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)
have cons : ∀ (head : α) (tail : List α),
  List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) tail = Comp.mk (List.traverse f <$> List.traverse g tail) →
    List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (head :: tail) =
      Comp.mk (List.traverse f <$> List.traverse g (head :: tail))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])
have nil : Eq.{u + 1} (α := Comp G F (List γ)) (pure []) (Comp.mk (pure (pure [])))
Tactic: simp! [*, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head : α
tail : List α
tail_ih :
  List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) tail = Comp.mk (List.traverse f <$> List.traverse g tail)
⊢ List.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (head :: tail) =
    Comp.mk (List.traverse f <$> List.traverse g (head :: tail))
have cons : Eq (α := Comp G F (List γ))
  (Comp.mk
    ((fun (a : β) ↦ (fun (x2 : F (List γ)) ↦ cons <$> f a <*> x2) ∘ List.traverse f) <$> g head <*>
      List.traverse g tail))
  (Comp.mk ((fun (a : β) ↦ List.traverse f ∘ cons a) <$> g head <*> List.traverse g tail))
Tactic: simp! [*, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α β : Type u_1
f : α → β
x : List α
⊢ Eq (α := Id (List β)) (List.traverse (pure ∘ f) x) (pure (f <$> x))
have nil : Eq (α := Id (List β)) (List.traverse (pure ∘ f) []) (pure (f <$> []))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
α β : Type u_1
f : α → β
x : List α
nil : Eq (α := Id (List β)) (List.traverse (pure ∘ f) []) (pure (f <$> []))
⊢ Eq (α := Id (List β)) (List.traverse (pure ∘ f) x) (pure (f <$> x))
have cons : ∀ (head : α) (tail : List α),
  Eq (α := Id (List β)) (List.traverse (pure ∘ f) tail) (pure (f <$> tail)) →
    Eq (α := Id (List β)) (List.traverse (pure ∘ f) (head :: tail)) (pure (f <$> (head :: tail)))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
⊢ Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f x))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have nil : Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f []))
  (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) [])
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
inst_3 : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
nil :
  Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f []))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) [])
⊢ Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f x))
    (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have cons : ∀ (head : α) (tail : List α),
  Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f tail))
      (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) tail) →
    Eq (α := G (List β)) ((fun {α : Type u} ↦ η.app α) (List.traverse f (head :: tail)))
      (List.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (head :: tail))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
F : Type u → Type u
inst : Applicative F
α' β' : Type u
f : α' → F β'
inst_1 : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = (fun (x1 x2 : List β') ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs
have simp : Eq (α := F (List β'))
  ((fun (a : β') ↦
          Function.comp (β := List β' → List β') (Function.comp fun (x2 : List β') ↦ a :: x2) fun (x1 x2 : List β') ↦
            x1 ++ x2) <$>
        f a <*>
      traverse f as <*>
    traverse f bs)
  ((fun (a : β') ↦ (fun (x1 x2 : List β') ↦ x1 ++ x2) ∘ fun (x2 : List β') ↦ a :: x2) <$> f a <*> traverse f as <*>
    traverse f bs)
Tactic: simp [traverse_append as bs, functor_norm]