mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
⊢ [Condensed.IsDiscrete M, IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 1 ↔ 6 :=
    (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
      (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
      CompHaus.isTerminalPUnit _).symm

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
⊢ [Condensed.IsDiscrete M, IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.obj).mapCocone S.asLimitCone.op))].TFAE
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ Sheaf.IsConstant (coherentTopology CompHaus)
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
constructor

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full
⊢ (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).essImage
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ Sheaf.IsConstant (coherentTopology LightProfinite)
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
constructor

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ (constantSheaf (coherentTopology LightProfinite) (Type u)).essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
x✝² x✝¹ : LightProfiniteᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.obj.map x✝ ≫
      ↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) =
    (↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) ≫
      X.toTopCat.toLightCondSet.obj.map x✝

Tactic:
ext

Goal state after:
X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
x✝³ x✝² : LightProfiniteᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ (ConcreteCategory.hom
          (X.obj.map x✝¹ ≫
            ↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ })).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ }) ≫
            X.toTopCat.toLightCondSet.obj.map x✝¹)).toFun
      x✝
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X Y✝ : LightCondSet
f : X ⟶ Y✝
Y : LightCondSet
⊢ lightCondSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
      { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (lightCondSetToTopCat.obj Y) =
    𝟙 (lightCondSetToTopCat.obj Y)

Tactic:
ext

Goal state after:
X Y✝ : LightCondSet
f : X ⟶ Y✝
Y : LightCondSet
x✝ : ↑(lightCondSetToTopCat.obj Y)
⊢ (ConcreteCategory.hom
        (lightCondSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
          { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (lightCondSetToTopCat.obj Y)))
      x✝ =
    (ConcreteCategory.hom (𝟙 (lightCondSetToTopCat.obj Y))) x✝
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ F.map (toProfinite.map x✝.unop).op ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
ext

Goal state after:
S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : F.obj (Opposite.op (toProfinite.obj (Opposite.unop X✝)))
x✝ : (Opposite.unop Y✝).obj
⊢ (ConcreteCategory.hom
          (F.map (toProfinite.map x✝².unop).op ≫
            (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom)).toFun
      x✝¹ x✝ =
    (ConcreteCategory.hom
          ((isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝²)).toFun
      x✝¹ x✝
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, CompHausLike.const_comp,
    ← isoFinYonedaComponents_hom_apply, Iso.inv_hom_id_apply, Function.comp_apply]

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ F.map (toLightProfinite.map x✝.unop).op ≫ (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
ext

Goal state after:
S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X✝)))
x✝ : (Opposite.unop Y✝).obj
⊢ (ConcreteCategory.hom
          (F.map (toLightProfinite.map x✝².unop).op ≫
            (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom)).toFun
      x✝¹ x✝ =
    (ConcreteCategory.hom
          ((isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝²)).toFun
      x✝¹ x✝
Module: Mathlib.Condensed.Solid

Goal state before:
pp: R : Type (u + 1)
inst✝ : Ring R
⊢ (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R)

Tactic:
dsimp only [profiniteSolidCounit, profiniteSolid]

Goal state after:
R : Type (u + 1)
inst✝ : Ring R
⊢ (FintypeCat.toProfinite.rightKanExtension (finFree R)).IsRightKanExtension
    (FintypeCat.toProfinite.rightKanExtensionCounit (finFree R))
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
⊢ Epi ((ihom P).map e)

Tactic:
rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite]
    intro S g
    specialize h e S ((ihomPoints _ _ _ _) g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (ihomPoints _ _ _ _).symm g', ?_⟩
    rw [ihom_map_val_app]
    have := ihomPoints_symm_comp R B P S' S π ((ihomPoints R P B S) g)
    dsimp at hh
    rw [hh] at this
    simp [this, Quiver.Hom.op]

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } ≫ f' = g'

Tactic:
ext

Goal state after:
X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } ≫ f'))
      a✝ =
    (ConcreteCategory.hom g') a✝
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
⊢ f ≫ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } = g

Tactic:
ext

Goal state after:
X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom
        (f ≫ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont }))
      a✝ =
    (ConcreteCategory.hom g) a✝
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ X : CondensedSet
x✝² x✝¹ : CompHausᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.obj.map x✝ ≫
      ↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) =
    (↾fun x ↦
        { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
          continuous_toFun := ⋯ }) ≫
      X.toTopCat.toCondensedSet.obj.map x✝

Tactic:
ext

Goal state after:
X✝ X : CondensedSet
x✝³ x✝² : CompHausᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ (ConcreteCategory.hom
          (X.obj.map x✝¹ ≫
            ↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ })).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦
              { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x,
                continuous_toFun := ⋯ }) ≫
            X.toTopCat.toCondensedSet.obj.map x✝¹)).toFun
      x✝
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
⊢ condensedSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
      { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (condensedSetToTopCat.obj Y) =
    𝟙 (condensedSetToTopCat.obj Y)

Tactic:
ext

Goal state after:
X Y : CondensedSet
x✝ : ↑(condensedSetToTopCat.obj Y)
⊢ (ConcreteCategory.hom
        (condensedSetToTopCat.map ({ app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 }.app Y) ≫
          { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }.app (condensedSetToTopCat.obj Y)))
      x✝ =
    (ConcreteCategory.hom (𝟙 (condensedSetToTopCat.obj Y))) x✝
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
⊢ traverse pure = pure

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x✝ : t α
⊢ (traverse pure x✝).run = (pure x✝).run
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ traverse (pure ∘ f) = pure ∘ map f

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
x✝ : t β
⊢ (traverse (pure ∘ f) x✝).run = ((pure ∘ map f) x✝).run
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
⊢ traverse (h ∘ g) = traverse h ∘ map g

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x✝ : t α
⊢ traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
⊢ traverse (map h ∘ g) = map (map h) ∘ traverse g

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
x✝ : t α
⊢ traverse (map h ∘ g) x✝ = (map (map h) ∘ traverse g) x✝
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) = (fun {α} ↦ η.app α) ∘ traverse f

Tactic:
ext

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) x✝ = ((fun {α} ↦ η.app α) ∘ traverse f) x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type u_1} (x : α × β), bitraverse pure pure x = pure x

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_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (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)

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_1} (f : α → β) (f' : α' → β') (x : α × α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
    (x : α × α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Sum

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type u_1} (x : α ⊕ β), bitraverse pure pure x = pure x

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_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (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)

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_1} (f : α → β) (f' : α' → β') (x : α ⊕ α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
    (x : α ⊕ α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Const

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {α β : Type u_1} (x : Const α β), bitraverse pure pure x = pure x

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_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u_1} (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)

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_1} (f : α → β) (f' : α' → β') (x : Const α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
    [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u_1} (f : α → F β) (f' : α' → F β')
    (x : Const α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x