awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : Dense s
ht : Dense t
x : X × Y
⊢ x ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)
have rw : x ∈ closure[inst] s ×ˢ closure[inst_1] t
Tactic: rw [closure_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x_1 : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
have simp_rw : 𝓝 (x, z) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
Tactic: simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x_1 : X × Z
x : X
z : Z
simp_rw : 𝓝 (x, z) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
have simp_rw₁ : 𝓝 x ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
Tactic: simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x_1 : X × Z
x : X
z : Z
simp_rw : 𝓝 (x, z) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
simp_rw₁ : 𝓝 x ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
have simp_rw₂ : comap f (𝓝 (f x)) ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
Tactic: simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x_1 : X × Z
x : X
z : Z
simp_rw : 𝓝 (x, z) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x, g z))
simp_rw₁ : 𝓝 x ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
simp_rw₂ : comap f (𝓝 (f x)) ×ˢ 𝓝 z = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
have simp_rw₃ : comap f (𝓝 (f x)) ×ˢ comap g (𝓝 (g z)) = comap (fun (p : X × Z) ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
Tactic: simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw₁ : inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
  inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
simp_rw₁ :
  inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw₂ : inst_1 =
    induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst) ⊓
      induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.snd inst_2) ↔
  inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
simp_rw₁ :
  inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₂ :
  inst_1 =
      induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst) ⊓
        induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw₃ : inst_1 =
    induced (comp (β := X × Z) Prod.fst fun (x' : Y) ↦ (x, f x')) inst ⊓
      induced (comp (β := X × Z) Prod.snd fun (x' : Y) ↦ (x, f x')) inst_2 ↔
  inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
simp_rw₁ :
  inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₂ :
  inst_1 =
      induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst) ⊓
        induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₃ :
  inst_1 =
      induced (comp (β := X × Z) Prod.fst fun (x' : Y) ↦ (x, f x')) inst ⊓
        induced (comp (β := X × Z) Prod.snd fun (x' : Y) ↦ (x, f x')) inst_2 ↔
    inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw₄ : inst_1 = induced (fun (x_1 : Y) ↦ x) inst ⊓ induced (fun (x : Y) ↦ f x) inst_2 ↔ inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
x : X
f : Y → Z
simp_rw : inst_1 = induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) instTopologicalSpaceProd ↔ inst_1 = induced f inst_2
simp_rw₁ :
  inst_1 = induced (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst ⊓ induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₂ :
  inst_1 =
      induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.fst inst) ⊓
        induced (Y := X × Z) (fun (x' : Y) ↦ (x, f x')) (induced Prod.snd inst_2) ↔
    inst_1 = induced f inst_2
simp_rw₃ :
  inst_1 =
      induced (comp (β := X × Z) Prod.fst fun (x' : Y) ↦ (x, f x')) inst ⊓
        induced (comp (β := X × Z) Prod.snd fun (x' : Y) ↦ (x, f x')) inst_2 ↔
    inst_1 = induced f inst_2
simp_rw₄ : inst_1 = induced (fun (x_1 : Y) ↦ x) inst ⊓ induced (fun (x : Y) ↦ f x) inst_2 ↔ inst_1 = induced f inst_2
⊢ (IsInducing (Y := X × Z) fun (x' : Y) ↦ (x, f x')) ↔ IsInducing f
have simp_rw₅ : inst_1 = ⊤ ⊓ induced (fun (x : Y) ↦ f x) inst_2 ↔ inst_1 = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, top_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw₁ : inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
simp_rw₁ :
  inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw₂ : inst =
    induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2) ⊓
      induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.snd inst_1) ↔
  inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
simp_rw₁ :
  inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
simp_rw₂ :
  inst =
      induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2) ⊓
        induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.snd inst_1) ↔
    inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw₃ : inst =
    induced (comp (β := Z × Y) Prod.fst fun (x : X) ↦ (f x, y)) inst_2 ⊓
      induced (comp (β := Z × Y) Prod.snd fun (x : X) ↦ (f x, y)) inst_1 ↔
  inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
simp_rw₁ :
  inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
simp_rw₂ :
  inst =
      induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2) ⊓
        induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.snd inst_1) ↔
    inst = induced f inst_2
simp_rw₃ :
  inst =
      induced (comp (β := Z × Y) Prod.fst fun (x : X) ↦ (f x, y)) inst_2 ⊓
        induced (comp (β := Z × Y) Prod.snd fun (x : X) ↦ (f x, y)) inst_1 ↔
    inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw₄ : inst = induced (fun (x : X) ↦ f x) inst_2 ⊓ induced (fun (x : X) ↦ y) inst_1 ↔ inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
y : Y
f : X → Z
simp_rw : inst = induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) instTopologicalSpaceProd ↔ inst = induced f inst_2
simp_rw₁ :
  inst = induced (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2 ⊓ induced Prod.snd inst_1) ↔ inst = induced f inst_2
simp_rw₂ :
  inst =
      induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.fst inst_2) ⊓
        induced (Y := Z × Y) (fun (x : X) ↦ (f x, y)) (induced Prod.snd inst_1) ↔
    inst = induced f inst_2
simp_rw₃ :
  inst =
      induced (comp (β := Z × Y) Prod.fst fun (x : X) ↦ (f x, y)) inst_2 ⊓
        induced (comp (β := Z × Y) Prod.snd fun (x : X) ↦ (f x, y)) inst_1 ↔
    inst = induced f inst_2
simp_rw₄ : inst = induced (fun (x : X) ↦ f x) inst_2 ⊓ induced (fun (x : X) ↦ y) inst_1 ↔ inst = induced f inst_2
⊢ (IsInducing (Y := Z × Y) fun (x : X) ↦ (f x, y)) ↔ IsInducing f
have simp_rw₅ : inst = induced (fun (x : X) ↦ f x) inst_2 ⊓ ⊤ ↔ inst = induced f inst_2
Tactic: simp_rw [isInducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose,
    Function.comp_def, induced_const, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Prod.map f g)
have rw : ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)
Tactic: rw [isOpenMap_iff_nhds_le]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))
have rw : 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
Tactic: rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClosed[instTopologicalSpaceSum] (range inl)
have rw : IsOpen[instTopologicalSpaceSum] (range inr)
Tactic: rw [← isOpen_compl_iff, compl_range_inl]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClosed[instTopologicalSpaceSum] (range inr)
have rw : IsOpen[instTopologicalSpaceSum] (range inl)
Tactic: rw [← isOpen_compl_iff, compl_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)
have rw : ∀ (hf : Continuous[inst, inst_2] f ∧ Injective f ∧ IsOpenMap f)
  (hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsOpenMap g) (h : Injective (Sum.elim f g)),
  Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)
Tactic: rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
Cleared hypotheses: hf, hg, h
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsClosedMap f ↔
    (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)
have mp : IsClosedMap f →
  (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X ⊕ Y → Z
mp :
  IsClosedMap f →
    (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)
⊢ IsClosedMap f ↔
    (IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)
have mpr : ((IsClosedMap.{u, u_2} (Y := Z) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z) fun (b : Y) ↦ f (inr b)) →
  IsClosedMap f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[instTopologicalSpaceSum] Z
⊢ IsClosed[inst_2] (f '' Z)
have hZ₁ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
Tactic: rw [isClosed_sum_iff] at hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
⊢ IsClosed[inst_2] (f '' Z)
have h₁ : f '' Z = (fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z
Tactic: convert! (h.1 _ hZ.1).union (h.2 _ hZ.2)
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z_1 : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z_1
f : X ⊕ Y → Z_1
h : (IsClosedMap.{u, u_2} (Y := Z_1) fun (a : X) ↦ f (inl a)) ∧ IsClosedMap.{v, u_2} (Y := Z_1) fun (b : Y) ↦ f (inr b)
Z : Set (X ⊕ Y)
hZ : IsClosed[inst] (inl ⁻¹' Z) ∧ IsClosed[inst_1] (inr ⁻¹' Z)
⊢ f '' Z = (fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z
have h₁ : ∀ (x : Z_1),
  x ∈ f '' Z ↔
    Membership.mem (γ := Set Z_1) ((fun (a : X) ↦ f (inl a)) '' inl ⁻¹' Z ∪ (fun (b : Y) ↦ f (inr b)) '' inr ⁻¹' Z) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsClosedEmbedding f
hg : IsClosedEmbedding g
h : Injective (Sum.elim f g)
⊢ IsClosedEmbedding (Sum.elim f g)
have rw : ∀ (hf : Continuous[inst, inst_2] f ∧ Injective f ∧ IsClosedMap f)
  (hg : Continuous[inst_1, inst_2] g ∧ Injective g ∧ IsClosedMap g) (h : Injective (Sum.elim f g)),
  Continuous[instTopologicalSpaceSum, inst_2] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)
Tactic: rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
Cleared hypotheses: hf, hg, h
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := X ⊕ Y ≃ₜ X ⊕ Y) (sumCongr (Homeomorph.refl X) (Homeomorph.refl Y)) (Homeomorph.refl (X ⊕ Y))
have H : ∀ (i : X ⊕ Y),
  Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : X ⊕ Y
⊢ Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
have H : ∀ (val : X),
  Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
i : X ⊕ Y
H :
  ∀ (val : X),
    Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
      ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inl val) : X ⊕ Y)
⊢ Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) i : X ⊕ Y)
have H₁ : ∀ (val : Y),
  Eq (α := X ⊕ Y) ((sumCongr (Homeomorph.refl X) (Homeomorph.refl Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)
    ((Homeomorph.refl (X ⊕ Y) : (a : X ⊕ Y) → X ⊕ Y) (inr val) : X ⊕ Y)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst_2 : TopologicalSpace X'
inst_3 : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst_4 : TopologicalSpace X''
inst_5 : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
⊢ (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)
have H : ∀ (i : X ⊕ Y),
  Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
X' : Type u_5
Y' : Type u_6
inst_2 : TopologicalSpace X'
inst_3 : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst_4 : TopologicalSpace X''
inst_5 : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
i : X ⊕ Y
⊢ Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') i : X'' ⊕ Y'')
have H : ∀ (val : X),
  Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inl val) : X'' ⊕ Y'')
Tactic: cases i
Cleared hypotheses: i