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
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
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'')
⊢ 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 : Y),
  Eq (α := X'' ⊕ Y'') (((h₁.sumCongr h₂).trans (h₃.sumCongr h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inr val) : X'' ⊕ Y'')
    (((h₁.trans h₃).sumCongr (h₂.trans h₄) : (a : X ⊕ Y) → X'' ⊕ Y'') (inr val) : X'' ⊕ Y'')
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ IsInducing (Sum.elim f g)
have hFg₁ : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
Tactic: rw [← disjoint_principal_nhdsSet] at hFg
Cleared hypotheses: hFg, hfG
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ IsInducing (Sum.elim f g)
have hfG₁ : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
Tactic: rw [← disjoint_nhdsSet_principal] at hfG
Cleared hypotheses: hfG
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
⊢ IsInducing (Sum.elim f g)
have rw : ∀ (x : X ⊕ Y), 𝓝 x = comap (Sum.elim f g) (𝓝 (Sum.elim f g x))
Tactic: rw [isInducing_iff_nhds]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X ⊕ Y
⊢ 𝓝 x = comap (Sum.elim f g) (𝓝 (Sum.elim f g x))
have apply : comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x
Tactic: apply le_antisymm ((hf.continuous.sumElim hg.continuous).tendsto x).le_comap
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X ⊕ Y
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x
have inl : ∀ (x : X), comap (Sum.elim f g) (𝓝 (Sum.elim f g (inl x))) ≤ 𝓝 (inl x)
Tactic: obtain x | x := x
Cleared hypotheses: x
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X ⊕ Y
inl : ∀ (x : X), comap (Sum.elim f g) (𝓝 (Sum.elim f g (Sum.inl x))) ≤ 𝓝 (Sum.inl x)
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x
have inr : ∀ (x : Y), comap (Sum.elim f g) (𝓝 (Sum.elim f g (inr x))) ≤ 𝓝 (inr x)
Tactic: obtain x | x := x
Cleared hypotheses: x
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g (inl x))) ≤ 𝓝 (inl x)
have inl : map inr (comap g (𝓝 (f x))) ≤ map inl (𝓝 x)
Tactic: simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g (inr x))) ≤ 𝓝 (inr x)
have inr : map inl (comap f (𝓝 (g x))) ≤ map inr (𝓝 x)
Tactic: simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ map inr (comap g (𝓝 (f x))) ≤ map inl (𝓝 x)
have h : Eq (α := Filter (X ⊕ Y)) (map inr (comap g (𝓝 (f x)))) ⊥
Tactic: convert! bot_le (α := Filter (X ⊕ Y))
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ map inl (comap f (𝓝 (g x))) ≤ map inr (𝓝 x)
have h : Eq (α := Filter (X ⊕ Y)) (map inl (comap f (𝓝 (g x)))) ⊥
Tactic: convert! bot_le (α := Filter (X ⊕ Y))
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ Eq (α := Filter (X ⊕ Y)) (map inr (comap g (𝓝 (f x)))) ⊥
have h : (range g)ᶜ ∈ 𝓝 (f x)
Tactic: rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ Eq (α := Filter (X ⊕ Y)) (map inl (comap f (𝓝 (g x)))) ⊥
have h : (range f)ᶜ ∈ 𝓝 (g x)
Tactic: rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)
have h : Disjoint (𝓝 (f x)) (𝓟 (range g))
Tactic: rw [← disjoint_principal_right]
-- 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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)
have h : Disjoint (𝓟 (range f)) (𝓝 (g x))
Tactic: rw [← disjoint_principal_left]
-- 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
h : IsInducing (Sum.elim f g)
⊢ Disjoint (closure[inst_2] (range f)) (range g)
have rcases : ∀ (C : Set Z) (C_closed : IsClosed[inst_2] C) (hC : Sum.elim f g ⁻¹' C = range inl),
  Disjoint (closure[inst_2] (range f)) (range g)
Tactic: rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ closure[inst_2] (range f) ⊆ C
have rw : range f ⊆ C
Tactic: rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
rw : range f ⊆ C
⊢ closure[inst_2] (range f) ⊆ C
have rw₁ : range (Sum.elim f g ∘ inl) ⊆ C
Tactic: rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
rw : range f ⊆ C
rw₁ : range (Sum.elim f g ∘ inl) ⊆ C
⊢ closure[inst_2] (range f) ⊆ C
have rw₂ : Sum.elim f g '' range inl ⊆ C
Tactic: rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
rw : range f ⊆ C
rw₁ : range (Sum.elim f g ∘ inl) ⊆ C
rw₂ : Sum.elim f g '' range inl ⊆ C
⊢ closure[inst_2] (range f) ⊆ C
have rw₃ : range inl ⊆ Sum.elim f g ⁻¹' C
Tactic: rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
rw : range f ⊆ C
rw₁ : range (Sum.elim f g ∘ inl) ⊆ C
rw₂ : Sum.elim f g '' range inl ⊆ C
rw₃ : range inl ⊆ Sum.elim f g ⁻¹' C
⊢ closure[inst_2] (range f) ⊆ C
have rw₄ : Subset (α := Set (X ⊕ Y)) (range inl) (range inl)
Tactic: rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
⊢ Disjoint (closure[inst_2] (range f)) (range g)
have A : closure[inst_2] (range f) ⊆ C
Tactic: have A : closure (range f) ⊆ C := by
    rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
-- 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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst_2] (range f) ⊆ C
⊢ Disjoint C (range g)
have rw : Disjoint (α := Set (X ⊕ Y)) (inl '' univ) (inr '' univ)
Tactic: rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC,
        ← disjoint_image_right, ← image_univ]
