internlm/Lean-Github huggingface dataset:
Theorem: divides_of_cong_four
Proof state before:
case refine_1
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1

case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
{ use 3380*t^2 + 416*t + 13
  ring }
Proof state after:
case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Theorem: divides_of_cong_four
Proof state before:
case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
{ use 1300*t^2 + 160*t + 5
  ring }
Proof state after:
no goals
Theorem: divides_of_cong_four
Proof state before:
case refine_1
t : ℕ
⊢ 5 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 3380*t^2 + 416*t + 13
Proof state after:
case refine_1
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)
Theorem: divides_of_cong_four
Proof state before:
case refine_1
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 5 * (3380 * t ^ 2 + 416 * t + 13)
Tactic:
ring
Proof state after:
no goals
Theorem: divides_of_cong_four
Proof state before:
case refine_2
t : ℕ
⊢ 13 ∣ 4 * (65 * t + 4) ^ 2 + 1
Tactic:
use 1300*t^2 + 160*t + 5
Proof state after:
case refine_2
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)
Theorem: divides_of_cong_four
Proof state before:
case refine_2
t : ℕ
⊢ 4 * (65 * t + 4) ^ 2 + 1 = 13 * (1300 * t ^ 2 + 160 * t + 5)
Tactic:
ring
Proof state after:
no goals
Theorem: arb_large_soln
Proof state before:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
intro N
Proof state after:
N : ℕ
⊢ ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Theorem: arb_large_soln
Proof state before:
N : ℕ
⊢ ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
use 65 * N + 4
Proof state after:
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Theorem: arb_large_soln
Proof state before:
N : ℕ
⊢ 65 * N + 4 > N ∧ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N

case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Theorem: arb_large_soln
Proof state before:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N

case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
{ linarith }
Proof state after:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Theorem: arb_large_soln
Proof state before:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
{ apply divides_of_cong_four }
Proof state after:
no goals
Theorem: arb_large_soln
Proof state before:
case refine_1
N : ℕ
⊢ 65 * N + 4 > N
Tactic:
linarith
Proof state after:
no goals
Theorem: arb_large_soln
Proof state before:
case refine_2
N : ℕ
⊢ 5 ∣ 4 * (65 * N + 4) ^ 2 + 1 ∧ 13 ∣ 4 * (65 * N + 4) ^ 2 + 1
Tactic:
apply divides_of_cong_four
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
refine ⟨?_, ?_⟩
Proof state after:
case refine_1
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S

case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S

case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Tactic:
{ intro h
  have h2 := Set.Infinite.exists_nat_lt h
  intro n
  rcases h2 n with ⟨m, hm, h3⟩
  use m
  exact ⟨h3, hm⟩
}
Proof state after:
case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Tactic:
{ contrapose! 
  intro h
  rw [Set.not_infinite] at h
  let S2 : Finset ℕ := Set.Finite.toFinset h
  have h2 : ∃ B, ∀n ∈ S2, n ≤ B
  { use Finset.sup S2 id
    intro n hn
    apply Finset.le_sup hn }
  cases' h2 with N hN
  use N
  have h3 : ∀n : ℕ, n ∈ S ↔ n ∈ S2 := by
    intro n
    exact (Set.Finite.mem_toFinset h).symm
  intros n hn h4
  rw [h3] at h4
  specialize hN n h4
  linarith
}
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
intro h
Proof state after:
case refine_1
S : Set ℕ
h : Set.Infinite S
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1
S : Set ℕ
h : Set.Infinite S
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
have h2 := Set.Infinite.exists_nat_lt h
Proof state after:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
intro n
Proof state after:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n : ℕ
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n : ℕ
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Tactic:
rcases h2 n with ⟨m, hm, h3⟩
Proof state after:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Tactic:
use m
Proof state after:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ m > n ∧ m ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ m > n ∧ m ∈ S
Tactic:
exact ⟨h3, hm⟩
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Tactic:
contrapose!
Proof state after:
case refine_2
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
intro h
Proof state after:
case refine_2
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
rw [Set.not_infinite] at h
Proof state after:
case refine_2
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
let S2 : Finset ℕ := Set.Finite.toFinset h
Proof state after:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
have h2 : ∃ B, ∀n ∈ S2, n ≤ B
Proof state after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B

case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B

case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
{ use Finset.sup S2 id
  intro n hn
  apply Finset.le_sup hn }
