Theorem: dependent_choice' (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ {A : Sort u_1} (Q : A → A → Prop) (a : A), (∀ (a : A), ∃ b, Q a b) → ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
intros A Q a forall_exists_Q
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
have choice_aut : ∃ f : A → A, ∀ x, Q x (f x) :=
by
  apply Classical.axiomOfChoice
  exact forall_exists_Q
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
match choice_aut with
 | Exists.intro f h =>
     exists (λ n ↦ f^[n] a)
     apply And.intro
     . simp [Nat.iterate]
     . intros n
       simp
       rw [iterate_left]
       apply h
State after:
no goals

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∃ f, ∀ (x : A), Q x (f x)
Tactic:
apply Classical.axiomOfChoice
State after:
case h
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∀ (x : A), ∃ y, Q x y

State before:
case h
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∀ (x : A), ∃ y, Q x y
Tactic:
exact forall_exists_Q
State after:
no goals

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
exists (λ n ↦ f^[n] a)
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a ∧ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a ∧ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
Tactic:
apply And.intro
State after:
case left
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a

case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))

State before:
case left
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a

case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
Tactic:
. simp [Nat.iterate]
State after:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))

State before:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
Tactic:
. intros n
  simp
  rw [iterate_left]
  apply h
State after:
no goals

State before:
case left
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a
Tactic:
simp [Nat.iterate]
State after:
no goals

State before:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
Tactic:
intros n
State after:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))

State before:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
Tactic:
simp
State after:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q (f^[n] a) (f^[n + 1] a)

State before:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q (f^[n] a) (f^[n + 1] a)
Tactic:
rw [iterate_left]
State after:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q (f^[n] a) (f (f^[n] a))

State before:
case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
n : ℕ
⊢ Q (f^[n] a) (f (f^[n] a))
Tactic:
apply h
State after:
no goals