awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
pos : ∀ (h₁ : a₁ < b), pair a₁ b < pair a₂ b
⊢ pair a₁ b < pair a₂ b
have neg : ∀ (h₁ : ¬a₁ < b), pair a₁ b < pair a₂ b
Tactic: by_cases h₁ : a₁ < b
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ pair a₁ b < pair a₂ b
have pos : b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Tactic: simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b
have neg : a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Tactic: simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
have pos : ∀ (h₂ : a₂ < b), b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Tactic: by_cases h₂ : a₂ < b
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
pos : ∀ (h₂ : a₂ < b), b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
have neg : ∀ (h₂ : ¬a₂ < b), b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Tactic: by_cases h₂ : a₂ < b
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
have neg : b * b + a₁ < a₂ * a₂ + (a₂ + b)
Tactic: simp only [h₂, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
have neg : b * b ≤ a₂ * a₂
Tactic: apply Nat.add_lt_add_of_le_of_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
neg : b * b ≤ a₂ * a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
have neg₁ : a₁ < a₂ + b
Tactic: apply Nat.add_lt_add_of_le_of_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
have h₂ : b ≤ a₁
Tactic: simp at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
have neg : a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
Tactic: simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
have neg : a₁ * a₁ < a₂ * a₂
Tactic: apply add_lt_add
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
neg : a₁ * a₁ < a₂ * a₂
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
have neg₁ : a₁ + b < a₂ + b
Tactic: apply add_lt_add
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂
have pos : ∀ (h₁ : a < b₁), pair a b₁ < pair a b₂
Tactic: by_cases h₁ : a < b₁
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
pos : ∀ (h₁ : a < b₁), pair a b₁ < pair a b₂
⊢ pair a b₁ < pair a b₂
have neg : ∀ (h₁ : ¬a < b₁), pair a b₁ < pair a b₂
Tactic: by_cases h₁ : a < b₁
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂
have neg : a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Tactic: simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
have pos : ∀ (h₂ : a < b₂), a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Tactic: by_cases h₂ : a < b₂
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
pos : ∀ (h₂ : a < b₂), a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
have neg : ∀ (h₂ : ¬a < b₂), a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Tactic: by_cases h₂ : a < b₂
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
have pos : a * a + (a + b₁) < b₂ * b₂ + a
Tactic: simp only [h₂, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a
have pos : b₁ + a * a < b₂ * b₂
Tactic: rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ + a * a < b₂ * b₂
have pos : b₁ ≤ a + a
Tactic: rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
⊢ pair m n < HPow.hPow (β := ℕ) (max m n + 1) 2
have simp : (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
Tactic: simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
have pos : m < n → n * n + m < max m n * max m n + (max m n + (max m n + 1))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
pos : m < n → n * n + m < max m n * max m n + (max m n + (max m n + 1))
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
have neg : ¬m < n → m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : m < n
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))
have pos : m < n + (n + 1)
Tactic: simp [Nat.le_of_lt, not_lt.1, *]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : ¬m < n
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))
have neg : n < m + 1
Tactic: simp [Nat.le_of_lt, not_lt.1, *]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inl : ∀ (h : m < n), HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
Tactic: rcases lt_or_ge m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
inl : ∀ (h : m < n), HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inr : ∀ (h : n ≤ m), HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
Tactic: rcases lt_or_ge m n with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : m < n
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inl : HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ n * n + m
Tactic: rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : m < n
inl : HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ n * n + m
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inl₁ : HPow.hPow (β := ℕ) n 2 + min m n ≤ n * n + m
Tactic: rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : m < n
inl : HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ n * n + m
inl₁ : HPow.hPow (β := ℕ) n 2 + min m n ≤ n * n + m
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inl₂ : HPow.hPow (β := ℕ) n 2 + m ≤ n * n + m
Tactic: rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : m < n
inl : HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ n * n + m
inl₁ : HPow.hPow (β := ℕ) n 2 + min m n ≤ n * n + m
inl₂ : HPow.hPow (β := ℕ) n 2 + m ≤ n * n + m
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inl₃ : n * n + m ≤ n * n + m
Tactic: rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
h : n ≤ m
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
have inr : n ≤ m + n
Tactic: rw [if_neg h.not_gt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc,
    Nat.add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
⊢ m + n ≤ pair m n
have simp : m + n ≤ if m < n then n * n + m else m * m + (m + n)
Tactic: simp only [pair, Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)
have pos : m < n → m + n ≤ n * n + m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
m n : ℕ
pos : m < n → m + n ≤ n * n + m
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)
have neg : ¬m < n → m + n ≤ m * m + (m + n)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (hypothesis)
Goal:
m n : ℕ
h : m < n
⊢ m + n ≤ n * n + m
have this : n ≤ n * n
Tactic: have := le_mul_self n
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (i : ℕ), ⨆ (j : ℕ), f i j)
have rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (x : ℕ × ℕ), f x.1 x.2)
Tactic: rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → ℕ → α
rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (x : ℕ × ℕ), f x.1 x.2)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (i : ℕ), ⨆ (j : ℕ), f i j)
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (x : ℕ), f (unpair x).1 (unpair x).2)
Tactic: rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]
-- Lean 4 proof step from Mathlib.Data.Nat.Pairing (goal)
Goal:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2 = SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n)
have rw : Eq (α := Set (α × β)) (⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2) (⋃ (x : ℕ × ℕ), s x.1 ×ˢ t x.2)
Tactic: rw [← Set.iUnion_prod]
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
have rw : f (n % a)
Tactic: rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n
have conv_rhs : f (n % a) = f n
Tactic: conv_rhs => rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
conv_rhs : f (n % a) = f n
⊢ f (n % a) = f n
have conv_rhs₁ : f (n % a) = f (n % a)
Tactic: conv_rhs => rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = count p a
have rw : Multiset.count True (map p (Ico n (n + a))) =
  Multiset.count True (map ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) (Ico n (n + a)))
