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
⊢ Continuous[instTopologicalSpaceProd, inst] Prod.fst

Tactic:
(continuous_prodMk.1 continuous_id).1

Premises used: continuous_id, And.left, Iff.mp, continuous_prodMk
-- 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 → Y × Z
hf : Continuous[inst, instTopologicalSpaceProd] f
⊢ Continuous[inst, inst_1] fun (x : X) ↦ (f x).1

Tactic:
continuous_fst.comp hf

Premises used: Continuous.comp, continuous_fst
-- 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
hf : Continuous[inst, inst_2] f
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (x : X × Y) ↦ f x.1

Tactic:
hf.comp continuous_fst

Premises used: Continuous.comp, continuous_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X × Y
⊢ ContinuousAt Prod.fst p

Tactic:
continuous_fst.continuousAt

Premises used: continuous_fst, Continuous.continuousAt
-- 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 → Y × Z
x : X
hf : ContinuousAt f x
⊢ ContinuousAt.{u, v} (Y := Y) (fun (x : X) ↦ (f x).1) x

Tactic:
continuousAt_fst.comp hf

Premises used: ContinuousAt.comp, continuousAt_fst
-- 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
x : X
y : Y
hf : ContinuousAt f x
⊢ ContinuousAt (Y := Z) (fun (x : X × Y) ↦ f x.1) (x, y)

Tactic:
ContinuousAt.comp hf continuousAt_fst

Premises used: ContinuousAt.comp, continuousAt_fst
-- 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
x : X × Y
hf : ContinuousAt f x.1
⊢ ContinuousAt (Y := Z) (fun (x : X × Y) ↦ f x.1) x

Tactic:
hf.comp continuousAt_fst

Premises used: ContinuousAt.comp, continuousAt_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
Y : Type v
Z : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
X : Type u_5
l : Filter X
f : X → Y × Z
p : Y × Z
h : Tendsto f l (𝓝 p)
⊢ Tendsto (fun (a : X) ↦ (f a).1) l (𝓝 p.1)

Tactic:
continuousAt_fst.tendsto.comp h

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp, continuousAt_fst
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst_1] Prod.snd

Tactic:
(continuous_prodMk.1 continuous_id).2

Premises used: continuous_id, And.right, Iff.mp, continuous_prodMk
-- 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 → Y × Z
hf : Continuous[inst, instTopologicalSpaceProd] f
⊢ Continuous[inst, inst_2] fun (x : X) ↦ (f x).2

Tactic:
continuous_snd.comp hf

Premises used: Continuous.comp, continuous_snd
-- 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 : Y → Z
hf : Continuous[inst_1, inst_2] f
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (x : X × Y) ↦ f x.2

Tactic:
hf.comp continuous_snd

Premises used: Continuous.comp, continuous_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X × Y
⊢ ContinuousAt Prod.snd p

Tactic:
continuous_snd.continuousAt

Premises used: continuous_snd, Continuous.continuousAt
-- 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 → Y × Z
x : X
hf : ContinuousAt f x
⊢ ContinuousAt.{u, u_2} (Y := Z) (fun (x : X) ↦ (f x).2) x

Tactic:
continuousAt_snd.comp hf

Premises used: ContinuousAt.comp, continuousAt_snd
-- 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 : Y → Z
x : X
y : Y
hf : ContinuousAt f y
⊢ ContinuousAt (Y := Z) (fun (x : X × Y) ↦ f x.2) (x, y)

Tactic:
ContinuousAt.comp hf continuousAt_snd

Premises used: ContinuousAt.comp, continuousAt_snd
-- 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 : Y → Z
x : X × Y
hf : ContinuousAt f x.2
⊢ ContinuousAt (Y := Z) (fun (x : X × Y) ↦ f x.2) x

Tactic:
hf.comp continuousAt_snd

Premises used: ContinuousAt.comp, continuousAt_snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
Y : Type v
Z : Type u_2
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
X : Type u_5
l : Filter X
f : X → Y × Z
p : Y × Z
h : Tendsto f l (𝓝 p)
⊢ Tendsto (fun (a : X) ↦ (f a).2) l (𝓝 p.2)

Tactic:
continuousAt_snd.tendsto.comp h

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp, continuousAt_snd
-- 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 : Z → X
g : Z → Y
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_2, inst_1] g
⊢ Continuous[inst_2, instTopologicalSpaceProd] fun (x : Z) ↦ (f x, g x)

Tactic:
continuous_prodMk.2 ⟨hf, hg⟩

Premises used: Iff.mpr, And.intro, continuous_prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
⊢ Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ Continuous[inst, instTopologicalSpaceProd] fun (x : X) ↦ (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Z
α : Type u_5
f : X → α → Z
s : Set α
t : Set Z
ht : IsClosed[inst_1] t
hf : ∀ a ∈ s, Continuous[inst, inst_1] fun (x : X) ↦ f x a
⊢ IsClosed[inst] {x : X | MapsTo (f x) s t}

Tactic:
simpa only [MapsTo, setOf_forall] using isClosed_biInter fun y hy ↦ ht.preimage (hf y hy)

Premises used: isClosed_biInter, Set.MapsTo, IsClosed.preimage, Set.setOf_forall
-- 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 Z
inst_3 : TopologicalSpace W
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_2] g
e : W → X
he : Continuous[inst_3, inst] e
f : W → Y
hf : Continuous[inst_3, inst_1] f
⊢ Continuous[inst_3, inst_2] fun (w : W) ↦ g (e w, f w)

