[GOAL]
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type ?u.941} (x : α × β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.941 → Type ?u.941} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type ?u.941} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : α × α'),
    bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α α' β β' : Type ?u.941} (f : α → β) (f' : α' → β') (x : α × α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.941 → Type ?u.941} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type ?u.941} (f : α → F β)
    (f' : α' → F β') (x : α × α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.941
x✝ : α✝ × β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
casesm _ × _
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.941 → Type ?u.941
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.941
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : α✝ × α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
casesm _ × _
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.941
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α✝ × α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
casesm _ × _
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.941 → Type ?u.941
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.941
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α✝ × α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
casesm _ × _
[GOAL]
case id_bitraverse.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.941
fst✝ : α✝
snd✝ : β✝
⊢ bitraverse pure pure (fst✝, snd✝) = pure (fst✝, snd✝)
[PROOFSTEP]
simp [bitraverse, Prod.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse.mk
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.941 → Type ?u.941
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.941
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) (fst✝, snd✝) =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (fst✝, snd✝))
[PROOFSTEP]
simp [bitraverse, Prod.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.941
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (fst✝, snd✝) = pure (bimap f✝ f'✝ (fst✝, snd✝))
[PROOFSTEP]
simp [bitraverse, Prod.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case binaturality.mk
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.941 → Type ?u.941
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.941
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ (fst✝, snd✝)) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) (fst✝, snd✝)
[PROOFSTEP]
simp [bitraverse, Prod.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case id_bitraverse.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.941
fst✝ : α✝
snd✝ : β✝
⊢ (Seq.seq (Prod.mk fst✝) fun x => snd✝) = (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case comp_bitraverse.mk
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.941 → Type ?u.941
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.941
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ Functor.Comp.mk
      (Seq.seq
        (((fun x => x ∘ f'✝) ∘ (fun x x_1 => Seq.seq x fun x => x_1) ∘ (fun x => Prod.mk <$> x) ∘ f✝) <$> g✝ fst✝)
        fun x => g'✝ snd✝) =
    Functor.Comp.mk
      (Seq.seq (((fun x => (fun x => Seq.seq (Prod.mk <$> f✝ x.fst) fun x_1 => f'✝ x.snd) ∘ x) ∘ Prod.mk) <$> g✝ fst✝)
        fun x => g'✝ snd✝)
[PROOFSTEP]
rfl
[GOAL]
case bitraverse_eq_bimap_id.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.941
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
fst✝ : α✝
snd✝ : α'✝
⊢ (Seq.seq (Prod.mk (f✝ fst✝)) fun x => f'✝ snd✝) = bimap f✝ f'✝ (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Sum
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type ?u.14627} (x : α ⊕ β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.14627 → Type ?u.14627} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type ?u.14627} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : α ⊕ α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α α' β β' : Type ?u.14627} (f : α → β) (f' : α' → β') (x : α ⊕ α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.14627 → Type ?u.14627} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type ?u.14627} (f : α → F β)
    (f' : α' → F β') (x : α ⊕ α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.14627
x✝ : α✝ ⊕ β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
casesm _ ⊕ _
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.14627
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : α✝ ⊕ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
casesm _ ⊕ _
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : α✝ ⊕ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
casesm _ ⊕ _
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : α✝ ⊕ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
casesm _ ⊕ _
[GOAL]
case id_bitraverse.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.14627
val✝ : α✝
⊢ bitraverse pure pure (Sum.inl val✝) = pure (Sum.inl val✝)
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case id_bitraverse.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.14627
val✝ : β✝
⊢ bitraverse pure pure (Sum.inr val✝) = pure (Sum.inr val✝)
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.14627
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
val✝ : α✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) (Sum.inl val✝) =
    Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (Sum.inl val✝))
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.14627
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
val✝ : α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) (Sum.inr val✝) =
    Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ (Sum.inr val✝))
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
val✝ : α✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (Sum.inl val✝) = pure (bimap f✝ f'✝ (Sum.inl val✝))
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
val✝ : α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) (Sum.inr val✝) = pure (bimap f✝ f'✝ (Sum.inr val✝))
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case binaturality.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
val✝ : α✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ (Sum.inl val✝)) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) (Sum.inl val✝)
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case binaturality.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
val✝ : α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ (Sum.inr val✝)) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) (Sum.inr val✝)
[PROOFSTEP]
simp [bitraverse, Sum.bitraverse, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse.inl
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.14627
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
val✝ : α✝
⊢ Comp.mk (((fun x => Sum.inl <$> x) ∘ f✝) <$> g✝ val✝) =
    Comp.mk
      (((fun x =>
            match x with
            | Sum.inl x => Sum.inl <$> f✝ x
            | Sum.inr x => Sum.inr <$> f'✝ x) ∘
          Sum.inl) <$>
        g✝ val✝)
[PROOFSTEP]
rfl
[GOAL]
case comp_bitraverse.inr
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.14627 → Type ?u.14627
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.14627
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
val✝ : α'✝
⊢ Comp.mk (((fun x => Sum.inr <$> x) ∘ f'✝) <$> g'✝ val✝) =
    Comp.mk
      (((fun x =>
            match x with
            | Sum.inl x => Sum.inl <$> f✝ x
            | Sum.inr x => Sum.inr <$> f'✝ x) ∘
          Sum.inr) <$>
        g'✝ val✝)
[PROOFSTEP]
rfl
[GOAL]
case bitraverse_eq_bimap_id.inl
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
val✝ : α✝
⊢ Sum.inl (f✝ val✝) = bimap f✝ f'✝ (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case bitraverse_eq_bimap_id.inr
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.14627
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
val✝ : α'✝
⊢ Sum.inr (f'✝ val✝) = bimap f✝ f'✝ (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Const
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type ?u.21603} (x : Const α β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.21603 → Type ?u.21603} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type ?u.21603} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : Const α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α α' β β' : Type ?u.21603} (f : α → β) (f' : α' → β') (x : Const α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type ?u.21603 → Type ?u.21603} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type ?u.21603} (f : α → F β)
    (f' : α' → F β') (x : Const α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type ?u.21603
x✝ : Const α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
simp [bitraverse, Const.bitraverse, functor_norm]
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.21603 → Type ?u.21603
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type ?u.21603
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : Const α✝ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Const.bitraverse, functor_norm]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.21603
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : Const α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Const.bitraverse, functor_norm]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.21603 → Type ?u.21603
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.21603
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : Const α✝ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
simp [bitraverse, Const.bitraverse, functor_norm]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type ?u.21603
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : Const α✝ α'✝
⊢ f✝ x✝ = bimap f✝ f'✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type ?u.21603 → Type ?u.21603
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type ?u.21603
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : Const α✝ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (f✝ x✝) = (fun {α} => ApplicativeTransformation.app η✝ α) (f✝ x✝)
[PROOFSTEP]
rfl
[GOAL]
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (_root_.flip t)
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : _root_.flip t α β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : _root_.flip t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : _root_.flip t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
    (f' : α' → F β') (x : _root_.flip t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : _root_.flip t α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
casesm LawfulBitraversable t
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
casesm LawfulBitraversable t
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
casesm LawfulBitraversable t
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : _root_.flip t α✝ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
casesm LawfulBitraversable t
[GOAL]
case id_bitraverse.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u
x✝ : _root_.flip t α✝ β✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
    (f' : α' → F β') (x : t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
apply_assumption only [*]
[GOAL]
case comp_bitraverse.mk
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
    (f' : α' → F β') (x : t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
apply_assumption only [*]
[GOAL]
case bitraverse_eq_bimap_id.mk
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
    (f' : α' → F β') (x : t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
apply_assumption only [*]
[GOAL]
case binaturality.mk
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : _root_.flip t α✝ α'✝
toLawfulBifunctor✝ : LawfulBifunctor t
id_bitraverse✝ : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
comp_bitraverse✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β)
    (g' : α' → G β') (x : t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)
bitraverse_eq_bimap_id✝ :
  ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
binaturality✝ :
  ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
    (f' : α' → F β') (x : t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
apply_assumption only [*]
[GOAL]
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ LawfulTraversable (t α)
[PROOFSTEP]
constructor
[GOAL]
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 : Type u} (x : t α α_1), traverse pure x = x
[PROOFSTEP]
intros
[GOAL]
case comp_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] {α_1 β γ : Type u} (f : β → F γ) (g : α_1 → G β) (x : t α α_1),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)
[PROOFSTEP]
intros
[GOAL]
case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), traverse (pure ∘ f) x = id.mk (f <$> x)
[PROOFSTEP]
intros
[GOAL]
case naturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α_1 β : Type u} (f : α_1 → F β) (x : t α α_1),
    (fun {α} => ApplicativeTransformation.app η α) (traverse f x) =
      traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
intros
[GOAL]
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ : Type u
x✝ : t α α✝
⊢ traverse pure x✝ = x✝
[PROOFSTEP]
simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_traverse
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f✝ : β✝ → F✝ γ✝
g✝ : α✝ → G✝ β✝
x✝ : t α α✝
⊢ traverse (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (traverse f✝ <$> traverse g✝ x✝)
[PROOFSTEP]
simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ traverse (pure ∘ f✝) x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (traverse f✝ x✝) =
    traverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝) x✝
[PROOFSTEP]
simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ tsnd (pure ∘ f✝) x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
simp [tsnd_eq_snd_id]
[GOAL]
case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : t α α✝
⊢ Bifunctor.snd f✝ x✝ = id.mk (f✝ <$> x✝)
[PROOFSTEP]
rfl
[GOAL]
case naturality
t : Type u → Type u → Type u
inst✝⁶ : Bitraversable t
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : LawfulBitraversable t
α : Type u
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ β✝ : Type u
f✝ : α✝ → F✝ β✝
x✝ : t α α✝
⊢ ApplicativeTransformation.app η✝ (t α β✝) (tsnd f✝ x✝) = tsnd (ApplicativeTransformation.app η✝ β✝ ∘ f✝) x✝
[PROOFSTEP]
simp [tsnd, binaturality, Function.comp, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompl t F G)
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : bicompl t F G α β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G_1 : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G_1] [inst_2 : LawfulApplicative F_1]
    [inst_3 : LawfulApplicative G_1] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G_1 β)
    (g' : α' → G_1 β') (x : bicompl t F G α α'),
    bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompl t F G α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G_1 : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G_1] [inst_2 : LawfulApplicative F_1]
    [inst_3 : LawfulApplicative G_1] (η : ApplicativeTransformation F_1 G_1) {α α' β β' : Type u} (f : α → F_1 β)
    (f' : α' → F_1 β') (x : bicompl t F G α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : bicompl t F G α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse, functor_norm,
  -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse, functor_norm,
  -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse, functor_norm,
  -ApplicativeTransformation.app_eq_coe]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse, functor_norm,
  -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (traverse (pure ∘ f✝)) (traverse (pure ∘ f'✝)) x✝ = bimap (Functor.map f✝) (Functor.map f'✝) x✝
[PROOFSTEP]
simp [traverse_eq_map_id', bitraverse_eq_bimap_id]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ ApplicativeTransformation.app η✝ (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (ApplicativeTransformation.app η✝ β✝ ∘ f✝))
      (traverse (ApplicativeTransformation.app η✝ β'✝ ∘ f'✝)) x✝
[PROOFSTEP]
dsimp only [bicompl]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ ApplicativeTransformation.app η✝ (t (F β✝) (G β'✝)) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (ApplicativeTransformation.app η✝ β✝ ∘ f✝))
      (traverse (ApplicativeTransformation.app η✝ β'✝ ∘ f'✝)) x✝
[PROOFSTEP]
simp [binaturality, naturality_pf]
[GOAL]
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)
[PROOFSTEP]
constructor
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : bicompr F t α β), bitraverse pure pure x = pure x
[PROOFSTEP]
intros
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F_1]
    [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β)
    (g' : α' → G β') (x : bicompr F t α α'),
    bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
[PROOFSTEP]
intros
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompr F t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
[PROOFSTEP]
intros
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F_1]
    [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F_1 G) {α α' β β' : Type u} (f : α → F_1 β)
    (f' : α' → F_1 β') (x : bicompr F t α α'),
    (fun {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) =
      bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f)
        ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
[PROOFSTEP]
intros
[GOAL]
case id_bitraverse
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : bicompr F t α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝
[PROOFSTEP]
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)
[PROOFSTEP]
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ (fun {α} => ApplicativeTransformation.app η✝ α) (bitraverse f✝ f'✝ x✝) =
    bitraverse ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f✝)
      ((fun {α} => ApplicativeTransformation.app η✝ α) ∘ f'✝) x✝
[PROOFSTEP]
simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm, -ApplicativeTransformation.app_eq_coe]
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = bimap f✝ f'✝ x✝
[PROOFSTEP]
simp [bitraverse_eq_bimap_id', traverse_eq_map_id']
[GOAL]
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ bimap f✝ f'✝ <$> x✝ = bimap f✝ f'✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ ApplicativeTransformation.app η✝ (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (ApplicativeTransformation.app η✝ β✝ ∘ f✝) (ApplicativeTransformation.app η✝ β'✝ ∘ f'✝)) x✝
[PROOFSTEP]
dsimp only [bicompr]
[GOAL]
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ ApplicativeTransformation.app η✝ (F (t β✝ β'✝)) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (ApplicativeTransformation.app η✝ β✝ ∘ f✝) (ApplicativeTransformation.app η✝ β'✝ ∘ f'✝)) x✝
[PROOFSTEP]
simp [naturality, binaturality']


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f✝ g✝ : G → E
f'✝ g'✝ : G →L[ℝ] E
s✝ : Set G
x✝ : G
n : ℕ∞
f g : ℝ → E
f' g' : E
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) s x
[PROOFSTEP]
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f✝ g✝ : G → E
f'✝ g'✝ : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
f g : ℝ → E
f' g' : E
x : ℝ
⊢ HasDerivAt f f' x →
    HasDerivAt g g' x → HasDerivAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) x
[PROOFSTEP]
simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ↑(fderiv ℝ (fun t => inner (f t) (g t)) x) y = inner (f x) (↑(fderiv ℝ g x) y) + inner (↑(fderiv ℝ f x) y) (g x)
[PROOFSTEP]
rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
y : G
⊢ ↑(ContinuousLinearMap.comp (fderivInnerClm 𝕜 (f x, g x)) (ContinuousLinearMap.prod (fderiv ℝ f x) (fderiv ℝ g x))) y =
    inner (f x) (↑(fderiv ℝ g x) y) + inner (↑(fderiv ℝ f x) y) (g x)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
⊢ ContDiff ℝ n fun x => ‖x‖ ^ 2
[PROOFSTEP]
convert (reClm : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (↑reClm ∘ fun x => inner (id x) (id x)) x✝
[PROOFSTEP]
exact (inner_self_eq_norm_sq _).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
[PROOFSTEP]
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
[PROOFSTEP]
simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => Dist.dist (f y) (g y)) x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ n (fun y => ‖f y - g y‖) x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => Dist.dist (f y) (g y)) s x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ n (fun y => ‖f y - g y‖) s x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
⊢ HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • ↑(innerSL ℝ) x) x
[PROOFSTEP]
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
⊢ HasStrictFDerivAt (fun x => ↑re (inner x x)) (2 • ↑(innerSL ℝ) x) x
[PROOFSTEP]
convert (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)
[GOAL]
case h.e'_10.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
⊢ 2 • ↑(innerSL ℝ) x =
    ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
      (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F))
[PROOFSTEP]
ext y
[GOAL]
case h.e'_10.h.h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : F
e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'
y : F
⊢ ↑(2 • ↑(innerSL ℝ) x) y =
    ↑(ContinuousLinearMap.comp (fderivInnerClm ℝ (id x, id x))
          (ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)))
      y
[PROOFSTEP]
simp [two_smul, real_inner_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => Dist.dist (f y) (g y)) x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => ‖f y - g y‖) x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => Dist.dist (f y) (g y)) s x
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (fun y => ‖f y - g y‖) s x
[PROOFSTEP]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableWithinAt_iff, differentiableWithinAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableAt_iff, differentiableAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiableOn_iff, differentiableOn_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_differentiable_iff, differentiable_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι), Differentiable 𝕜 fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x => f x i
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i)
        (comp (proj i) (comp (↑(EuclideanSpace.equiv ι 𝕜)) f')) y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i)
        (comp (proj i) (comp (↑(EuclideanSpace.equiv ι 𝕜)) f')) t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) (comp (EuclideanSpace.proj i) f') t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffAt_iff, contDiffAt_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiffOn_iff, contDiffOn_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
[PROOFSTEP]
rw [← (EuclideanSpace.equiv ι 𝕜).comp_contDiff_iff, contDiff_pi]
[GOAL]
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : Fintype ι
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
n : ℕ∞
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x => (↑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i
[PROOFSTEP]
rfl
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n ↑univUnitBall
[PROOFSTEP]
suffices ContDiff ℝ n fun x : E => ((1 : ℝ) + ‖x‖ ^ 2).sqrt⁻¹ from this.smul contDiff_id
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => (sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
refine' ContDiff.inv _ fun x => Real.sqrt_ne_zero'.mpr (h x)
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ n fun x => sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffWithinAt ℝ n (↑(LocalHomeomorph.symm univUnitBall)) (ball 0 1) y
[PROOFSTEP]
apply ContDiffAt.contDiffWithinAt
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n (↑(LocalHomeomorph.symm univUnitBall)) y
[PROOFSTEP]
suffices ContDiffAt ℝ n (fun y : E => ((1 : ℝ) - ‖y‖ ^ 2).sqrt⁻¹) y from this.smul contDiffAt_id
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
[PROOFSTEP]
have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
  rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => (sqrt (1 - ‖y‖ ^ 2))⁻¹) y
[PROOFSTEP]
refine' ContDiffAt.inv _ (Real.sqrt_ne_zero'.mpr h)
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => sqrt (1 - ‖y‖ ^ 2)) y
[PROOFSTEP]
refine' (contDiffAt_sqrt h.ne').comp y _
[GOAL]
case h
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ n (fun y => 1 - ‖y‖ ^ 2) y
[PROOFSTEP]
exact contDiffAt_const.sub (contDiff_norm_sq ℝ).contDiffAt
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ n ↑(univBall c r)
[PROOFSTEP]
unfold univBall
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ n
    ↑(if h : 0 < r then
        LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
      else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ n
    ↑(LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
        (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))
[PROOFSTEP]
exact (contDiff_unitBallBall h).comp contDiff_univUnitBall
[GOAL]
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ n ↑(Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
[PROOFSTEP]
exact contDiff_id.add contDiff_const
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ n (↑(LocalHomeomorph.symm (univBall c r))) (ball c r)
[PROOFSTEP]
unfold univBall
[GOAL]
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm
        (if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    (ball c r)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm
        (LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))))
    (ball c r)
[PROOFSTEP]
refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ball c r ⊆ (fun x => ↑(LocalEquiv.symm (unitBallBall c r h).toLocalEquiv) x) ⁻¹' ball 0 1
[PROOFSTEP]
rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
[GOAL]
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ (unitBallBall c r h).toLocalEquiv.target ⊆
    (fun x => ↑(LocalEquiv.symm (unitBallBall c r h).toLocalEquiv) x) ⁻¹' (unitBallBall c r h).toLocalEquiv.source
[PROOFSTEP]
apply LocalHomeomorph.symm_mapsTo
[GOAL]
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ n
    (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))))
    (ball c r)
