Theorem: IMOSL.IMO2014A4.final_solution_case2 (IMOSLLean4/IMO2014/A4/A4.lean)

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⟩
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)

State before:
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)
Tactic:
have h1 := c_eq_b_sub_one_mul_map_zero h2 h h0
State after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)

State before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Tactic:
have h3 := (mul_ne_zero_iff.mp h0).1
State after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)

State before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Tactic:
rw [Int.mul_ediv_cancel_left _ h3]
State after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k

State before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Tactic:
rw [mul_eq_mul_left_iff, or_iff_left h3] at h1
State after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k

State before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Tactic:
rw [h1]
State after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + f 0

State before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + f 0
Tactic:
exact funext (map_is_linear h2 h h0)
State after:
no goals