internlm/Lean-Github huggingface dataset:
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fderiv ℂ (fun x => bottcher d (↑x)⁻¹) 0 ≠ 0
Tactic:
rw [bottcher_hasDerivAt_one.hasFDerivAt.fderiv]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
rw [Ne, ContinuousLinearMap.ext_iff, not_forall]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ x, ¬(ContinuousLinearMap.smulRight 1 1) x = 0 x
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ x, ¬(ContinuousLinearMap.smulRight 1 1) x = 0 x
Tactic:
use 1
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬(ContinuousLinearMap.smulRight 1 1) 1 = 0 1
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬(ContinuousLinearMap.smulRight 1 1) 1 = 0 1
Tactic:
simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  Algebra.id.smul_eq_mul, mul_one, ContinuousLinearMap.zero_apply]
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬1 = 0 1
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬1 = 0 1
Tactic:
convert one_ne_zero
Proof state after:
case h.convert_4
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ NeZero 1
Theorem: bottcher_mfderiv_inf_ne_zero
Proof state before:
case h.convert_4
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ NeZero 1
Tactic:
exact NeZero.one
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof state before:
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ Nonseparating (univ ×ˢ t)
Tactic:
have e : ((univ : Set X) ×ˢ t)ᶜ = univ ×ˢ tᶜ := by
  apply Set.ext; intro ⟨a, x⟩; rw [mem_compl_iff]
  simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff]
Proof state after:
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Nonseparating (univ ×ˢ t)
Theorem: Nonseparating.univ_prod
Proof state before:
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Nonseparating (univ ×ˢ t)
Tactic:
constructor
Proof state after:
case dense
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Dense (univ ×ˢ t)ᶜ

case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ ∀ (x : X × Y) (u : Set (X × Y)),
    x ∈ univ ×ˢ t → u ∈ 𝓝 x → ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] x ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ ∀ (x : X × Y), x ∈ (univ ×ˢ t)ᶜ ↔ x ∈ univ ×ˢ tᶜ
Theorem: Nonseparating.univ_prod
Proof state before:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
⊢ ∀ (x : X × Y), x ∈ (univ ×ˢ t)ᶜ ↔ x ∈ univ ×ˢ tᶜ
Tactic:
intro ⟨a, x⟩
Proof state after:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∈ (univ ×ˢ t)ᶜ ↔ (a, x) ∈ univ ×ˢ tᶜ
Theorem: Nonseparating.univ_prod
Proof state before:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∈ (univ ×ˢ t)ᶜ ↔ (a, x) ∈ univ ×ˢ tᶜ
Tactic:
rw [mem_compl_iff]
Proof state after:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∉ univ ×ˢ t ↔ (a, x) ∈ univ ×ˢ tᶜ
Theorem: Nonseparating.univ_prod
Proof state before:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
a : X
x : Y
⊢ (a, x) ∉ univ ×ˢ t ↔ (a, x) ∈ univ ×ˢ tᶜ
Tactic:
simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff]
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof state before:
case dense
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Dense (univ ×ˢ t)ᶜ
Tactic:
rw [e]
Proof state after:
case dense
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Dense (univ ×ˢ tᶜ)
Theorem: Nonseparating.univ_prod
Proof state before:
case dense
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ Dense (univ ×ˢ tᶜ)
Tactic:
exact dense_univ.prod n.dense
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof state before:
case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
⊢ ∀ (x : X × Y) (u : Set (X × Y)),
    x ∈ univ ×ˢ t → u ∈ 𝓝 x → ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] x ∧ IsPreconnected c
Tactic:
intro ⟨a, x⟩ u m un
Proof state after:
case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
m : (a, x) ∈ univ ×ˢ t
un : u ∈ 𝓝 (a, x)
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
m : (a, x) ∈ univ ×ˢ t
un : u ∈ 𝓝 (a, x)
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
simp only [mem_prod_eq, mem_univ, true_and_iff] at m
Proof state after:
case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
case loc
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases mem_nhds_prod_iff.mp un with ⟨u0, n0, u1, n1, uu⟩
Proof state after:
case loc.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
case loc.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases n.loc x u1 m n1 with ⟨c1, cs1, cn1, cp1⟩
Proof state after:
case loc.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
case loc.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
rcases locallyConnectedSpace_iff_open_connected_subsets.mp (by infer_instance) a u0 n0 with
  ⟨c0, cs0, co0, cm0, cc0⟩
Proof state after:
case loc.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Theorem: Nonseparating.univ_prod
Proof state before:
case loc.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ ∃ c ⊆ u \ univ ×ˢ t, c ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected c
Tactic:
use c0 ×ˢ c1
Proof state after:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ⊆ u \ univ ×ˢ t ∧ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected (c0 ×ˢ c1)
Theorem: Nonseparating.univ_prod
Proof state before:
case h
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ⊆ u \ univ ×ˢ t ∧ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x) ∧ IsPreconnected (c0 ×ˢ c1)
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ⊆ u \ univ ×ˢ t

case h.refine_2
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x)

case h.refine_3
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ IsPreconnected (c0 ×ˢ c1)
Theorem: Nonseparating.univ_prod
Proof state before:
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
⊢ LocallyConnectedSpace X
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ⊆ u \ univ ×ˢ t
Tactic:
intro ⟨b, y⟩ m'
Proof state after:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : (b, y) ∈ c0 ×ˢ c1
⊢ (b, y) ∈ u \ univ ×ˢ t
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : (b, y) ∈ c0 ×ˢ c1
⊢ (b, y) ∈ u \ univ ×ˢ t
Tactic:
simp only [mem_prod_eq, mem_diff, mem_univ, true_and_iff] at m' ⊢
Proof state after:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u ∧ y ∉ t
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u ∧ y ∉ t
Tactic:
refine ⟨?_, (cs1 m'.2).2⟩
Proof state after:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_1
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u
Tactic:
apply uu
Proof state after:
case h.refine_1.a
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u0 ×ˢ u1
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_1.a
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
b : X
y : Y
m' : b ∈ c0 ∧ y ∈ c1
⊢ (b, y) ∈ u0 ×ˢ u1
Tactic:
use cs0 m'.1, (cs1 m'.2).1
Proof state after:
no goals
Theorem: Nonseparating.univ_prod
Proof state before:
case h.refine_2
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ∈ 𝓝[(univ ×ˢ t)ᶜ] (a, x)
Tactic:
rw [e, nhdsWithin_prod_eq, nhdsWithin_univ]
Proof state after:
case h.refine_2
X : Type
inst✝⁵ : TopologicalSpace X
Y : Type
inst✝⁴ : TopologicalSpace Y
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
inst✝ : LocallyConnectedSpace X
t : Set Y
n : Nonseparating t
e : (univ ×ˢ t)ᶜ = univ ×ˢ tᶜ
a : X
x : Y
u : Set (X × Y)
un : u ∈ 𝓝 (a, x)
m : x ∈ t
u0 : Set X
n0 : u0 ∈ 𝓝 a
u1 : Set Y
n1 : u1 ∈ 𝓝 x
uu : u0 ×ˢ u1 ⊆ u
c1 : Set Y
cs1 : c1 ⊆ u1 \ t
cn1 : c1 ∈ 𝓝[tᶜ] x
cp1 : IsPreconnected c1
c0 : Set X
cs0 : c0 ⊆ u0
co0 : IsOpen c0
cm0 : a ∈ c0
cc0 : IsConnected c0
⊢ c0 ×ˢ c1 ∈ 𝓝 a ×ˢ 𝓝[tᶜ] x