awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
have inl : ∀ (val : σ), Sum.traverse f (g <$> inl val) = Sum.traverse (f ∘ g) (inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
inl : ∀ (val : σ), Sum.traverse f (g <$> Sum.inl val) = Sum.traverse (f ∘ g) (Sum.inl val)
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x
have inr : ∀ (val : α), Eq (α := G (σ ⊕ γ)) (Sum.traverse f (g <$> inr val)) (Sum.traverse (f ∘ g) (inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : σ
⊢ Sum.traverse f (g <$> inl val) = Sum.traverse (f ∘ g) (inl val)
have inl : Eq (α := G (σ ⊕ γ))
  (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> inl val with
    | inl x => pure (inl x)
    | inr x => inr <$> f x :
    G (σ ⊕ γ))
  (pure (inl val) : G (σ ⊕ γ))
Tactic: simp [Sum.traverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val : α
⊢ Eq (α := G (σ ⊕ γ)) (Sum.traverse f (g <$> inr val)) (Sum.traverse (f ∘ g) (inr val))
have inr : Eq (α := G (σ ⊕ γ))
  (match (motive := σ ⊕ β → G (σ ⊕ γ)) g <$> inr val with
    | inl x => pure (inl x)
    | inr x => inr <$> f x :
    G (σ ⊕ γ))
  (inr <$> f (g val) : G (σ ⊕ γ))
Tactic: simp [Sum.traverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x
have inl : ∀ (val : σ), Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (inl val) : Id (σ ⊕ α)) (inl val : σ ⊕ α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ α : Type u_1
x : σ ⊕ α
inl : ∀ (val : σ), Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (Sum.inl val) : Id (σ ⊕ α)) (Sum.inl val : σ ⊕ α)
⊢ Sum.traverse pure x = x
have inr : ∀ (val : α), Eq (α := Id (σ ⊕ α)) (Sum.traverse pure (inr val)) (inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)
have inl : ∀ (val : σ),
  Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (inl val) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
inl :
  ∀ (val : σ),
    Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (Sum.inl val) =
      Comp.mk (Sum.traverse f <$> Sum.traverse g (Sum.inl val))
⊢ Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)
have inr : ∀ (val : α),
  Eq (α := Comp G F (σ ⊕ γ)) (Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (inr val))
    (Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val)))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
F G : Type u → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val : σ
⊢ Sum.traverse (Comp.mk ∘ (fun (x : G β) ↦ f <$> x) ∘ g) (inl val) =
    Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val))
have inl : Eq (α := Comp G F (σ ⊕ γ)) (pure (inl val)) (Comp.mk (pure (pure (inl val))))
Tactic: simp! [Sum.traverse, map_id, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) x) (pure (f <$> x))
have inl : ∀ (val : σ), Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (inl val)) (pure (f <$> inl val))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ α β : Type u
f : α → β
x : σ ⊕ α
inl : ∀ (val : σ), Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (Sum.inl val)) (pure (f <$> Sum.inl val))
⊢ Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) x) (pure (f <$> x))
have inr : ∀ (val : α), Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (inr val)) (pure (f <$> inr val))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ α β : Type u
f : α → β
val : α
⊢ Eq (α := Id (σ ⊕ β)) (Sum.traverse (pure ∘ f) (inr val)) (pure (f <$> inr val))
have inr : Eq (α := Id (σ ⊕ β)) (pure (inr (f val))) (pure (f <$> inr val))
Tactic: simp! [*, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g x) (Sum.traverse (fun (x : α) ↦ f <$> g x) x)
have inl : ∀ (val : σ),
  Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (inl val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
inl :
  ∀ (val : σ),
    Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (Sum.inl val))
      (Sum.traverse (fun (x : α) ↦ f <$> g x) (Sum.inl val))
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g x) (Sum.traverse (fun (x : α) ↦ f <$> g x) x)
have inr : ∀ (val : α),
  Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (inr val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : σ
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (inl val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (inl val))
have inl : Eq (α := G (σ ⊕ γ)) (pure (f <$> inl val)) (pure (inl val))
Tactic: simp [Sum.traverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val : α
⊢ Eq (α := G (σ ⊕ γ)) ((fun (x : σ ⊕ β) ↦ f <$> x) <$> Sum.traverse g (inr val))
    (Sum.traverse (fun (x : α) ↦ f <$> g x) (inr val))
have inr : Eq (α := G (σ ⊕ γ)) ((fun (a : β) ↦ f <$> inr a) <$> g val) ((fun (a : β) ↦ inr (f a)) <$> g val)
Tactic: simp [Sum.traverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
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 : σ ⊕ α
⊢ Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f x))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have inl : ∀ (val : σ),
  Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (inl val)))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Instances (goal)
