internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
⊢ ∃ k, f = fun x => k * x
Tactic:
rcases good_is_linear h0 with ⟨k, h1⟩
Proof state after:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
k : ℕ
h1 : g = fun x => k * x
⊢ ∃ k, f = fun x => k * x
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
k : ℕ
h1 : g = fun x => k * x
⊢ ∃ k, f = fun x => k * x
Tactic:
replace h0 : 0 < k := by rw [← k.mul_one, ← congr_fun h1]; exact (f 1).pos
Proof state after:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
⊢ ∃ k, f = fun x => k * x
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
⊢ ∃ k, f = fun x => k * x
Tactic:
refine ⟨⟨k, h0⟩, funext λ x ↦ ?_⟩
Proof state after:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
x : ℕ+
⊢ f x = ⟨k, h0⟩ * x
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
x : ℕ+
⊢ f x = ⟨k, h0⟩ * x
Tactic:
rw [← PNat.coe_inj, PNat.mul_coe, PNat.mk_coe, ← congr_fun h1, eq_comm]
Proof state after:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
x : ℕ+
⊢ g ↑x = ↑(f x)
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case intro
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
k : ℕ
h1 : g = fun x => k * x
h0 : 0 < k
x : ℕ+
⊢ g ↑x = ↑(f x)
Tactic:
exact dif_pos x.pos
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
⊢ a + g b ∣ a ^ 2 + b * g a
Tactic:
rcases a.eq_zero_or_pos with rfl | ha
Proof state after:
case inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
b : ℕ
H : ↑C < 0 + b
⊢ 0 + g b ∣ 0 ^ 2 + b * g 0

case inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
⊢ a + g b ∣ a ^ 2 + b * g a
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
⊢ a + g b ∣ a ^ 2 + b * g a
Tactic:
rcases b.eq_zero_or_pos with rfl | hb
Proof state after:
case inr.inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a : ℕ
ha : a > 0
H : ↑C < a + 0
⊢ a + g 0 ∣ a ^ 2 + 0 * g a

case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ a + g b ∣ a ^ 2 + b * g a
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
b : ℕ
H : ↑C < 0 + b
⊢ 0 + g b ∣ 0 ^ 2 + b * g 0
Tactic:
exact ⟨0, rfl⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr.inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a : ℕ
ha : a > 0
H : ↑C < a + 0
⊢ a + g 0 ∣ a ^ 2 + 0 * g a
Tactic:
rw [zero_mul]
Proof state after:
case inr.inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a : ℕ
ha : a > 0
H : ↑C < a + 0
⊢ a + g 0 ∣ a ^ 2 + 0
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr.inl
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a : ℕ
ha : a > 0
H : ↑C < a + 0
⊢ a + g 0 ∣ a ^ 2 + 0
Tactic:
exact ⟨a, sq a⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ a + g b ∣ a ^ 2 + b * g a
Tactic:
dsimp only [g]
Proof state after:
case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ (a + if h : 0 < b then ↑(f ⟨b, h⟩) else 0) ∣ a ^ 2 + b * if h : 0 < a then ↑(f ⟨a, h⟩) else 0
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ (a + if h : 0 < b then ↑(f ⟨b, h⟩) else 0) ∣ a ^ 2 + b * if h : 0 < a then ↑(f ⟨a, h⟩) else 0
Tactic:
rw [dif_pos ha, dif_pos hb]
Proof state after:
case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ a + ↑(f ⟨b, hb⟩) ∣ a ^ 2 + b * ↑(f ⟨a, ha⟩)
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
case inr.inr
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
a b : ℕ
H : ↑C < a + b
ha : a > 0
hb : b > 0
⊢ a + ↑(f ⟨b, hb⟩) ∣ a ^ 2 + b * ↑(f ⟨a, ha⟩)
Tactic:
exact PNat.dvd_iff.mp (h ⟨a, ha⟩ ⟨b, hb⟩ H)
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
k : ℕ
h1 : g = fun x => k * x
⊢ 0 < k
Tactic:
rw [← k.mul_one, ← congr_fun h1]
Proof state after:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
k : ℕ
h1 : g = fun x => k * x
⊢ 0 < g 1
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
h0 : good (↑C) g
k : ℕ
h1 : g = fun x => k * x
⊢ 0 < g 1
Tactic:
exact (f 1).pos
Proof state after:
no goals
Theorem: IMOSL.Extra.IntLinearSolver
Proof state before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n : ℤ
⊢ f 0 = 0 • g + f 0
Tactic:
rw [zero_zsmul, zero_add]
Proof state after:
no goals
Theorem: IMOSL.Extra.IntLinearSolver
Proof state before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n k : ℤ
x✝ : 0 ≤ k
h1 : f k = k • g + f 0
⊢ f (k + 1) = (k + 1) • g + f 0
Tactic:
rw [h, h1, ← add_assoc, add_comm, one_add_zsmul]
Proof state after:
no goals
Theorem: IMOSL.Extra.IntLinearSolver
Proof state before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n k : ℤ
x✝ : k ≤ 0
h1 : f k = k • g + f 0
⊢ f (k - 1) = (k - 1) • g + f 0
Tactic:
rwa [← add_right_inj g, ← h, sub_add_cancel,
  ← add_assoc, ← one_add_zsmul, add_sub_cancel]
