[GOAL]
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ (Seq.seq (f <$> x) fun x => g <$> y) = Seq.seq ((flip (fun x x_1 => x ∘ x_1) g ∘ f) <$> x) fun x => y
[PROOFSTEP]
simp [flip, functor_norm]
[GOAL]
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β
⊢ (fun x x_1 => Seq.seq x fun x => x_1) (pure f) = (fun x x_1 => x <$> x_1) f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β
x✝ : F α
⊢ (fun x x_1 => Seq.seq x fun x => x_1) (pure f) x✝ = (fun x x_1 => x <$> x_1) f x✝
[PROOFSTEP]
simp [functor_norm]
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
obtain rfl : @p1 = @p2 := by
  funext α x
  apply H1
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
⊢ p1 = p2
[PROOFSTEP]
funext α x
[GOAL]
case h.h
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
α : Type u
x : α
⊢ p1 x = p2 x
[PROOFSTEP]
apply H1
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
obtain rfl : @s1 = @s2 := by
  funext α β f x
  exact H2 f (x Unit.unit)
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
⊢ s1 = s2
[PROOFSTEP]
funext α β f x
[GOAL]
case h.h.h.h
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
α β : Type u
f : F (α → β)
x : Unit → F α
⊢ s1 f x = s2 f x
[PROOFSTEP]
exact H2 f (x Unit.unit)
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
[GOAL]
case mk
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
[GOAL]
case mk.mk
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
obtain rfl : F1 = F2 := by
  apply Functor.ext
  intros
  exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)
[GOAL]
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ F1 = F2
[PROOFSTEP]
apply Functor.ext
[GOAL]
case a
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ ∀ (α β : Type u) (f : α → β) (x : F α), f <$> x = f <$> x
[PROOFSTEP]
intros
[GOAL]
case a
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : F α✝
⊢ f✝ <$> x✝ = f✝ <$> x✝
[PROOFSTEP]
exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)
[GOAL]
case mk.mk
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ mk = mk
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSeqLeft.e_seqLeft
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ sl1 = sl2
[PROOFSTEP]
funext α β x y
[GOAL]
case mk.mk.e_toSeqRight.e_seqRight
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α β γ σ : Type u
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 β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
⊢ sr1 = sr2
[PROOFSTEP]
funext α β x y
[GOAL]
case mk.mk.e_toSeqLeft.e_seqLeft.h.h.h.h
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ γ σ : Type u
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 β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
α β : Type u
x : F α
y : Unit → F β
⊢ sl1 x y = sl2 x y
[PROOFSTEP]
exact (seqLeft_eq1 _ (y Unit.unit)).trans (seqLeft_eq2 _ _).symm
[GOAL]
case mk.mk.e_toSeqRight.e_seqRight.h.h.h.h
F✝ : Type u → Type v
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ γ σ : Type u
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 β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq1 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝¹ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
seqRight_eq2 :
  ∀ {α β : Type u} (x : F α) (y : F β), (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
seq_assoc✝ :
  ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (comp <$> h) fun x => g) fun x_1 => x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y
