awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
y : e ⊕ β_1
⊢ x <* y = Function.const β_1 <$> x <*> y
have inl : ∀ (x : e), Eq (α := e ⊕ α_1) (inl x <* y) (Function.const β_1 <$> inl x <*> y)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
y : e ⊕ β_1
inl : ∀ (x : e), Eq (α := e ⊕ α_1) (Sum.inl x <* y) (Function.const β_1 <$> Sum.inl x <*> y)
⊢ x <* y = Function.const β_1 <$> x <*> y
have inr : ∀ (x : α_1), Eq (α := e ⊕ α_1) (inr x <* y) (Function.const β_1 <$> inr x <*> y)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
y : e ⊕ β_1
⊢ Eq (α := e ⊕ β_1) (x *> y) (Function.const α_1 id <$> x <*> y)
have inl : ∀ (x : e), Eq (α := e ⊕ β_1) (inl x *> y) (Function.const α_1 id <$> inl x <*> y)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
y : e ⊕ β_1
inl : ∀ (x : e), Eq (α := e ⊕ β_1) (Sum.inl x *> y) (Function.const α_1 id <$> Sum.inl x <*> y)
⊢ Eq (α := e ⊕ β_1) (x *> y) (Function.const α_1 id <$> x <*> y)
have inr : ∀ (x : α_1), Eq (α := e ⊕ β_1) (inr x *> y) (Function.const α_1 id <$> inr x <*> y)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : e
⊢ Eq (α := e ⊕ β_1) (inl x *> y) (Function.const α_1 id <$> inl x <*> y)
have inl : ∀ (y : e), Eq (α := e ⊕ β_1) (inl x *> inl y) (Function.const α_1 id <$> inl x <*> inl y)
Tactic: casesm Sum _ _
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : e
inl : ∀ (y : e), Eq (α := e ⊕ β_1) (Sum.inl x *> Sum.inl y) (Function.const α_1 id <$> Sum.inl x <*> Sum.inl y)
⊢ Eq (α := e ⊕ β_1) (Sum.inl x *> y) (Function.const α_1 id <$> Sum.inl x <*> y)
have inl₁ : ∀ (y : β_1), Eq (α := e ⊕ β_1) (Sum.inl x *> inr y) (Function.const α_1 id <$> Sum.inl x <*> inr y)
Tactic: casesm Sum _ _
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : α_1
⊢ Eq (α := e ⊕ β_1) (inr x *> y) (Function.const α_1 id <$> inr x <*> y)
have inr : ∀ (y : e), Eq (α := e ⊕ β_1) (inr x *> inl y) (Function.const α_1 id <$> inr x <*> inl y)
Tactic: casesm Sum _ _
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : α_1
inr : ∀ (y : e), Eq (α := e ⊕ β_1) (Sum.inr x *> inl y) (Function.const α_1 id <$> Sum.inr x <*> inl y)
⊢ Eq (α := e ⊕ β_1) (Sum.inr x *> y) (Function.const α_1 id <$> Sum.inr x <*> y)
have inr₁ : ∀ (y : β_1), Eq (α := e ⊕ β_1) (Sum.inr x *> Sum.inr y) (Function.const α_1 id <$> Sum.inr x <*> Sum.inr y)
Tactic: casesm Sum _ _
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : α_1 → β_1
x : e ⊕ α_1
⊢ (do
      let a ← x
      pure (f a)) =
    f <$> x
have inl : ∀ (x : e),
  (do
      let a ← inl x
      pure (f a)) =
    f <$> inl x
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : α_1 → β_1
x : e ⊕ α_1
inl :
  ∀ (x : e),
    (do
        let a ← Sum.inl x
        pure (f a)) =
      f <$> Sum.inl x
⊢ (do
      let a ← x
      pure (f a)) =
    f <$> x
have inr : ∀ (x : α_1),
  Eq (α := e ⊕ β_1)
    (do
      let a ← inr x
      pure (f a))
    (f <$> inr x)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : Sum.{v, u} e (α_1 → β_1)
