internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2006N3.g_succ
Proof state before:
n : ℕ
⊢ ∑ k ∈ range n.succ, n.succ / (k + 1) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card
Tactic:
simp only [Nat.succ_div]
Proof state after:
n : ℕ
⊢ ∑ x ∈ range n.succ, (n / (x + 1) + if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card
Theorem: IMOSL.IMO2006N3.g_succ
Proof state before:
n : ℕ
⊢ ∑ x ∈ range n.succ, (n / (x + 1) + if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card
Tactic:
rw [card_filter, sum_Ico_eq_sum_range, Nat.add_sub_cancel, sum_add_distrib,
  sum_range_succ, Nat.div_eq_of_lt n.lt_succ_self]
Proof state after:
n : ℕ
⊢ (∑ x ∈ range n, n / (x + 1) + 0 + ∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0
Theorem: IMOSL.IMO2006N3.g_succ
Proof state before:
n : ℕ
⊢ (∑ x ∈ range n, n / (x + 1) + 0 + ∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) =
    ∑ k ∈ range n, n / (k + 1) + ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0
Tactic:
exact congrArg₂ _ rfl (by simp only [add_comm 1])
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.g_succ
Proof state before:
n : ℕ
⊢ (∑ x ∈ range n.succ, if x + 1 ∣ n + 1 then 1 else 0) = ∑ k ∈ range n.succ, if 1 + k ∣ n.succ then 1 else 0
Tactic:
simp only [add_comm 1]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.g_eq_sum_divisors_card
Proof state before:
⊢ g 0 = ∑ k ∈ range 0, k.succ.divisors.card
Tactic:
rw [sum_range_zero, g_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.g_eq_sum_divisors_card
Proof state before:
n : ℕ
⊢ g (n + 1) = ∑ k ∈ range (n + 1), k.succ.divisors.card
Tactic:
rw [g_succ, sum_range_succ, ← g_eq_sum_divisors_card]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.two_le_card_divisors
Proof state before:
n : ℕ
h : 2 ≤ n
⊢ 2 ≤ n.divisors.card
Tactic:
rw [← Nat.insert_self_properDivisors (Nat.not_eq_zero_of_lt h), Nat.succ_le_iff,
  card_insert_of_not_mem Nat.properDivisors.not_self_mem, Nat.succ_lt_succ_iff, card_pos]
Proof state after:
n : ℕ
h : 2 ≤ n
⊢ n.properDivisors.Nonempty
Theorem: IMOSL.IMO2006N3.two_le_card_divisors
Proof state before:
n : ℕ
h : 2 ≤ n
⊢ n.properDivisors.Nonempty
Tactic:
exact ⟨1, Nat.one_mem_properDivisors_iff_one_lt.mpr h⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.two_mul_lt_g
Proof state before:
⊢ 12 < 14
Tactic:
norm_num
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.two_mul_lt_g
Proof state before:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * (n + 1) < g (n + 1)
Tactic:
rw [Nat.mul_succ, g_succ]
Proof state after:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * n + 2 < g n + n.succ.divisors.card
Theorem: IMOSL.IMO2006N3.two_mul_lt_g
Proof state before:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * n + 2 < g n + n.succ.divisors.card
Tactic:
exact add_lt_add_of_lt_of_le h0 <| two_le_card_divisors <|
  Nat.succ_le_succ (Nat.one_le_of_lt h)
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.exists_lt_card_divisor_succ
Proof state before:
c : ℕ
⊢ c < (2 ^ c - 1).succ.divisors.card
Tactic:
rw [Nat.succ_eq_add_one, Nat.sub_add_cancel Nat.one_le_two_pow,
Nat.divisors_prime_pow Nat.prime_two, card_map, card_range, Nat.lt_succ_iff]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
a b : ℕ
h : g a * b < g b * a
⊢ f a < f b
Tactic:
unfold f
Proof state after:
a b : ℕ
h : g a * b < g b * a
⊢ ↑↑(g a) / ↑↑a < ↑↑(g b) / ↑↑b
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
a b : ℕ
h : g a * b < g b * a
⊢ ↑↑(g a) / ↑↑a < ↑↑(g b) / ↑↑b
Tactic:
rcases a with _ | a
Proof state after:
case zero
b : ℕ
h : g 0 * b < g b * 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b

case succ
b a : ℕ
h : g (a + 1) * b < g b * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g b) / ↑↑b
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ
b a : ℕ
h : g (a + 1) * b < g b * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g b) / ↑↑b
Tactic:
rcases b with _ | b
Proof state after:
case succ.zero
a : ℕ
h : g (a + 1) * 0 < g 0 * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0

case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case zero
b : ℕ
h : g 0 * b < g b * 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b
Tactic:
rw [g_zero, zero_mul, mul_zero] at h
Proof state after:
case zero
b : ℕ
h : 0 < 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case zero
b : ℕ
h : 0 < 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b
Tactic:
exact absurd rfl h.ne
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ.zero
a : ℕ
h : g (a + 1) * 0 < g 0 * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0
Tactic:
rw [g_zero, zero_mul, mul_zero] at h
Proof state after:
case succ.zero
a : ℕ
h : 0 < 0
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ.zero
a : ℕ
h : 0 < 0
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0
Tactic:
exact absurd rfl h.ne
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Tactic:
have X (n : ℕ) : 0 < (n.succ : ℤ) := Int.natCast_pos.mpr n.succ_pos
Proof state after:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Tactic:
rw [Rat.div_lt_div_iff_mul_lt_mul (X a) (X b), ← Nat.cast_mul, ← Nat.cast_mul]
Proof state after:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑(g (a + 1) * b.succ) < ↑(g (b + 1) * a.succ)
Theorem: IMOSL.IMO2006N3.f_lt_f_of_g
Proof state before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑(g (a + 1) * b.succ) < ↑(g (b + 1) * a.succ)
Tactic:
exact Int.ofNat_lt.mpr h
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_self_lt_f_succ_of_divisors_card
Proof state before:
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ f n < f n.succ
Tactic:
apply f_lt_f_of_g
Proof state after:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ g n * n.succ < g n.succ * n
Theorem: IMOSL.IMO2006N3.f_self_lt_f_succ_of_divisors_card
Proof state before:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ g n * n.succ < g n.succ * n
Tactic:
rw [Nat.mul_succ, g_succ, add_mul, add_lt_add_iff_left, g_eq_sum_divisors_card]
Proof state after:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ k ∈ range n, k.succ.divisors.card < n.succ.divisors.card * n
Theorem: IMOSL.IMO2006N3.f_self_lt_f_succ_of_divisors_card
Proof state before:
case h
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ k ∈ range n, k.succ.divisors.card < n.succ.divisors.card * n
Tactic:
calc _ < (range n).sum λ _ ↦ n.succ.divisors.card :=
      sum_lt_sum_of_nonempty (nonempty_range_iff.mpr h) (λ k h1 ↦ h0 k (mem_range.mp h1))
     _ = n.succ.divisors.card * n := by
      rw [sum_const, card_range, smul_eq_mul, mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_self_lt_f_succ_of_divisors_card
Proof state before:
n : ℕ
h : n ≠ 0
h0 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∑ x ∈ range n, n.succ.divisors.card = n.succ.divisors.card * n
Tactic:
rw [sum_const, card_range, smul_eq_mul, mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.final_solution_part1
Proof state before:
N : ℕ
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b
Tactic:
obtain ⟨n, h0, h1⟩ : ∃ n : ℕ, N < n ∧
    ∀ k : ℕ, k < n → k.succ.divisors.card < n.succ.divisors.card := by
  obtain ⟨K, h0⟩ : ∃ K : ℕ, ∀ k : ℕ, k ≤ N → k.succ.divisors.card ≤ K :=
    ⟨Extra.seqMax (λ n ↦ n.succ.divisors.card) N,
    λ _ ↦ Extra.le_seqMax_of_le (λ n ↦ n.succ.divisors.card)⟩
  have h1 := exists_lt_card_divisor_succ K
  refine ⟨Nat.find h1,
    (Nat.lt_find_iff h1 _).mpr λ k h2 ↦ (h0 k h2).not_lt,
    λ k h2 ↦ (le_of_not_lt (Nat.find_min h1 h2)).trans_lt (Nat.find_spec h1)⟩
Proof state after:
case intro.intro
N n : ℕ
h0 : N < n
h1 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b
Theorem: IMOSL.IMO2006N3.final_solution_part1
Proof state before:
case intro.intro
N n : ℕ
h0 : N < n
h1 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b
Tactic:
exact ⟨n, f_self_lt_f_succ_of_divisors_card (Nat.not_eq_zero_of_lt h0) h1, h0⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.final_solution_part1
Proof state before:
N : ℕ
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
obtain ⟨K, h0⟩ : ∃ K : ℕ, ∀ k : ℕ, k ≤ N → k.succ.divisors.card ≤ K :=
  ⟨Extra.seqMax (λ n ↦ n.succ.divisors.card) N,
  λ _ ↦ Extra.le_seqMax_of_le (λ n ↦ n.succ.divisors.card)⟩
Proof state after:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Theorem: IMOSL.IMO2006N3.final_solution_part1
Proof state before:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
have h1 := exists_lt_card_divisor_succ K
Proof state after:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
h1 : ∃ n, K < n.succ.divisors.card
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Theorem: IMOSL.IMO2006N3.final_solution_part1
Proof state before:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
h1 : ∃ n, K < n.succ.divisors.card
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
refine ⟨Nat.find h1,
  (Nat.lt_find_iff h1 _).mpr λ k h2 ↦ (h0 k h2).not_lt,
  λ k h2 ↦ (le_of_not_lt (Nat.find_min h1 h2)).trans_lt (Nat.find_spec h1)⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.f_succ_lt_self_of_succ_prime_large
Proof state before:
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ f n.succ < f n
Tactic:
apply f_lt_f_of_g
Proof state after:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ g n.succ * n < g n * n.succ
Theorem: IMOSL.IMO2006N3.f_succ_lt_self_of_succ_prime_large
Proof state before:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ g n.succ * n < g n * n.succ
Tactic:
rw [g_succ, card_divisors_prime h0, add_mul, Nat.mul_succ, add_lt_add_iff_left]
Proof state after:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ 2 * n < g n
Theorem: IMOSL.IMO2006N3.f_succ_lt_self_of_succ_prime_large
Proof state before:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ 2 * n < g n
Tactic:
exact two_mul_lt_g n h
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
N : ℕ
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b
Tactic:
obtain ⟨n, h, h0, h1⟩ : ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n := by
  rcases (max 6 (N + 1) + 1).exists_infinite_primes with ⟨_ | n, h, h0⟩
  exact absurd h0 Nat.not_prime_zero
  rw [Nat.add_le_add_iff_right, max_le_iff] at h
  exact ⟨n, h.1, h0, h.2⟩
Proof state after:
case intro.intro.intro
N n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
h1 : N < n
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
case intro.intro.intro
N n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
h1 : N < n
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b
Tactic:
exact ⟨n, f_succ_lt_self_of_succ_prime_large h h0, h1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
N : ℕ
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
rcases (max 6 (N + 1) + 1).exists_infinite_primes with ⟨_ | n, h, h0⟩
Proof state after:
case intro.zero.intro
N : ℕ
h : max 6 (N + 1) + 1 ≤ 0
h0 : Nat.Prime 0
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
case intro.zero.intro
N : ℕ
h : max 6 (N + 1) + 1 ≤ 0
h0 : Nat.Prime 0
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
exact absurd h0 Nat.not_prime_zero
Proof state after:
case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
rw [Nat.add_le_add_iff_right, max_le_iff] at h
Proof state after:
case intro.succ.intro
N n : ℕ
h : 6 ≤ n ∧ N + 1 ≤ n
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Theorem: IMOSL.IMO2006N3.final_solution_part2
Proof state before:
case intro.succ.intro
N n : ℕ
h : 6 ≤ n ∧ N + 1 ≤ n
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
exact ⟨n, h.1, h0, h.2⟩
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_of_singleton
Proof state before:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ NatSeq_ofList [c] n = c
Tactic:
rw [NatSeq_ofList, List.length_singleton, Nat.mod_one]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ [c].getI 0 = c
Theorem: IMOSL.Extra.NatSeq_of_singleton
Proof state before:
α : Type u_1
inst✝ : Inhabited α
c : α
n : ℕ
⊢ [c].getI 0 = c
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_ofList_of_PeriodicNatSeq_eq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
hN : 0 < N
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n
Tactic:
replace hN := List.length_pos.mp <| hN.trans_eq (List_ofNatSeq_length a N).symm
Proof state after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n
Theorem: IMOSL.Extra.NatSeq_ofList_of_PeriodicNatSeq_eq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ NatSeq_ofList (List_ofNatSeq a N) n = a n
Tactic:
rw [NatSeq_nonempty_eq_get hN]
Proof state after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List_ofNatSeq a N).get ⟨n % (List_ofNatSeq a N).length, ⋯⟩ = a n
Theorem: IMOSL.Extra.NatSeq_ofList_of_PeriodicNatSeq_eq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List_ofNatSeq a N).get ⟨n % (List_ofNatSeq a N).length, ⋯⟩ = a n
Tactic:
unfold List_ofNatSeq
Proof state after:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List.map a (List.range N)).get ⟨n % (List.map a (List.range N)).length, ⋯⟩ = a n
Theorem: IMOSL.Extra.NatSeq_ofList_of_PeriodicNatSeq_eq
Proof state before:
α : Type u_1
inst✝ : Inhabited α
N : ℕ
a : ℕ → α
ha : Function.Periodic a N
n : ℕ
hN : List_ofNatSeq a N ≠ []
⊢ (List.map a (List.range N)).get ⟨n % (List.map a (List.range N)).length, ⋯⟩ = a n
Tactic:
rw [List.get_map, List.get_range, Fin.val_mk,
  List.length_map, List.length_range, ha.map_mod_nat]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.pullback_of_inj
Proof state before:
R : Type u_1
R' : Type u_2
inst✝² : AddMonoid R
inst✝¹ : CharTwo R
inst✝ : AddMonoid R'
φ : R' →+ R
h : Function.Injective ⇑φ
x : R'
⊢ φ (x + x) = φ 0
Tactic:
rw [φ.map_add, φ.map_zero, CharTwo.add_self_eq_zero]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.forward_of_surj
Proof state before:
R : Type u_2
R' : Type u_1
inst✝² : AddMonoid R
inst✝¹ : CharTwo R
inst✝ : AddMonoid R'
φ : R →+ R'
h : Function.Surjective ⇑φ
x : R'
c : R
h0 : φ c = x
⊢ x + x = 0
Tactic:
rw [← h0, ← φ.map_add, add_self_eq_zero, φ.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.one_sub_is_good
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => 1 - x) ((fun x => 1 - x) x * (fun x => 1 - x) y) + (fun x => 1 - x) (x + y) = (fun x => 1 - x) (x * y)
Tactic:
rw [sub_add_sub_comm, mul_one_sub, one_sub_mul, sub_sub, sub_add, add_sub_sub_cancel,
  add_sub_add_left_eq_sub, sub_sub_cancel_left, ← sub_eq_add_neg]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_neg
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ (-f) ((-f) x * (-f) y) + (-f) (x + y) = (-f) (x * y)
Tactic:
simp only [Pi.neg_apply]
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Theorem: IMOSL.IMO2017A6.good_neg
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Tactic:
rw [neg_mul_neg, ← neg_add, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_special_equality
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
f : R → R
h : good f
x y : R
h0 : x * y = 1
⊢ f (f (x + 1) * f (y + 1)) = 0
Tactic:
rw [← add_left_eq_self, h, add_one_mul x, mul_add_one x, h0, add_comm 1 x]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ f (f 0 ^ 2) = 0
Tactic:
specialize h 0 0
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : f (f 0 * f 0) + f (0 + 0) = f (0 * 0)
⊢ f (f 0 ^ 2) = 0
Theorem: IMOSL.IMO2017A6.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : f (f 0 * f 0) + f (0 + 0) = f (0 * 0)
⊢ f (f 0 ^ 2) = 0
Tactic:
rwa [add_zero, mul_zero, add_left_eq_self, ← sq] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
x : R
⊢ f (f x) + f x = 1
Tactic:
rw [← h0, ← mul_zero x, ← h, add_zero, h0, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = 1 - x
Tactic:
rw [eq_sub_iff_add_eq', ← h2 x, add_left_inj]
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ x = f (f x)
Theorem: IMOSL.IMO2017A6.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ x = f (f x)
Tactic:
apply h1
Proof state after:
case a
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
Theorem: IMOSL.IMO2017A6.good_eq_of_inj
Proof state before:
case a
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Function.Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
Tactic:
rw [eq_sub_of_add_eq (h2 (f x)), ← h2 x, add_sub_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_map_eq_zero
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
⊢ f = 0
Tactic:
have h3 := good_special_equality h (mul_inv_cancel <| sub_ne_zero_of_ne h2)
Proof state after:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
Theorem: IMOSL.IMO2017A6.good_map_eq_zero
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
Tactic:
rw [sub_add_cancel, h1, zero_mul] at h3
Proof state after:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0
Theorem: IMOSL.IMO2017A6.good_map_eq_zero
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0
Tactic:
ext x
Proof state after:
case h
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x
Theorem: IMOSL.IMO2017A6.good_map_eq_zero
Proof state before:
case h
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x
Tactic:
rw [Pi.zero_apply, ← h3, ← mul_zero x, ← h,
  h3, mul_zero, h3, zero_add, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_map_eq_zero_iff
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
c : D
h1 : f = 0
⊢ 0 = 1
Tactic:
rwa [h1] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_shift
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) + 1 = f x
Tactic:
have h1 := h x 1
Proof state after:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x
Theorem: IMOSL.IMO2017A6.good_shift
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x
Tactic:
rwa [good_map_one h, mul_zero, h0, add_comm, mul_one] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_shift2
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x - 1) = f x + 1
Tactic:
rw [← good_shift h h0, sub_add_cancel]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.good_map_add_one_eq_zero_iff
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) = 0 ↔ x = 0
Tactic:
rw [good_map_eq_zero_iff h h0, add_left_eq_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ f = 0 ∨ (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
rw [or_iff_not_imp_left]
Proof state after:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ ¬f = 0 → (f = fun x => 1 - x) ∨ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
⊢ ¬f = 0 → (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
intros h1
Proof state after:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = fun x => x - 1
Tactic:
apply (good_map_zero h0 h1).imp <;> intro h1
Proof state after:
case f
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x

case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = -1
⊢ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case f
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x
Tactic:
exact good_eq_of_inj h0 h1 (h f h0 h1)
Proof state after:
no goals