-- Mathlib/Control/Applicative.lean
theorem Applicative.ext {F} :
    ∀ {A1 : Applicative F} {A2 : Applicative F} [@LawfulApplicative F A1] [@LawfulApplicative F A2],
      (∀ {α : Type u} (x : α), @Pure.pure _ A1.toPure _ x = @Pure.pure _ A2.toPure _ x) →
      (∀ {α β : Type u} (f : F (α → β)) (x : F α),
          @Seq.seq _ A1.toSeq _ _ f (fun _ => x) = @Seq.seq _ A2.toSeq _ _ f (fun _ => x)) →
      A1 = A2
  | { toFunctor := F1, seq := s1, pure := p1, seqLeft := sl1, seqRight := sr1 },
    { toFunctor := F2, seq := s2, pure := p2, seqLeft := sl2, seqRight := sr2 },
    L1, L2, H1, H2 => by
    obtain rfl : @p1 = @p2

Proof state:
case h.h
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
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α : Type u
x : α
⊢ p1 x = p2 x

Tactic:
apply H1

Result:
no goals

Proof state:
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
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ s1 = s2

Tactic:
funext α β f x

Result:
case h.h.h.h
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
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x

Proof state:
case h.h.h.h
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
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x

Tactic:
exact H2 f (x Unit.unit)

Result:
no goals

Proof state:
case a
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 : α), 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 β), 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 β), 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
seq_assoc✝ : ∀ {α β γ : 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 _ _)

Result:
no goals

Proof state:
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
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ mk = mk

Tactic:
obtain rfl : @s1 = @s2 := by
  funext α β f x
  exact H2 f (x Unit.unit)

Result:
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 β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ mk = mk