awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Basic
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)
inr : ∀ (x : α_1), Eq (α := e ⊕ β_1) (Sum.inr x *> y) (Function.const α_1 id <$> Sum.inr x <*> y)
⊢ Eq (α := e ⊕ β_1) (x *> y) (Function.const α_1 id <$> x <*> y)

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
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)
inl₁ : ∀ (y : β_1), Eq (α := e ⊕ β_1) (Sum.inl x *> inr y) (Function.const α_1 id <$> Sum.inl x <*> inr y)
⊢ Eq (α := e ⊕ β_1) (Sum.inl x *> y) (Function.const α_1 id <$> Sum.inl x <*> y)

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
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)
inr₁ : ∀ (y : β_1), Eq (α := e ⊕ β_1) (Sum.inr x *> Sum.inr y) (Function.const α_1 id <$> Sum.inr x <*> Sum.inr y)
⊢ Eq (α := e ⊕ β_1) (Sum.inr x *> y) (Function.const α_1 id <$> Sum.inr x <*> y)

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x y : e
⊢ Eq (α := e ⊕ β_1) (inl x *> inl y) (Function.const α_1 id <$> inl x <*> inl y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e
y : β_1
⊢ Eq (α := e ⊕ β_1) (inl x *> inr y) (Function.const α_1 id <$> inl x <*> inr y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : α_1
y : e
⊢ Eq (α := e ⊕ β_1) (inr x *> inl y) (Function.const α_1 id <$> inr x <*> inl y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : α_1
y : β_1
⊢ Eq (α := e ⊕ β_1) (inr x *> inr y) (Function.const α_1 id <$> inr x <*> inr y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
g : α_1 → β_1
x : e ⊕ α_1
⊢ pure g <*> x = g <$> x

Tactic:
rfl
-- Module: Mathlib.Control.Basic
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
inr :
  ∀ (x : α_1),
    Eq (α := e ⊕ β_1)
      (do
        let a ← Sum.inr x
        pure (f a))
      (f <$> Sum.inr x)
⊢ (do
      let a ← x
      pure (f a)) =
    f <$> x

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : α_1 → β_1
x : e
⊢ (do
      let a ← inl x
      pure (f a)) =
    f <$> inl x

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
f : α_1 → β_1
x : α_1
⊢ Eq (α := e ⊕ β_1)
    (do
      let a ← inr x
      pure (f a))
    (f <$> inr x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
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)
inr :
  ∀ (f : α_1 → β_1),
    Eq (α := e ⊕ β_1)
      (do
        let x_1 ← Sum.inr f
        x_1 <$> x)
      (Sum.inr f <*> x)
⊢ (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
f : e
⊢ Eq (α := e ⊕ β_1)
    (do
      let x_1 ← inl f
      x_1 <$> x)
    (inl f <*> x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
f : α_1 → β_1
⊢ Eq (α := e ⊕ β_1)
    (do
      let x_1 ← inr f
      x_1 <$> x)
    (inr f <*> x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : α_1
f : α_1 → e ⊕ β_1
⊢ pure x >>= f = f x

Tactic:
rfl
-- Module: Mathlib.Control.Basic
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
inr : ∀ (x : α_1), Sum.inr x >>= f >>= g = Sum.inr x >>= fun (x : α_1) ↦ f x >>= g
⊢ x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
f : α_1 → e ⊕ β_1
g : β_1 → e ⊕ γ_1
x : e
⊢ inl x >>= f >>= g = inl x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
f : α_1 → e ⊕ β_1
g : β_1 → e ⊕ γ_1
x : α_1
⊢ inr x >>= f >>= g = inr x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ f <$> a <*> b = (fun (p : α × β) ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b)

Tactic:
simp only [map_seq, map_map, Function.comp_def]

Premises used: Function.comp_def, Functor.map_map, map_seq
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
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)
⊢ Eq (α := m γ) ((fun (p : α × β) ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b))
    ((fun (b : β) (a : α) ↦ f a b) <$> b <*> a)

Tactic:
rw [@CommApplicative.commutative_prod m h]

Premises used: CommApplicative.commutative_prod
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
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)
⊢ 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:
simp [map_seq, map_map]

Premises used: Functor.map_map, map_seq
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
h : Applicative m
inst : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ 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:
rfl
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
⊢ ∀ {α : Type u₀} {β : Type u₁} (x : F α β), fst (F := F) id x = x

Tactic:
@id_bimap _ _ _

Premises used: LawfulBifunctor.id_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
⊢ ∀ {α : Type u₀} {β : Type u₁} (x : F α β), snd (F := F) id x = x

Tactic:
@id_bimap _ _ _

Premises used: LawfulBifunctor.id_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α₀ α₁ α₂ : Type u₀
β : Type u₁
f : α₀ → α₁
f' : α₁ → α₂
x : F α₀ β
⊢ fst (F := F) f' (fst (F := F) f x) = fst (F := F) (f' ∘ f) x

Tactic:
simp [fst, bimap_bimap]

Premises used: Bifunctor.fst, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ fst (F := F) f (snd (F := F) f' x) = bimap (F := F) f f' x

Tactic:
simp [fst, bimap_bimap]

Premises used: Bifunctor.fst, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ snd (F := F) f' (fst (F := F) f x) = bimap (F := F) f f' x

Tactic:
simp [snd, bimap_bimap]

Premises used: Bifunctor.snd, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α : Type u₀
β₀ β₁ β₂ : Type u₁
g : β₀ → β₁
g' : β₁ → β₂
x : F α β₀
⊢ snd (F := F) g' (snd (F := F) g x) = snd (F := F) (g' ∘ g) x

Tactic:
simp [snd, bimap_bimap]

Premises used: Bifunctor.snd, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
⊢ ∀ {α : Type u₁} {β : Type u₀} (x : _root_.flip F α β), bimap (F := _root_.flip F) id id x = x

Tactic:
simp [bimap, functor_norm]

Premises used: Bifunctor.bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u₁} {β₀ β₁ β₂ : Type u₀} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂)
    (x : _root_.flip F α₀ β₀),
    bimap (F := _root_.flip F) f' g' (bimap (F := _root_.flip F) f g x) = bimap (F := _root_.flip F) (f' ∘ f) (g' ∘ g) x

Tactic:
simp [bimap, functor_norm]

Premises used: Bifunctor.bimap
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
⊢ ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), bimap (F := Sum) id id x = x

Tactic:
aesop
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
⊢ ∀ {α₀ α₁ α₂ : Type u_1} {β₀ β₁ β₂ : Type u_2} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : α₀ ⊕ β₀),
    bimap (F := Sum) f' g' (bimap (F := Sum) f g x) = bimap (F := Sum) (f' ∘ f) (g' ∘ g) x

