Theorem: HTPI.Lemma_8_2_2_2 (HTPILib/Chap8Part2.lean)

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)
State after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
apply Exists.intro f
State after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∀ A ∈ F, fcnl_onto_from_nat (f A) A

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
fix A : Set U
State after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
A : Set U
⊢ A ∈ F → fcnl_onto_from_nat (f A) A

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
A : Set U
⊢ A ∈ F → fcnl_onto_from_nat (f A) A
Tactic:
show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)
State after:
no goals

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
⊢ ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
fix A : Set U
State after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

State before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
by_cases h2 : A ∈ F
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
have h3 : ctble A := h A h2
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ctble A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ctble A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
rewrite [Theorem_8_1_5_2] at h3
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
apply Exists.intro SA
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ A ∈ F → fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ A ∈ F → fcnl_onto_from_nat SA A
Tactic:
assume h5 : A ∈ F
State after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
h5 : A ∈ F
⊢ fcnl_onto_from_nat SA A

State before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
h5 : A ∈ F
⊢ fcnl_onto_from_nat SA A
Tactic:
show fcnl_onto_from_nat SA A from h4
State after:
no goals

State before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
apply Exists.intro (emptyRel Nat U)
State after:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ A ∈ F → fcnl_onto_from_nat (emptyRel ℕ U) A

State before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ A ∈ F → fcnl_onto_from_nat (emptyRel ℕ U) A
Tactic:
assume h3 : A ∈ F
State after:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
h3 : A ∈ F
⊢ fcnl_onto_from_nat (emptyRel ℕ U) A

State before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
h3 : A ∈ F
⊢ fcnl_onto_from_nat (emptyRel ℕ U) A
Tactic:
show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2
State after:
no goals