awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU :
  ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)),
    IsOpen[inst 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))
⊢ IsOpen[inst i]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i)) ⁻¹' U)

Tactic:
hU ⟨_, continuous_id⟩

Premises used: Set.Mem, ContinuousMap.mk, setOf, continuous_id, Set.preimage, Topology.WithGeneratedByTopology
-- 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 :
  ∀ ⦃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))
⊢ IsOpen[inst_1 i]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i)) ⁻¹' U)

Tactic:
exact hU ⟨_, continuous_id⟩

Premises used: ContinuousMap.mk, continuous_id
-- 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
rw :
  ∀ (s : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))),
    IsOpen s →
      IsOpen (X := WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          s)
⊢ Continuous.{v, v} (X := WithGeneratedByTopology X Y) (Y := WithGeneratedByTopology X (WithGeneratedByTopology X Y))
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X 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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU : IsOpen U
rw :
  ∀
    (hU :
      ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
        IsOpen[inst i]
          (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
            ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
                (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
              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 (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
              (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
            U)))
⊢ IsOpen (X := WithGeneratedByTopology X Y)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
        (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
      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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
    IsOpen[inst i]
      (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          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 (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U)))

Tactic:
hU ⟨WithGeneratedByTopology.equiv.symm ∘ f, ?_⟩

Premises used: Topology.WithGeneratedByTopology.instTopologicalSpace._aux_1, Set.Mem, iSup, ContinuousMap.mk, setOf, Function.comp, Topology.WithGeneratedByTopology.equiv, Set.preimage, Topology.WithGeneratedByTopology, Equiv.symm, DFunLike.coe
-- 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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
    IsOpen[inst i]
      (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U))
i : ι
f : ContinuousMap.{u, v} (X i) Y
refine :
  Continuous[inst i, _]
    (Function.comp (β := Y)
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
      (⇑f : (a : X i) → Y))
⊢ IsOpen[inst i]
    (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
      (Set.preimage (β := WithGeneratedByTopology X Y)
        (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U)))

Tactic:
refine hU ⟨WithGeneratedByTopology.equiv.symm ∘ f, ?_⟩

Premises used: ContinuousMap.mk, Function.comp, Topology.WithGeneratedByTopology.equiv, Equiv.symm, DFunLike.coe
-- 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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
    IsOpen[inst i]
      (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U))
i : ι
f : ContinuousMap.{u, v} (X i) Y
rw :
  ∀ ⦃i_1 : ι⦄ (f_1 : C(X i_1, X i)),
    Continuous[inst i_1, _]
      (Function.comp (β := X i)
        (Function.comp (β := Y)
          (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))
        (⇑f_1 : (a : X i_1) → X i))
⊢ Continuous[inst i, _]
    (Function.comp (β := Y)
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
      (⇑f : (a : X i) → Y))

Tactic:
rw [continuous_iff 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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
    IsOpen[inst i]
      (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U))
i : ι
f : ContinuousMap.{u, v} (X i) Y
j : ι
g : C(X j, X i)
rw : Continuous[inst j, tY] (Function.comp (β := X i) (⇑f : (a : X i) → Y) (⇑g : (a : X j) → X i))
⊢ Continuous[inst j, _]
    (Function.comp (β := X i)
      (Function.comp (β := Y)
        (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        (⇑f : (a : X i) → Y))
      (⇑g : (a : X j) → X i))

Tactic:
rw [Function.comp_assoc, equiv_symm_comp_continuous_iff]

Premises used: Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, 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
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) (WithGeneratedByTopology X Y)),
    IsOpen[inst i]
      (Set.preimage (β := WithGeneratedByTopology X Y) (⇑f : (a : X i) → WithGeneratedByTopology X Y)
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
          U))
i : ι
f : ContinuousMap.{u, v} (X i) Y
j : ι
g : C(X j, X i)
⊢ Continuous[inst j, tY] (Function.comp (β := X i) (⇑f : (a : X i) → Y) (⇑g : (a : X j) → X i))

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
rw : instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X
⊢ IsGeneratedBy X PUnit.{v + 1}

Tactic:
rw [iff_le_generatedBy]

Premises used: Topology.IsGeneratedBy.iff_le_generatedBy
-- 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
⊢ instTopologicalSpacePUnit = TopologicalSpace.generatedBy X

Tactic:
subsingleton
-- 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
⊢ instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X

Tactic:
exact Eq.le (by subsingleton)

Premises used: Eq.le
-- 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 : IsGeneratedBy X Y
f : Y → Z
x : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ IsGeneratedBy X Z

Tactic:
iff_le_generatedBy.2 ?_

Premises used: Iff.mpr, Topology.IsGeneratedBy.iff_le_generatedBy
-- 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 : IsGeneratedBy X Y
f : Y → Z
x : TopologicalSpace Z := TopologicalSpace.coinduced f tY
refine : TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X
⊢ IsGeneratedBy X Z

Tactic:
refine iff_le_generatedBy.2 ?_