Tactic:
hg.comp <| he.prodMk hf

Premises used: Continuous.comp, Continuous.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
g : X × Y × Z → ε
hg : Continuous[instTopologicalSpaceProd, inst_4] g
e : W → X
he : Continuous[inst_3, inst] e
f : W → Y
hf : Continuous[inst_3, inst_1] f
k : W → Z
hk : Continuous[inst_3, inst_2] k
⊢ Continuous[inst_3, inst_4] fun (w : W) ↦ g (e w, f w, k w)

Tactic:
hg.comp₂ he <| hf.prodMk hk

Premises used: Continuous.comp₂, Continuous.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
g : X × Y × Z × ζ → ε
hg : Continuous[instTopologicalSpaceProd, inst_4] g
e : W → X
he : Continuous[inst_3, inst] e
f : W → Y
hf : Continuous[inst_3, inst_1] f
k : W → Z
hk : Continuous[inst_3, inst_2] k
l : W → ζ
hl : Continuous[inst_3, inst_5] l
⊢ Continuous[inst_3, inst_4] fun (w : W) ↦ g (e w, f w, k w, l w)

Tactic:
hg.comp₃ he hf <| hk.prodMk hl

Premises used: Continuous.comp₃, Continuous.prodMk
-- 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 Z
inst_3 : TopologicalSpace W
f : Z → X
g : W → Y
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_3, inst_1] g
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g)

Tactic:
hf.fst'.prodMk hg.snd'

Premises used: Continuous.fst', Continuous.snd', Prod.map, Continuous.prodMk
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
haveI : (this : TopologicalSpace X) → Prop
⊢ Prop

Tactic:
haveI := ta1
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
haveI : (this : TopologicalSpace Y) → Prop
⊢ Prop

Tactic:
haveI := tb1
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this_1 : TopologicalSpace X
this : TopologicalSpace Y
⊢ Prop

Tactic:
exact Continuous fun p : X × Y => f p.1 p.2

Premises used: Continuous, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
haveI : (this : TopologicalSpace X) → Prop
⊢ Prop

Tactic:
haveI := ta1 ⊓ ta2
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
this : TopologicalSpace X
haveI : (this : TopologicalSpace Y) → Prop
⊢ Prop

Tactic:
haveI := tb1 ⊓ tb2
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
this_1 : TopologicalSpace X
this : TopologicalSpace Y
⊢ Prop

Tactic:
exact Continuous fun p : X × Y => f p.1 p.2

Premises used: Continuous, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[ta1 ⊓ ta2, ta1] id

Tactic:
have ha := @continuous_inf_dom_left _ _ id ta1 ta2 ta1 (@continuous_id _ (id _))
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
⊢ Continuous[tb1 ⊓ tb2, tb1] id

Tactic:
have hb := @continuous_inf_dom_left _ _ id tb1 tb2 tb1 (@continuous_id _ (id _))
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
hb : Continuous[tb1 ⊓ tb2, tb1] id
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ ta1 tb1 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
hb : Continuous[tb1 ⊓ tb2, tb1] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
@Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta1] id
hb : Continuous[tb1 ⊓ tb2, tb1] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
haveI : (this : TopologicalSpace X) → Prop
⊢ Prop

Tactic:
haveI := ta2
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
this : TopologicalSpace X
haveI : (this : TopologicalSpace Y) → Prop
⊢ Prop

Tactic:
haveI := tb2
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[ta1 ⊓ ta2, ta2] id

Tactic:
have ha := @continuous_inf_dom_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
⊢ Continuous[tb1 ⊓ tb2, tb2] id

Tactic:
have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
@Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
h : Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2
ha : Continuous[ta1 ⊓ ta2, ta2] id
hb : Continuous[tb1 ⊓ tb2, tb2] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc1] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
haveI : (this : TopologicalSpace X) → Prop
⊢ Prop

Tactic:
haveI := sInf tas
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
this : TopologicalSpace X
haveI : (this : TopologicalSpace Y) → Prop
⊢ Prop

Tactic:
haveI := sInf tbs
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X_1 : Type u
Y_1 : Type v
W : Type u_1
Z_1 : Type u_2
ε : Type u_3
ζ : Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
inst_2 : TopologicalSpace Z_1
inst_3 : TopologicalSpace W
inst_4 : TopologicalSpace ε
inst_5 : TopologicalSpace ζ
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
this_1 : TopologicalSpace X
this : TopologicalSpace Y
⊢ Prop

Tactic:
exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Premises used: Continuous, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
⊢ Continuous[sInf tas, tX] id

Tactic:
have hX := continuous_sInf_dom hX continuous_id
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
⊢ Continuous[sInf tbs, tY] id

Tactic:
have hY := continuous_sInf_dom hY continuous_id
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY_1 : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY_1 : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
@Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX_1 : tX ∈ tas
hY_1 : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
hY : Continuous[sInf tbs, tY] id
h_continuous_id : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map id id)
⊢ Continuous[instTopologicalSpaceProd, tc] fun (p : X × Y) ↦ f p.1 p.2

Tactic:
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
p : X → Prop
x : X
h : ∀ᶠ (x : X) in 𝓝 x, p x
y : Y
⊢ ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x.1

Tactic:
continuousAt_fst h

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, continuousAt_fst