internlm/Lean-Github huggingface dataset:
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.step.base.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ trans_clos R a✝¹ c✝
Tactic:
aesop
Proof state after:
no goals
Theorem: refl_sym_is_sym_refl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (sym_clos R)) (sym_clos (refl_clos R))
Tactic:
apply both_inclusions <;> intros x y hyp <;> aesop
Proof state after:
no goals
Theorem: refl_trans_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) (refl_trans_clos R) (refl_trans_clos R')
Tactic:
intros le x y refl
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
refl : refl_trans_clos R x y
⊢ refl_trans_clos R' x y
Theorem: refl_trans_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
refl : refl_trans_clos R x y
⊢ refl_trans_clos R' x y
Tactic:
induction refl <;> aesop
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (trans_clos (sym_clos R))) (trans_clos (sym_clos (refl_clos R)))
Tactic:
apply both_inclusions <;> intros
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
. apply trans_clos_monotone
  . intros
    apply (refl_sym_is_sym_refl _ _ _).1
    trivial
  . apply (refl_trans_is_trans_refl _ _ _).1
    trivial
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
. apply (refl_trans_is_trans_refl _ _ _).2
  apply trans_clos_monotone
  . intros x y red
    apply  (refl_sym_is_sym_refl _ _ _).2
    trivial
  . trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝
Tactic:
apply trans_clos_monotone
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ A → A → Prop
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ A → A → Prop
Tactic:
. intros
  apply (refl_sym_is_sym_refl _ _ _).1
  trivial
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝
Tactic:
. apply (refl_trans_is_trans_refl _ _ _).1
  trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y
Tactic:
intros
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ sym_clos (refl_clos R) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ sym_clos (refl_clos R) x✝ y✝
Tactic:
apply (refl_sym_is_sym_refl _ _ _).1
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ refl_clos (sym_clos R) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝¹ y✝¹ : A
a✝¹ : refl_clos (trans_clos (sym_clos R)) x✝¹ y✝¹
x✝ y✝ : A
a✝ : ?a.R✝ x✝ y✝
⊢ refl_clos (sym_clos R) x✝ y✝
Tactic:
trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝
Tactic:
apply (refl_trans_is_trans_refl _ _ _).1
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝
Tactic:
apply (refl_trans_is_trans_refl _ _ _).2
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (refl_clos (sym_clos R)) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (refl_clos (sym_clos R)) x✝ y✝
Tactic:
apply trans_clos_monotone
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ A → A → Prop
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ A → A → Prop
Tactic:
. intros x y red
  apply  (refl_sym_is_sym_refl _ _ _).2
  trivial
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝
Tactic:
. trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → refl_clos (sym_clos R) x y
Tactic:
intros x y red
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ refl_clos (sym_clos R) x y
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ refl_clos (sym_clos R) x y
Tactic:
apply  (refl_sym_is_sym_refl _ _ _).2
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ sym_clos (refl_clos R) x y
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
x y : A
red : ?a.R✝ x y
⊢ sym_clos (refl_clos R) x y
Tactic:
trivial
Proof state after:
no goals
Theorem: refl_trans_sym_is_trans_sym_refl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ trans_clos (fun x y => sym_clos (refl_clos R) x y) x✝ y✝
Tactic:
trivial
Proof state after:
no goals
Theorem: trans_is_refl_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ trans_clos R x y → refl_trans_clos R x y
Tactic:
intros red
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : trans_clos R x y
⊢ refl_trans_clos R x y
Theorem: trans_is_refl_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : trans_clos R x y
⊢ refl_trans_clos R x y
Tactic:
induction red <;> aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_or_eq
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ refl_trans_clos R x y → x = y ∨ trans_clos R x y
Tactic:
intros red
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : refl_trans_clos R x y
⊢ x = y ∨ trans_clos R x y
Theorem: refl_trans_is_trans_or_eq
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : refl_trans_clos R x y
⊢ x = y ∨ trans_clos R x y
Tactic:
induction red <;> aesop
Proof state after:
no goals
Theorem: refl_trans_step_is_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
⊢ R x z → refl_trans_clos R z y → trans_clos R x y
Tactic:
intros red_x_z red_z_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_z : R x z
red_z_y : refl_trans_clos R z y
⊢ trans_clos R x y
Theorem: refl_trans_step_is_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_z : R x z
red_z_y : refl_trans_clos R z y
⊢ trans_clos R x y
Tactic:
revert red_x_z x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
z y : A
red_z_y : refl_trans_clos R z y
⊢ ∀ {x : A}, R x z → trans_clos R x y
Theorem: refl_trans_step_is_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
z y : A
red_z_y : refl_trans_clos R z y
⊢ ∀ {x : A}, R x z → trans_clos R x y
Tactic:
induction red_z_y <;> aesop
Proof state after:
no goals
Theorem: sym_inv
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) ((fun R x y => R y x) R) (sym_clos R)
Tactic:
aesop
Proof state after:
no goals
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ normal R x → normalizes R x
Tactic:
simp [normal]
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ (∀ (x_1 : A), ¬R x x_1) → normalizes R x
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ (∀ (x_1 : A), ¬R x x_1) → normalizes R x
Tactic:
intros norm_x div_x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False
Tactic:
match div_x with
  | Exists.intro xs (And.intro zero_case incr_case) =>
  apply norm_x (xs 1)
  rw [←zero_case]
  apply incr_case