Goal:
σ : Type u
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 : σ ⊕ α
inl :
  ∀ (val : σ),
    Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (Sum.inl val)))
      (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (Sum.inl val))
⊢ Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f x))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
have inr : ∀ (val : α),
  Eq (α := G (σ ⊕ β)) ((fun {α : Type u} ↦ η.app α) (Sum.traverse f (inr val)))
    (Sum.traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
f_1 : β → γ
α_1 β_1 : Type u
f : Id (α_1 → β_1)
x : Id α_1
⊢ Eq (α := F β_1) (pure (f <*> x)) (pure f <*> pure x)
have simp : Eq (α := F β_1) (pure (f <*> x)) (pure (f x))
Tactic: simp only [map_pure, seq_pure]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ map f <$> traverse g x = traverse (map f ∘ g) x
have rw : (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x
Tactic: rw [map_eq_traverse_id f]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x
have refine : traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
Tactic: refine (comp_traverse (pure ∘ f) g x).symm.trans ?_
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x
have h : Comp.instApplicativeComp = inst_2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f (g <$> x) = traverse (f ∘ g) x
have rw : traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x
Tactic: rw [@map_eq_traverse_id t _ _ _ _ g]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f ((Id.run ∘ traverse (pure ∘ g)) x) = traverse (f ∘ g) x
have refine : traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
Tactic: refine (comp_traverse (G := Id) f (pure ∘ g) x).symm.trans ?_
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x
have h : Comp.instApplicativeComp = inst_2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (hypothesis)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α : Type u
x : t α
⊢ Eq (α := F (t α)) (traverse pure x) (pure x)
have this : Eq (α := F (t α)) (traverse pure x) (pure (traverse pure x))
Tactic: have : traverse pure x = pure (traverse (m := Id) pure x) :=
      (naturality (PureTransformation F) pure x).symm
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
α : Type u
x : t α
this : Eq (α := F (t α)) (traverse pure x) (pure (traverse pure x))
⊢ Eq (α := F (t α)) (traverse pure x) (pure x)
have rwa : ∀ (this : Eq (α := F (t α)) (traverse pure x) (pure (pure x))), Eq (α := F (t α)) (traverse pure x) (pure x)
Tactic: rwa [id_traverse] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)
have simp : traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
Tactic: simp only [sequence, traverse_map, id_comp]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
have rw : traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
Tactic: rw [← comp_traverse]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
⊢ Eq.{u + 1} (α := t α → Id (t α)) (traverse pure) pure
have h : ∀ (x : t α), Id.run (traverse pure x) = Id.run (pure x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
⊢ Eq (α := t α → Comp F G (t γ)) (traverse (Comp.mk ∘ map h ∘ g)) (Comp.mk ∘ map (traverse h) ∘ traverse g)
have h₁ : ∀ (x : t α), traverse (Comp.mk ∘ map h ∘ g) x = (Comp.mk ∘ map (traverse h) ∘ traverse g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ Eq (α := t β → Id (t γ)) (traverse (pure ∘ f)) (pure ∘ map f)
have h : ∀ (x : t β), Id.run (traverse (pure ∘ f) x) = Id.run ((pure ∘ map f) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
⊢ Eq (α := t α → G (t γ)) (traverse (h ∘ g)) (traverse h ∘ map g)
have h₁ : ∀ (x : t α), traverse (h ∘ g) x = (traverse h ∘ map g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x : t α
⊢ traverse (h ∘ g) x = (traverse h ∘ map g) x
have h₁ : traverse (h ∘ g) x = traverse h (g <$> x)
Tactic: rw [comp_apply, traverse_map]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x : t α
h₁ : traverse (h ∘ g) x = traverse h (g <$> x)
⊢ traverse (h ∘ g) x = (traverse h ∘ map g) x
have h₂ : traverse (h ∘ g) x = traverse (h ∘ g) x
Tactic: rw [comp_apply, traverse_map]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
⊢ Eq (α := t α → G (t γ)) (traverse (map h ∘ g)) (map (map h) ∘ traverse g)
have h₁ : ∀ (x : t α), traverse (map h ∘ g) x = (map (map h) ∘ traverse g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x : t α
⊢ traverse (map h ∘ g) x = (map (map h) ∘ traverse g) x
have h₁ : traverse (map h ∘ g) x = map h <$> traverse g x
Tactic: rw [comp_apply, map_traverse]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
G : Type u → Type u
inst_2 : Applicative G
inst_3 : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x : t α
h₁ : traverse (map h ∘ g) x = map h <$> traverse g x
⊢ traverse (map h ∘ g) x = (map (map h) ∘ traverse g) x
have h₂ : traverse (map h ∘ g) x = traverse (map h ∘ g) x
Tactic: rw [comp_apply, map_traverse]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
⊢ Eq (α := t α → G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f)) ((fun {α : Type u} ↦ η.app α) ∘ traverse f)
have h : ∀ (x : t α),
  Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (((fun {α : Type u} ↦ η.app α) ∘ traverse f) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x : t α
⊢ Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (((fun {α : Type u} ↦ η.app α) ∘ traverse f) x)
have h : Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) ((fun {α : Type u} ↦ η.app α) (traverse f x))
Tactic: rw [comp_apply, naturality]
-- Lean 4 proof step from Mathlib.Control.Traversable.Lemmas (goal)
Goal:
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
F G : Type u → Type u
inst_2 : Applicative F
inst_3 : LawfulApplicative F
inst_4 : Applicative G
inst_5 : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x : t α
h : Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) ((fun {α : Type u} ↦ η.app α) (traverse f x))
⊢ Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (((fun {α : Type u} ↦ η.app α) ∘ traverse f) x)
have h₁ : Eq (α := G (t β)) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x) (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
Tactic: rw [comp_apply, naturality]
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε α
⊢ Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) f) = f
have error : ∀ (a : ε),
  Eq (α := Except ε α)
    (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α)
      (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (error a)))
    (error a)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε α
error :
  ∀ (a : ε),
    Eq (α := Except ε α)
      (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α)
        (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.error a)))
      (Except.error a)