x : e ⊕ α_1
⊢ (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x
have inl : ∀ (f : e),
  Eq (α := e ⊕ β_1)
    (do
      let x_1 ← inl f
      x_1 <$> x)
    (inl f <*> x)
Tactic: casesm Sum _ _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : Sum.{v, u} e (α_1 → β_1)
x : e ⊕ α_1
inl :
  ∀ (f : e),
    Eq (α := e ⊕ β_1)
      (do
        let x_1 ← Sum.inl f
        x_1 <$> x)
      (Sum.inl f <*> x)
⊢ (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x
have inr : ∀ (f : α_1 → β_1),
  Eq (α := e ⊕ β_1)
    (do
      let x_1 ← inr f
      x_1 <$> x)
    (inr f <*> x)
Tactic: casesm Sum _ _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
x : e ⊕ α_1
f : α_1 → e ⊕ β_1
g : β_1 → e ⊕ γ_1
⊢ x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have inl : ∀ (x : e), inl x >>= f >>= g = inl x >>= fun (x : α_1) ↦ f x >>= g
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
x : e ⊕ α_1
f : α_1 → e ⊕ β_1
g : β_1 → e ⊕ γ_1
inl : ∀ (x : e), Sum.inl x >>= f >>= g = Sum.inl x >>= fun (x : α_1) ↦ f x >>= g
⊢ x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have inr : ∀ (x : α_1), inr x >>= f >>= g = inr x >>= fun (x : α_1) ↦ f x >>= g
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ Eq (α := m γ) ((fun (p : α × β) ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b))
    ((fun (b : β) (a : α) ↦ f a b) <$> b <*> a)
have rw : Eq (α := m γ) ((fun (p : α × β) ↦ f p.fst p.snd) <$> ((fun (b : β) (a : α) ↦ (a, b)) <$> b <*> a))
  ((fun (b : β) (a : α) ↦ f a b) <$> b <*> a)
Tactic: rw [@CommApplicative.commutative_prod m h]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ Eq (α := m γ) ((fun (p : α × β) ↦ f p.fst p.snd) <$> ((fun (b : β) (a : α) ↦ (a, b)) <$> b <*> a))
    ((fun (b : β) (a : α) ↦ f a b) <$> b <*> a)
have simp : Eq (α := m γ) ((fun (a : β) ↦ (fun (p : α × β) ↦ f p.fst p.snd) ∘ fun (a_1 : α) ↦ (a_1, a)) <$> b <*> a)
  ((fun (b : β) (a : α) ↦ f a b) <$> b <*> a)
Tactic: simp [map_seq, map_map]
-- Lean 4 proof step from Mathlib.Control.Bifunctor (goal)
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst_1 : Functor G
inst_2 : Functor H
inst_3 : LawfulFunctor G
inst_4 : LawfulFunctor H
inst_5 : LawfulBifunctor F
⊢ LawfulBifunctor.{u_1, u_2, u₂} (bicompl F G H)
have id_bimap : ∀ {α : Type u_1} {β : Type u_2} (x : bicompl F G H α β), bimap (F := bicompl F G H) id id x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bifunctor (goal)
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst_1 : Functor G
inst_2 : Functor H
inst_3 : LawfulFunctor G
inst_4 : LawfulFunctor H
inst_5 : LawfulBifunctor F
id_bimap : ∀ {α : Type u_1} {β : Type u_2} (x : bicompl F G H α β), bimap (F := bicompl F G H) id id x = x
⊢ LawfulBifunctor.{u_1, u_2, u₂} (bicompl F G H)
have bimap_bimap : ∀ {α₀ α₁ α₂ : Type u_1} {β₀ β₁ β₂ : Type u_2} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
  (x : bicompl F G H α₀ β₀),
  bimap (F := bicompl F G H) f' g' (bimap (F := bicompl F G H) f g x) = bimap (F := bicompl F G H) (f' ∘ f) (g' ∘ g) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bifunctor (goal)
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
G : Type u₂ → Type u_1
inst_1 : Functor G
inst_2 : LawfulFunctor G
inst_3 : LawfulBifunctor F
⊢ LawfulBifunctor.{u₀, u₁, u_1} (bicompr G F)
have id_bimap : ∀ {α : Type u₀} {β : Type u₁} (x : bicompr G F α β), bimap (F := bicompr G F) id id x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bifunctor (goal)
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
G : Type u₂ → Type u_1
inst_1 : Functor G
inst_2 : LawfulFunctor G
inst_3 : LawfulBifunctor F
id_bimap : ∀ {α : Type u₀} {β : Type u₁} (x : bicompr G F α β), bimap (F := bicompr G F) id id x = x
⊢ LawfulBifunctor.{u₀, u₁, u_1} (bicompr G F)
have bimap_bimap : ∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
  (x : bicompr G F α₀ β₀),
  bimap (F := bicompr G F) f' g' (bimap (F := bicompr G F) f g x) = bimap (F := bicompr G F) (f' ∘ f) (g' ∘ g) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
⊢ LawfulBitraversable Prod
have id_bitraverse : ∀ {α β : Type u_1} (x : α × β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α × β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)
⊢ LawfulBitraversable Prod
have comp_bitraverse : ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
  (x : α × α'),
  bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α × β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : α × α'),
    bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' x)
⊢ LawfulBitraversable Prod
have bitraverse_eq_bimap_id : ∀ {α α' β β' : Type u_1} (f : α → β) (f' : α' → β') (x : α × α'),
  Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Prod) f f' x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α × β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : α × α'),
    bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u_1} (f : α → β) (f' : α' → β') (x : α × α'),
    Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Prod) f f' x))
