awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set X), f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
s : Set Y
hs : IsClosed[inst_1] s
grw : f ⁻¹' closure[inst_1] (f '' f ⁻¹' s) ⊆ f ⁻¹' s
grw₁ : f ⁻¹' closure[inst_1] s ⊆ f ⁻¹' s
grw₂ grw₃ : f ⁻¹' s ⊆ f ⁻¹' s
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' s

Tactic:
grw [image_subset_iff.mp <| h <| f ⁻¹' s, image_preimage_subset, hs.closure_subset]

Premises used: IsClosed.closure_subset, Set.image_preimage_subset, Iff.mp, Set.image_subset_iff
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
t : Set Y
hf : Continuous[inst, inst_1] f
hx : x ∈ closure[inst] s
ht : MapsTo f s t
⊢ f x ∈ closure[inst_1] t

Tactic:
ht.closure hf hx

Premises used: Set.MapsTo.closure
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst, inst_1] f
ht : IsClosed[inst_1] t
⊢ MapsTo f (closure[inst] s) t

Tactic:
ht.closure_eq ▸ h.closure hc

Premises used: Set.MapsTo.closure, IsClosed.closure_eq, Eq.rec
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
⊢ ∀ a ∈ closure[inst] (f ⁻¹' s), f a ∈ closure[inst_1] s

Tactic:
(mapsTo_preimage _ _).closure hf

Premises used: Set.MapsTo.closure, Set.mapsTo_preimage, Set.MapsTo
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        x ∈ closure[inst] (f ⁻¹' s) → Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ f a ∈ closure[inst_1] s) x} x}
      a
h₂ : ∀ a ∈ closure[inst] (f ⁻¹' s), f a ∈ closure[inst_1] s
⊢ ∀ᶠ (a : X) in l.lift' closure[inst], f a ∈ closure[inst_1] s

Tactic:
filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

Premises used: Set.MapsTo.closure, Filter.mem_lift', Set.mapsTo_preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
x : X
⊢ Tendsto f ((𝓝 x).lift' closure[inst]) ((𝓝 (f x)).lift' closure[inst_1])

Tactic:
(hf.tendsto x).lift'_closure hf

Premises used: Continuous.tendsto, Filter.Tendsto.lift'_closure
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
hf : Surjective f
x : X
⊢ x ∈ closure[inst] (range f)

Tactic:
simp [hf.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ DenseRange.{u_1, u_1} (X := X) id

Tactic:
Function.Surjective.denseRange Function.surjective_id

Premises used: Function.Surjective.denseRange, Function.surjective_id
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
⊢ DenseRange f ↔ closure[inst] (range f) = univ

Tactic:
dense_iff_closure_eq

Premises used: dense_iff_closure_eq, DenseRange
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
h : DenseRange f
⊢ closure[inst] (range f) = univ

Tactic:
h.closure_eq

Premises used: Dense.closure_eq
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
p : X → Prop
⊢ DenseRange.{u_1, u_1} (X := X) (α := Subtype p) (Subtype.val (p := p)) ↔ Dense.{u_1} (X := X) {x : X | p x}

Tactic:
simp [DenseRange]

Premises used: DenseRange
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : Dense s
⊢ DenseRange.{u_1, u_1} (X := X) (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
denseRange_subtype_val.2 h

Premises used: Iff.mpr, denseRange_subtype_val
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst, inst_1] f
hs : Dense s
rw : f '' closure[inst] s ⊆ closure[inst_1] (f '' s)
⊢ range f ⊆ closure[inst_1] (f '' s)

Tactic:
rw [← image_univ, ← hs.closure_eq]

Premises used: Set.image_univ, Dense.closure_eq
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst, inst_1] f
hs : Dense s
⊢ f '' closure[inst] s ⊆ closure[inst_1] (f '' s)

Tactic:
image_closure_subset_closure_image hf

Premises used: image_closure_subset_closure_image
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst, inst_1] f
hs : Dense s
⊢ f '' closure[inst] s ⊆ closure[inst_1] (f '' s)

Tactic:
exact image_closure_subset_closure_image hf

Premises used: image_closure_subset_closure_image
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf' : DenseRange f
hf : Continuous[inst, inst_1] f
hs : Dense s
⊢ Dense (f '' s)

Tactic:
(hf'.mono <| hf.range_subset_closure_image_dense hs).of_closure

Premises used: Continuous.range_subset_closure_image_dense, Dense.of_closure, Dense.mono
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst] s
rw : s ⊆ closure[inst] (s ∩ range f)
⊢ s ⊆ closure[inst] (f '' f ⁻¹' s)

Tactic:
rw [image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst] s
⊢ s ⊆ closure[inst] (s ∩ range f)

Tactic:
hf.open_subset_closure_inter hs

Premises used: Dense.open_subset_closure_inter
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst] s
⊢ s ⊆ closure[inst] (s ∩ range f)

Tactic:
exact hf.open_subset_closure_inter hs

Premises used: Dense.open_subset_closure_inter
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf' : DenseRange f
hf : Continuous[inst, inst_1] f
hs : Dense s
t : Set Y
ht : MapsTo f s t
⊢ Dense t

Tactic:
(hf'.dense_image hf hs).mono ht.image_subset

Premises used: Dense.mono, DenseRange.dense_image, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.Continuous
Goal:
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst, inst_1] g
rw : Dense (g '' range f)
⊢ DenseRange (g ∘ f)

Tactic:
rw [DenseRange, range_comp]

Premises used: Set.range_comp, DenseRange
-- Module: Mathlib.Topology.Continuous
Goal:
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst, inst_1] g
⊢ Dense (g '' range f)

Tactic:
hg.dense_image cg hf

Premises used: DenseRange.dense_image
-- Module: Mathlib.Topology.Continuous
Goal:
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst, inst_1] g
⊢ Dense (g '' range f)

