internlm/Lean-Github huggingface dataset:
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
⊢ False
Tactic:
have h_3lel : 3 ≤ l := by
  sorry
Proof state after:
case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
h_3lel : 3 ≤ l
⊢ False
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
h_3lel : 3 ≤ l
⊢ False
Tactic:
have h₄ : n < k^3 := by
  sorry
Proof state after:
case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
h_3lel : 3 ≤ l
h₄ : n < k ^ 3
⊢ False
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
h_3lel : 3 ≤ l
h₄ : n < k ^ 3
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
⊢ 3 ≤ l
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
h_3lel : 3 ≤ l
⊢ n < k ^ 3
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inl
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h_2k : n ≥ 2 * k
⊢ n.choose k ≠ m ^ l
Tactic:
exact h_wlog k h_4lek h_klen4 h_2k
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : ¬n ≥ 2 * k
⊢ n.choose k ≠ m ^ l
Tactic:
simp only [not_le] at h
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
⊢ n.choose k ≠ m ^ l
Tactic:
have h_klen : k ≤ n := le_trans h_klen4 (Nat.sub_le n 4)
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l
Tactic:
rw [← choose_symm h_klen]
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
let k' := n - k
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_k'_def : k' = n - k := by rfl
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_2k'len : 2 * k' ≤ n := by
  sorry
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_k'len4 : k' ≤ n - 4 := by
  simp [h_k'_def]
  have help : k + k ≤ n - 4 + k := add_le_add_right h_klen4 k
  rw [← (two_mul k)] at help
  exact le_trans (le_of_lt h) help
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_4lek' : 4 ≤ k' := by
  have h_4len : 4 ≤ n := le_trans (le_trans h_4lek h_klen4) (Nat.sub_le n 4)
  exact Iff.mp (le_tsub_iff_le_tsub h_klen h_4len) h_klen4
Proof state after:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4lek' : 4 ≤ k'
⊢ n.choose (n - k) ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4lek' : 4 ≤ k'
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
exact h_wlog k' h_4lek' h_k'len4 h_2k'len
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
⊢ k' = n - k
Tactic:
rfl
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ 2 * k' ≤ n
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ k' ≤ n - 4
Tactic:
simp [h_k'_def]
Proof state after:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n ≤ n - 4 + k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n ≤ n - 4 + k
Tactic:
have help : k + k ≤ n - 4 + k := add_le_add_right h_klen4 k
Proof state after:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : k + k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : k + k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Tactic:
rw [← (two_mul k)] at help
Proof state after:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : 2 * k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : 2 * k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Tactic:
exact le_trans (le_of_lt h) help
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ 4 ≤ k'
Tactic:
have h_4len : 4 ≤ n := le_trans (le_trans h_4lek h_klen4) (Nat.sub_le n 4)
Proof state after:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4len : 4 ≤ n
⊢ 4 ≤ k'
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4len : 4 ≤ n
⊢ 4 ≤ k'
Tactic:
exact Iff.mp (le_tsub_iff_le_tsub h_klen h_4len) h_klen4
Proof state after:
no goals
Theorem: chapter07.Theorem₁
Proof state before:
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
h : A.IsHermitian
⊢ ∃ Q ∈ orthogonalGroup (Fin n) ℝ, ∃ d, diagonal d = Q.conjTranspose * A * Q
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter07.Theorem₂
Proof state before:
n : ℕ
⊢ ∃ M, (∀ (i j : Fin n), M i j = -1 ∨ M i j = 1) ∧ ↑M.det > (↑n.factorial).sqrt
Tactic:
sorry
Proof state after:
no goals
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
let n := 1 + ∏ q in S, q
Proof state after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
⊢ ∃ p, p.Prime ∧ p ∉ S
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
let p := n.minFac
Proof state after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∃ p, p.Prime ∧ p ∉ S
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
use p
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime ∧ p ∉ S
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime ∧ p ∉ S
Tactic:
have hp : Nat.Prime p := by
  have hn : 0 < ∏ q in S, q := by
    refine' Finset.prod_pos _
    intros q hq
    refine' Prime.pos <| h hq
  exact Nat.minFac_prime <| Nat.ne_of_gt <| lt_add_of_pos_right 1 hn
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p.Prime ∧ p ∉ S
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p.Prime ∧ p ∉ S
Tactic:
refine' ⟨hp, _⟩
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p ∉ S
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p ∉ S
Tactic:
by_contra a
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
⊢ False
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
⊢ False
Tactic:
have h_p_div_prod : p ∣ ∏ q in S, q := dvd_prod_of_mem (fun (i : ℕ) => i) a
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
⊢ False
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
⊢ False
Tactic:
have h_p_div_diff : p ∣ n - ∏ q in S, q := dvd_sub' (minFac_dvd n) h_p_div_prod
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ False
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ False
Tactic:
have h_p_div_one : p ∣ 1 := by aesop
Proof state after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
h_p_div_one : p ∣ 1
⊢ False
Theorem: infinity_of_primes₁
Proof state before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
h_p_div_one : p ∣ 1
⊢ False
Tactic:
exact Nat.Prime.not_dvd_one hp h_p_div_one
Proof state after:
no goals
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime
Tactic:
have hn : 0 < ∏ q in S, q := by
  refine' Finset.prod_pos _
  intros q hq
  refine' Prime.pos <| h hq
Proof state after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hn : 0 < ∏ q ∈ S, q
⊢ p.Prime
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hn : 0 < ∏ q ∈ S, q
⊢ p.Prime
Tactic:
exact Nat.minFac_prime <| Nat.ne_of_gt <| lt_add_of_pos_right 1 hn
Proof state after:
no goals
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ 0 < ∏ q ∈ S, q
Tactic:
refine' Finset.prod_pos _
Proof state after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∀ i ∈ S, 0 < i
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∀ i ∈ S, 0 < i
Tactic:
intros q hq
Proof state after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
q : ℕ
hq : q ∈ S
⊢ 0 < q
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
q : ℕ
hq : q ∈ S
⊢ 0 < q
Tactic:
refine' Prime.pos <| h hq
Proof state after:
no goals
Theorem: infinity_of_primes₁
Proof state before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ p ∣ 1
Tactic:
aesop
Proof state after:
no goals
Theorem: F₀
Proof state before:
⊢ F 0 = 3
Tactic:
rw [F]
Proof state after:
⊢ 2 ^ 2 ^ 0 + 1 = 3
Theorem: F₀
Proof state before:
⊢ 2 ^ 2 ^ 0 + 1 = 3
Tactic:
simp only [Nat.pow_zero, pow_one]
Proof state after:
no goals
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
⊢ F n < F n.succ
Tactic:
have : NeZero 1 := by infer_instance
Proof state after:
n : ℕ
this : NeZero 1
⊢ F n < F n.succ
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
this : NeZero 1
⊢ F n < F n.succ
Tactic:
rw [F, F]
Proof state after:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n.succ + 1
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n + 1 < 2 ^ 2 ^ n.succ + 1
Tactic:
simp only [add_lt_add_iff_right, Nat.pow_succ]
Proof state after:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n < 2 ^ (2 ^ n * 2)
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
this : NeZero 1
⊢ 2 ^ 2 ^ n < 2 ^ (2 ^ n * 2)
Tactic:
refine' (pow_lt_pow_iff_right one_lt_two).mpr _
Proof state after:
n : ℕ
this : NeZero 1
⊢ 2 ^ n < 2 ^ n * 2
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
this : NeZero 1
⊢ 2 ^ n < 2 ^ n * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: fermat_stricly_monotone
Proof state before:
n : ℕ
⊢ NeZero 1
Tactic:
infer_instance
Proof state after:
no goals
Theorem: fermat_bounded
Proof state before:
n : ℕ
⊢ 2 < F n
Tactic:
induction' n with n h
Proof state after:
case zero

⊢ 2 < F 0

case succ
n : ℕ
h : 2 < F n
⊢ 2 < F (n + 1)
Theorem: fermat_bounded
Proof state before:
case zero

⊢ 2 < F 0
Tactic:
rw [F₀]
Proof state after:
case zero

⊢ 2 < 3
Theorem: fermat_bounded
Proof state before:
case zero

⊢ 2 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: fermat_bounded
Proof state before:
case succ
n : ℕ
h : 2 < F n
⊢ 2 < F (n + 1)
Tactic:
exact lt_trans h fermat_stricly_monotone
Proof state after:
no goals
Theorem: fermat_odd
Proof state before:
n : ℕ
⊢ Odd (F n)
Tactic:
rw [F, odd_iff_not_even, even_add_one, not_not, even_pow]
Proof state after:
n : ℕ
⊢ Even 2 ∧ 2 ^ n ≠ 0
Theorem: fermat_odd
Proof state before:
n : ℕ
⊢ Even 2 ∧ 2 ^ n ≠ 0
Tactic:
refine' ⟨even_two, Nat.ne_of_gt (pow_pos _ _)⟩
Proof state after:
n : ℕ
⊢ 0 < 2
Theorem: fermat_odd
Proof state before:
n : ℕ
⊢ 0 < 2
Tactic:
exact zero_lt_two
Proof state after:
no goals
Theorem: fermat_product
Proof state before:
n : ℕ
⊢ ∏ k ∈ range n, F k = F n - 2
Tactic:
induction' n with n hn
Proof state after:
case zero

⊢ ∏ k ∈ range 0, F k = F 0 - 2

case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ ∏ k ∈ range (n + 1), F k = F (n + 1) - 2
Theorem: fermat_product
Proof state before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ ∏ k ∈ range (n + 1), F k = F (n + 1) - 2
Tactic:
rw [prod_range_succ, hn]
Proof state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (F n - 2) * F n = F (n + 1) - 2
Theorem: fermat_product
Proof state before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (F n - 2) * F n = F (n + 1) - 2
Tactic:
unfold F
Proof state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n + 1 - 2) * (2 ^ 2 ^ n + 1) = 2 ^ 2 ^ (n + 1) + 1 - 2
Theorem: fermat_product
Proof state before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n + 1 - 2) * (2 ^ 2 ^ n + 1) = 2 ^ 2 ^ (n + 1) + 1 - 2
Tactic:
rw [mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by aesop),  ← Nat.sq_sub_sq]
Proof state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
Theorem: fermat_product
Proof state before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
Tactic:
ring_nf
Proof state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2
Theorem: fermat_product
Proof state before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2
Tactic:
omega
Proof state after:
no goals
Theorem: fermat_product
Proof state before:
case zero

