Theorem: Cantor (LeanCourse/MIL/C04_Sets_and_Functions/S02_Functions.lean)

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
⊢ ∀ (f : α → Set α), ¬Surjective f
Tactic:
intro f surjf
State after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
⊢ False
Tactic:
let S := { i | i ∉ f i }
State after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
⊢ False
Tactic:
rcases surjf S with ⟨j, h⟩
State after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False

State before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ False
Tactic:
have h₁ : j ∉ f j := by
  intro h'
  have : j ∉ f j := by rwa [h] at h'
  contradiction
State after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False

State before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ False
Tactic:
have h₂ : j ∈ S
State after:
case h₂
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ j ∈ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False

State before:
case h₂
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
⊢ j ∈ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
sorry
State after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False

State before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ False
Tactic:
have h₃ : j ∉ S
State after:
case h₃
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False

State before:
case h₃
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
⊢ j ∉ S

case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Tactic:
sorry
State after:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False

State before:
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
⊢ j ∉ f j
Tactic:
intro h'
State after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ False
Tactic:
have : j ∉ f j := by rwa [h] at h'
State after:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
this : j ∉ f j
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h' : j ∈ f j
⊢ j ∉ f j
Tactic:
rwa [h] at h'
State after:
no goals