internlm/Lean-Github huggingface dataset:
Theorem: dependent_choice'
Proof 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
Proof state after:
no goals
Theorem: dependent_choice'
Proof 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)
Proof 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))
Theorem: dependent_choice'
Proof 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
Proof 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))
Theorem: dependent_choice'
Proof 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]
Proof 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))
Theorem: dependent_choice'
Proof 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
Proof state after:
no goals
Theorem: dependent_choice'
Proof 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]
Proof state after:
no goals
Theorem: dependent_choice'
Proof 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
Proof 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))
Theorem: dependent_choice'
Proof 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
Proof 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)
Theorem: dependent_choice'
Proof 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]
Proof 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))
Theorem: dependent_choice'
Proof 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
Proof state after:
no goals
Theorem: dependent_choice
Proof 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
Proof 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))
Theorem: dependent_choice
Proof 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
Proof 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))
Theorem: dependent_choice
Proof 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
Proof 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))
Theorem: dependent_choice
Proof 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
Proof state after:
no goals
Theorem: dependent_choice
Proof 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
Proof state after:
no goals
Theorem: dependent_choice
Proof 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
Proof state after:
no goals
Theorem: dependent_choice
Proof 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
Proof 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))
Theorem: dependent_choice
Proof 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
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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
Proof 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))
Theorem: dependent_choice''
Proof 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)
Proof 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))
Theorem: dependent_choice''
Proof 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
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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) _)
Proof 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
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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)
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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)
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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)
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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)
Proof state after:
no goals
Theorem: dependent_choice''
Proof 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)
Proof 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))
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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]
Proof 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
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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
Proof 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
Theorem: dependent_choice''
Proof 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
Proof state after:
no goals
Theorem: normalizes_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), normalizes R x → P x
Tactic:
intros P IH x norm
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
⊢ P x
Theorem: normalizes_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
⊢ P x
Tactic:
apply Classical.byContradiction
Proof state after:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
⊢ ¬P x → False
Theorem: normalizes_ind
Proof state before:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
⊢ ¬P x → False
Tactic:
intro h
Proof state after:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ False
Theorem: normalizes_ind
Proof state before:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ False
Tactic:
apply norm
Proof state after:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ diverge_from R x
Theorem: normalizes_ind
Proof state before:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ diverge_from R x
Tactic:
have h' : ∃ f : ℕ → A, f 0 = x ∧ ∀ n, ¬ P (f n) ∧ f n ~> f (n+1) :=
by
  apply (dependent_choice''  (λ a ↦ ¬ P a))
  . exact h
  . intros a npa
    apply Classical.byContradiction
    simp; intros p
    apply npa
    apply IH; intros y ry
    apply Classical.byContradiction; intros npy
    apply (p y npy ry)
Proof state after:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ diverge_from R x
Theorem: normalizes_ind
Proof state before:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ diverge_from R x
Tactic:
rw [diverge_from]
Proof state after:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))