mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1

pp: case h.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst✝³] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V

Tactic:
·

Goal state after:
case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst✝³] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V

Tactic:
·

Goal state after:
case h.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst✝³] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, K_1 ∈ 𝓝 x ∧ MapsTo (⇑f) K_1 V
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ 𝓝 ↑x

pp: case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f) (Subtype.val '' (K U) n) V

Tactic:
·

Goal state after:
case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ 𝓝 ↑x
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f) (Subtype.val '' (K U) n) V

Tactic:
·

Goal state after:
case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f) (Subtype.val '' (K U) n) V
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
    match x with
    | (x₁, x₂) => g (f₂ x₂, f₁ x₁)

pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g

Tactic:
·

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
    match x with
    | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace

pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace ≤ t

Tactic:
·

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace ≤ t

Tactic:
·

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace ≤ t
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g

Tactic:
·

Goal state after:
case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ s, ⨅ (_ : IsOpen[inst✝] s), ⨅ (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Tactic:
by
  simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ some '' Metric.eball a r
⊢ x ∈ Metric.eball (some a) r

pp: case mpr
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ Metric.eball (some a) r
⊢ x ∈ some '' Metric.eball a r

Tactic:
·

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ some '' Metric.eball a r
⊢ x ∈ Metric.eball (some a) r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case refine_1
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ IsOpen[inst✝] (some '' s')

pp: case refine_2
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ Subtype.val ⁻¹' some '' s' = Subtype.val ⁻¹' Metric.eball (some x) r

Tactic:
·

Goal state after:
case refine_1
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝ : Option α
r : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
s's : Subtype.val ⁻¹' s' = Subtype.val ⁻¹' Metric.eball x r
⊢ IsOpen[inst✝] (some '' s')
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case none.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
xy : edist none none = 0
⊢ none = none

pp: case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝

pp: case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

pp: case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝

Tactic:
·

Goal state after:
case none.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
xy : edist none none = 0
⊢ none = none
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝

pp: case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

pp: case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝

Tactic:
·

Goal state after:
case none.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist none (some val✝) = 0
⊢ none = some val✝
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none

pp: case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝¹ = some val✝

Tactic:
·

Goal state after:
case some.none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝ : α
xy : edist (some val✝) none = 0
⊢ some val✝ = none
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top.top
⊢ ¬edist ∞ ∞ = ∞

pp: case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞

pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
·

Goal state after:
case top.top
⊢ ¬edist ∞ ∞ = ∞
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞

pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
·

Goal state after:
case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
·

Goal state after:
case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
·

Goal state after:
case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
        x

pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ?map_zero_left,
                    map_one_left := ?map_one_left }.toFun
                (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x

Tactic:
·

Goal state after:
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
        x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ?map_one_left }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x

Tactic:
·

Goal state after:
case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x

Tactic:
·

Goal state after:
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
        x

pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ?map_zero_left,
                    map_one_left := ?map_one_left }.toFun
                (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x

Tactic:
·

Goal state after:
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
        x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ?map_one_left }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x

Tactic:
·

Goal state after:
case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x