[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : (fun {α} => app η α) = fun {α} => app η' α
⊢ η = η'
[PROOFSTEP]
cases η
[GOAL]
case mk
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η' : ApplicativeTransformation F G
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (Seq.seq x fun x => y) = Seq.seq (app✝ (α → β) x) fun x => app✝ α y
h :
  (fun {α} => app { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } α) =
    fun {α} => app η' α
⊢ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } = η'
[PROOFSTEP]
cases η'
[GOAL]
case mk.mk
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α),
    app✝¹ β (Seq.seq x fun x => y) = Seq.seq (app✝¹ (α → β) x) fun x => app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ :
  ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (Seq.seq x fun x => y) = Seq.seq (app✝ (α → β) x) fun x => app✝ α y
h :
  (fun {α} => app { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } α) =
    fun {α} => app { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ } α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ η = η'
[PROOFSTEP]
apply coe_inj
[GOAL]
case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ (fun {α} => app η α) = fun {α} => app η' α
[PROOFSTEP]
ext1 α
[GOAL]
case h.h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
α : Type u
⊢ app η α = app η' α
[PROOFSTEP]
exact funext (h α)
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} => app η α) (x <$> y) = x <$> (fun {α} => app η α) y
[PROOFSTEP]
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
⊢ (fun {α} => app η α) ∘ Functor.map x = Functor.map x ∘ fun {α} => app η α
[PROOFSTEP]
ext y
[GOAL]
case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => app η α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => app η α) y
[PROOFSTEP]
exact preserves_map η x y
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
⊢ ∀ {α : Type u} (x : α), (fun α => id) α (pure x) = pure x
[PROOFSTEP]
simp
[GOAL]
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun α => id) β✝ (Seq.seq x fun x => y) = Seq.seq ((fun α => id) (α✝ → β✝) x) fun x => (fun α => id) α✝ y
[PROOFSTEP]
simp
[GOAL]
F : Type u → Type v
inst✝⁵ : Applicative F
inst✝⁴ : LawfulApplicative F
G : Type u → Type w
inst✝³ : Applicative G
inst✝² : LawfulApplicative G
H : Type u → Type s
inst✝¹ : Applicative H
inst✝ : LawfulApplicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ : Type u
x : α✝
⊢ (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) α✝ (pure x) = pure x
[PROOFSTEP]
simp only [preserves_pure]
[GOAL]
F : Type u → Type v
inst✝⁵ : Applicative F
inst✝⁴ : LawfulApplicative F
G : Type u → Type w
inst✝³ : Applicative G
inst✝² : LawfulApplicative G
H : Type u → Type s
inst✝¹ : Applicative H
inst✝ : LawfulApplicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α✝ β✝ : Type u
x : F (α✝ → β✝)
y : F α✝
⊢ (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) β✝ (Seq.seq x fun x => y) =
    Seq.seq ((fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) (α✝ → β✝) x) fun x =>
      (fun α x => (fun {α} => app η' α) ((fun {α} => app η α) x)) α✝ y
[PROOFSTEP]
simp only [preserves_seq]
[GOAL]
⊢ LawfulTraversable Id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
⊢ ∀ {α β : Type ?u.11560}, mapConst = map ∘ const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
⊢ ∀ {α : Type ?u.11560} (x : Id α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
⊢ ∀ {α β γ : Type ?u.11560} (g : α → β) (h : β → γ) (x : Id α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_4
⊢ ∀ {α : Type ?u.11560} (x : Id α), traverse pure x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_5
⊢ ∀ {F G : Type ?u.11560 → Type ?u.11560} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α β γ : Type ?u.11560} (f : β → F γ) (g : α → G β) (x : Id α),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_6
⊢ ∀ {α β : Type ?u.11560} (f : α → β) (x : Id α), traverse (pure ∘ f) x = id.mk (f <$> x)
[PROOFSTEP]
intros
[GOAL]
case refine'_7
⊢ ∀ {F G : Type ?u.11560 → Type ?u.11560} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type ?u.11560} (f : α → F β) (x : Id α),
    (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =
      traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.11560
⊢ mapConst = map ∘ const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α✝ : Type ?u.11560
x✝ : Id α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.11560
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Id α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α✝ : Type ?u.11560
x✝ : Id α✝
⊢ traverse pure x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
F✝ G✝ : Type ?u.11560 → Type ?u.11560
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type ?u.11560
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : Id α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α✝ β✝ : Type ?u.11560
f✝ : α✝ → β✝
x✝ : Id α✝
⊢ traverse (pure ∘ f✝) x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
F✝ G✝ : Type ?u.11560 → Type ?u.11560
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type ?u.11560
f✝ : α✝ → F✝ β✝
x✝ : Id α✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (traverse f✝ x✝) =
    traverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝) x✝
[PROOFSTEP]
rfl