⊢ Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) f) = f
have ok : ∀ (a : α),
  Eq (α := Except ε α) (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.map (⇑e : (a : α) → β) (ok a)))
    (ok a)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε β
⊢ Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) f) = f
have error : ∀ (a : ε),
  Eq (α := Except ε β)
    (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β)
      (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (error a)))
    (error a)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α : Type v₁
β : Type v₂
e : α ≃ β
f : Except ε β
error :
  ∀ (a : ε),
    Eq (α := Except ε β)
      (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β)
        (Except.map.{u₀, v₂, v₁} (α := β) (⇑e.symm : (a : β) → α) (Except.error a)))
      (Except.error a)
⊢ Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) f) = f
have ok : ∀ (a : β),
  Eq (α := Except ε β) (Except.map.{u₀, v₁, v₂} (α := α) (⇑e : (a : α) → β) (Except.map (⇑e.symm : (a : β) → α) (ok a)))
    (ok a)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option α
⊢ Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) f) = f
have none : Eq.{u₀ + 1} (α := Option α)
  (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) none)) none
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option α
none :
  Eq.{u₀ + 1} (α := Option α)
    (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) Option.none))
    Option.none
⊢ Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) f) = f
have some : ∀ (val : α), Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) (Option.map (⇑e : (a : α) → β) (some val)) = some val
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option β
⊢ Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) f) = f
have none : Eq.{u₁ + 1} (α := Option β)
  (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) none)) none
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.ULiftable (goal)
Goal:
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α : Type u₀
β : Type u₁
e : α ≃ β
f : Option β
none :
  Eq.{u₁ + 1} (α := Option β)
    (Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map.{u₁, u₀} (α := β) (⇑e.symm : (a : β) → α) Option.none))
    Option.none
⊢ Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) f) = f
have some : ∀ (val : β), Option.map.{u₀, u₁} (α := α) (⇑e : (a : α) → β) (Option.map (⇑e.symm : (a : β) → α) (some val)) = some val
Tactic: cases f
Cleared hypotheses: f