Theorem: dependent_choice'' (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (P : A → Prop) (Q : A → A → Prop) (a : A),
    P a → (∀ (a : A), P a → ∃ b, P b ∧ Q a b) → ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))
Tactic:
intros P Q a pa ex
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))
Tactic:
have h : ∃ (f : ℕ → {x : A // P x}), f 0 = ⟨a, pa⟩
         ∧ ∀ n, P (f n) ∧ Q (f n) (f (n+1)) :=
by
  apply (@dependent_choice' {x : A // P x} (λ p q => P p ∧ Q p q) _)
  intros ap
  match ap with
  | Subtype.mk a' p =>
    simp
    apply And.intro
    . exact p
    . match (ex a' p) with
      | Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))
Tactic:
match h with
| Exists.intro f ⟨zf, sf⟩ =>
  exists (λ n ↦ (f n).val)
  simp; rw [zf]; simp
  intros n; apply sf
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
Tactic:
apply (@dependent_choice' {x : A // P x} (λ p q => P p ∧ Q p q) _)
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∀ (a : { x // P x }), ∃ b, P a.val ∧ Q a.val b.val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∀ (a : { x // P x }), ∃ b, P a.val ∧ Q a.val b.val
Tactic:
intros ap
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
⊢ ∃ b, P ap.val ∧ Q ap.val b.val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
⊢ ∃ b, P ap.val ∧ Q ap.val b.val
Tactic:
match ap with
| Subtype.mk a' p =>
  simp
  apply And.intro
  . exact p
  . match (ex a' p) with
    | Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ b, P { val := a', property := p }.val ∧ Q { val := a', property := p }.val b.val
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ P a' ∧ ∃ x, Q a' x.val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ P a' ∧ ∃ x, Q a' x.val
Tactic:
apply And.intro
State after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ P a'

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ x, Q a' x.val

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ P a'

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ x, Q a' x.val
Tactic:
. exact p
State after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ x, Q a' x.val

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ x, Q a' x.val
Tactic:
. match (ex a' p) with
  | Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
State after:
no goals

State before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ P a'
Tactic:
exact p
State after:
no goals

State before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
⊢ ∃ x, Q a' x.val
Tactic:
match (ex a' p) with
| Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
ap : { x // P x }
a' : A
p : (fun x => P x) a'
b : A
pb : P b
qb : Q a' b
⊢ ∃ x, Q a' x.val
Tactic:
exists (Subtype.mk b pb)
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))
Tactic:
exists (λ n ↦ (f n).val)
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ (fun n => (f n).val) 0 = a ∧
    ∀ (n : ℕ), P ((fun n => (f n).val) n) ∧ Q ((fun n => (f n).val) n) ((fun n => (f n).val) (n + 1))

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ (fun n => (f n).val) 0 = a ∧
    ∀ (n : ℕ), P ((fun n => (f n).val) n) ∧ Q ((fun n => (f n).val) n) ((fun n => (f n).val) (n + 1))
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ (f 0).val = a ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ (f 0).val = a ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
Tactic:
rw [zf]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ { val := a, property := pa }.val = a ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ { val := a, property := pa }.val = a ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
Tactic:
intros n
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
n : ℕ
⊢ P (f n).val ∧ Q (f n).val (f (n + 1)).val

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
f : ℕ → { x // P x }
zf : f 0 = { val := a, property := pa }
sf : ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
n : ℕ
⊢ P (f n).val ∧ Q (f n).val (f (n + 1)).val
Tactic:
apply sf
State after:
no goals