-- Lean 4 proof step from Mathlib.Topology.Constructions.SumProd (hypothesis)
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
h : IsInducing (Sum.elim f g)
C : Set Z
C_closed : IsClosed[inst_2] C
hC : Sum.elim f g ⁻¹' C = range inl
A : closure[inst_2] (range f) ⊆ C
⊢ Disjoint (closure[inst_2] (range f)) (range g)
have B : Disjoint C (range g)
Tactic: have B : Disjoint C (range g) := by
    rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC,
        ← disjoint_image_right, ← image_univ]
    exact disjoint_image_inl_image_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
⊢ IsEmbedding (Sum.elim f g) ↔
    IsEmbedding f ∧
      IsEmbedding g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
have simp_rw : ((IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) ↔
  (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
Tactic: simp_rw [isEmbedding_iff, isInducing_sumElim, Sum.elim_injective]
-- 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
⊢ ((IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) ↔
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
have mp : ((IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
  (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
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 → Z
g : Y → Z
mp :
  ((IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
⊢ ((IsInducing f ∧
        IsInducing g ∧
          Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) ↔
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))
have mpr : (IsInducing f ∧ Injective f) ∧
    (IsInducing g ∧ Injective g) ∧
      Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g)) →
  (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g 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 → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst_2] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst_2] (range g))
⊢ (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b
have mpr : ∀ (a : X) (b : Y), f a ≠ g b
Tactic: refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
⊢ 𝓝 x = comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X))
have rw : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
Tactic: rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
rw :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
⊢ 𝓝 x = comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X))
have rw₁ : Eq (α := Filter { x : X // x ∈ s })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X)))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
Tactic: rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : { x : X // x ∈ s }
rw :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
rw₁ :
  Eq (α := Filter { x : X // x ∈ s })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s))
      (𝓝[range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))] (↑x : X)))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
⊢ 𝓝 x = comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X))
have rw₂ : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[s] (↑x : X)))
Tactic: rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw : 𝓝[s ↓∩ t] x = ⊥ ↔ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw₁ : 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₁ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw₂ : 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X) ⊓ 𝓟 t)) ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₁ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₂ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X) ⊓ 𝓟 t)) ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw₃ : 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
  Eq (α := Filter { x : X // x ∈ s })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓟 t))
    ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]
-- Lean 4 proof step from Mathlib.Topology.Constructions (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
x : (↑s : Type u)
rw :
  𝓝[s ↓∩ t] x = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₁ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[t] (↑x : X))) ⊥
rw₂ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X) ⊓ 𝓟 t)) ⊥
rw₃ :
  𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
    Eq (α := Filter { x : X // x ∈ s })
      (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓
        comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓟 t))
      ⊥
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] (↑x : X) ⊓ 𝓟 s = ⊥
have rw₄ : 𝓝 x ⊓ 𝓟 (s ↓∩ t) = ⊥ ↔
  Eq (α := Filter { x : X // x ∈ s })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 (↑x : X)) ⊓ 𝓟 (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) ⊥
Tactic: rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]