Proof state after:
no goals
Theorem: IMOSL.Extra.IntIntLinearSolverAlt
Proof state before:
g : ℤ
f : ℤ → ℤ
h : ∀ (n : ℤ), f (n + 1) = g + f n
n : ℤ
⊢ f n = g * n + f 0
Tactic:
rw [IntLinearSolver h, smul_eq_mul, mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂ε.add_mul
Proof state before:
x y z : 𝔽₂ε
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [𝔽₂ε.mul_comm, 𝔽₂ε.mul_add, z.mul_comm, z.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂ε.castRingHom_injective
Proof state before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
r : R
h : r * r = 0
h0 : r ≠ 0
h1 : 1 = 0
⊢ r = 0
Tactic:
rw [← one_mul r, h1, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂ε.castRingHom_injective
Proof state before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
r : R
h : r * r = 0
h0 : r ≠ 0
h1 : 1 ≠ 0
x : 𝔽₂ε
h2 : (castRingHom h) Y = 0
⊢ 1 = 0
Tactic:
rwa [add_eq_zero_iff_eq.mp h2, one_mul] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.exists_ne_pow_eq
Proof state before:
k : ℤ
h : k ≠ 0
b : ℤ
h0 : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k
Tactic:
obtain ⟨m, -, n, -, h, h0⟩ :=
  Set.infinite_univ.exists_ne_map_eq_of_mapsTo h0 (Set.toFinite _)
Proof state after:
case intro.intro.intro.intro.intro
k : ℤ
h✝ : k ≠ 0
b : ℤ
h0✝ : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
m n : ℕ
h : m ≠ n
h0 : b ^ m % k = b ^ n % k
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k
Theorem: IMOSL.IMO2014A4.exists_ne_pow_eq
Proof state before:
case intro.intro.intro.intro.intro
k : ℤ
h✝ : k ≠ 0
b : ℤ
h0✝ : Set.MapsTo (fun x => b ^ x % k) Set.univ ↑(Finset.Ico 0 |k|)
m n : ℕ
h : m ≠ n
h0 : b ^ m % k = b ^ n % k
⊢ ∃ m n, m ≠ n ∧ b ^ m % k = b ^ n % k
Tactic:
exact ⟨m, n, h, h0⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.exists_ne_pow_eq
Proof state before:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ (fun x => b ^ x % k) x ∈ ↑(Finset.Ico 0 |k|)
Tactic:
rw [Finset.coe_Ico, Set.mem_Ico]
Proof state after:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ 0 ≤ (fun x => b ^ x % k) x ∧ (fun x => b ^ x % k) x < |k|
Theorem: IMOSL.IMO2014A4.exists_ne_pow_eq
Proof state before:
k : ℤ
h : k ≠ 0
b : ℤ
x : ℕ
x✝ : x ∈ Set.univ
⊢ 0 ≤ (fun x => b ^ x % k) x ∧ (fun x => b ^ x % k) x < |k|
Tactic:
exact ⟨(b ^ x).emod_nonneg h, (b ^ x).emod_lt h⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.linear_good'
Proof state before:
k m x y : ℤ
⊢ (fun x => k * x + m) (y + (fun x => k * x + m) x) - (fun x => k * x + m) y =
    (fun x => k * x + m) ((k + 1) * x) - (fun x => k * x + m) x + k * m
Tactic:
rw [add_sub_add_right_eq_sub, mul_add, add_sub_cancel_left, add_one_mul (α := ℤ),
  add_sub_add_right_eq_sub, ← mul_sub, add_sub_cancel_right, ← mul_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.linear_good
Proof state before:
b c : ℤ
h : b - 1 ∣ c
⊢ good b c fun x => (b - 1) * x + c / (b - 1)
Tactic:
nth_rw 1 [← sub_add_cancel b 1, ← Int.mul_ediv_cancel' h]
Proof state after:
b c : ℤ
h : b - 1 ∣ c
⊢ good (b - 1 + 1) ((b - 1) * (c / (b - 1))) fun x => (b - 1) * x + c / (b - 1)
Theorem: IMOSL.IMO2014A4.linear_good
Proof state before:
b c : ℤ
h : b - 1 ∣ c
⊢ good (b - 1 + 1) ((b - 1) * (c / (b - 1))) fun x => (b - 1) * x + c / (b - 1)
Tactic:
exact linear_good' (b - 1) (c / (b - 1))
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_map_zero_add
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y : ℤ
⊢ f (y + f 0) = c + f y
Tactic:
rw [← sub_eq_iff_eq_add, h, mul_zero, sub_self, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_mul_map_zero_add
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
have h0 n : f (y + f 0 * (n + 1)) = c + f (y + f 0 * n) := by
  rw [mul_add_one (α := ℤ), ← add_assoc, map_map_zero_add h]
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : ∀ (n : ℤ), f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
⊢ f (y + f 0 * k) = c * k + f y
Theorem: IMOSL.IMO2014A4.map_mul_map_zero_add
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : ∀ (n : ℤ), f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
replace h0 := Extra.IntIntLinearSolverAlt (f := λ n ↦ f (y + f 0 * n)) h0 k
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : f (y + f 0 * k) = c * k + f (y + f 0 * 0)
⊢ f (y + f 0 * k) = c * k + f y
Theorem: IMOSL.IMO2014A4.map_mul_map_zero_add
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k : ℤ
h0 : f (y + f 0 * k) = c * k + f (y + f 0 * 0)
⊢ f (y + f 0 * k) = c * k + f y
Tactic:
rwa [mul_zero, add_zero] at h0
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_mul_map_zero_add
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
y k n : ℤ
⊢ f (y + f 0 * (n + 1)) = c + f (y + f 0 * n)
Tactic:
rw [mul_add_one (α := ℤ), ← add_assoc, map_map_zero_add h]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_b_pow_mul_eq_of_map_eq
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
⊢ f (b ^ 0 * x) = f (b ^ 0 * y)
Tactic:
rwa [pow_zero, one_mul, one_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_b_pow_mul_eq_of_map_eq
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b ^ (k + 1) * x) = f (b ^ (k + 1) * y)
Tactic:
rw [pow_succ', mul_assoc, mul_assoc]
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Theorem: IMOSL.IMO2014A4.map_b_pow_mul_eq_of_map_eq
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Tactic:
have h1 := h (b ^ k * y) 0
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
h1 : f (0 + f (b ^ k * y)) - f 0 = f (b * (b ^ k * y)) - f (b ^ k * y) + c
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Theorem: IMOSL.IMO2014A4.map_b_pow_mul_eq_of_map_eq
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
x y : ℤ
h0 : f x = f y
k : ℕ
h1 : f (0 + f (b ^ k * y)) - f 0 = f (b * (b ^ k * y)) - f (b ^ k * y) + c
⊢ f (b * (b ^ k * x)) = f (b * (b ^ k * y))
Tactic:
rwa [← map_b_pow_mul_eq_of_map_eq h0 k,
  h, add_left_inj, sub_left_inj] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ ∀ (n : ℤ), f n = (b - 1) * n + f 0
Tactic:
suffices f.Injective by
intro n
  have h2 := eq_add_of_sub_eq' (h 0 (b * n))
  rw [mul_zero, sub_self, zero_add, ← sub_left_inj (a := f n),
    add_sub_right_comm, ← h n n, sub_left_inj] at h2
  rw [sub_one_mul, ← add_sub_right_comm, this h2, add_sub_cancel_left]
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ Function.Injective f
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ Function.Injective f
Tactic:
have h2 : f 0 ≠ 0 := λ h2 ↦ by
  have h3 := map_map_zero_add h 0
  rw [zero_add, h2, h2, add_zero] at h3
  exact h1 h3.symm
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
⊢ Function.Injective f
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
⊢ Function.Injective f
Tactic:
obtain ⟨m, n, h3, h4⟩ := exists_ne_pow_eq h2 b
Proof state after:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : b ^ m % f 0 = b ^ n % f 0
⊢ Function.Injective f
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : b ^ m % f 0 = b ^ n % f 0
⊢ Function.Injective f
Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero, ← Int.dvd_iff_emod_eq_zero] at h4
Proof state after:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : f 0 ∣ b ^ m - b ^ n
⊢ Function.Injective f
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
h4 : f 0 ∣ b ^ m - b ^ n
⊢ Function.Injective f
Tactic:
rcases h4 with ⟨N, h4⟩
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
⊢ Function.Injective f
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
⊢ Function.Injective f
Tactic:
intro x y h5
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : f x = f y
⊢ x = y
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : f x = f y
⊢ x = y
Tactic:
apply map_b_pow_mul_eq_of_map_eq h at h5
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
⊢ x = y
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
⊢ x = y
Tactic:
have h6 := h5 m
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
⊢ x = y
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
⊢ x = y
Tactic:
have h7 := map_mul_map_zero_add h
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : f (b ^ m * x) = f (b ^ m * y)
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Tactic:
rw [eq_add_of_sub_eq' h4, add_mul, mul_assoc, h7, add_mul,
  mul_assoc, h7, h5, add_left_inj, Int.mul_eq_mul_left_iff h1] at h6
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
⊢ x = y
Tactic:
refine (Int.mul_eq_mul_left_iff λ h8 ↦ ?_).mp h6
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m - b ^ n = f 0 * N
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Tactic:
rw [h8, mul_zero, sub_eq_zero] at h4
Proof state after:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m = b ^ n
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
case intro.intro.intro.intro
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 ≠ 0
m n : ℕ
h3 : m ≠ n
N : ℤ
h4 : b ^ m = b ^ n
x y : ℤ
h5 : ∀ (k : ℕ), f (b ^ k * x) = f (b ^ k * y)
h6 : N * x = N * y
h7 : ∀ (y k : ℤ), f (y + f 0 * k) = c * k + f y
h8 : N = 0
⊢ False
Tactic:
exact h3 (Int.pow_right_injective h0 h4)
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
⊢ ∀ (n : ℤ), f n = (b - 1) * n + f 0
Tactic:
intro n
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
⊢ f n = (b - 1) * n + f 0
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
⊢ f n = (b - 1) * n + f 0
Tactic:
have h2 := eq_add_of_sub_eq' (h 0 (b * n))
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (b * n) + (f (b * 0) - f 0 + c)
⊢ f n = (b - 1) * n + f 0
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (b * n) + (f (b * 0) - f 0 + c)
⊢ f n = (b - 1) * n + f 0
Tactic:
rw [mul_zero, sub_self, zero_add, ← sub_left_inj (a := f n),
  add_sub_right_comm, ← h n n, sub_left_inj] at h2
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (n + f n)
⊢ f n = (b - 1) * n + f 0
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
this : Function.Injective f
n : ℤ
h2 : f (b * n + f 0) = f (n + f n)
⊢ f n = (b - 1) * n + f 0
Tactic:
rw [sub_one_mul, ← add_sub_right_comm, this h2, add_sub_cancel_left]
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
⊢ False
Tactic:
have h3 := map_map_zero_add h 0
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : f (0 + f 0) = c + f 0
⊢ False
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : f (0 + f 0) = c + f 0
⊢ False
Tactic:
rw [zero_add, h2, h2, add_zero] at h3
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : 0 = c
⊢ False
Theorem: IMOSL.IMO2014A4.map_is_linear
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h2 : f 0 = 0
h3 : 0 = c
⊢ False
Tactic:
exact h1 h3.symm
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.c_eq_b_sub_one_mul_map_zero
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
⊢ c = (b - 1) * f 0
Tactic:
have h3 := h 0 0
Proof state after:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h3 : f (0 + f 0) - f 0 = f (b * 0) - f 0 + c
⊢ c = (b - 1) * f 0
Theorem: IMOSL.IMO2014A4.c_eq_b_sub_one_mul_map_zero
Proof state before:
b c : ℤ
f : ℤ → ℤ
h : good b c f
h0 : 1 < b.natAbs
h1 : c ≠ 0
h3 : f (0 + f 0) - f 0 = f (b * 0) - f 0 + c
⊢ c = (b - 1) * f 0
Tactic:
rwa [zero_add, mul_zero, sub_self, zero_add,
  map_is_linear h h0 h1, add_sub_cancel_right, eq_comm] at h3
Proof state after:
no goals
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
b c : ℤ
h : 1 < b.natAbs
h0 : c ≠ 0
f : ℤ → ℤ
h1 : b - 1 ∣ c
h2 : good b c f
⊢ f = fun x => (b - 1) * x + c / (b - 1)
Tactic:
rcases h1 with ⟨k, rfl⟩
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)