Tactic: rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ←
    multiset_Ico_map_mod n, ← map_count_True_eq_filter_card, ← map_count_True_eq_filter_card,
    map_map]
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) (Ico n (n + a)))
have e_a : p = (fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Periodic (goal)
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
⊢ p = (fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a
have e_a : ∀ (n : ℕ), p n = ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a
have refine : a ∣ p → p = a
Tactic: refine ⟨?_, by rintro rfl; rfl⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
have inl : Prime a → ∀ (hp : Prime (a * 1)), a * 1 = a
Tactic: rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
Cleared hypotheses: j, hp
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
inl : Prime a → ∀ (hp : Prime (a * 1)), a * 1 = a
⊢ a * j = a
have inr : Prime j → ∀ (a1 : Ne (α := ℕ) 1 1) (hp : Prime (1 * j)), 1 * j = 1
Tactic: rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
Cleared hypotheses: a, a1, hp
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p
have by_contra! : ∀ (h : p < 5), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
have revert : ∀ (hp : Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3), False
Tactic: revert h_two h_three hp
Cleared hypotheses: hp, h_two, h_three
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ ¬Prime n ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
have rw : ¬(2 ≤ n ∧ ¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
Tactic: rw [prime_iff_not_exists_mul_eq, and_iff_right h, Classical.not_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
rw : ¬(2 ≤ n ∧ ¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
⊢ ¬Prime n ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
have rw₁ : (¬¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
Tactic: rw [prime_iff_not_exists_mul_eq, and_iff_right h, Classical.not_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
rw : ¬(2 ≤ n ∧ ¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
rw₁ : (¬¬∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
⊢ ¬Prime n ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
have rw₂ : (∃ (m : ℕ), ∃ (n_1 : ℕ), m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
Tactic: rw [prime_iff_not_exists_mul_eq, and_iff_right h, Classical.not_not]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b
have inl : ∀ (hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b), 1 ∣ b
Tactic: obtain rfl | ha := eq_or_ne a 1
Cleared hypotheses: a, hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
inl : ∀ (hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b), 1 ∣ b
⊢ a ∣ b
have inr : ∀ (ha : a ≠ 1), a ∣ b
Tactic: obtain rfl | ha := eq_or_ne a 1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b
have inr : ∀ (p : ℕ) (hp : Prime p ∧ p ∣ a), a ∣ b
Tactic: obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2
have rw : 2 ∣ p ↔ p = 2
Tactic: rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
rw : 2 ∣ p ↔ p = 2
⊢ Even p ↔ p = 2
have rw₁ : 2 = p ↔ p = 2
Tactic: rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
rw : 2 ∣ p ↔ p = 2
rw₁ : 2 = p ↔ p = 2
⊢ Even p ↔ p = 2
have rw₂ : p = 2 ↔ p = 2
Tactic: rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
⊢ Odd p ↔ 3 ≤ p
have rw : p = 2 ↔ p < 3
Tactic: rw [← not_iff_not, not_odd_iff_even, hp.even_iff, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n
have rw : 2 * n + 1 - 1 = n + n
Tactic: rw [hn, Nat.add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
rw : 2 * n + 1 - 1 = n + n
⊢ p - 1 = n + n
have rw₁ : 2 * n = n + n
Tactic: rw [hn, Nat.add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
rw : 2 * n + 1 - 1 = n + n
rw₁ : 2 * n = n + n
⊢ p - 1 = n + n
have rw₂ : n + n = n + n
Tactic: rw [hn, Nat.add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2
have refine : ∀ (h : p % 2 = 1) (hf : p = 2), False
Tactic: refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
Goal:
p : ℕ
hp : Prime p
h : p % 2 = 1
hf : p = 2
⊢ False
have h₁ : HMod.hMod (α := ℕ) 2 2 = 1
Tactic: rw [hf] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
m n : ℕ
⊢ ¬m.Coprime n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
have mp : ¬m.Coprime n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
m n : ℕ
mp : ¬m.Coprime n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
have mpr : (∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
m n : ℕ
h : ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n
have mpr : ∀ (p : ℕ) (hp : Prime p ∧ p ∣ m ∧ p ∣ n), ¬m.Coprime n
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.Coprime m
have rw : ¬∃ (p : ℕ), Prime p ∧ p ∣ n ∧ p ∣ m
Tactic: rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ¬∃ (p : ℕ), Prime p ∧ p ∣ n ∧ p ∣ m
have push : ∀ (p : ℕ) (_ : Prime p) (_ : p ∣ n), ¬p ∣ m
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
⊢ Coprime 2 n ↔ Odd n
have rw : ¬2 ∣ n ↔ Odd n
Tactic: rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
rw : ¬2 ∣ n ↔ Odd n
⊢ Coprime 2 n ↔ Odd n
have rw₁ : ¬2 ∣ n ↔ ¬Even n
Tactic: rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
n : ℕ
rw : ¬2 ∣ n ↔ Odd n
rw₁ : ¬2 ∣ n ↔ ¬Even n
⊢ Coprime 2 n ↔ Odd n
have rw₂ : ¬2 ∣ n ↔ ¬2 ∣ n
Tactic: rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p
have rw : p ^ k = p
Tactic: rw [h.1, h.2, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
rw : p ^ k = p
⊢ a ^ k = p
have rw₁ : HPow.hPow (β := ℕ) p 1 = p
Tactic: rw [h.1, h.2, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
rw : p ^ k = p
rw₁ : HPow.hPow (β := ℕ) p 1 = p
⊢ a ^ k = p
have rw₂ : p = p
Tactic: rw [h.1, h.2, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1
have refine : ∀ (h : a ^ k = p), a = p ∧ k = 1
Tactic: refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
Goal:
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1
have hp₁ : Prime (a ^ k)
Tactic: rw [← h] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
have rw : a = a ^ k ∧ k = 1
Tactic: rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
rw : a = a ^ k ∧ k = 1
⊢ a = p ∧ k = 1
have rw₁ : a = HPow.hPow (β := ℕ) a 1 ∧ Eq (α := ℕ) 1 1
Tactic: rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
rw : a = a ^ k ∧ k = 1
rw₁ : a = HPow.hPow (β := ℕ) a 1 ∧ Eq (α := ℕ) 1 1
⊢ a = p ∧ k = 1
have rw₂ : a = HPow.hPow (β := ℕ) a 1 ∧ True
Tactic: rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
rw : a = a ^ k ∧ k = 1
rw₁ : a = HPow.hPow (β := ℕ) a 1 ∧ Eq (α := ℕ) 1 1
rw₂ : a = HPow.hPow (β := ℕ) a 1 ∧ True
⊢ a = p ∧ k = 1
have rw₃ : a = HPow.hPow (β := ℕ) a 1
Tactic: rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
rw : a = a ^ k ∧ k = 1
rw₁ : a = HPow.hPow (β := ℕ) a 1 ∧ Eq (α := ℕ) 1 1
rw₂ : a = HPow.hPow (β := ℕ) a 1 ∧ True
rw₃ : a = HPow.hPow (β := ℕ) a 1
⊢ a = p ∧ k = 1
have rw₄ : a = a
Tactic: rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
⊢ x * y = HPow.hPow (β := ℕ) p 2 ↔ x = p ∧ y = p
have refine : ∀ (h : x * y = HPow.hPow (β := ℕ) p 2), x = p ∧ y = p
Tactic: refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
⊢ p ∣ x * y
have rw : p ∣ HPow.hPow (β := ℕ) p 2
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (hypothesis)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
⊢ x = p ∧ y = p
have pdvdxy : p ∣ x * y
Tactic: have pdvdxy : p ∣ x * y := by rw [h]; simp [sq]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
have inl : ∀ (hx : p ∣ x), x = p ∧ y = p
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Basic (goal)
Goal:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = HPow.hPow (β := ℕ) p 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = HPow.hPow (β := ℕ) p 2 → p ∣ x' → x' = p ∧ y' = p
inl : ∀ (hx : p ∣ x), x = p ∧ y = p
⊢ x = p ∧ y = p
have inr : ∀ (hy : p ∣ y), x = p ∧ y = p
Tactic: obtain hx | hy := hp.dvd_mul.1 pdvdxy