Tactic:
aesop
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β : Type u₁}, Eq (α := α_1 → F α β → F α α_1) mapConst (map ∘ Function.const β)

Tactic:
simp [mapConst, Functor.map]

Premises used: Functor.mapConst, Functor.map
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 : Type u₁} (x : F α α_1), id <$> x = x

Tactic:
simp [Functor.map, functor_norm]

Premises used: Functor.map
-- Module: Mathlib.Control.Bifunctor
Goal:
F : Type u₀ → Type u₁ → Type u₂
inst : Bifunctor F
inst_1 : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β γ : Type u₁} (g : α_1 → β) (h : β → γ) (x : F α α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
simp [Functor.map, functor_norm]

Premises used: Functor.map
-- Module: Mathlib.Control.Bifunctor
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
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
⊢ LawfulBifunctor.{u_1, u_2, u₂} (bicompl F G H)

Tactic:
constructor
-- Module: Mathlib.Control.Bifunctor
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
α : Type u_1
β : Type u_2
x : bicompl F G H α β
⊢ bimap (F := bicompl F G H) id id x = x

Tactic:
simp [bimap, map_id, map_comp_map, functor_norm]

Premises used: Bifunctor.bimap, Functor.map_comp_map, Functor.map_id
-- Module: Mathlib.Control.Bifunctor
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
α₀ α₁ α₂ : 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:
simp [bimap, map_id, map_comp_map, functor_norm]

Premises used: Bifunctor.bimap, Functor.map_comp_map, Functor.map_id
-- Module: Mathlib.Control.Bifunctor
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
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
⊢ LawfulBifunctor.{u₀, u₁, u_1} (bicompr G F)

Tactic:
constructor
-- Module: Mathlib.Control.Bifunctor
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
α : Type u₀
β : Type u₁
x : bicompr G F α β
⊢ bimap (F := bicompr G F) id id x = x

Tactic:
simp [bimap, functor_norm]

Premises used: Bifunctor.bimap
-- Module: Mathlib.Control.Bifunctor
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
α₀ α₁ α₂ : 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:
simp [bimap, functor_norm]

Premises used: Bifunctor.bimap
-- Module: Mathlib.Control.Bitraversable.Instances
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))
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)
⊢ LawfulBitraversable Prod