Tactic:
exact hg.dense_image cg hf

Premises used: DenseRange.dense_image
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
hf : DenseRange f
⊢ Nonempty α ↔ Nonempty X

Tactic:
range_nonempty_iff_nonempty.symm.trans hf.nonempty_iff

Premises used: Set.range_nonempty_iff_nonempty, Dense.nonempty_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
h : Nonempty X
hf : DenseRange f
⊢ Nonempty α

Tactic:
hf.nonempty_iff.mpr h

Premises used: Iff.mpr, DenseRange.nonempty_iff
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
ho : IsOpen[inst] s
hs : s.Nonempty
⊢ ∃ (a : α), f a ∈ s

Tactic:
exists_range_iff.1 <| hf.exists_mem_open ho hs

Premises used: Set.exists_range_iff, Iff.mp, Dense.exists_mem_open
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
α : Type u_4
f : α → X
s : Set X
h : DenseRange f
hs : s ∈ 𝓝 x
⊢ ∃ (a : α), f a ∈ s

Tactic:
let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨x, mem_interior_iff_mem_nhds.2 hs⟩
  ⟨a, interior_subset ha⟩

Premises used: _private.0.DenseRange.mem_nhds.match_1, Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, Membership.mem, Exists, Exists.intro, DenseRange.exists_mem_open
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Mul β
inst_3 : ContinuousMul β
f g : C(α, β)
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Mul β
inst_3 : ContinuousMul β
f g : C(α, β)
x : α
⊢ (f * g : (a : α) → β) x = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Mul γ
inst_4 : ContinuousMul γ
f₁ f₂ : C(β, γ)
g : C(α, β)
⊢ (f₁ * f₂).comp g = f₁.comp g * f₂.comp g

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : One β
⊢ Eq (α := (a : α) → β) (⇑1 : (a : α) → β) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : One β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((1 : (a : α) → β) x : β) (1 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : One γ
g : C(α, β)
⊢ Eq (α := C(α, γ)) (comp 1 g) 1

Tactic:
rfl

Premises used: ContinuousMap.comp, ContinuousMap.const, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : One β
g : C(β, γ)
⊢ Eq (α := C(α, γ)) (g.comp 1) (const α ((g : (a : β) → γ) 1))

Tactic:
rfl

Premises used: ContinuousMap.comp, ContinuousMap.const, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : One β
⊢ Eq (α := C(α, β)) (const α 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NatCast β
n : ℕ
⊢ Eq (α := (a : α) → β) (⇑(↑n : C(α, β)) : (a : α) → β) (↑n : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NatCast β
n : ℕ
x : α
⊢ Eq.{u_2 + 1} (α := β) (((↑n : C(α, β)) : (a : α) → β) x : β) ((↑n : β) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : IntCast β
n : ℤ
⊢ Eq (α := (a : α) → β) (⇑(↑n : C(α, β)) : (a : α) → β) (↑n : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : IntCast β
n : ℤ
x : α
⊢ Eq.{u_2 + 1} (α := β) (((↑n : C(α, β)) : (a : α) → β) x : β) ((↑n : β) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Monoid β
inst_3 : ContinuousMul β
f : C(α, β)
n : ℕ
⊢ (⇑(f ^ n) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Monoid β
inst_3 : ContinuousMul β
f : C(α, β)
n : ℕ
x : α
⊢ (f ^ n : (a : α) → β) x = HPow.hPow (α := β) ((f : (a : α) → β) x : β) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Monoid γ
inst_4 : ContinuousMul γ
f : C(β, γ)
n : ℕ
g : C(α, β)
⊢ (f ^ n).comp g = f.comp g ^ n

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Inv β
inst_3 : ContinuousInv β
f : C(α, β)
⊢ Eq (α := (a : α) → β) (⇑f⁻¹ : (a : α) → β) (⇑f : (a : α) → β)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Inv β
inst_3 : ContinuousInv β
f : C(α, β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f⁻¹ : (a : α) → β) x : β) (((f : (a : α) → β) x)⁻¹ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Inv γ
inst_4 : ContinuousInv γ
f : C(β, γ)
g : C(α, β)
⊢ f⁻¹.comp g = (f.comp g)⁻¹

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Div β
inst_3 : ContinuousDiv β
f g : C(α, β)
⊢ (⇑(f / g) : (a : α) → β) = HDiv.hDiv (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Div β
inst_3 : ContinuousDiv β
f g : C(α, β)
x : α
⊢ (f / g : (a : α) → β) x = HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Div γ
inst_4 : ContinuousDiv γ
f g : C(β, γ)
h : C(α, β)
⊢ (f / g).comp h = f.comp h / g.comp h

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group β
inst_3 : IsTopologicalGroup β
f : C(α, β)
z : ℤ
⊢ (⇑(f ^ z) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group β
inst_3 : IsTopologicalGroup β
f : C(α, β)
z : ℤ
x : α
⊢ (f ^ z : (a : α) → β) x = HPow.hPow (α := β) ((f : (a : α) → β) x : β) z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Group γ
inst_4 : IsTopologicalGroup γ
f : C(β, γ)
z : ℤ
g : C(α, β)
⊢ (f ^ z).comp g = f.comp g ^ z

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2

Tactic:
continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
refine :
  Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
    (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2

Tactic:
refine continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
⊢ Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2

Tactic:
have h1 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.fst x.snd :=
      continuous_eval.comp (continuous_fst.prodMap continuous_id)
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
h1 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2
⊢ Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.2 : (a : α) → β) x.2

Tactic:
have h2 : Continuous fun x : (C(α, β) × C(α, β)) × α => x.fst.snd x.snd :=
      continuous_eval.comp (continuous_snd.prodMap continuous_id)
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
h1 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2
h2 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.2 : (a : α) → β) x.2
⊢ Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
    (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)

Tactic:
h1.mul h2

Premises used: Continuous.mul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LocallyCompactSpace α
inst_3 : Mul β
inst_4 : ContinuousMul β
h1 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.1 : (a : α) → β) x.2
h2 : Continuous (Y := β) fun (x : (C(α, β) × C(α, β)) × α) ↦ (x.1.2 : (a : α) → β) x.2
⊢ Continuous (X := (C(α, β) × C(α, β)) × α) (Y := β)
    (Function.uncurry fun (x : C(α, β) × C(α, β)) (y : α) ↦ (x.1 * x.2 : (a : α) → β) y)

Tactic:
exact h1.mul h2

Premises used: Continuous.mul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommMonoid β
inst_3 : ContinuousMul β
ι : Type u_3
s : Finset ι
f : ι → C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(∏ i ∈ s, f i) : (a : α) → β) (∏ i ∈ s, (⇑(f i) : (a : α) → β))

Tactic:
map_prod coeFnMonoidHom f s

Premises used: ContinuousMap.coeFnMonoidHom, map_prod
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommMonoid β
inst_3 : ContinuousMul β
ι : Type u_3
s : Finset ι
f : ι → C(α, β)
a : α
⊢ Eq.{u_2 + 1} (α := β) ((∏ i ∈ s, f i : (a : α) → β) a : β) (∏ i ∈ s, (f i : (a : α) → β) a : β)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
⊢ IsUniformGroup β

Tactic:
have : IsUniformGroup β := isUniformGroup_of_commGroup
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
rw : ∀ (x : C(α, β) × C(α, β)), ContinuousAt (Y := C(α, β)) (fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2) x
⊢ Continuous (Y := C(α, β)) fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
rw :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β) × C(α, β)) (a : α) ↦ (i.1 * i.2 : (a : α) → β) a)
        (⇑((f, g).1 * (f, g).2) : (a : α) → β) (nhds f ×ˢ nhds g) K
⊢ ContinuousAt (Y := C(α, β)) (fun (p : C(α, β) × C(α, β)) ↦ p.1 * p.2) (f, g)

Tactic:
rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_prod_eq]

Premises used: ContinuousAt, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_prod_eq
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
⊢ ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β) × C(α, β)) (a : α) ↦ (i.1 * i.2 : (a : α) → β) a)
        (⇑((f, g).1 * (f, g).2) : (a : α) → β) (nhds f ×ˢ nhds g) K

Tactic:
fun K hK =>
      uniformContinuous_mul.comp_tendstoUniformlyOn
        ((tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK).prodMk
          (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK))

Premises used: uniformContinuous_mul, Set.Mem, Filter.tendsto_id, setOf, UniformContinuous.comp_tendstoUniformlyOn, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, TendstoUniformlyOn.prodMk, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f g : C(α, β)
⊢ ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β) × C(α, β)) (a : α) ↦ (i.1 * i.2 : (a : α) → β) a)
        (⇑((f, g).1 * (f, g).2) : (a : α) → β) (nhds f ×ˢ nhds g) K

Tactic:
exact fun K hK =>
      uniformContinuous_mul.comp_tendstoUniformlyOn
        ((tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK).prodMk
          (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK))

Premises used: uniformContinuous_mul, Filter.tendsto_id, UniformContinuous.comp_tendstoUniformlyOn, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, TendstoUniformlyOn.prodMk, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
rw : ∀ (x : C(α, β)), ContinuousAt (Y := C(α, β)) (fun (a : C(α, β)) ↦ a⁻¹) x
⊢ Continuous (Y := C(α, β)) fun (a : C(α, β)) ↦ a⁻¹

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt