awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact fun _ f ↦ hg.comp f.continuous

Premises used: Continuous.comp
-- 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
x x_1 : ContinuousMapGeneratedBy X Y Z
h :
  Eq (α := (a : Y) → Z) ((fun (f : ContinuousMapGeneratedBy X Y Z) ↦ f.toFun (X := X)) x)
    ((fun (f : ContinuousMapGeneratedBy X Y Z) ↦ f.toFun (X := X)) x_1)
⊢ x = x_1

Tactic:
aesop
-- 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
i : ι
f : ContinuousMap.{u, v} (X i) Y
rw : Continuous[inst i, inst_1] (⇑f : (a : X i) → Y)
⊢ Continuous[inst i, _]
    (Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
      (⇑f : (a : X i) → Y))

Tactic:
rw [IsGeneratedBy.equiv_symm_comp_continuous_iff]

Premises used: Topology.IsGeneratedBy.equiv_symm_comp_continuous_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
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ Continuous[inst i, inst_1] (⇑f : (a : X i) → Y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
⊢ Eq (α := (a : Y) → WithGeneratedByTopology X Y)
    (⇑(equivSymmAsContinuousMapGeneratedBy X Y) : (a : Y) → WithGeneratedByTopology X Y)
    (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X 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
⊢ Eq (α := (a : WithGeneratedByTopology X Y) → Y)
    (⇑(equivAsContinuousMapGeneratedBy X Y) : (a : WithGeneratedByTopology X Y) → Y)
    (⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set (WithGeneratedByTopology X Y)
⊢ IsOpen U ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      IsOpen[inst i]
        (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
          ((⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y) ⁻¹' U))

Tactic:
simp [isOpen_iSup_iff, isOpen_coinduced, equiv, Equiv.refl]

Premises used: isOpen_iSup_iff, Topology.WithGeneratedByTopology.equiv, isOpen_coinduced, Equiv.refl
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set (WithGeneratedByTopology X Y)
⊢ IsClosed U ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      IsClosed[inst i]
        (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
          ((⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y) ⁻¹' U))

Tactic:
simp [isClosed_iSup_iff, isClosed_coinduced, equiv, Equiv.refl]

Premises used: isClosed_iSup_iff, Topology.WithGeneratedByTopology.equiv, Equiv.refl, isClosed_coinduced
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
simp :
  (∀ (i : ι) (i_1 : ContinuousMap.{u, v} (X i) Y),
      Continuous[TopologicalSpace.coinduced (⇑i_1 : (a : X i) → Y) inferInstance, inst_1] g) ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_1]
        (g ∘
          Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
            (⇑f : (a : X i) → Y))
⊢ Continuous[_, inst_1] g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_1]
        (g ∘
          Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
            (⇑f : (a : X i) → Y))

Tactic:
simp only [continuous_iSup_dom]

Premises used: continuous_iSup_dom
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : ContinuousMap.{u, v} (X i) Y
rw :
  Continuous[inferInstance, inst_1] (g ∘ (⇑f : (a : X i) → Y)) ↔
    Continuous[inst i, inst_1]
      (g ∘
        Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))
⊢ Continuous[TopologicalSpace.coinduced (⇑f : (a : X i) → Y) inferInstance, inst_1] g ↔
    Continuous[inst i, inst_1]
      (g ∘
        Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ Continuous[inferInstance, inst_1] (g ∘ (⇑f : (a : X i) → Y)) ↔
    Continuous[inst i, inst_1]
      (g ∘
        Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))

Tactic:
simp [equiv, Equiv.refl]

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

Tactic:
exact forall_congr' (fun i ↦ forall_congr'
    (fun f ↦ (by rw [continuous_coinduced_dom]; simp [equiv, Equiv.refl])))

Premises used: forall_congr'
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
rw :
  ∀ (s : Set Y),
    IsOpen[tY] s →
      IsOpen (X := WithGeneratedByTopology X Y) ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' s)
⊢ Continuous[_, tY] (⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
rw :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
    IsOpen[inst i]
      (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
        (Set.preimage (β := WithGeneratedByTopology X Y)
          (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)))
⊢ IsOpen (X := WithGeneratedByTopology X Y) ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)

Tactic:
rw [isOpen_iff]

Premises used: Topology.WithGeneratedByTopology.isOpen_iff
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ IsOpen[inst i]
    (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
      (Set.preimage (β := WithGeneratedByTopology X Y)
        (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)))

Tactic:
f.continuous.isOpen_preimage _ hU

Premises used: ContinuousMap.continuous, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ IsOpen[inst i]
    (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
      (Set.preimage (β := WithGeneratedByTopology X Y)
        (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)))

Tactic:
exact f.continuous.isOpen_preimage _ hU

Premises used: ContinuousMap.continuous, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ generatedBy X ≤ tY

Tactic:
fun U hU ↦ WithGeneratedByTopology.continuous_equiv.isOpen_preimage U hU

Premises used: Topology.WithGeneratedByTopology.instTopologicalSpace._aux_1, Set.Mem, iSup, setOf, Set.preimage, Topology.WithGeneratedByTopology.continuous_equiv, Topology.WithGeneratedByTopology, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
t₁ t₂ : TopologicalSpace Y
h : t₁ ≤ t₂
⊢ LE.le.{v} (α := TopologicalSpace Y) (generatedBy X) (generatedBy X)

Tactic:
iSup₂_le fun i f ↦ le_iSup₂_of_le i ⟨f, continuous_le_rng h @f.2⟩ le_rfl

Premises used: iSup₂_le, le_rfl, ContinuousMap.mk, continuous_le_rng, ContinuousMap.continuous_toFun, le_iSup₂_of_le, DFunLike.coe
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
⊢ tY ≤ TopologicalSpace.generatedBy X

Tactic:
fun U hU ↦ continuous_equiv_symm.isOpen_preimage U hU

Premises used: Set.Mem, setOf, Topology.IsGeneratedBy.continuous_equiv_symm, Set.preimage, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
⊢ TopologicalSpace.generatedBy X = tY

Tactic:
le_antisymm TopologicalSpace.generatedBy_le le_generatedBy

Premises used: Topology.IsGeneratedBy.le_generatedBy, le_antisymm, TopologicalSpace.generatedBy_le
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
h : tY ≤ TopologicalSpace.generatedBy X
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (s : Set (WithGeneratedByTopology X Y)),
    IsOpen s →
      IsOpen[tY]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y) ⁻¹' s)
⊢ Continuous[tY, _] (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)

Tactic:
rwa [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
dsimp : Continuous[_, tY] (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)
⊢ Continuous[_, tY] (Equiv.toFun (WithGeneratedByTopology.equiv (X := X)))

Tactic:
dsimp
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
⊢ Continuous[_, tY] (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
dsimp :
  Continuous[tY, _] (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
⊢ Continuous[tY, _] (Equiv.invFun (WithGeneratedByTopology.equiv (X := X)))

Tactic:
dsimp
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
⊢ Continuous[tY, _] (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
⊢ Eq.{v + 1} (α := (a : WithGeneratedByTopology X Y) → Y)
    (⇑(homeomorph (X := X)) : (a : WithGeneratedByTopology X Y) → Y)
    (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
⊢ Eq.{v + 1} (α := (a : Y) → WithGeneratedByTopology X Y)
    (⇑(Homeomorph.symm (homeomorph (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)

Tactic:
rfl

Premises used: Topology.WithGeneratedByTopology.equiv, Equiv.refl, rfl
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
U : Set Y
⊢ IsOpen[tY] U ↔ ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), IsOpen[inst i] ((⇑f : (a : X i) → Y) ⁻¹' U)

Tactic:
simp [← (homeomorph (X := X)).isQuotientMap.isOpen_preimage,
    WithGeneratedByTopology.isOpen_iff]

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsGeneratedBy.homeomorph, Topology.IsQuotientMap.isCoinducing, Topology.WithGeneratedByTopology.isOpen_iff, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
inst_1 : IsGeneratedBy X Y
U : Set Y
⊢ IsClosed[tY] U ↔ ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), IsClosed[inst i] ((⇑f : (a : X i) → Y) ⁻¹' U)

Tactic:
simp [← (homeomorph (X := X)).isQuotientMap.isClosed_preimage,
    WithGeneratedByTopology.isClosed_iff]

Premises used: Topology.IsCoinducing.isClosed_preimage, Topology.IsGeneratedBy.homeomorph, Topology.IsQuotientMap.isCoinducing, Topology.WithGeneratedByTopology.isClosed_iff, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
rw :
  (∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_1]
        (Function.comp (β := WithGeneratedByTopology X Y)
          (g ∘ (⇑(homeomorph (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)))) ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_1] (g ∘ (⇑f : (a : X i) → Y))
⊢ Continuous[tY, inst_1] g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_1] (g ∘ (⇑f : (a : X i) → Y))

Tactic:
rw [(homeomorph (X := X)).isQuotientMap.continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]

Premises used: Topology.WithGeneratedByTopology.continuous_from_iff, Topology.IsGeneratedBy.homeomorph, Topology.IsQuotientMap.continuous_iff, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
⊢ (∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_1]
        (Function.comp (β := WithGeneratedByTopology X Y)
          (g ∘ (⇑(homeomorph (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)))) ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_1] (g ∘ (⇑f : (a : X i) → Y))

Tactic:
simp [Function.comp_assoc g, ← Function.comp_assoc WithGeneratedByTopology.equiv]

Premises used: Topology.WithGeneratedByTopology.equiv, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
⊢ Continuous[tY, _]
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ↔
    Continuous[tY, inst_1] g

Tactic:
⟨fun hg ↦ WithGeneratedByTopology.continuous_equiv.comp hg, fun hg ↦ ?_⟩

Premises used: Continuous.comp, Iff.intro, Topology.WithGeneratedByTopology.continuous_equiv
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
refine :
  ∀ (hg : Continuous[tY, inst_1] g),
    Continuous[tY, _]
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g)
⊢ Continuous[tY, _]
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ↔
    Continuous[tY, inst_1] g

Tactic:
refine ⟨fun hg ↦ WithGeneratedByTopology.continuous_equiv.comp hg, fun hg ↦ ?_⟩
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst_1] g
rw :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
    Continuous[inst i, _]
      (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
        (⇑f : (a : X i) → Y))
⊢ Continuous[tY, _]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g)

Tactic:
rw [continuous_iff (X := X)]

Premises used: Topology.IsGeneratedBy.continuous_iff
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst_1] g
i : ι
f : ContinuousMap.{u, v} (X i) Y
rw :
  ∀ (s : Set (WithGeneratedByTopology X Z)),
    IsOpen s →
      IsOpen[inst i]
        (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
            (⇑f : (a : X i) → Y) ⁻¹'
          s)
⊢ Continuous[inst i, _]
    (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
      (⇑f : (a : X i) → Y))

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst_1] g
i : ι
f : ContinuousMap.{u, v} (X i) Y
U : Set (WithGeneratedByTopology X Z)
hU : IsOpen U
⊢ ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z),
    IsOpen[inst i]
      (Set.preimage (β := Z) (⇑f : (a : X i) → Z)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ⁻¹' U))

Tactic:
rw [WithGeneratedByTopology.isOpen_iff] at hU

Premises used: Topology.WithGeneratedByTopology.isOpen_iff
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst_1] g
i : ι
f : ContinuousMap.{u, v} (X i) Y
U : Set (WithGeneratedByTopology X Z)
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z),
    IsOpen[inst i]
      (Set.preimage (β := Z) (⇑f : (a : X i) → Z)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ⁻¹' U))
⊢ IsOpen[inst i]
    (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
        (⇑f : (a : X i) → Y) ⁻¹'
      U)

Tactic:
hU (ContinuousMap.comp ⟨g, hg⟩ f)

Premises used: Set.Mem, ContinuousMap.mk, setOf, ContinuousMap.comp, Set.preimage, Topology.WithGeneratedByTopology
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst_1] g
i : ι
f : ContinuousMap.{u, v} (X i) Y
U : Set (WithGeneratedByTopology X Z)
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z),
    IsOpen[inst i]
      (Set.preimage (β := Z) (⇑f : (a : X i) → Z)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ⁻¹' U))
⊢ IsOpen[inst i]
    (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
        (⇑f : (a : X i) → Y) ⁻¹'
      U)

Tactic:
exact hU (ContinuousMap.comp ⟨g, hg⟩ f)

Premises used: ContinuousMap.mk, ContinuousMap.comp
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst_1 : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
i : ι
rw :
  ∀ (s : Set (WithGeneratedByTopology X (X i))),
    IsOpen s →
      IsOpen[inst_1 i]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i)) ⁻¹' s)
⊢ Continuous[inst_1 i, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i))

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst_1 : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : IsOpen U
⊢ ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)),
    IsOpen[inst_1 i_1]
      (Set.preimage (β := X i) (⇑f : (a : X i_1) → X i)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i)) ⁻¹' U))

Tactic:
rw [WithGeneratedByTopology.isOpen_iff] at hU

Premises used: Topology.WithGeneratedByTopology.isOpen_iff