awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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.invFun (WithGeneratedByTopology.equiv (X := X)))
have dsimp : Continuous[tY, _] (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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, inst_1] g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y), Continuous[inst i, inst_1] (g ∘ (⇑f : (a : X i) → Y))
have 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))
Tactic: rw [(homeomorph (X := X)).isQuotientMap.continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
have refine : ∀ (hg : Continuous[tY, inst_1] g),
  Continuous[tY, _]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g)
Tactic: refine ⟨fun hg ↦ WithGeneratedByTopology.continuous_equiv.comp hg, fun hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
⊢ Continuous[tY, _]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g)
have 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))
Tactic: rw [continuous_iff (X := X)]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
⊢ Continuous[inst i, _]
    (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
      (⇑f : (a : X i) → Y))
have 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)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (hypothesis)
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
⊢ IsOpen[inst i]
    (((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘ g) ∘
        (⇑f : (a : X i) → Y) ⁻¹'
      U)
have 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))
Tactic: rw [WithGeneratedByTopology.isOpen_iff] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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 : ι
⊢ Continuous[inst_1 i, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i))
have 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)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (hypothesis)
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
⊢ IsOpen[inst_1 i]
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : X i) → WithGeneratedByTopology X (X i)) ⁻¹' U)
have 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))
Tactic: rw [WithGeneratedByTopology.isOpen_iff] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
⊢ 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))
have 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)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
⊢ IsOpen (X := WithGeneratedByTopology X Y)
    ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
        (a : WithGeneratedByTopology X Y) → WithGeneratedByTopology X (WithGeneratedByTopology X Y)) ⁻¹'
      U)
have 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)))
Tactic: rw [WithGeneratedByTopology.isOpen_iff] at hU ⊢
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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)))
have refine : Continuous[inst i, _]
  (Function.comp (β := Y)
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
    (⇑f : (a : X i) → Y))
Tactic: refine hU ⟨WithGeneratedByTopology.equiv.symm ∘ f, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
⊢ Continuous[inst i, _]
    (Function.comp (β := Y)
      (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
      (⇑f : (a : X i) → Y))
have 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))
Tactic: rw [continuous_iff X]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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, _]
    (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))
have rw : Continuous[inst j, tY] (Function.comp (β := X i) (⇑f : (a : X i) → Y) (⇑g : (a : X j) → X i))
Tactic: rw [Function.comp_assoc, equiv_symm_comp_continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
⊢ IsGeneratedBy X PUnit.{v + 1}
have rw : instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X
Tactic: rw [iff_le_generatedBy]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
have refine : TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X
Tactic: refine iff_le_generatedBy.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
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
have rw : IsGeneratedBy X Y
Tactic: rw [sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (goal)
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
⊢ Continuous (X := ContinuousMapGeneratedBy X Z T) (precomp (X := X) f)
have rw : LE.le (α := TopologicalSpace (ContinuousMapGeneratedBy X Z T)) (instTopologicalSpace (X := X))
  (TopologicalSpace.induced (precomp (X := X) f) ContinuousMap.compactOpen)
Tactic: rw [continuous_iff_le_induced]
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (goal)
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
⊢ 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)
have 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)
Tactic: simp only [continuousGeneratedBy_def, continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (goal)
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₁)
have refine_1 : ∀ (h : 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: refine ⟨fun h i₁ f₁ i₂ f₂ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (goal)
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
refine_1 :
  ∀ (h : 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₁)
⊢ 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₁)
have refine_2 : ∀
  (h :
    ∀ (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₁)),
  ContinuousGeneratedBy X g
Tactic: refine ⟨fun h i₁ f₁ i₂ f₂ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (goal)
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
h : 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₁)
have refine_1 : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)),
  Continuous[inst i, 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₁)) ∘
      (⇑f : (a : X i) → X i₁ × X i₂))
Tactic: rw [IsGeneratedBy.continuous_iff X]
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (hypothesis)
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
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
⊢ Continuous[inst j, 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₁)) ∘
      (⇑p : (a : X j) → X i₁ × X i₂))
have h₁ : ContinuousGeneratedBy X (g ∘ φ)
Tactic: replace h := h.comp (show Continuous φ by fun_prop).continuousGeneratedBy
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Convenient.HomSpace (hypothesis)
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
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
h : ContinuousGeneratedBy X (g ∘ φ)
⊢ Continuous[inst j, 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₁)) ∘
      (⇑p : (a : X j) → X i₁ × X i₂))
have h₁ : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst i, inst_3] ((g ∘ φ) ∘ (⇑f : (a : X i) → X i₁ × X i₂))
Tactic: rw [continuousGeneratedBy_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑U : Type u_3)
have hg : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
  Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
Tactic: have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage
-- Lean 4 proof step from Mathlib.Topology.Convenient.OpenClosed (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑U : Type u_3)
have continuous_equiv_symm : Continuous[instTopologicalSpaceSubtype, _]
  (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
    (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3))
Tactic: constructor