-- Mathlib/Topology/Separation/NotNormal.lean
theorem IsClosed.mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s)
    [DiscreteTopology s] : #s < 𝔠

Proof state:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ False

Tactic:
refine (Cardinal.cantor 𝔠).not_le ?_

Result:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ #C(↑s, ℝ)

Tactic:
rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum,
  lift_uzero]

Result:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠 ^ #↑s

Proof state:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠

Tactic:
calc
  2 ^ 𝔠 ≤ #C(s, ℝ) := by
    rw [(ContinuousMap.equivFnOfDiscrete _ _).cardinal_eq, mk_arrow, mk_real, lift_continuum,
      lift_uzero]
    exact (power_le_power_left two_ne_zero h).trans (power_le_power_right (nat_lt_continuum 2).le)
  _ ≤ #C(X, ℝ) := by
    choose f hf using ContinuousMap.exists_restrict_eq (Y := ℝ) hs
    have hfi : Injective f := LeftInverse.injective hf
    exact mk_le_of_injective hfi
  _ ≤ #C(t, ℝ) := mk_le_of_injective <| ContinuousMap.injective_restrict htd
  _ ≤ #(t → ℝ) := mk_le_of_injective DFunLike.coe_injective
  _ ≤ 𝔠 := by
    rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]
    exact power_le_power_left two_ne_zero mk_le_aleph0

Result:
no goals

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
⊢ #↑s < 𝔠

Tactic:
by_contra! h

Result:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
⊢ False

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (f_1 : C(↑s, ℝ)), ContinuousMap.restrict s (f f_1) = f_1
hfi : Injective f
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)

Tactic:
exact mk_le_of_injective hfi

Result:
no goals

Proof state:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
⊢ False

Tactic:
haveI := htc.to_subtype

Result:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ False

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)

Tactic:
choose f hf using ContinuousMap.exists_restrict_eq (Y := ℝ) hs

Result:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (f_1 : C(↑s, ℝ)), ContinuousMap.restrict s (f f_1) = f_1
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ (ℵ₀ * #↑t) ≤ 2 ^ ℵ₀

Tactic:
exact power_le_power_left two_ne_zero mk_le_aleph0

Result:
no goals

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (f_1 : C(↑s, ℝ)), ContinuousMap.restrict s (f f_1) = f_1
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)

Tactic:
have hfi : Injective f := LeftInverse.injective hf

Result:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
f : C(↑s, ℝ) → C(X, ℝ)
hf : ∀ (f_1 : C(↑s, ℝ)), ContinuousMap.restrict s (f f_1) = f_1
hfi : Injective f
⊢ #C(↑s, ℝ) ≤ #C(X, ℝ)

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ #(↑t → ℝ) ≤ 𝔠

Tactic:
rw [mk_arrow, mk_real, lift_uzero, lift_continuum, continuum, ← power_mul]

Result:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ (ℵ₀ * #↑t) ≤ 2 ^ ℵ₀

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
this : Countable ↑t
⊢ 2 ^ 𝔠 ≤ 𝔠 ^ #↑s

Tactic:
exact (power_le_power_left two_ne_zero h).trans (power_le_power_right (nat_lt_continuum 2).le)

Result:
no goals

Proof state:
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
⊢ False

Tactic:
rcases exists_countable_dense X with ⟨t, htc, htd⟩

Result:
case intro.intro
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : SeparableSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
h : 𝔠 ≤ #↑s
t : Set X
htc : t.Countable
htd : Dense t
⊢ False