Theorem: IMOSL.IMO2019N4.goodPNat_is_linear (IMOSLLean4/IMO2019/N4/N4.lean)

State before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
⊢ ∃ k, f = fun x => k * x
Tactic:
let g : ℕ → ℕ := λ n ↦ dite (0 < n) (λ h ↦ f ⟨n, h⟩) (λ _ ↦ 0)
State after:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
⊢ ∃ k, f = fun x => k * x

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

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

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 ↦ ?_⟩
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

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

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
State after:
no goals

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

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

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⟩
State after:
no goals

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]
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

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⟩
State after:
no goals

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]
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

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

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)
State after:
no goals

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]
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

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
State after:
no goals