Premises used: Iff.mpr, Topology.IsGeneratedBy.iff_le_generatedBy
-- 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 : IsGeneratedBy X Y
f : Y → Z
x : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X

Tactic:
((equiv_symm_comp_continuous_iff (X := X) f).2 continuous_coinduced_rng).coinduced_le

Premises used: Iff.mpr, Topology.WithGeneratedByTopology.instTopologicalSpace._aux_1, Set.Mem, iSup, setOf, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.WithGeneratedByTopology, continuous_coinduced_rng, Continuous.coinduced_le
-- 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 : IsGeneratedBy X Y
f : Y → Z
x : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X

Tactic:
exact ((equiv_symm_comp_continuous_iff (X := X) f).2 continuous_coinduced_rng).coinduced_le

Premises used: Iff.mpr, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, continuous_coinduced_rng, Continuous.coinduced_le
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
κ : Sort u_2
t : κ → TopologicalSpace Y
h : ∀ (k : κ), IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
iff_le_generatedBy.2 <| iSup_le_iff.2 fun k ↦
    (h k).le_generatedBy.trans <| TopologicalSpace.generatedBy_mono <| le_iSup t k

Premises used: Iff.mpr, TopologicalSpace.generatedBy_mono, Topology.IsGeneratedBy.le_generatedBy, Topology.IsGeneratedBy.iff_le_generatedBy, le_iSup, iSup_le_iff, LE.le.trans
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
rw : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
rw [sup_eq_iSup]

Premises used: sup_eq_iSup
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
.iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, Bool.forall_bool, And.intro, Topology.IsGeneratedBy.iSup
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, Bool.forall_bool, And.intro
-- 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
f : Y → Z
hf : IsQuotientMap f
inst_2 : IsGeneratedBy X Y
⊢ IsGeneratedBy X Z

Tactic:
hf.eq_coinduced ▸ IsGeneratedBy.coinduced f

Premises used: Topology.IsGeneratedBy.coinduced, Eq.rec, Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, Eq.symm
-- 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
r : Y → Y → Prop
⊢ IsGeneratedBy.{v, t, u} X (Quot r)

Tactic:
isQuotientMap_quot_mk.isGeneratedBy

Premises used: Topology.IsQuotientMap.isGeneratedBy, isQuotientMap_quot_mk
-- 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
s : Setoid Y
⊢ IsGeneratedBy.{v, t, u} X (Quotient s)

Tactic:
isQuotientMap_quotient_mk'.isGeneratedBy

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.isGeneratedBy
-- 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
inst_3 : IsGeneratedBy X Z
⊢ IsGeneratedBy X (Y ⊕ Z)

Tactic:
IsGeneratedBy.sup (.coinduced Sum.inl) (.coinduced Sum.inr)

Premises used: Topology.IsGeneratedBy.coinduced, setOf, Topology.IsGeneratedBy.sup, Sum.inl, Sum.inr
-- Module: Mathlib.Topology.Convenient.GeneratedBy
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y_1 : Type v
tY : TopologicalSpace Y_1
Z : Type v'
inst_1 : TopologicalSpace Z
κ : Type u_1
Y : κ → Type u_2
inst_2 : (k : κ) → TopologicalSpace (Y k)
inst_3 : ∀ (k : κ), IsGeneratedBy.{u_2, t, u} X (Y k)
⊢ IsGeneratedBy X ((k : κ) × Y k)

Tactic:
.iSup fun _ ↦ .coinduced _