[PROOFSTEP]
exact (seqRight_eq1 _ (y Unit.unit)).trans (seqRight_eq2 _ (y Unit.unit)).symm
[GOAL]
⊢ CommApplicative Id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
⊢ ∀ {α β : Type ?u.6279}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
⊢ ∀ {α : Type ?u.6279} (x : Id α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
⊢ ∀ {α β γ : Type ?u.6279} (g : α → β) (h : β → γ) (x : Id α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_4
⊢ ∀ {α β : Type ?u.6279} (x : Id α) (y : Id β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_5
⊢ ∀ {α β : Type ?u.6279} (x : Id α) (y : Id β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_6
⊢ ∀ {α β : Type ?u.6279} (g : α → β) (x : Id α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_7
⊢ ∀ {α β : Type ?u.6279} (g : α → β) (x : α), g <$> pure x = pure (g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_8
⊢ ∀ {α β : Type ?u.6279} (g : Id (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
[PROOFSTEP]
intros
[GOAL]
case refine'_9
⊢ ∀ {α β γ : Type ?u.6279} (x : Id α) (g : Id (α → β)) (h : Id (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
case refine'_10
⊢ ∀ {α β : Type ?u.6279} (a : Id α) (b : Id β),
    (Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => (a, b)) <$> b) fun x => a
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.6279
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α✝ : Type ?u.6279
x✝ : Id α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.6279
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Id α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α✝ β✝ : Type ?u.6279
x✝ : Id α✝
y✝ : Id β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α✝ β✝ : Type ?u.6279
x✝ : Id α✝
y✝ : Id β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α✝ β✝ : Type ?u.6279
g✝ : α✝ → β✝
x✝ : Id α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α✝ β✝ : Type ?u.6279
g✝ : α✝ → β✝
x✝ : α✝
⊢ g✝ <$> pure x✝ = pure (g✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α✝ β✝ : Type ?u.6279
g✝ : Id (α✝ → β✝)
x✝ : α✝
⊢ (Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <$> g✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α✝ β✝ γ✝ : Type ?u.6279
x✝ : Id α✝
g✝ : Id (α✝ → β✝)
h✝ : Id (β✝ → γ✝)
⊢ (Seq.seq h✝ fun x => Seq.seq g✝ fun x => x✝) = Seq.seq (Seq.seq (Function.comp <$> h✝) fun x => g✝) fun x => x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α✝ β✝ : Type ?u.6279
a✝ : Id α✝
b✝ : Id β✝
⊢ (Seq.seq (Prod.mk <$> a✝) fun x => b✝) = Seq.seq ((fun b a => (a, b)) <$> b✝) fun x => a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
f : α → β
x : α
⊢ run (f <$> pure x) = run (pure (f x))
[PROOFSTEP]
simp
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
f : Comp F G (α → β)
x : α
⊢ run (Seq.seq f fun x_1 => pure x) = run ((fun g => g x) <$> f)
[PROOFSTEP]
simp [(· ∘ ·), functor_norm]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
x : Comp F G α
f : Comp F G (α → β)
g : Comp F G (β → γ)
⊢ run (Seq.seq g fun x_1 => Seq.seq f fun x_2 => x) =
    run (Seq.seq (Seq.seq (Function.comp <$> g) fun x => f) fun x_1 => x)
[PROOFSTEP]
simp [(· ∘ ·), functor_norm]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
f : α → β
x : Comp F G α
⊢ run (Seq.seq (pure f) fun x_1 => x) = run (f <$> x)
[PROOFSTEP]
simp [Applicative.pure_seq_eq_map', functor_norm]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ α✝ β✝ : Type v
x✝ : Comp F G α✝
y✝ : Comp F G β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
F✝ : Type u → Type w
G : Type v → Type u
inst✝⁴ : Applicative F✝
inst✝³ : Applicative G
inst✝² : LawfulApplicative F✝
inst✝¹ : LawfulApplicative G
α β γ : Type v
F : Type u_1 → Type u_2
AF : Applicative F
inst✝ : LawfulApplicative F
α✝ β✝ : Type u_1
f : F (α✝ → β✝)
x : F α✝
⊢ (Seq.seq (id <$> f) fun x_1 => x) = Seq.seq f fun x_1 => x
[PROOFSTEP]
rw [id_map]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
⊢ CommApplicative (Comp f g)
[PROOFSTEP]
refine' { @instLawfulApplicativeComp f g _ _ _ _ with .. }
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
⊢ ∀ {α β : Type v} (a : Comp f g α) (b : Comp f g β),
    (Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => (a, b)) <$> b) fun x => a
[PROOFSTEP]
intros
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
⊢ (Seq.seq (Prod.mk <$> a✝) fun x => b✝) = Seq.seq ((fun b a => (a, b)) <$> b✝) fun x => a✝
[PROOFSTEP]
simp! [map, Seq.seq, functor_norm]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
⊢ mk (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> mk ((fun x => Prod.mk <$> x) <$> a✝)) fun x => b✝) =
    mk
      (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> mk ((fun x => (fun b a => (a, b)) <$> x) <$> b✝)) fun x => a✝)
[PROOFSTEP]
rw [commutative_map]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
⊢ mk (Seq.seq ((flip fun x x_1 => Seq.seq x fun x => x_1) <$> b✝) fun x => mk ((fun x => Prod.mk <$> x) <$> a✝)) =
    mk
      (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> mk ((fun x => (fun b a => (a, b)) <$> x) <$> b✝)) fun x => a✝)
[PROOFSTEP]
simp [Comp.mk, flip, (· ∘ ·), functor_norm]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
⊢ (Seq.seq ((fun x x_1 => Seq.seq (Prod.mk <$> x_1) fun x_2 => x) <$> b✝) fun x => a✝) =
    Seq.seq ((fun x x_1 => Seq.seq ((fun b a => (a, b)) <$> x) fun x => x_1) <$> b✝) fun x => a✝
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
⊢ (fun x x_1 => Seq.seq (Prod.mk <$> x_1) fun x_2 => x) = fun x x_1 => Seq.seq ((fun b a => (a, b)) <$> x) fun x => x_1
[PROOFSTEP]
funext x y
[GOAL]
case e_a.e_a.h.h
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ (Seq.seq (Prod.mk <$> y) fun x_1 => x) = Seq.seq ((fun b a => (a, b)) <$> x) fun x => y
[PROOFSTEP]
rw [commutative_map]
[GOAL]
case e_a.e_a.h.h
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
src✝ : LawfulApplicative (Comp f g) := instLawfulApplicativeComp
α✝ β✝ : Type v
a✝ : Comp f g α✝
b✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ (Seq.seq (flip Prod.mk <$> x) fun x => y) = Seq.seq ((fun b a => (a, b)) <$> x) fun x => y
[PROOFSTEP]
congr
[GOAL]
α : Type ?u.61704
inst✝ : Monoid α
⊢ LawfulApplicative (Const α)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 : Type ?u.61710} (x : Const α α_1), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β γ : Type ?u.61710} (g : α_1 → β) (h : β → γ) (x : Const α α_1), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710} (x : Const α α_1) (y : Const α β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710} (x : Const α α_1) (y : Const α β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α_1 id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710} (g : α_1 → β) (x : Const α α_1), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710} (g : α_1 → β) (x : α_1), g <$> pure x = pure (g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β : Type ?u.61710} (g : Const α (α_1 → β)) (x : α_1), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type ?u.61704
inst✝ : Monoid α
⊢ ∀ {α_1 β γ : Type ?u.61710} (x : Const α α_1) (g : Const α (α_1 → β)) (h : Const α (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_2
α : Type ?u.61704
inst✝ : Monoid α
α✝ : Type ?u.61710
x✝ : Const α α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_3
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ γ✝ : Type ?u.61710
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const α α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_4
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
x✝ : Const α α✝
y✝ : Const α β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_5
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
x✝ : Const α α✝
y✝ : Const α β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_6
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : α✝ → β✝
x✝ : Const α α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_7
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : α✝ → β✝
x✝ : α✝
⊢ g✝ <$> pure x✝ = pure (g✝ x✝)
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_8
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : Const α (α✝ → β✝)
x✝ : α✝
⊢ (Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <$> g✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_9
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ γ✝ : Type ?u.61710
x✝ : Const α α✝
g✝ : Const α (α✝ → β✝)
h✝ : Const α (β✝ → γ✝)
⊢ (Seq.seq h✝ fun x => Seq.seq g✝ fun x => x✝) = Seq.seq (Seq.seq (Function.comp <$> h✝) fun x => g✝) fun x => x✝
[PROOFSTEP]
simp [mul_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_1
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
⊢ mapConst = Const.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type ?u.61704
inst✝ : Monoid α
α✝ : Type ?u.61710
x✝ : Const α α✝
⊢ Const.map id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ γ✝ : Type ?u.61710
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const α α✝
⊢ Const.map (h✝ ∘ g✝) x✝ = Const.map h✝ (Const.map g✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
x✝ : Const α α✝
y✝ : Const α β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Const.map (Function.const β✝) x✝ * y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
x✝ : Const α α✝
y✝ : Const α β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Const.map (Function.const α✝ id) x✝ * y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : α✝ → β✝
x✝ : Const α α✝
⊢ x✝ = Const.map g✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : α✝ → β✝
x✝ : α✝
⊢ Const.map g✝ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ : Type ?u.61710
g✝ : Const α (α✝ → β✝)
x✝ : α✝
⊢ g✝ = Const.map (fun h => h x✝) g✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type ?u.61704
inst✝ : Monoid α
α✝ β✝ γ✝ : Type ?u.61710
x✝ : Const α α✝
g✝ : Const α (α✝ → β✝)
h✝ : Const α (β✝ → γ✝)
⊢ h✝ * (g✝ * x✝) = Const.map Function.comp h✝ * (g✝ * x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ LawfulApplicative (AddConst α)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 : Type ?u.64153} (x : AddConst α α_1), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β γ : Type ?u.64153} (g : α_1 → β) (h : β → γ) (x : AddConst α α_1), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153} (x : AddConst α α_1) (y : AddConst α β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153} (x : AddConst α α_1) (y : AddConst α β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α_1 id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153} (g : α_1 → β) (x : AddConst α α_1), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153} (g : α_1 → β) (x : α_1), g <$> pure x = pure (g x)
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β : Type ?u.64153} (g : AddConst α (α_1 → β)) (x : α_1), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <$> g
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type ?u.64148
inst✝ : AddMonoid α
⊢ ∀ {α_1 β γ : Type ?u.64153} (x : AddConst α α_1) (g : AddConst α (α_1 → β)) (h : AddConst α (β → γ)),
    (Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun x => g) fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_2
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ : Type ?u.64153
x✝ : AddConst α α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_3
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type ?u.64153
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : AddConst α α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_4
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
x✝ : AddConst α α✝
y✝ : AddConst α β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_5
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
x✝ : AddConst α α✝
y✝ : AddConst α β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_6
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : α✝ → β✝
x✝ : AddConst α α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_7
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : α✝ → β✝
x✝ : α✝
⊢ g✝ <$> pure x✝ = pure (g✝ x✝)
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_8
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : AddConst α (α✝ → β✝)
x✝ : α✝
⊢ (Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <$> g✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_9
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type ?u.64153
x✝ : AddConst α α✝
g✝ : AddConst α (α✝ → β✝)
h✝ : AddConst α (β✝ → γ✝)
⊢ (Seq.seq h✝ fun x => Seq.seq g✝ fun x => x✝) = Seq.seq (Seq.seq (Function.comp <$> h✝) fun x => g✝) fun x => x✝
[PROOFSTEP]
simp [add_assoc, (· <$> ·), Seq.seq, pure]
[GOAL]
case refine'_1
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
⊢ mapConst = Const.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ : Type ?u.64153
x✝ : AddConst α α✝
⊢ Const.map id x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type ?u.64153
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : AddConst α α✝
⊢ Const.map (h✝ ∘ g✝) x✝ = Const.map h✝ (Const.map g✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
x✝ : AddConst α α✝
y✝ : AddConst α β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Const.map (Function.const β✝) x✝ + y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
x✝ : AddConst α α✝
y✝ : AddConst α β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Const.map (Function.const α✝ id) x✝ + y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : α✝ → β✝
x✝ : AddConst α α✝
⊢ x✝ = Const.map g✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : α✝ → β✝
x✝ : α✝
⊢ Const.map g✝ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ : Type ?u.64153
g✝ : AddConst α (α✝ → β✝)
x✝ : α✝
⊢ g✝ = Const.map (fun h => h x✝) g✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type ?u.64148
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type ?u.64153
x✝ : AddConst α α✝
g✝ : AddConst α (α✝ → β✝)
h✝ : AddConst α (β✝ → γ✝)
⊢ h✝ + (g✝ + x✝) = Const.map Function.comp h✝ + (g✝ + x✝)
[PROOFSTEP]
rfl


[GOAL]
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m', mapConst := mc' }
[PROOFSTEP]
cases show @m = @m' by funext α β f x; apply H
[GOAL]
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ m = m'
[PROOFSTEP]
funext α β f x
[GOAL]
case h.h.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x
[PROOFSTEP]
apply H
[GOAL]
case refl
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m, mapConst := mc' }
[PROOFSTEP]
congr
[GOAL]
case refl.e_mapConst
F✝ : Type u → Type v
α β γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ mc = mc'
[PROOFSTEP]
funext α β
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
⊢ mc = mc'
[PROOFSTEP]
have E1 := @map_const _ ⟨@m, @mc⟩ H1
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
⊢ mc = mc'
[PROOFSTEP]
have E2 := @map_const _ ⟨@m, @mc'⟩ H2
[GOAL]
case refl.e_mapConst.h.h
F✝ : Type u → Type v
α✝ β✝ γ : Type u
inst✝¹ : Functor F✝
inst✝ : LawfulFunctor F✝
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
E2 : ∀ {α β : Type u_1}, mapConst = map ∘ Function.const β
⊢ mc = mc'
[PROOFSTEP]
exact E1.trans E2.symm
[GOAL]
γ : Type ?u.2497
⊢ LawfulFunctor (Const γ)
[PROOFSTEP]
constructor
[GOAL]
case map_const
γ : Type ?u.2497
⊢ ∀ {α β : Type ?u.2498}, mapConst = map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case id_map
γ : Type ?u.2497
⊢ ∀ {α : Type ?u.2498} (x : Const γ α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case comp_map
γ : Type ?u.2497
⊢ ∀ {α β γ_1 : Type ?u.2498} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case map_const
γ : Type ?u.2497
α✝ β✝ : Type ?u.2498
⊢ mapConst = map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case id_map
γ : Type ?u.2497
α✝ : Type ?u.2498
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
case comp_map
γ : Type ?u.2497
α✝ β✝ γ✝ : Type ?u.2498
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x
[PROOFSTEP]
simp [Comp.map, Functor.map_id]
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
x : F (G α)
⊢ mk (mk x) = mk x
[PROOFSTEP]
rfl
  -- porting note: `rfl` wasn't needed in mathlib3
[GOAL]
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))
[PROOFSTEP]
simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm]
  -- porting note: `Comp.mk` wasn't needed in mathlib3