awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions.SumProd
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''
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:
rfl
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := Y ⊕ X ≃ₜ X ⊕ Y) (Homeomorph.symm (sumComm X Y)) (sumComm Y X)

Tactic:
rfl

Premises used: Homeomorph.sumComm, Sum.swap, Equiv.sumComm, Homeomorph.symm, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := (a : X ⊕ Y) → Y ⊕ X) (⇑(sumComm X Y) : (a : X ⊕ Y) → Y ⊕ X) Sum.swap

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim inl (inr ∘ inl))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
⊢ Continuous[inst_2, instTopologicalSpaceSum] (inr ∘ inr)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
⊢ Continuous[inst, instTopologicalSpaceSum] (inl ∘ inl)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceSum, instTopologicalSpaceSum] (Sum.elim (inl ∘ inr) inr)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
⊢ toEquiv (sumAssoc X Y Z) = Equiv.sumAssoc X Y Z

Tactic:
rfl

Premises used: Equiv.sumAssoc, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
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 W
inst_3 : TopologicalSpace Z
⊢ toEquiv (sumSumSumComm W X Y Z) = Equiv.sumSumSumComm W X Y Z

Tactic:
rfl

Premises used: Equiv.sumSumSumComm, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
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 W
inst_3 : TopologicalSpace Z
⊢ Eq (α := (X ⊕ W) ⊕ Y ⊕ Z ≃ₜ (X ⊕ Y) ⊕ W ⊕ Z) (Homeomorph.symm (sumSumSumComm X Y W Z)) (sumSumSumComm X W Y Z)

Tactic:
rfl

Premises used: Sum.swap, Equiv.sumSumSumComm, Homeomorph.sumSumSumComm, Homeomorph.symm, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IsEmpty Y
⊢ toEquiv (emptySum X Y) = Equiv.emptySum Y X

Tactic:
rfl

Premises used: Equiv.trans, Equiv.emptySum, rfl
-- Module: Mathlib.Topology.Constructions.SumProd
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)
⊢ IsInducing f

Tactic:
elim_comp_inl f g ▸ h.comp IsEmbedding.inl.isInducing

Premises used: Topology.IsEmbedding.inl, Sum.elim_comp_inl, Topology.IsInducing.comp, Eq.rec, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.Constructions.SumProd
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)
⊢ IsInducing g

Tactic:
elim_comp_inr f g ▸ h.comp IsEmbedding.inr.isInducing

Premises used: Sum.elim_comp_inr, Topology.IsInducing.comp, Eq.rec, Topology.IsEmbedding.isInducing, Topology.IsEmbedding.inr
-- Module: Mathlib.Topology.Constructions.SumProd
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))
⊢ Disjoint (𝓟 (range f)) (𝓝ˢ (range g))

Tactic:
rw [← disjoint_principal_nhdsSet] at hFg

Premises used: disjoint_principal_nhdsSet
-- Module: Mathlib.Topology.Constructions.SumProd
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))
hFg₁ : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
⊢ Disjoint (range f) (closure[inst_2] (range g))

Tactic:
rw [← disjoint_principal_nhdsSet] at hFg

Premises used: disjoint_principal_nhdsSet
-- Module: Mathlib.Topology.Constructions.SumProd
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))
⊢ Disjoint (𝓝ˢ (range f)) (𝓟 (range g))

Tactic:
rw [← disjoint_nhdsSet_principal] at hfG

Premises used: disjoint_nhdsSet_principal
-- Module: Mathlib.Topology.Constructions.SumProd
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))
rw : ∀ (x : X ⊕ Y), 𝓝 x = comap (Sum.elim f g) (𝓝 (Sum.elim f g x))
⊢ IsInducing (Sum.elim f g)

Tactic:
rw [isInducing_iff_nhds]

Premises used: Topology.isInducing_iff_nhds
-- Module: Mathlib.Topology.Constructions.SumProd
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
apply : comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x
⊢ 𝓝 x = comap (Sum.elim f g) (𝓝 (Sum.elim f g x))

Tactic:
apply le_antisymm ((hf.continuous.sumElim hg.continuous).tendsto x).le_comap

Premises used: Filter.Tendsto.le_comap, Continuous.tendsto, le_antisymm, Topology.IsInducing.continuous, Continuous.sumElim
-- Module: Mathlib.Topology.Constructions.SumProd
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)
inr : ∀ (x : Y), comap (Sum.elim f g) (𝓝 (Sum.elim f g (Sum.inr x))) ≤ 𝓝 (Sum.inr x)
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x

