awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor : LawfulFunctor F
⊢ ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
⊢ ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
⊢ ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
⊢ ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
⊢ ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
a : ∀ (α β : Type u) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ F1 = F2

Tactic:
apply Functor.ext

Premises used: Functor.ext
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
f : α → β
x : F α
⊢ f <$> x = f <$> x

Tactic:
(pure_seq1 _ _).symm.trans (pure_seq2 _ _)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
f : α → β
x : F α
⊢ f <$> x = f <$> x

Tactic:
exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
obtain :
  ∀ (H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x))
    (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) [LawfulFunctor F]
    (seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y)
    (seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y))
    (pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x),
    (∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g) →
      (∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x) →
        Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
          { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain rfl : F1 = F2 := by
      apply Functor.ext
      intros
      exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)

Premises used: rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
e_toSeqLeft : @sl1 = @sl2
e_toSeqRight : @sr1 = @sr2
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }

Tactic:
congr
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
e_toSeqLeft : ∀ (α β : Type u) (x : F α) (y : Unit → F β), sl1 x y = sl2 x y
⊢ @sl1 = @sl2

Tactic:
funext α β x y
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
e_toSeqRight : ∀ (α β : Type u) (x : F α) (y : Unit → F β), sr1 x y = sr2 x y
⊢ @sr1 = @sr2

Tactic:
funext α β x y
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sl1 x y = sl2 x y

Tactic:
(seqLeft_eq1 _ (y Unit.unit)).trans (seqLeft_eq2 _ _).symm

Premises used: Unit.unit, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sl1 x y = sl2 x y

Tactic:
exact (seqLeft_eq1 _ (y Unit.unit)).trans (seqLeft_eq2 _ _).symm

Premises used: Unit.unit, Eq.symm, Eq.trans