Premises used: Topology.IsGeneratedBy.coinduced, Sigma.mk, Topology.IsGeneratedBy.iSup
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst_1 : TopologicalSpace Z
T : Type v''
inst_2 : TopologicalSpace T
i : ι
f : ContinuousMap.{u, v'} (X i) Z
g : ContinuousMapGeneratedBy X Z T
⊢ Eq (α := (a : X i) → T) (⇑(precomp (X := X) f g) : (a : X i) → T)
    (Function.comp.{u + 1, v' + 1, v'' + 1} (β := Z) (⇑g : (a : Z) → T) (⇑f : (a : X i) → Z))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst_1 : TopologicalSpace Z
T : Type v''
inst_2 : TopologicalSpace T
A : Type u_1
inst_3 : TopologicalSpace A
φ : A → ContinuousMapGeneratedBy X Z T
⊢ Continuous[inst_3, _] φ ↔
    ∀ (i : ι) (f : ContinuousMap.{u, v'} (X i) Z), Continuous[inst_3, _] (precomp (X := X) f ∘ φ)

Tactic:
simp only [continuous_iInf_rng, continuous_induced_rng]

Premises used: continuous_iInf_rng, continuous_induced_rng
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst_1 : TopologicalSpace Z
T : Type v''
inst_2 : TopologicalSpace T
i : ι
f : ContinuousMap.{u, v'} (X i) Z
rw :
  LE.le (α := TopologicalSpace (ContinuousMapGeneratedBy X Z T)) (instTopologicalSpace (X := X))
    (TopologicalSpace.induced (precomp (X := X) f) ContinuousMap.compactOpen)
⊢ Continuous (X := ContinuousMapGeneratedBy X Z T) (precomp (X := X) f)

Tactic:
rw [continuous_iff_le_induced]

Premises used: continuous_iff_le_induced
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst_1 : TopologicalSpace Z
T : Type v''
inst_2 : TopologicalSpace T
i : ι
f : ContinuousMap.{u, v'} (X i) Z
⊢ LE.le (α := TopologicalSpace (ContinuousMapGeneratedBy X Z T)) (instTopologicalSpace (X := X))
    (TopologicalSpace.induced (precomp (X := X) f) ContinuousMap.compactOpen)

Tactic:
(iInf_le _ i).trans (iInf_le _ _)

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst_1 : TopologicalSpace Z
T : Type v''
inst_2 : TopologicalSpace T
i : ι
f : ContinuousMap.{u, v'} (X i) Z
⊢ LE.le (α := TopologicalSpace (ContinuousMapGeneratedBy X Z T)) (instTopologicalSpace (X := X))
    (TopologicalSpace.induced (precomp (X := X) f) ContinuousMap.compactOpen)

Tactic:
exact (iInf_le _ i).trans (iInf_le _ _)

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.Convenient.HomSpace
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
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
g : Z → ContinuousMapGeneratedBy X Y T
simp :
  (∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z) (i_1 : ι) (f_1 : ContinuousMap.{u, v} (X i_1) Y),
      Continuous[inst i, _] (precomp (X := X) f_1 ∘ g ∘ (⇑f : (a : X i) → Z))) ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : ContinuousMap.{u, v'} (X i₁) Z) ⦃i₂ : ι⦄ (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        (g ((f₁ : (a : X i₁) → Z) x.1) : (a : Y) → T) ((f₂ : (a : X i₂) → Y) x.2 : Y)
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : ContinuousMap.{u, v'} (X i₁) Z) ⦃i₂ : ι⦄ (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        match (motive := X i₁ × X i₂ → T) x with
        | (x₁, x₂) => (g ((f₁ : (a : X i₁) → Z) x₁) : (a : Y) → T) ((f₂ : (a : X i₂) → Y) x₂ : Y)

Tactic:
simp only [continuousGeneratedBy_def, continuous_iff]

Premises used: Topology.ContinuousMapGeneratedBy.continuous_iff, Topology.continuousGeneratedBy_def
-- Module: Mathlib.Topology.Convenient.HomSpace
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
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
g : Z → ContinuousMapGeneratedBy X Y T
⊢ (∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z) (i_1 : ι) (f_1 : ContinuousMap.{u, v} (X i_1) Y),
      Continuous[inst i, _] (precomp (X := X) f_1 ∘ g ∘ (⇑f : (a : X i) → Z))) ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : ContinuousMap.{u, v'} (X i₁) Z) ⦃i₂ : ι⦄ (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        (g ((f₁ : (a : X i₁) → Z) x.1) : (a : Y) → T) ((f₂ : (a : X i₂) → Y) x.2 : Y)

Tactic:
forall_congr' (fun i₁ ↦ forall_congr' (fun f₁ ↦
    forall_congr' (fun i₂ ↦ forall_congr' (fun f₂ ↦
      ⟨fun h ↦ ContinuousMap.continuous_uncurry_of_continuous ⟨_, h⟩,
        fun h ↦ (ContinuousMap.curry ⟨_, h⟩).continuous⟩))))

Premises used: ContinuousMap.continuous, Topology.ContinuousMapGeneratedBy.precomp, ContinuousMap.curry, ContinuousMap.mk, Function.comp, Prod.fst, ContinuousMap.continuous_uncurry_of_continuous, Iff.intro, forall_congr', Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.Convenient.HomSpace
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
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
g : Z → ContinuousMapGeneratedBy X Y T
⊢ (∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v'} (X i) Z) (i_1 : ι) (f_1 : ContinuousMap.{u, v} (X i_1) Y),
      Continuous[inst i, _] (precomp (X := X) f_1 ∘ g ∘ (⇑f : (a : X i) → Z))) ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : ContinuousMap.{u, v'} (X i₁) Z) ⦃i₂ : ι⦄ (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        (g ((f₁ : (a : X i₁) → Z) x.1) : (a : Y) → T) ((f₂ : (a : X i₂) → Y) x.2 : Y)

Tactic:
exact forall_congr' (fun i₁ ↦ forall_congr' (fun f₁ ↦
    forall_congr' (fun i₂ ↦ forall_congr' (fun f₂ ↦
      ⟨fun h ↦ ContinuousMap.continuous_uncurry_of_continuous ⟨_, h⟩,
        fun h ↦ (ContinuousMap.curry ⟨_, h⟩).continuous⟩))))

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Topology.Convenient.HomSpace
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
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
⊢ ContinuousGeneratedBy X g ↔
    ∀ (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι) (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        match (motive := X i₁ × X i₂ → T) x with
        | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)

Tactic:
⟨fun h i₁ f₁ i₂ f₂ ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro