awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u

Tactic:
exact inter_subset_right.trans <| preimage_mono hv.2.2

Premises used: HasSubset.Subset.trans, Set.preimage_mono, And.right, Set.inter_subset_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u : Set β
h : u ∈ 𝓝ˢ t
⊢ f ⁻¹' u ∈ 𝓝ˢ[s] (s ∩ f ⁻¹' t)

Tactic:
simpa [h] using ContinuousOn.preimage_mem_nhdsSetWithin hf (t := t) (u := u) (t' := univ)

Premises used: ContinuousOn.preimage_mem_nhdsSetWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
s u s' : Set β
h : u ∈ 𝓝ˢ[s'] s
⊢ f ⁻¹' u ∈ 𝓝ˢ[f ⁻¹' s'] (f ⁻¹' s)

Tactic:
simpa using (hf.continuousOn (s := univ)).preimage_mem_nhdsSetWithin h

Premises used: ContinuousOn.preimage_mem_nhdsSetWithin, Continuous.continuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
s u : Set β
h : u ∈ 𝓝ˢ s
⊢ f ⁻¹' u ∈ 𝓝ˢ (f ⁻¹' s)

Tactic:
simpa [h] using hf.preimage_mem_nhdsSetWithin (s := s) (u := u) (s' := univ)

Premises used: Continuous.preimage_mem_nhdsSetWithin
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : TopCat
⊢ generatedBy X Y ↔ IsGeneratedBy.{v, t, u} X (↑Y : Type v)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : GeneratedByTopCat X
⊢ IsGeneratedBy.{v, t, u} X (↑(Functor.obj (toTopCat (X := X)) Y) : Type v)

Tactic:
Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : IsGeneratedBy X Y
⊢ TopCat.generatedBy.{v, t, u} X (TopCat.of Y)

Tactic:
assumption
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : GeneratedByTopCat X
⊢ IsGeneratedBy.{v, t, u} X (↑(Y.obj (P := TopCat.generatedBy X)) : Type v)

Tactic:
Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
⊢ (↑(of (X := X) Y) : Type v) = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ of (X := X) (↑Y : Type v) = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.Faithful.{v, v, v + 1, v + 1} (D := ContinuousGeneratedByCat X) (TopCat.toContinuousGeneratedByCat X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
f : Y ⟶ Z
y : WithGeneratedByTopology X (↑Y : Type v)
⊢ Eq (α := WithGeneratedByTopology X (↑Z : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := TopCat.of (WithGeneratedByTopology X (↑Y : Type v))) (Y :=
              TopCat.of (WithGeneratedByTopology X (↑Z : Type v)))
              (CategoryTheory.Functor.map (toTopCat X) f : Functor.obj (toTopCat X) Y ⟶ Functor.obj (toTopCat X) Z) :
            C((↑(TopCat.of (WithGeneratedByTopology X (↑Y : Type v))) : Type v),
              (↑(TopCat.of (WithGeneratedByTopology X (↑Z : Type v))) : Type v))) :
          (a : WithGeneratedByTopology X (↑Y : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
        y :
      WithGeneratedByTopology X (↑Z : Type v))
    ((Equiv.symm (WithGeneratedByTopology.equiv (X := X)) :
          (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
        ((ConcreteCategory.hom (FC := fun (Y Z : ContinuousGeneratedByCat X) ↦
              ContinuousMapGeneratedBy X (↑Y : Type v) (↑Z : Type v)) (CC := carrier (X := X)) f :
            (a : (↑Y : Type v)) → (↑Z : Type v))
          ((WithGeneratedByTopology.equiv (X := X) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v)) y :
            (↑Y : Type v))) :
      WithGeneratedByTopology X (↑Z : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : Functor.obj (toTopCat X) Y ⟶ Functor.obj (toTopCat X) Z
rw :
  Continuous (X := WithGeneratedByTopology X (↑Y : Type v)) (Y := WithGeneratedByTopology X (↑Z : Type v))
    (Function.comp (β := (↑Z : Type v))
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
        (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
      (Function.comp (β := (↑Y : Type v))
        (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
          (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
          (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
            (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
            (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
              (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))
        (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v))))
⊢ ContinuousGeneratedBy X (Y := (↑Y : Type v)) (Z := (↑Z : Type v))
    (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
      (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
      (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
        (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
        (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
          (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))

Tactic:
rw [continuousGeneratedBy_iff]

Premises used: Topology.continuousGeneratedBy_iff
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : Functor.obj (toTopCat X) Y ⟶ Functor.obj (toTopCat X) Z
⊢ Continuous (X := WithGeneratedByTopology X (↑Y : Type v)) (Y := WithGeneratedByTopology X (↑Z : Type v))
    (Function.comp (β := (↑Z : Type v))
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
        (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
      (Function.comp (β := (↑Y : Type v))
        (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
          (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
          (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
            (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
            (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
              (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))
        (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v))))

Tactic:
g.hom.continuous

Premises used: ContinuousMap.continuous, Topology.WithGeneratedByTopology.instTopologicalSpace._aux_1, iSup, TopCat.Hom.hom, Topology.WithGeneratedByTopology
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : Functor.obj (toTopCat X) Y ⟶ Functor.obj (toTopCat X) Z
⊢ Continuous (X := WithGeneratedByTopology X (↑Y : Type v)) (Y := WithGeneratedByTopology X (↑Z : Type v))
    (Function.comp (β := (↑Z : Type v))
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
        (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
      (Function.comp (β := (↑Y : Type v))
        (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
          (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
          (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
            (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
            (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
              (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))
        (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v))))

Tactic:
exact g.hom.continuous

Premises used: ContinuousMap.continuous, TopCat.Hom.hom
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.Full.{v, v, v + 1, v + 1} (C := ContinuousGeneratedByCat X) (toTopCat X)

Tactic:
(fullyFaithfulToTopCat X).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, ContinuousGeneratedByCat.fullyFaithfulToTopCat
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.Faithful.{v, v, v + 1, v + 1} (C := ContinuousGeneratedByCat X) (toTopCat X)

Tactic:
(fullyFaithfulToTopCat X).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, ContinuousGeneratedByCat.fullyFaithfulToTopCat
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsLeftAdjoint.{v, v, v + 1, v + 1} (C := ContinuousGeneratedByCat X) (toTopCat X)

Tactic:
adj.isLeftAdjoint

Premises used: ContinuousGeneratedByCat.adj, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsRightAdjoint.{v, v, v + 1, v + 1} (C := ContinuousGeneratedByCat X) (TopCat.toContinuousGeneratedByCat X)

Tactic:
adj.isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, ContinuousGeneratedByCat.adj
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ IsIso.{v + 1, v + 1} (C := ContinuousGeneratedByCat X ⥤ ContinuousGeneratedByCat X) (Iso.hom (adjUnitIso (X := X)))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
dsimp : IsGeneratedBy.{v, t, u} X (WithGeneratedByTopology X (↑Y : Type v))
⊢ IsGeneratedBy.{v, t, u} X (↑(Functor.obj (toTopCat X) Y) : Type v)

Tactic:
dsimp +instances
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ IsGeneratedBy.{v, t, u} X (WithGeneratedByTopology X (↑Y : Type v))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
f : Y ⟶ Z
y : WithGeneratedByTopology X (↑Y : Type v)
⊢ Eq (α := WithGeneratedByTopology X (↑Z : Type v))
    (((ConcreteCategory.hom (FC := fun (X_1 Y : (TopCat.generatedBy X).FullSubcategory) ↦
              C((↑(X_1.obj (P := TopCat.generatedBy X)) : Type v), (↑(Y.obj (P := TopCat.generatedBy X)) : Type v)))
              (CC := fun (X_1 : (TopCat.generatedBy X).FullSubcategory) ↦
              (↑(X_1.obj (P := TopCat.generatedBy X)) : Type v)) (X :=
              ObjectProperty.FullSubcategory.mk (P := TopCat.generatedBy X)
                (TopCat.of (WithGeneratedByTopology X (↑Y : Type v))) ⋯)
              (Y :=
              ObjectProperty.FullSubcategory.mk (P := TopCat.generatedBy X)
                (TopCat.of (WithGeneratedByTopology X (↑Z : Type v))) ⋯)
              (CategoryTheory.Functor.map (toGeneratedByTopCat (X := X)) f :
                Functor.obj (toGeneratedByTopCat (X := X)) Y ⟶ Functor.obj (toGeneratedByTopCat (X := X)) Z) :
            C((↑(ObjectProperty.FullSubcategory.obj (P := TopCat.generatedBy X)
                    (ObjectProperty.FullSubcategory.mk (P := TopCat.generatedBy X)
                      (TopCat.of (WithGeneratedByTopology X (↑Y : Type v))) ⋯)) :
                Type v),
              (↑(ObjectProperty.FullSubcategory.obj (P := TopCat.generatedBy X)
                    (ObjectProperty.FullSubcategory.mk (P := TopCat.generatedBy X)
                      (TopCat.of (WithGeneratedByTopology X (↑Z : Type v))) ⋯)) :
                Type v))) :
          (a : WithGeneratedByTopology X (↑Y : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
        y :
      WithGeneratedByTopology X (↑Z : Type v))
    ((Equiv.symm (WithGeneratedByTopology.equiv (X := X)) :
          (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
        ((ConcreteCategory.hom (FC := fun (Y Z : ContinuousGeneratedByCat X) ↦
              ContinuousMapGeneratedBy X (↑Y : Type v) (↑Z : Type v)) (CC := carrier (X := X)) f :
            (a : (↑Y : Type v)) → (↑Z : Type v))
          ((WithGeneratedByTopology.equiv (X := X) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v)) y :
            (↑Y : Type v))) :
      WithGeneratedByTopology X (↑Z : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsEquivalence.{v, v, v + 1, v + 1} (C := GeneratedByTopCat X) (fromGeneratedByTopCat (X := X))

Tactic:
equivalence.isEquivalence_functor

Premises used: ContinuousGeneratedByCat.fromGeneratedByTopCat, CategoryTheory.Equivalence.isEquivalence_functor, ContinuousGeneratedByCat.equivalence
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsEquivalence.{v, v, v + 1, v + 1} (C := ContinuousGeneratedByCat X) (toGeneratedByTopCat (X := X))

Tactic:
equivalence.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.ObjectProperty.lift, ContinuousGeneratedByCat.toGeneratedByTopCat, ContinuousGeneratedByCat.equivalence
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ IsIso.{v + 1, v + 1} (C := GeneratedByTopCat X ⥤ GeneratedByTopCat X) (Iso.hom (adjUnitIso (X := X)))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsLeftAdjoint.{v, v, v + 1, v + 1} (C := GeneratedByTopCat X) (toTopCat (X := X))

Tactic:
adj.isLeftAdjoint

Premises used: GeneratedByTopCat.adj, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
⊢ Functor.IsRightAdjoint.{v, v, v + 1, v + 1} (C := GeneratedByTopCat X) (TopCat.toGeneratedByTopCat (X := X))

Tactic:
adj.isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, GeneratedByTopCat.adj
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : TopCat
⊢ IsIso (C := GeneratedByTopCat X) (X :=
    Functor.obj (TopCat.toGeneratedByTopCat (X := X))
      ((Functor.comp (D := GeneratedByTopCat X) (TopCat.toGeneratedByTopCat (X := X)) (toTopCat (X := X))).obj Z))
    (CategoryTheory.Functor.map (TopCat.toGeneratedByTopCat (X := X)) (NatTrans.app (adjCounit (X := X)) Z))

Tactic:
inferInstanceAs (IsIso (TopCat.toGeneratedByTopCat.map (GeneratedByTopCat.adj.counit.app Z)))

Premises used: _private.0.GeneratedByTopCat.instIsIsoMapTopCatToGeneratedByTopCatAppAdjCounit._proof_1
-- Module: Mathlib.Topology.Convenient.Category
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : TopCat
⊢ IsIso (C := ContinuousGeneratedByCat X) (X :=
    Functor.obj (TopCat.toContinuousGeneratedByCat X)
      ((Functor.comp (D := GeneratedByTopCat X) (TopCat.toGeneratedByTopCat (X := X)) (toTopCat (X := X))).obj Z))
    (CategoryTheory.Functor.map (TopCat.toContinuousGeneratedByCat X) (NatTrans.app (adjCounit (X := X)) Z))

Tactic:
inferInstanceAs (IsIso ((TopCat.toContinuousGeneratedByCat X).map
    (ContinuousGeneratedByCat.adj.counit.app Z)))

Premises used: _private.0.GeneratedByTopCat.instIsIsoContinuousGeneratedByCatMapTopCatToContinuousGeneratedByCatAppAdjCounit._proof_1
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_2] (g ∘ (⇑f : (a : X i) → Y))

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.ContinuousGeneratedBy
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
rw :
  ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_2]
        (Function.comp (β := WithGeneratedByTopology X Y)
          (g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))
          (Function.comp (β := Y)
            (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
            (⇑f : (a : X i) → Y)))
⊢ ContinuousGeneratedBy X g ↔
    Continuous (X := WithGeneratedByTopology X Y) (Y := WithGeneratedByTopology X Z)
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
        g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))

Tactic:
rw [IsGeneratedBy.equiv_symm_comp_continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]

Premises used: Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.WithGeneratedByTopology.continuous_from_iff
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_2]
        (Function.comp (β := WithGeneratedByTopology X Y)
          (g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))
          (Function.comp (β := Y)
            (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
            (⇑f : (a : X i) → Y)))

Tactic:
rfl
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg rwa rwa₁ rwa₂ rwa₃ : ContinuousGeneratedBy X g
⊢ Continuous (X := WithGeneratedByTopology X Y) (Y := WithGeneratedByTopology X Z)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
      g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))

Tactic:
rwa [← continuousGeneratedBy_iff]

Premises used: Topology.continuousGeneratedBy_iff
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
⊢ Eq (α := (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X Z)
    (⇑(hg.continuousMap (X := X)) : (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X Z)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
      g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
⊢ ContinuousGeneratedBy.{v, v, t, u} X (Y := Y) _root_.id

Tactic:
simpa [continuousGeneratedBy_iff] using continuous_id

Premises used: continuous_id, Topology.continuousGeneratedBy_iff
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst_3 : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
rw :
  Continuous (X := WithGeneratedByTopology X T) (Y := WithGeneratedByTopology X Z)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
      (g ∘ f) ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X T) → T))
⊢ ContinuousGeneratedBy X (g ∘ f)

Tactic:
rw [continuousGeneratedBy_iff]

Premises used: Topology.continuousGeneratedBy_iff
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst_3 : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ Continuous (X := WithGeneratedByTopology X T) (Y := WithGeneratedByTopology X Z)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
      (g ∘ f) ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X T) → T))

Tactic:
(hg.continuousMap.comp hf.continuousMap).continuous

Premises used: ContinuousMap.continuous, ContinuousMap.comp, Topology.ContinuousGeneratedBy.continuousMap
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst_3 : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ Continuous (X := WithGeneratedByTopology X T) (Y := WithGeneratedByTopology X Z)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
      (g ∘ f) ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X T) → T))

Tactic:
exact (hg.continuousMap.comp hf.continuousMap).continuous

Premises used: ContinuousMap.continuous, ContinuousMap.comp, Topology.ContinuousGeneratedBy.continuousMap
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst_1, inst_2] g
⊢ ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_2] (g ∘ (⇑f : (a : X i) → Y))

Tactic:
fun _ f ↦ hg.comp f.continuous

Premises used: ContinuousMap.continuous, Continuous.comp