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), Inhabited A → (∀ (a : A), ∃ b, Q a b) → ∃ f, ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
intros A Q inhab forall_exists_Q
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∃ f, ∀ (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
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ ∃ f, ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
have a : A := by match inhab with | Inhabited.mk a => exact a
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
⊢ ∃ f, ∀ (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
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
⊢ ∃ f, ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
have h := dependent_choice' _ a forall_exists_Q
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
h : ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
⊢ ∃ f, ∀ (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
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
h : ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
⊢ ∃ f, ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
match h with
| Exists.intro f h' =>
  exists f
  apply h'.2
State after:
no goals

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
⊢ A
Tactic:
match inhab with | Inhabited.mk a => exact a
State after:
no goals

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

State before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
h : ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
f : ℕ → A
h' : (fun f => f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))) f
⊢ ∃ f, ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
exists f
State after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
h : ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
f : ℕ → A
h' : (fun f => f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))) f
⊢ ∀ (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
inhab : Inhabited A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
a : A
h : ∃ f, f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))
f : ℕ → A
h' : (fun f => f 0 = a ∧ ∀ (n : ℕ), Q (f n) (f (n + 1))) f
⊢ ∀ (n : ℕ), Q (f n) (f (n + 1))
Tactic:
apply h'.2
State after:
no goals