⊢ ∏ k ∈ range 0, F k = F 0 - 2
Tactic:
trivial
Proof state after:
no goals
Theorem: fermat_product
Proof state before:
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1
Tactic:
aesop
Proof state after:
no goals
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
⊢ (F n).Coprime (F k)
Tactic:
let m := (F n).gcd (F k)
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
⊢ (F n).Coprime (F k)
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
⊢ (F n).Coprime (F k)
Tactic:
have h_n : m ∣ F n := (F n).gcd_dvd_left (F k)
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
⊢ (F n).Coprime (F k)
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
⊢ (F n).Coprime (F k)
Tactic:
have h_k : m ∣ F k := (F n).gcd_dvd_right (F k)
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ (F n).Coprime (F k)
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ (F n).Coprime (F k)
Tactic:
have h_m : m ∣ 2 :=  by
  have h_m_prod : m ∣ (∏ k in range n, F k) :=
    dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
  have h_prod : (∏ k in range n, F k) + 2 = F n := by
    rw [fermat_product, Nat.sub_add_cancel]
    refine' le_of_lt _
    simp [fermat_bounded]
  refine' (Nat.dvd_add_right h_m_prod).mp _
  rw [h_prod]
  exact h_n
Proof state after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
⊢ (F n).Coprime (F k)
Theorem: infinity_of_primes₂
Proof state before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
⊢ (F n).Coprime (F k)
Tactic:
cases' (dvd_prime prime_two).mp h_m with h_one h_two
Proof state after:
case inl
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_one : m = 1
⊢ (F n).Coprime (F k)

case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
⊢ (F n).Coprime (F k)