Tactic:
obtain x | x := x
-- Module: Mathlib.Topology.Constructions.SumProd
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
inl : map inr (comap g (𝓝 (f x))) ≤ map Sum.inl (𝓝 x)
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g (Sum.inl x))) ≤ 𝓝 (Sum.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]

Premises used: Topology.IsInducing.nhds_eq_comap, le_rfl, and_true, nhds_inl, nhds_inr, Sum.elim_inr, sup_le_iff, Filter.comap_sumElim_eq, Sum.elim_inl, true_and
-- Module: Mathlib.Topology.Constructions.SumProd
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
inr : map inl (comap f (𝓝 (g x))) ≤ map Sum.inr (𝓝 x)
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g (Sum.inr x))) ≤ 𝓝 (Sum.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]

Premises used: Topology.IsInducing.nhds_eq_comap, le_rfl, and_true, nhds_inl, nhds_inr, Sum.elim_inr, sup_le_iff, Filter.comap_sumElim_eq, Sum.elim_inl, true_and
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ LE.le (α := Filter (X ⊕ Y)) ⊥ (map inl (𝓝 x))

Tactic:
bot_le (α := Filter (X ⊕ Y))

Premises used: bot_le
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : Eq (α := Filter (X ⊕ Y)) (map inr (comap g (𝓝 (f x)))) ⊥
⊢ map inr (comap g (𝓝 (f x))) ≤ map inl (𝓝 x)

Tactic:
convert! bot_le (α := Filter (X ⊕ Y))

Premises used: bot_le
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ LE.le (α := Filter (X ⊕ Y)) ⊥ (map inr (𝓝 x))

Tactic:
bot_le (α := Filter (X ⊕ Y))

Premises used: bot_le
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : Eq (α := Filter (X ⊕ Y)) (map inl (comap f (𝓝 (g x)))) ⊥
⊢ map inl (comap f (𝓝 (g x))) ≤ map inr (𝓝 x)

Tactic:
convert! bot_le (α := Filter (X ⊕ Y))

Premises used: bot_le
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : (range g)ᶜ ∈ 𝓝 (f x)
⊢ Eq (α := Filter (X ⊕ Y)) (map inr (comap g (𝓝 (f x)))) ⊥

Tactic:
rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]

Premises used: Filter.map_eq_bot_iff, Filter.comap_eq_bot_iff_compl_range
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : (range f)ᶜ ∈ 𝓝 (g x)
⊢ Eq (α := Filter (X ⊕ Y)) (map inl (comap f (𝓝 (g x)))) ⊥

Tactic:
rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]

Premises used: Filter.map_eq_bot_iff, Filter.comap_eq_bot_iff_compl_range
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : Disjoint (𝓝 (f x)) (𝓟 (range g))
⊢ (range g)ᶜ ∈ 𝓝 (f x)

Tactic:
rw [← disjoint_principal_right]

Premises used: Filter.disjoint_principal_right
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ Disjoint (𝓝 (f x)) (𝓟 (range g))

Tactic:
hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))

Premises used: Set.mem_range_self, nhds_le_nhdsSet, Disjoint.mono_left
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ Disjoint (𝓝 (f x)) (𝓟 (range g))

Tactic:
exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))

Premises used: Set.mem_range_self, nhds_le_nhdsSet, Disjoint.mono_left
-- Module: Mathlib.Topology.Constructions.SumProd
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
h : Disjoint (𝓟 (range f)) (𝓝 (g x))
⊢ (range f)ᶜ ∈ 𝓝 (g x)

Tactic:
rw [← disjoint_principal_left]

Premises used: Filter.disjoint_principal_left
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ Disjoint (𝓟 (range f)) (𝓝 (g x))

Tactic:
hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

Premises used: Set.mem_range_self, nhds_le_nhdsSet, Disjoint.mono_right
-- Module: Mathlib.Topology.Constructions.SumProd
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
⊢ Disjoint (𝓟 (range f)) (𝓝 (g x))

Tactic:
exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

Premises used: Set.mem_range_self, nhds_le_nhdsSet, Disjoint.mono_right
-- Module: Mathlib.Topology.Constructions.SumProd
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)
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)
⊢ Disjoint (closure[inst_2] (range f)) (range g)

Tactic:
rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩

Premises used: isClosed_range_inl, Iff.mp, Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw₄ rw₅ : Subset (α := Set (X ⊕ Y)) (range inl) (range inl)
⊢ closure[inst_2] (range f) ⊆ C

Tactic:
rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]

