internlm/Lean-Github huggingface dataset:
Theorem: LoVe.FnExp.progress
Proof state before:
e : FnExp
τ : FnType
htp : e ∶ τ
⊢ Value e ∨ ∃ e', e ⇒ e'
Tactic:
induction htp with
| fn => exact Or.inl Value.fn
| arg => exact Or.inl Value.arg
| @appZero f x hf hx ihf ihx =>
  apply Or.inr
  cases ihf with
  | inl hval =>
    cases hval with
    | @fn n =>
      cases hf
      apply Exists.intro x
      apply Step.appZero
    | arg => cases hf
  | inr hstep =>
    cases hstep with | intro f' hf' =>
    apply Exists.intro (app f' x)
    exact Step.appArg hf'      
| @appSucc f x n hf hx ihf ihx =>
  apply Or.inr
  cases ihf with
  | inl hval =>
    cases hf with
    | fn =>
      apply Exists.intro (fn n)
      exact Step.appSucc
    | appSucc => cases hval
  | inr hstep =>
    cases hstep with | intro f' hf' =>
    apply Exists.intro (app f' x)
    exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case fn
e : FnExp
τ : FnType
n✝ : ℕ
⊢ Value (fn n✝) ∨ ∃ e', fn n✝ ⇒ e'
Tactic:
exact Or.inl Value.fn
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case arg
e : FnExp
τ : FnType
⊢ Value arg ∨ ∃ e', arg ⇒ e'
Tactic:
exact Or.inl Value.arg
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ Value (app f x) ∨ ∃ e', app f x ⇒ e'
Tactic:
apply Or.inr
Proof state after:
case appZero.h
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases ihf with
| inl hval =>
  cases hval with
  | @fn n =>
    cases hf
    apply Exists.intro x
    apply Step.appZero
  | arg => cases hf
| inr hstep =>
  cases hstep with | intro f' hf' =>
  apply Exists.intro (app f' x)
  exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inl
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hval with
| @fn n =>
  cases hf
  apply Exists.intro x
  apply Step.appZero
| arg => cases hf
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
n : ℕ
hf : fn n ∶ function 0
⊢ ∃ e', app (fn n) x ⇒ e'
Tactic:
cases hf
Proof state after:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app (fn 0) x ⇒ e'
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app (fn 0) x ⇒ e'
Tactic:
apply Exists.intro x
Proof state after:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ app (fn 0) x ⇒ x
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ app (fn 0) x ⇒ x
Tactic:
apply Step.appZero
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inl.arg
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hf : arg ∶ function 0
⊢ ∃ e', app arg x ⇒ e'
Tactic:
cases hf
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inr
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hstep : ∃ e', f ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hstep with | intro f' hf' =>
apply Exists.intro (app f' x)
exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ ∃ e', app f x ⇒ e'
Tactic:
apply Exists.intro (app f' x)
Proof state after:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Theorem: LoVe.FnExp.progress
Proof state before:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Tactic:
exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ Value (app f x) ∨ ∃ e', app f x ⇒ e'
Tactic:
apply Or.inr
Proof state after:
case appSucc.h
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases ihf with
| inl hval =>
  cases hf with
  | fn =>
    apply Exists.intro (fn n)
    exact Step.appSucc
  | appSucc => cases hval
| inr hstep =>
  cases hstep with | intro f' hf' =>
  apply Exists.intro (app f' x)
  exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inl
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hf with
| fn =>
  apply Exists.intro (fn n)
  exact Step.appSucc
| appSucc => cases hval
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ ∃ e', app (fn (Nat.succ n)) x ⇒ e'
Tactic:
apply Exists.intro (fn n)
Proof state after:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ app (fn (Nat.succ n)) x ⇒ fn n
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ app (fn (Nat.succ n)) x ⇒ fn n
Tactic:
exact Step.appSucc
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inl.appSucc
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f✝ x✝ : FnExp
a✝¹ : x✝ ∶ argument
hval : Value (app f✝ x✝)
a✝ : f✝ ∶ function (Nat.succ (Nat.succ n))
⊢ ∃ e', app (app f✝ x✝) x ⇒ e'
Tactic:
cases hval
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inr
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hstep : ∃ e', f ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hstep with | intro f' hf' =>
apply Exists.intro (app f' x)
exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ ∃ e', app f x ⇒ e'
Tactic:
apply Exists.intro (app f' x)
Proof state after:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Theorem: LoVe.FnExp.progress
Proof state before:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Tactic:
exact Step.appArg hf'
Proof state after:
no goals
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
⊢ ¬∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
Tactic:
intro hneg
Proof state after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
⊢ False
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
⊢ False
Tactic:
have htp : app (app (fn 1) arg) arg ∶ argument :=
  HasType.appZero (HasType.appSucc HasType.fn HasType.arg) HasType.arg
Proof state after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
⊢ False
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
⊢ False
Tactic:
have hexp_step := hneg htp
Proof state after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hexp_step : Value (app (app (fn 1) arg) arg) ∨ ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hexp_step : Value (app (app (fn 1) arg) arg) ∨ ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases hexp_step with
| inl hval =>  cases hval
| inr hstep =>
  cases hstep with | intro e' he' =>
  cases he'
Proof state after:
no goals
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
case inl
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hval : Value (app (app (fn 1) arg) arg)
⊢ False
Tactic:
cases hval
Proof state after:
no goals
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
case inr
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hstep : ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases hstep with | intro e' he' =>
cases he'
Proof state after:
no goals
Theorem: LoVe.FnExp.negation_of_coherence_property
Proof state before:
case inr.intro
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
e' : FnExp
he' : BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases he'
Proof state after:
no goals
Theorem: LoVe.List.elems_mirror_counterexample
Proof state before:
⊢ elems badTree ≠ elems (mirror badTree)
Tactic:
simp [List.elems]
Proof state after:
⊢ ¬elems badTree = elems (mirror badTree)
Theorem: infinitude_of_primes
Proof state before:
⊢ ∀ (N : ℕ), ∃ p, p ≥ N ∧ Nat.Prime p
Tactic:
intro M
Proof state after:
M : ℕ
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Theorem: infinitude_of_primes
Proof state before:
M : ℕ
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
let F := M ! + 1
Proof state after:
M : ℕ
F : ℕ := M ! + 1
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Theorem: infinitude_of_primes
Proof state before:
M : ℕ
F : ℕ := M ! + 1
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
let q := minFac F
Proof state after:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Theorem: infinitude_of_primes
Proof state before:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
use q
Proof state after:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ q ≥ M ∧ Nat.Prime q
Theorem: infinitude_of_primes
Proof state before:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
have qPrime : Nat.Prime q
Proof state after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q

case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Theorem: infinitude_of_primes
Proof state before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q

case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
{ refine' minFac_prime _
  have hn : M ! > 0 := factorial_pos M 
  linarith }
Proof state after:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Theorem: infinitude_of_primes
Proof state before:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
apply And.intro
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M

case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M

case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
{ by_contra hqM
  have h1 : q ∣ M ! + 1 := minFac_dvd F
  have hqM2 : q ≤ M := by linarith
  have hqM3 : q ∣ M ! := Iff.mpr (Prime.dvd_factorial qPrime) hqM2
  have hq1 : q ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
  apply Nat.Prime.not_dvd_one qPrime hq1
}
Proof state after:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Theorem: infinitude_of_primes
Proof state before:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
{ assumption }
Proof state after:
no goals
Theorem: infinitude_of_primes
Proof state before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q
Tactic:
refine' minFac_prime _
Proof state after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ F ≠ 1
Theorem: infinitude_of_primes
Proof state before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ F ≠ 1
Tactic:
have hn : M ! > 0 := factorial_pos M
Proof state after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
hn : M ! > 0
⊢ F ≠ 1
Theorem: infinitude_of_primes
Proof state before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
hn : M ! > 0
⊢ F ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M
Tactic:
by_contra hqM
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
⊢ False
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
⊢ False
Tactic:
have h1 : q ∣ M ! + 1 := minFac_dvd F
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ False
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ False
Tactic:
have hqM2 : q ≤ M := by linarith
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
⊢ False
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
⊢ False
Tactic:
have hqM3 : q ∣ M ! := Iff.mpr (Prime.dvd_factorial qPrime) hqM2
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
⊢ False
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
⊢ False
Tactic:
have hq1 : q ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
Proof state after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
hq1 : q ∣ 1
⊢ False
Theorem: infinitude_of_primes
Proof state before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
hq1 : q ∣ 1
⊢ False
Tactic:
apply Nat.Prime.not_dvd_one qPrime hq1
Proof state after:
no goals
Theorem: infinitude_of_primes
Proof state before:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ q ≤ M
Tactic:
linarith
Proof state after:
no goals
Theorem: infinitude_of_primes
Proof state before:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
assumption
Proof state after:
no goals
Theorem: biggerPrimeIsPrime
Proof state before:
⊢ ∀ (N : ℕ), Nat.Prime (biggerPrime N)
Tactic:
intro M
Proof state after:
M : ℕ
⊢ Nat.Prime (biggerPrime M)
Theorem: biggerPrimeIsPrime
Proof state before:
M : ℕ
⊢ Nat.Prime (biggerPrime M)
Tactic:
refine' minFac_prime _
Proof state after:
M : ℕ
⊢ M ! + 1 ≠ 1
Theorem: biggerPrimeIsPrime
Proof state before:
M : ℕ
⊢ M ! + 1 ≠ 1
Tactic:
have hn : M ! > 0 := factorial_pos M
Proof state after:
M : ℕ
hn : M ! > 0
⊢ M ! + 1 ≠ 1
Theorem: biggerPrimeIsPrime
Proof state before:
M : ℕ
hn : M ! > 0
⊢ M ! + 1 ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: biggerPrimeIsBigger
Proof state before:
⊢ ∀ (N : ℕ), biggerPrime N ≥ N
Tactic:
intro M
Proof state after:
M : ℕ
⊢ biggerPrime M ≥ M
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
⊢ biggerPrime M ≥ M
Tactic:
by_contra hqM
Proof state after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
⊢ False
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
⊢ False
Tactic:
have h1 : (biggerPrime M) ∣ M ! + 1 := minFac_dvd _
Proof state after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ False
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ False
Tactic:
have hqM2 : biggerPrime M ≤ M := by linarith
Proof state after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
⊢ False
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
⊢ False
Tactic:
have hqM3 : biggerPrime M ∣ M ! :=
  Iff.mpr (Prime.dvd_factorial (biggerPrimeIsPrime _)) hqM2
Proof state after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
⊢ False
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
⊢ False
Tactic:
have hq1 : biggerPrime M ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
Proof state after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
hq1 : biggerPrime M ∣ 1
⊢ False
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
hq1 : biggerPrime M ∣ 1
⊢ False
Tactic:
apply Nat.Prime.not_dvd_one (biggerPrimeIsPrime _) hq1
Proof state after:
no goals
Theorem: biggerPrimeIsBigger
Proof state before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ biggerPrime M ≤ M
Tactic:
linarith
Proof state after:
no goals
Theorem: infinitude_of_primes2
Proof state before:
⊢ ∀ (N : ℕ), ∃ p, p ≥ N ∧ Nat.Prime p
Tactic:
intro N
Proof state after:
N : ℕ
⊢ ∃ p, p ≥ N ∧ Nat.Prime p
Theorem: infinitude_of_primes2
Proof state before:
N : ℕ
⊢ ∃ p, p ≥ N ∧ Nat.Prime p
Tactic:
use biggerPrime N
Proof state after:
case h
N : ℕ
⊢ biggerPrime N ≥ N ∧ Nat.Prime (biggerPrime N)
Theorem: infinitude_of_primes2
Proof state before:
case h
N : ℕ
⊢ biggerPrime N ≥ N ∧ Nat.Prime (biggerPrime N)
Tactic:
apply And.intro
Proof state after:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N

case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Theorem: infinitude_of_primes2
Proof state before:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N

case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
{ exact biggerPrimeIsBigger _ }
Proof state after:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Theorem: infinitude_of_primes2
Proof state before:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
{ exact biggerPrimeIsPrime _ }
Proof state after:
no goals
Theorem: infinitude_of_primes2
Proof state before:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N
Tactic:
exact biggerPrimeIsBigger _
Proof state after:
no goals
Theorem: infinitude_of_primes2
Proof state before:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
exact biggerPrimeIsPrime _
Proof state after:
no goals
Theorem: a_silly_theorem
Proof state before:
⊢ True
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Nat.succ_neq_self
Proof state before:
n : ℕ
⊢ Nat.succ n ≠ n
Tactic:
induction n with
| zero       => simp
| succ n' ih => simp [ih]
Proof state after:
no goals
Theorem: LoVe.Nat.succ_neq_self
Proof state before:
case zero

⊢ Nat.succ Nat.zero ≠ Nat.zero
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.Nat.succ_neq_self
Proof state before:
case succ
n' : ℕ
ih : Nat.succ n' ≠ n'
⊢ Nat.succ (Nat.succ n') ≠ Nat.succ n'
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: LoVe.proof_of_False
Proof state before:
hi : immoral 0 = immoral 0 + 1
⊢ immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
Tactic:
rw [←hi]
Proof state after:
no goals
Theorem: LoVe.proof_of_False
Proof state before:
hi : immoral 0 = immoral 0 + 1
him : immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
⊢ 0 = 1
Tactic:
simp at him
Proof state after:
no goals
Theorem: LoVe.proof_of_False
Proof state before:
hi : immoral 0 = immoral 0 + 1
him : immoral 0 - immoral 0 = immoral 0 + 1 - immoral 0
h0eq1 : 0 = 1
⊢ False
Tactic:
simp at h0eq1
Proof state after:
no goals
Theorem: LoVe.shuffle_shuffle_shuffle
Proof state before:
c : RGB
⊢ shuffle (shuffle (shuffle c)) = c
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.head_head
Proof state before:
α : Type
inst✝ : Inhabited α
xs : List α
⊢ head [head xs] = head xs
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.head_head_cases
Proof state before:
α : Type
inst✝ : Inhabited α
xs : List α
⊢ head [head xs] = head xs
Tactic:
cases xs with
| nil        => rfl
| cons x xs' => rfl
Proof state after:
no goals
Theorem: LoVe.head_head_cases
Proof state before:
case nil
α : Type
inst✝ : Inhabited α
⊢ head [head []] = head []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.head_head_cases
Proof state before:
case cons
α : Type
inst✝ : Inhabited α
x : α
xs' : List α
⊢ head [head (x :: xs')] = head (x :: xs')
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.head_head_match
Proof state before:
α : Type
inst✝ : Inhabited α
xs : List α
⊢ head [head []] = head []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.head_head_match
Proof state before:
α : Type
inst✝ : Inhabited α
xs : List α
x : α
xs' : List α
⊢ head [head (x :: xs')] = head (x :: xs')
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.injection_example
Proof state before:
α : Type
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys
Tactic:
cases h
Proof state after:
case refl
α : Type
x : α
xs : List α
⊢ x = x ∧ xs = xs
Theorem: LoVe.injection_example
Proof state before:
case refl
α : Type
x : α
xs : List α
⊢ x = x ∧ xs = xs
Tactic:
simp
Proof state after:
no goals
Theorem: LoVe.distinctness_example
Proof state before:
α : Type
y : α
ys : List α
h : [] = y :: ys
⊢ false = true
Tactic:
cases h
Proof state after:
no goals
Theorem: LoVe.map_ident
Proof state before:
α : Type
xs : List α
⊢ map (fun x => x) xs = xs
Tactic:
induction xs with
| nil           => rfl
| cons x xs' ih => simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.map_ident
Proof state before:
case nil
α : Type
⊢ map (fun x => x) [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.map_ident
Proof state before:
case cons
α : Type
x : α
xs' : List α
ih : map (fun x => x) xs' = xs'
⊢ map (fun x => x) (x :: xs') = x :: xs'
Tactic:
simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.map_comp
Proof state before:
α β γ : Type
f : α → β
g : β → γ
xs : List α
⊢ map g (map f xs) = map (fun x => g (f x)) xs
Tactic:
induction xs with
| nil           => rfl
| cons x xs' ih => simp [map, ih]
Proof state after:
no goals
Theorem: LoVe.map_comp
Proof state before:
case nil
α β γ : Type
f : α → β
g : β → γ
⊢ map g (map f []) = map (fun x => g (f x)) []
Tactic:
rfl
Proof state after:
no goals