[PROOFSTEP]
exact contDiffOn_id.sub contDiffOn_const


[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
⊢ x = y
[PROOFSTEP]
unfold ContT
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
⊢ x = y
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
x✝ : α → m r
⊢ x x✝ = y x✝
[PROOFSTEP]
apply h
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α : Type ?u.3230} (x : ContT r m α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ : Type ?u.3230
x✝ : ContT r m α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β : Type ?u.3230} (x : α) (f : α → ContT r m β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.3230
x✝ : α✝
f✝ : α✝ → ContT r m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.3230
x✝ : α✝
f✝¹ : α✝ → ContT r m β✝
f✝ : β✝ → m r
⊢ run (pure x✝ >>= f✝¹) f✝ = run (f✝¹ x✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β γ : Type ?u.3230} (x : ContT r m α) (f : α → ContT r m β) (g : β → ContT r m γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ γ✝ : Type ?u.3230
x✝ : ContT r m α✝
f✝ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ γ✝ : Type ?u.3230
x✝ : ContT r m α✝
f✝¹ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
f✝ : γ✝ → m r
⊢ run (x✝ >>= f✝¹ >>= g✝) f✝ = run (x✝ >>= fun x => f✝¹ x >>= g✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α✝ β✝ γ ω : Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ monadLift (x >>= f) = monadLift x >>= monadLift ∘ f
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α✝ β✝ γ ω : Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
f✝ : β → m r
⊢ run (monadLift (x >>= f)) f✝ = run (monadLift x >>= monadLift ∘ f) f✝
[PROOFSTEP]
simp only [monadLift, MonadLift.monadLift, (· ∘ ·), (· >>= ·), bind_assoc, id.def, run, ContT.monadLift]
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α ω γ : Type ?u.4864} (cmd : ContT r m α) (next : Label ω (ContT r m) γ → α → ContT r m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ ω✝ γ✝ : Type ?u.4864
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ ω✝ γ✝ : Type ?u.4864
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
f✝ : ω✝ → m r
⊢ run (callCC fun f => cmd✝ >>= next✝ f) f✝ =
    run
      (do
        let x ← cmd✝
        callCC fun f => next✝ f x)
      f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α : Type ?u.4864} (β : Type ?u.4864) (x : α) (dead : Label α (ContT r m) β → β → ContT r m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
f✝ : α✝ → m r
⊢ run (callCC fun f => goto f x✝ >>= dead✝ f) f✝ = run (pure x✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β : Type ?u.4864} (dummy : ContT r m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
dummy✝ : ContT r m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
dummy✝ : ContT r m α✝
f✝ : α✝ → m r
⊢ run (callCC fun x => dummy✝) f✝ = run dummy✝ f✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ExceptT ε m α) (next : Label ω (ExceptT ε m) γ → α → ExceptT ε m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, ExceptT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (ExceptT.mk do
      let x ← ExceptT.run cmd✝
      callCC fun f =>
          match x with
          | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
          | Except.error e => pure (Except.error e)) =
    do
    let x ← cmd✝
    ExceptT.mk (callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x))
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ ExceptT.run
      (ExceptT.mk do
        let x ← ExceptT.run cmd✝
        callCC fun f =>
            match x with
            | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
            | Except.error e => pure (Except.error e)) =
    ExceptT.run do
      let x ← cmd✝
      ExceptT.mk (callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x))
[PROOFSTEP]
dsimp
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (do
      let x ← ExceptT.run cmd✝
      callCC fun f =>
          match x with
          | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
          | Except.error e => pure (Except.error e)) =
    do
    let x ← ExceptT.run cmd✝
    match x with
      | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
      | Except.error e => pure (Except.error e)
[PROOFSTEP]
congr with ⟨⟩
[GOAL]
case h.e_a.h.error
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : ε
⊢ (callCC fun f =>
      match Except.error a✝ with
      | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
      | Except.error e => pure (Except.error e)) =
    match Except.error a✝ with
    | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
    | Except.error e => pure (Except.error e)
[PROOFSTEP]
simp [ExceptT.bindCont, @callCC_dummy m _]
[GOAL]
case h.e_a.h.ok
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : α✝
⊢ (callCC fun f =>
      match Except.ok a✝ with
      | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
      | Except.error e => pure (Except.error e)) =
    match Except.ok a✝ with
    | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
    | Except.error e => pure (Except.error e)
[PROOFSTEP]
simp [ExceptT.bindCont, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ExceptT ε m) β → β → ExceptT ε m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, ExceptT.callCC, callCC_bind_right, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, bind_assoc,
  @callCC_bind_left m _, Function.comp]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ ExceptT.mk (pure (Except.ok x✝)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ ExceptT.run (ExceptT.mk (pure (Except.ok x✝))) = ExceptT.run (pure x✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : ExceptT ε m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, ExceptT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.mk (ExceptT.run dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.run (ExceptT.mk (ExceptT.run dummy✝)) = ExceptT.run dummy✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : OptionT m α) (next : Label ω (OptionT m) γ → α → OptionT m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, OptionT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (OptionT.mk do
      let x ← OptionT.run cmd✝
      callCC fun f =>
          match x with
          | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
          | none => pure none) =
    do
    let x ← cmd✝
    OptionT.mk (callCC fun x_1 => OptionT.run (next✝ (OptionT.mkLabel x_1) x))
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ OptionT.run
      (OptionT.mk do
        let x ← OptionT.run cmd✝
        callCC fun f =>
            match x with
            | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
            | none => pure none) =
    OptionT.run do
      let x ← cmd✝
      OptionT.mk (callCC fun x_1 => OptionT.run (next✝ (OptionT.mkLabel x_1) x))
[PROOFSTEP]
dsimp
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (do
      let x ← OptionT.run cmd✝
      callCC fun f =>
          match x with
          | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
          | none => pure none) =
    do
    let x ← OptionT.run cmd✝
    match x with
      | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
      | none => pure none
[PROOFSTEP]
congr with ⟨⟩
[GOAL]
case h.e_a.h.none
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f =>
      match none with
      | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
      | none => pure none) =
    match none with
    | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
    | none => pure none
[PROOFSTEP]
simp [@callCC_dummy m _]
[GOAL]
case h.e_a.h.some
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
val✝ : α✝
⊢ (callCC fun f =>
      match some val✝ with
      | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
      | none => pure none) =
    match some val✝ with
    | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
    | none => pure none
[PROOFSTEP]
simp [@callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (OptionT m) β → β → OptionT m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, OptionT.callCC, callCC_bind_right, OptionT.goto_mkLabel, map_eq_bind_pure_comp, bind_assoc,
  @callCC_bind_left m _, Function.comp]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ OptionT.mk (pure (some x✝)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ OptionT.run (OptionT.mk (pure (some x✝))) = OptionT.run (pure x✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : OptionT m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, OptionT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ OptionT.mk (OptionT.run dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ OptionT.run (OptionT.mk (OptionT.run dummy✝)) = OptionT.run dummy✝
[PROOFSTEP]
rfl
  /- Porting note: In Lean 3, `One ω` is required for `MonadLift (WriterT ω m)`. In Lean 4,
                   `EmptyCollection ω` or `Monoid ω` is required. So we give definitions for the both
                   instances. -/
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = StateT.mk fun s => goto x (i, s)
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = StateT.mk fun s => goto { apply := apply✝ } (i, s)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : StateT σ m α) (next : Label ω (StateT σ m) γ → α → StateT σ m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (StateT.mk fun r => do
      let x ← StateT.run cmd✝ r
      callCC fun f => StateT.run (next✝ (StateT.mkLabel f) x.fst) x.snd) =
    do
    let x ← cmd✝
    StateT.mk fun r => callCC fun f' => StateT.run (next✝ (StateT.mkLabel f') x) r
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
s✝ : σ
⊢ StateT.run
      (StateT.mk fun r => do
        let x ← StateT.run cmd✝ r
        callCC fun f => StateT.run (next✝ (StateT.mkLabel f) x.fst) x.snd)
      s✝ =
    StateT.run
      (do
        let x ← cmd✝
        StateT.mk fun r => callCC fun f' => StateT.run (next✝ (StateT.mkLabel f') x) r)
      s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (StateT σ m) β → β → StateT σ m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_left, StateT.goto_mkLabel]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
⊢ (StateT.mk fun r => pure (x✝, r)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
s✝ : σ
⊢ StateT.run (StateT.mk fun r => pure (x✝, r)) s✝ = StateT.run (pure x✝) s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : StateT σ m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_right, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (StateT.mk fun r => StateT.run dummy✝ r) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
s✝ : σ
⊢ StateT.run (StateT.mk fun r => StateT.run dummy✝ r) s✝ = StateT.run dummy✝ s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ReaderT ρ m α) (next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, ReaderT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (ReaderT.mk fun r => do
      let x ← ReaderT.run cmd✝ r
      callCC fun f => ReaderT.run (next✝ (ReaderT.mkLabel ρ f) x) r) =
    do
    let x ← cmd✝
    ReaderT.mk fun r => callCC fun f' => ReaderT.run (next✝ (ReaderT.mkLabel ρ f') x) r
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ ReaderT.run
      (ReaderT.mk fun r => do
        let x ← ReaderT.run cmd✝ r
        callCC fun f => ReaderT.run (next✝ (ReaderT.mkLabel ρ f) x) r)
      ctx✝ =
    ReaderT.run
      (do
        let x ← cmd✝
        ReaderT.mk fun r => callCC fun f' => ReaderT.run (next✝ (ReaderT.mkLabel ρ f') x) r)
      ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, ReaderT.callCC, callCC_bind_left, ReaderT.goto_mkLabel]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (ReaderT.mk fun r => pure x✝) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ ReaderT.run (ReaderT.mk fun r => pure x✝) ctx✝ = ReaderT.run (pure x✝) ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : ReaderT ρ m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, ReaderT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r => ReaderT.run dummy✝ r) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ ReaderT.run (ReaderT.mk fun r => ReaderT.run dummy✝ r) ctx✝ = ReaderT.run dummy✝ ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) ((fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) f) = f
[PROOFSTEP]
funext r
[GOAL]
case h
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) ((fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) f) r = f r
[PROOFSTEP]
simp
[GOAL]
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) ((fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) f) = f
[PROOFSTEP]
funext r
[GOAL]
case h
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) ((fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) f) r = f r
[PROOFSTEP]
simp