Proof state after:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
cases' h2 with N hN
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
use N
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
have h3 : ∀n : ℕ, n ∈ S ↔ n ∈ S2 := by
  intro n
  exact (Set.Finite.mem_toFinset h).symm
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
intros n hn h4
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False
Tactic:
rw [h3] at h4
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False
Tactic:
specialize hN n h4
Proof state after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False
Theorem: infinite_iff_arb_large
Proof state before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
Tactic:
use Finset.sup S2 id
Proof state after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ (n : ℕ), n ∈ S2 → n ≤ Finset.sup S2 id
Theorem: infinite_iff_arb_large
Proof state before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ (n : ℕ), n ∈ S2 → n ≤ Finset.sup S2 id
Tactic:
intro n hn
Proof state after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n : ℕ
hn : n ∈ S2
⊢ n ≤ Finset.sup S2 id
Theorem: infinite_iff_arb_large
Proof state before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n : ℕ
hn : n ∈ S2
⊢ n ≤ Finset.sup S2 id
Tactic:
apply Finset.le_sup hn
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
Tactic:
intro n
Proof state after:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2
Theorem: infinite_iff_arb_large
Proof state before:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2
Tactic:
exact (Set.Finite.mem_toFinset h).symm
Proof state after:
no goals
Theorem: infinite_set_of_solutions
Proof state before:
⊢ Set.Infinite { n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1 }
Tactic:
rw [infinite_iff_arb_large]
Proof state after:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ { n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1 }
Theorem: infinite_set_of_solutions
Proof state before:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ { n | 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1 }
Tactic:
exact arb_large_soln
Proof state after:
no goals
Theorem: MyGroup.mul_eq_of_eq_inv_mul
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_one
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_inv_self
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b c a : G
⊢ a * a⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.inv_mul_cancel_left
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a⁻¹ * (a * b) = b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_inv_cancel_left
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a * (a⁻¹ * b) = b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.left_inv_eq_right_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a✝ b✝ c✝ a b c : G
h1 : b * a = 1
h2 : a * c = 1
⊢ b = c
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.one_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ 1⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.inv_inv
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ a⁻¹⁻¹ = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_inv_rev
Proof state before:
G : Type
inst✝ : MyGroup G
a b c : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.add_zero
Proof state before:
n : MyNat
⊢ n + 0 = n
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_succ
Proof state before:
n m : MyNat
⊢ n + succ m = succ (n + m)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.easy
Proof state before:
⊢ two + two = four
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.easy2
Proof state before:
⊢ two + one = one + two
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
n : MyNat
⊢ 0 + n = n
Tactic:
induction' n with d hd
Proof state after:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
{ rfl }
Proof state after:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Theorem: MyNat.zero_add
Proof state before:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
{ rw [add_succ] rw [hd] }
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ 0 + 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
rw [add_succ]
Proof state after:
case succ
d : MyNat
hd : 0 + d = d
⊢ succ (0 + d) = succ d
Theorem: MyNat.zero_add
Proof state before:
case succ
d : MyNat
hd : 0 + d = d
⊢ succ (0 + d) = succ d
Tactic:
rw [hd]
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
a b : MyNat
⊢ succ a + b = succ (a + b)
Tactic:
induction' b with d hd
Proof state after:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)

case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Theorem: MyNat.succ_add
Proof state before:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)

case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
{ rfl }
Proof state after:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Theorem: MyNat.succ_add
Proof state before:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
{ rw [add_succ, add_succ, hd] }
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Tactic:
rw [add_succ, add_succ, hd]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
a b : MyNat
⊢ a + b = b + a
Tactic:
induction' b with d hd
Proof state after:
case zero
a : MyNat
⊢ a + 0 = 0 + a

case succ
a d : MyNat
hd : a + d = d + a
⊢ a + succ d = succ d + a
Theorem: MyNat.add_comm
Proof state before:
case zero
a : MyNat
⊢ a + 0 = 0 + a
Tactic:
rw [add_zero]
Proof state after:
case zero
a : MyNat
⊢ a = 0 + a
Theorem: MyNat.add_comm
Proof state before:
case zero
a : MyNat
⊢ a = 0 + a
Tactic:
rw [zero_add]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case succ
a d : MyNat
hd : a + d = d + a
⊢ a + succ d = succ d + a
Tactic:
rw [add_succ]
Proof state after:
case succ
a d : MyNat
hd : a + d = d + a
⊢ succ (a + d) = succ d + a
Theorem: MyNat.add_comm
Proof state before:
case succ
a d : MyNat
hd : a + d = d + a
⊢ succ (a + d) = succ d + a
Tactic:
rw [hd]
Proof state after:
case succ
a d : MyNat
hd : a + d = d + a
⊢ succ (d + a) = succ d + a
Theorem: MyNat.add_comm
Proof state before:
case succ
a d : MyNat
hd : a + d = d + a
⊢ succ (d + a) = succ d + a
Tactic:
rw [succ_add]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
a b c : MyNat
⊢ a + b + c = a + (b + c)
Tactic:
induction' c with d hd
Proof state after:
case zero
a b : MyNat
⊢ a + b + 0 = a + (b + 0)