Proof state after:
no goals
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ False
Tactic:
apply norm_x (xs 1)
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R x (xs 1)
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R x (xs 1)
Tactic:
rw [←zero_case]
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R (xs 0) (xs 1)
Theorem: normal_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R (xs 0) (xs 1)
Tactic:
apply incr_case
Proof state after:
no goals
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ normal R x → refl_trans_clos R x y → x = y
Tactic:
intros norm red
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
red : refl_trans_clos R x y
⊢ x = y
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
red : refl_trans_clos R x y
⊢ x = y
Tactic:
cases red
Proof state after:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm : normal R x
⊢ x = x

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y
Theorem: normal_red
Proof state before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm : normal R x
⊢ x = x

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y
Tactic:
trivial
Proof state after:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
⊢ x = y✝
Tactic:
case step y _ _ =>
by_contra
apply norm; exists y
Proof state after:
no goals
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
⊢ x = y✝
Tactic:
by_contra
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ False
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ False
Tactic:
apply norm
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ ∃ x', R x x'
Theorem: normal_red
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ ∃ x', R x x'
Tactic:
exists y
Proof state after:
no goals
Theorem: exists_iff
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (T : Sort u_1) (P Q : T → Prop), (∀ (t : T), Q t ↔ P t) → (∃ t, P t) → ∃ t, Q t
Tactic:
intros T P Q equiv ex_t
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
⊢ ∃ t, Q t
Theorem: exists_iff
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
⊢ ∃ t, Q t
Tactic:
match ex_t with
 | Exists.intro w h =>
   exists w
   simp [equiv]
   exact h
Proof state after:
no goals
Theorem: exists_iff
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ ∃ t, Q t
Tactic:
exists w
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ Q w
Theorem: exists_iff
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ Q w
Tactic:
simp [equiv]
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ P w
Theorem: exists_iff
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ P w
Tactic:
exact h
Proof state after:
no goals
Theorem: iterate_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ {A : Sort u_1} (f : A → A) (n : ℕ) (x : A), f^[n + 1] x = f (f^[n] x)
Tactic:
intros A f n
Proof state after:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
⊢ ∀ (x : A), f^[n + 1] x = f (f^[n] x)
Theorem: iterate_left
Proof state before:
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
⊢ ∀ (x : A), f^[n + 1] x = f (f^[n] x)
Tactic:
induction' n with n ihn
Proof state after:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)

case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Theorem: iterate_left
Proof state before:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)

case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
. simp [Nat.iterate]
Proof state after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Theorem: iterate_left
Proof state before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
. simp [Nat.add, Nat.iterate]
  intros x
  apply ihn
Proof state after:
no goals
Theorem: iterate_left
Proof state before:
case zero
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
⊢ ∀ (x : A), f^[Nat.zero + 1] x = f (f^[Nat.zero] x)
Tactic:
simp [Nat.iterate]
Proof state after:
no goals
Theorem: iterate_left
Proof state before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[Nat.succ n + 1] x = f (f^[Nat.succ n] x)
Tactic:
simp [Nat.add, Nat.iterate]
Proof state after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[n] (f (f x)) = f (f^[n] (f x))
Theorem: iterate_left
Proof state before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
⊢ ∀ (x : A), f^[n] (f (f x)) = f (f^[n] (f x))
Tactic:
intros x
Proof state after:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
x : A
⊢ f^[n] (f (f x)) = f (f^[n] (f x))
Theorem: iterate_left
Proof state before:
case succ
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
f : A → A
n : ℕ
ihn : ∀ (x : A), f^[n + 1] x = f (f^[n] x)
x : A
⊢ f^[n] (f (f x)) = f (f^[n] (f x))
Tactic:
apply ihn
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), (∀ (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
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
⊢ ∃ f, f 0 = a ∧ ∀ (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
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
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, f 0 = a ∧ ∀ (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
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
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
⊢ ∃ f, ∀ (x : A), Q x (f x)
Tactic:
apply Classical.axiomOfChoice
Proof 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