⊢ LawfulBitraversable Prod
have binaturality : ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
  (x : α × α'),
  Eq (α := G (β × β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Prod) f f' x))
    (bitraverse (t := Prod) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α β : Type u_1
x : α × β
⊢ Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)
have id_bitraverse : ∀ (fst : α) (snd : β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure (fst, snd)) (pure (fst, snd))
Tactic: casesm _ × _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : α × α'
⊢ bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' x)
have comp_bitraverse : ∀ (fst : α) (snd : α'),
  bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') (fst, snd) =
    Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' (fst, snd))
Tactic: casesm _ × _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α × α'
⊢ Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Prod) f f' x))
have bitraverse_eq_bimap_id : ∀ (fst : α) (snd : α'),
  Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') (fst, snd))
    (pure (bimap (F := Prod) f f' (fst, snd)))
Tactic: casesm _ × _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α α' β β' : Type u_1
f : α → F_1 β
f' : α' → F_1 β'
x : α × α'
⊢ Eq (α := G (β × β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Prod) f f' x))
    (bitraverse (t := Prod) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)
have binaturality : ∀ (fst : α) (snd : α'),
  Eq (α := G (β × β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Prod) f f' (fst, snd)))
    (bitraverse (t := Prod) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') (fst, snd))
Tactic: casesm _ × _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
fst : α
snd : α'
⊢ bitraverse (t := Prod) (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') (fst, snd) =
    Functor.Comp.mk (bitraverse (t := Prod) f f' <$> bitraverse (t := Prod) g g' (fst, snd))
have comp_bitraverse : Eq (α := Functor.Comp G F_1 (γ × γ'))
  (Functor.Comp.mk ((fun (a : β) ↦ (fun (x2 : F_1 γ') ↦ Prod.mk <$> f a <*> x2) ∘ f') <$> g fst <*> g' snd))
  (Functor.Comp.mk ((fun (a : β) ↦ Prod.bitraverse f f' ∘ Prod.mk a) <$> g fst <*> g' snd))
Tactic: simp [bitraverse, Prod.bitraverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u_1
f : α → β
f' : α' → β'
fst : α
snd : α'
⊢ Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') (fst, snd))
    (pure (bimap (F := Prod) f f' (fst, snd)))
have bitraverse_eq_bimap_id : Eq (α := Id (β × β')) (pure (f fst, f' snd)) (pure (bimap (F := Prod) f f' (fst, snd)))
Tactic: simp [bitraverse, Prod.bitraverse, functor_norm]
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
⊢ LawfulBitraversable Sum
have id_bitraverse : ∀ {α β : Type u_1} (x : α ⊕ β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α ⊕ β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
⊢ LawfulBitraversable Sum
have comp_bitraverse : ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
  (x : α ⊕ α'),
  bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α ⊕ β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : α ⊕ α'),
    bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' x)
⊢ LawfulBitraversable Sum
have bitraverse_eq_bimap_id : ∀ {α α' β β' : Type u_1} (f : α → β) (f' : α' → β') (x : α ⊕ α'),
  Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Sum) f f' x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
id_bitraverse : ∀ {α β : Type u_1} (x : α ⊕ β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
comp_bitraverse :
  ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
    (x : α ⊕ α'),
    bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
      Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' x)
bitraverse_eq_bimap_id :
  ∀ {α α' β β' : Type u_1} (f : α → β) (f' : α' → β') (x : α ⊕ α'),
    Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Sum) f f' x))
⊢ LawfulBitraversable Sum
have binaturality : ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
  (x : α ⊕ α'),
  Eq (α := G (β ⊕ β')) ((fun {α : Type u_1} ↦ η.app α) (bitraverse (t := Sum) f f' x))
    (bitraverse (t := Sum) ((fun {α : Type u_1} ↦ η.app α) ∘ f) ((fun {α : Type u_1} ↦ η.app α) ∘ f') x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α β : Type u_1
x : α ⊕ β
⊢ Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
have id_bitraverse : ∀ (x : α), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inl x)) (pure (Sum.inl x))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α β : Type u_1
x : α ⊕ β
id_bitraverse : ∀ (x : α), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inl x)) (pure (Sum.inl x))
⊢ Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)
have id_bitraverse₁ : ∀ (x : β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inr x)) (pure (Sum.inr x))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : α ⊕ α'
⊢ bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' x)
have comp_bitraverse : ∀ (x : α),
  bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') (Sum.inl x) =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' (Sum.inl x))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
F_1 G : Type u_1 → Type u_1
inst_2 : Applicative F_1
inst_3 : Applicative G
inst_4 : LawfulApplicative F_1
inst_5 : LawfulApplicative G
α α' β β' γ γ' : Type u_1
f : β → F_1 γ
f' : β' → F_1 γ'
g : α → G β
g' : α' → G β'
x : α ⊕ α'
comp_bitraverse :
  ∀ (x : α),
    bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') (Sum.inl x) =
      Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' (Sum.inl x))
⊢ bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' x)
have comp_bitraverse₁ : ∀ (x : α'),
  bitraverse (t := Sum) (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') (Sum.inr x) =
    Comp.mk (bitraverse (t := Sum) f f' <$> bitraverse (t := Sum) g g' (Sum.inr x))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α ⊕ α'
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Sum) f f' x))
have bitraverse_eq_bimap_id : ∀ (x : α),
  Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inl x))
    (pure (bimap (F := Sum) f f' (Sum.inl x)))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Bitraversable.Instances (goal)
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α α' β β' : Type u_1
f : α → β
f' : α' → β'
x : α ⊕ α'
bitraverse_eq_bimap_id :
  ∀ (x : α),
    Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inl x))
      (pure (bimap (F := Sum) f f' (Sum.inl x)))
⊢ Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Sum) f f' x))
have bitraverse_eq_bimap_id₁ : ∀ (x : α'),
  Eq (α := Id (β ⊕ β')) (bitraverse (t := Sum) (pure ∘ f) (pure ∘ f') (Sum.inr x))
    (pure (bimap (F := Sum) f f' (Sum.inr x)))
Tactic: casesm _ ⊕ _
Cleared hypotheses: x