case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ a + b + succ d = a + (b + succ d)
Theorem: MyNat.add_assoc
Proof state before:
case zero
a b : MyNat
⊢ a + b + 0 = a + (b + 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ a + b + succ d = a + (b + succ d)
Tactic:
rw [add_succ, hd]
Proof state after:
case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ succ (a + (b + d)) = a + (b + succ d)
Theorem: MyNat.add_assoc
Proof state before:
case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ succ (a + (b + d)) = a + (b + succ d)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_add_add
Proof state before:
a b c d : MyNat
⊢ a + b + (c + d) = a + c + (b + d)
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.is_zero_zero_eq_True
Proof state before:
⊢ is_zero 0 = True
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.is_zero_succ_eq_False
Proof state before:
n : MyNat
⊢ is_zero (succ n) = False
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.zero_ne_one
Proof state before:
⊢ 0 ≠ 1
Tactic:
intro h
Proof state after:
h : 0 = 1
⊢ False
Theorem: MyNat.zero_ne_one
Proof state before:
h : 0 = 1
⊢ False
Tactic:
rw [← is_zero_one_eq_False]
Proof state after:
h : 0 = 1
⊢ is_zero 1
Theorem: MyNat.zero_ne_one
Proof state before:
h : 0 = 1
⊢ is_zero 1
Tactic:
rw [← h]
Proof state after:
h : 0 = 1
⊢ is_zero 0
Theorem: MyNat.zero_ne_one
Proof state before:
h : 0 = 1
⊢ is_zero 0
Tactic:
rw [is_zero_zero_eq_True]
Proof state after:
h : 0 = 1
⊢ True
Theorem: MyNat.zero_ne_one
Proof state before:
h : 0 = 1
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: MyNat.pred_succ
Proof state before:
a : MyNat
⊢ pred (succ a) = a
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_inj
Proof state before:
a b : MyNat
h : succ a = succ b
⊢ a = b
Tactic:
suffices h : pred (succ a) = pred (succ b) by
{ rw [pred_succ, pred_succ] at h
  exact h }
Proof state after:
a b : MyNat
h : succ a = succ b
⊢ pred (succ a) = pred (succ b)
Theorem: MyNat.succ_inj
Proof state before:
a b : MyNat
h : succ a = succ b
⊢ pred (succ a) = pred (succ b)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MyNat.succ_inj
Proof state before:
a b : MyNat
h✝ : succ a = succ b
h : pred (succ a) = pred (succ b)
⊢ a = b
Tactic:
rw [pred_succ, pred_succ] at h
Proof state after:
a b : MyNat
h✝ : succ a = succ b
h : a = b
⊢ a = b
Theorem: MyNat.succ_inj
Proof state before:
a b : MyNat
h✝ : succ a = succ b
h : a = b
⊢ a = b
Tactic:
exact h
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
a : MyNat
⊢ 0 * a = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.succ_eq_add_one
Proof state before:
a : MyNat
⊢ succ a = a + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_one
Proof state before:
a : MyNat
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.one_mul
Proof state before:
a : MyNat
⊢ one * a = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b : MyNat
⊢ succ a * b = a * b + b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
t a b : MyNat
⊢ t * (a + b) = t * a + t * b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
a b c : MyNat
⊢ a * b * c = a * (b * c)
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.add_mul
Proof state before:
a b t : MyNat
⊢ (a + b) * t = a * t + b * t
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
a b : MyNat
⊢ a * b = b * a
Tactic:
sorry
Proof state after:
no goals
Theorem: sixteen_pow_sixtyfour_mod_nineteen
Proof state before:
⊢ 16 ^ 64 = 16
Tactic:
rfl
Proof state after:
no goals
Theorem: arb_large_soln
Proof state before:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: infinite_iff_arb_large
Proof state before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
a : MyNat
⊢ 0 + a = a
Tactic:
induction' a using MyNat.induction with d hd
Proof state after:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ 0 + 0 = 0
Tactic:
rw [add_zero]
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
rw [add_succ, hd]
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
a b : MyNat
⊢ succ a + b = succ (a + b)
Tactic:
induction' b using MyNat.induction with d hd
Proof state after:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)

case succ
a d : MyNat
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)
Theorem: MyNat.succ_add
Proof state before:
case zero
a : MyNat
⊢ succ a + 0 = succ (a + 0)
Tactic:
rw [add_zero, add_zero]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
a b : MyNat
⊢ a + b = b + a
Tactic:
induction' b using MyNat.induction with d hd
Proof state after:
case zero
a : MyNat
⊢ a + 0 = 0 + a

case succ
a d : MyNat
hd : a + d = d + a
⊢ a + succ d = succ d + a
Theorem: MyNat.add_comm
Proof state before:
case zero
a : MyNat
⊢ a + 0 = 0 + a
Tactic:
rw [add_zero, zero_add]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case succ
a d : MyNat
hd : a + d = d + a
⊢ a + succ d = succ d + a
Tactic:
rw [add_succ, succ_add, hd]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
a b c : MyNat
⊢ a + b + c = a + (b + c)
Tactic:
induction' c using MyNat.induction with d hd
Proof state after:
case zero
a b : MyNat
⊢ a + b + 0 = a + (b + 0)

case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ a + b + succ d = a + (b + succ d)
Theorem: MyNat.add_assoc
Proof state before:
case zero
a b : MyNat
⊢ a + b + 0 = a + (b + 0)
Tactic:
rw [add_zero, add_zero]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ a + b + succ d = a + (b + succ d)
Tactic:
rw [add_succ, add_succ, add_succ, hd]
Proof state after:
no goals