Tactic:
constructor
-- Module: Mathlib.Control.Bitraversable.Instances
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 :
  ∀ (fst : α) (snd : β), Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure (fst, snd)) (pure (fst, snd))
⊢ Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure x) (pure x)

Tactic:
casesm _ × _
-- Module: Mathlib.Control.Bitraversable.Instances
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 :
  ∀ (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))
⊢ 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:
casesm _ × _
-- Module: Mathlib.Control.Bitraversable.Instances
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 :
  ∀ (fst : α) (snd : α'),
    Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') (fst, snd))
      (pure (bimap (F := Prod) f f' (fst, snd)))
⊢ Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') x) (pure (bimap (F := Prod) f f' x))

Tactic:
casesm _ × _
-- Module: Mathlib.Control.Bitraversable.Instances
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 : α × α'
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))
⊢ 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:
casesm _ × _
-- Module: Mathlib.Control.Bitraversable.Instances
Goal:
t : Type u → Type u → Type u
inst : Bitraversable t
F : Type u → Type u
inst_1 : Applicative F
α β : Type u_1
fst : α
snd : β
⊢ Eq (α := Id (α × β)) (bitraverse (t := Prod) pure pure (fst, snd)) (pure (fst, snd))

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

Premises used: Prod.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
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 : α'
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))
⊢ 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:
simp [bitraverse, Prod.bitraverse, functor_norm]

Premises used: Prod.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
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 : α'
bitraverse_eq_bimap_id : Eq (α := Id (β × β')) (pure (f fst, f' snd)) (pure (bimap (F := Prod) f f' (fst, snd)))
⊢ Eq (α := Id (β × β')) (bitraverse (t := Prod) (pure ∘ f) (pure ∘ f') (fst, snd))
    (pure (bimap (F := Prod) f f' (fst, snd)))

Tactic:
simp [bitraverse, Prod.bitraverse, functor_norm]

Premises used: Prod.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
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 β'
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:
simp [bitraverse, Prod.bitraverse, functor_norm]

Premises used: Prod.bitraverse, Bitraversable.bitraverse
-- Module: Mathlib.Control.Bitraversable.Instances
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 : α'
⊢ 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:
rfl
-- Module: Mathlib.Control.Bitraversable.Instances
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 (β × β')) (pure (f fst, f' snd)) (pure (bimap (F := Prod) f f' (fst, snd)))

Tactic:
rfl
-- Module: Mathlib.Control.Bitraversable.Instances
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))
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)
⊢ LawfulBitraversable Sum

Tactic:
constructor
-- Module: Mathlib.Control.Bitraversable.Instances
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))
id_bitraverse₁ : ∀ (x : β), Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure (Sum.inr x)) (pure (Sum.inr x))
⊢ Eq (α := Id (α ⊕ β)) (bitraverse (t := Sum) pure pure x) (pure x)

Tactic:
casesm _ ⊕ _
-- Module: Mathlib.Control.Bitraversable.Instances
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))
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))
⊢ 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:
casesm _ ⊕ _