Premises used: Set.range_comp, Sum.elim_comp_inl, IsClosed.closure_subset_iff, Set.image_subset_iff
-- Module: Mathlib.Topology.Constructions.SumProd
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

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]
-- Module: Mathlib.Topology.Constructions.SumProd
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
rw : Disjoint (α := Set (X ⊕ Y)) (inl '' univ) (inr '' univ)
⊢ Disjoint C (range g)

Tactic:
rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC,
        ← disjoint_image_right, ← image_univ]

Premises used: Set.image_univ, Sum.elim_comp_inr, Set.preimage_comp, Set.disjoint_image_right
-- Module: Mathlib.Topology.Constructions.SumProd
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 (α := Set (X ⊕ Y)) (inl '' univ) (inr '' univ)

Tactic:
disjoint_image_inl_image_inr

Premises used: Set.disjoint_image_inl_image_inr
-- Module: Mathlib.Topology.Constructions.SumProd
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 (α := Set (X ⊕ Y)) (inl '' univ) (inr '' univ)

Tactic:
exact disjoint_image_inl_image_inr

Premises used: Set.disjoint_image_inl_image_inr
-- Module: Mathlib.Topology.Constructions.SumProd
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)

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
-- Module: Mathlib.Topology.Constructions.SumProd
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
B : Disjoint C (range g)
⊢ Disjoint (closure[inst_2] (range f)) (range g)

Tactic:
B.mono_left A

Premises used: Disjoint.mono_left
-- Module: Mathlib.Topology.Constructions.SumProd
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
B : Disjoint C (range g)
⊢ Disjoint (closure[inst_2] (range f)) (range g)

Tactic:
exact B.mono_left A

Premises used: Disjoint.mono_left
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsOpenEmbedding (X := X ⊕ Y) Sum.swap

Tactic:
(Homeomorph.sumComm X Y).isOpenEmbedding

Premises used: Homeomorph.sumComm, Sum.swap, Homeomorph.isOpenEmbedding, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsInducing (X := X ⊕ Y) Sum.swap

Tactic:
IsOpenEmbedding.sumSwap.isInducing

Premises used: IsOpenEmbedding.sumSwap, Topology.IsOpenEmbedding.isInducing
-- Module: Mathlib.Topology.Constructions.SumProd
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 (Sum.elim f g) ↔
    IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst_2] (range f)) (range g) ∧ Disjoint (range f) (closure[inst_2] (range g))

Tactic:
⟨fun h ↦ ⟨h.sumElim_left, h.sumElim_right, h.disjoint_of_sumElim_aux,
    ((Sum.elim_swap ▸ h.comp IsInducing.sumSwap).disjoint_of_sumElim_aux ).symm⟩,
    fun ⟨hf, hg, hFg, hfG⟩ ↦ hf.sumElim hg hFg hfG⟩

Premises used: _private.0.isInducing_sumElim.match_1, Topology.IsInducing.sumElim, Topology.IsInducing.disjoint_of_sumElim_aux, Topology.IsInducing, Topology.IsInducing.sumElim_left, And.intro, Iff.intro, Topology.IsInducing.sumElim_right, Sum.elim
-- Module: Mathlib.Topology.Constructions.SumProd
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
hsep : SeparatedNhds (range f) (range g)
⊢ IsInducing (Sum.elim f g)

Tactic:
hf.sumElim hg hsep.disjoint_closure_left hsep.disjoint_closure_right

Premises used: Topology.IsInducing.sumElim, SeparatedNhds.disjoint_closure_left, SeparatedNhds.disjoint_closure_right
-- Module: Mathlib.Topology.Constructions.SumProd
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 : IsEmbedding (Sum.elim f g)
⊢ IsEmbedding f

Tactic:
elim_comp_inl f g ▸ h.comp IsEmbedding.inl

Premises used: Topology.IsEmbedding.inl, Sum.elim_comp_inl, Eq.rec, Topology.IsEmbedding.comp
-- Module: Mathlib.Topology.Constructions.SumProd
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 : IsEmbedding (Sum.elim f g)
⊢ IsEmbedding g

Tactic:
elim_comp_inr f g ▸ h.comp IsEmbedding.inr

Premises used: Sum.elim_comp_inr, Eq.rec, Topology.IsEmbedding.comp, Topology.IsEmbedding.inr
-- Module: Mathlib.Topology.Constructions.SumProd
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
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))
⊢ 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))

Tactic:
simp_rw [isEmbedding_iff, isInducing_sumElim, Sum.elim_injective]

Premises used: Sum.elim_injective, Topology.isEmbedding_iff, isInducing_sumElim