Theorem: uncountable_minus_countably_infinite_uncountable (meetings/ex5.lean)

State before:
α : Type
A B : Set α
hsub : A ⊆ B
hcntiA : Countably_Infinite A
hucnt : Uncountable B
⊢ Uncountable (B \ A)
Tactic:
rcases hcntiA with ⟨hcntA, _⟩
State after:
case intro
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Uncountable (B \ A)

State before:
case intro
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Uncountable (B \ A)
Tactic:
constructor
State after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ ¬Set.Countable (B \ A)

case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Set.Infinite (B \ A)

State before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ ¬Set.Countable (B \ A)
Tactic:
intro hcntmin
State after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
⊢ False

State before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
⊢ False
Tactic:
have hcntB := Set.Countable.union hcntA hcntmin
State after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False

State before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Tactic:
rw [Set.union_diff_cancel hsub] at hcntB
State after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False

State before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Tactic:
exact hucnt.1 hcntB
State after:
no goals

State before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Set.Infinite (B \ A)
Tactic:
intro hfin
State after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
⊢ False

State before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
⊢ False
Tactic:
have hcnt := Set.Finite.countable hfin
State after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
⊢ False

State before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
⊢ False
Tactic:
have hcntB := Set.Countable.union hcntA hcnt
State after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False

State before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Tactic:
rw [Set.union_diff_cancel hsub] at hcntB
State after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False

State before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Tactic:
exact hucnt.1 hcntB
State after:
no goals