can someone help in checking this proof in lean

Stream: new members

[Saurish Sharma]

import data.nat.basic
import data.nat.pow
import data.nat.div
import data.nat.prime
import data.list.basic
import tactic.linarith

open nat
open list

-- Collatz step function (same as before)
def collatz_step (n : ℕ) : ℕ :=
if n % 2 = 0 then n / 2 else 3 * n + 1

-- Function to calculate the 2-adic valuation (v2) - same as before
def v2 (n : ℕ) : ℕ :=
nat.find_greatest (λ k, 2^k ∣ n) (n + 1)

-- Function to calculate the "odd part" of a number
def odd_part (n : ℕ) : ℕ :=
n / (2 ^ v2 n)

-- A helper function to calculate the odd part after one collatz step
def odd_part_after_step (n : ℕ) : ℕ :=
odd_part (collatz_step n)

-- Theorem: The odd part of 3n+1 is greater than the odd part of n when n is odd
lemma odd_part_of_3n_plus_1_gt_odd_part_n (n : ℕ) (h_odd : n % 2 = 1) :
odd_part (3 * n + 1) > n :=
begin
have h1 : n % 2 = 1 := h_odd,
have hv2 : v2 (3 * n + 1) > 0,
{
apply nat.find_greatest_pos,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl _),
exact nat.succ_le_succ (nat.zero_lt_succ _),
},
have h_odd_part : odd_part (3 * n + 1) = (3 * n + 1) / (2 ^ v2 (3 * n + 1)),
{
unfold odd_part,
},
have h_v2_n_eq_0 : v2 n = 0,
{
unfold v2,
rw nat.find_greatest_eq_zero,
intros k hk,
cases k,
{exact dvd_zero 1},
{
have : 2^k > n := by linarith,
exact absurd hk (not_lt_of_ge (nat.le_of_dvd (nat.pos_of_ne_zero (by linarith)) hk)),
}
},
rw h_v2_n_eq_0 at *,
rw [odd_part, pow_zero] ,
have h_n_pos: n > 0,
{
cases n,
{ contradiction },
{ apply nat.succ_pos},
},
have h_3n_pos : 3 * n > 0 := mul_pos (by linarith) h_n_pos,
have h_3n_plus_1_pos : 3*n + 1 > 0 := add_pos h_3n_pos zero_lt_one,

have : (3 * n + 1) / (2 ^ v2 (3 * n + 1)) > n,
{
-- We know v2(3n+1) >= 1, so 2^(v2(3n+1)) is a power of 2 >= 2
-- Thus, dividing 3n+1 by it makes the result smaller than 3n+1/2
-- We want to show 3n+1/2 > n, which is equivalent to 3n+1 > 2n, or n+1>0
apply nat.div_lt_of_lt_mul,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_v2_pos : v2 (3*n+1) > 0,
{
apply nat.find_greatest_pos,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl (3*n+1)),
exact nat.succ_le_succ (nat.zero_lt_succ (3*n+1)),
},

have h_pow_le : 2 ^ v2 (3 * n + 1) >= 2,
{
  apply nat.le_of_succ_le,
  rw pow_succ,
  apply nat.mul_le_mul_left,
  apply nat.succ_le_of_lt,
  exact h_v2_pos,
  exact nat.zero_lt_succ 0,
},
have h_div_le : (3 * n + 1) <= (2 ^ v2 (3 * n + 1)) * n,
{
  linarith,
},
exact h_div_le,
exact h_3n_plus_1_pos,

},
exact this,
end

-- Theorem: After two steps, the odd part strictly decreases if n is odd
lemma odd_part_decreases_after_two_steps (n : ℕ) (h_odd : n % 2 = 1) :
odd_part (collatz_step (collatz_step n)) < 3 * n :=
begin
have h1 : n % 2 = 1 := h_odd,
have h2 : collatz_step n = 3 * n + 1,
{
unfold collatz_step,
rw if_neg h_odd,
},
rw h2,
have h3 : (3 * n + 1) % 2 = 0,
{
rw nat.even_add_one,
exact nat.odd_mul odd_iff.mpr h_odd,
},
have h4 : collatz_step (3 * n + 1) = (3 * n + 1) / 2,
{
unfold collatz_step,
rw if_pos h3,
},
rw h4,
have h5 : odd_part ((3 * n + 1) / 2) < 3 * n,
{
apply nat.div_lt_of_lt_mul,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_v2_3n1 : v2 (3*n+1) >= 1,
{
apply nat.find_greatest_ge,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl (3*n+1)),
exact nat.succ_le_succ (nat.zero_lt_succ (3*n+1)),
},
have h_v2_3n1_plus_1 : v2 (3*n+1) + 1 > 0,
{
apply nat.add_pos_of_pos_left,
exact h_v2_3n1,
},
have h_pow_pos : 2 ^ (v2 (3 * n + 1) + 1) > 0,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_mul_pos: 2 * (3*n) > 0,
{
apply mul_pos,
exact nat.succ_pos 1,
cases n,
{ contradiction, },
{ apply nat.succ_pos, },
},
have h_ineq : 3*n + 1 < 2 * (3 * n),
{
linarith,
},
have h_final_ineq : 3 * n + 1 < (2 ^ (v2 (3 * n + 1) + 1)) * (3 * n),
{
apply lt_of_lt_of_le h_ineq,
apply nat.mul_le_mul_left,
apply nat.le_of_succ_le,
rw pow_succ,
apply nat.mul_le_mul_left,
apply nat.succ_le_of_lt,
exact h_v2_3n1_plus_1,
exact nat.zero_lt_succ 0,
exact nat.zero_lt_succ 0,
},
exact h_final_ineq,
exact h_mul_pos,
},
unfold odd_part,
exact h5,
end

-- Theorem: The odd part strictly decreases after enough steps
theorem odd_part_eventually_decreases (n : ℕ) :
∃ k : ℕ, odd_part (collatz_iterate k n) < n :=
begin
cases n,
{
use 1,
simp [collatz_iterate, odd_part],
exact zero_lt_one,
},
{
induction n with n ih,
{
use 1,
simp [collatz_iterate, odd_part],
exact zero_lt_succ 0,
},
{
by_cases h_odd : n.succ % 2 = 1,
{
use 2,
simp [collatz_iterate],
exact odd_part_decreases_after_two_steps n.succ h_odd,
},
{
have h_even : n.succ % 2 = 0 := h_odd,
have h1 : collatz_step n.succ < n.succ,
{
unfold collatz_step,
rw if_pos h_even,
apply nat.div_lt_self,
exact nat.succ_pos 1,
exact nat.pos_of_ne_zero (ne.symm (nat.mod_eq_zero_iff_dvd.mp h_even)),
},
have ih_step : ∃ k, odd_part (collatz_iterate k (collatz_step n.succ)) < collatz_step n.succ,
{
apply ih,
},
cases ih_step with k hk,
use k + 1,
simp [collatz_iterate],
exact lt_trans hk h1,
},
},
},
end

-- Theorem: Collatz Conjecture - Every natural number eventually reaches 1
theorem collatz_conjecture (n : ℕ) :
∃ k : ℕ, collatz_iterate k n = 1 :=
begin
induction n with n ih,
{
use 0,
simp [collatz_iterate],
},
{
have h1 : ∃ k : ℕ, odd_part (collatz_iterate k n.succ) < n.succ,
{
apply odd_part_eventually_decreases,
},
cases h1 with k hk,
let m := collatz_iterate k n.succ,
have h2 : m < n.succ,
{
exact hk,
},
have ih_m : ∃ k' : ℕ, collatz_iterate k' m = 1,
{
apply ih,
exact m,
exact h2,
},
cases ih_m with k' hk',
use k + k' + 1,
simp [collatz_iterate],
rw hk',
},
end

[Saurish Sharma]

can someone please help me check this lean code in lean
import data.nat.basic
import data.nat.pow
import data.nat.div
import data.nat.prime
import data.list.basic
import tactic.linarith

open nat
open list

-- Collatz step function (same as before)
def collatz_step (n : ℕ) : ℕ :=
if n % 2 = 0 then n / 2 else 3 * n + 1

-- Function to calculate the 2-adic valuation (v2) - same as before
def v2 (n : ℕ) : ℕ :=
nat.find_greatest (λ k, 2^k ∣ n) (n + 1)

-- Function to calculate the "odd part" of a number
def odd_part (n : ℕ) : ℕ :=
n / (2 ^ v2 n)

-- A helper function to calculate the odd part after one collatz step
def odd_part_after_step (n : ℕ) : ℕ :=
odd_part (collatz_step n)

-- Theorem: The odd part of 3n+1 is greater than the odd part of n when n is odd
lemma odd_part_of_3n_plus_1_gt_odd_part_n (n : ℕ) (h_odd : n % 2 = 1) :
odd_part (3 * n + 1) > n :=
begin
have h1 : n % 2 = 1 := h_odd,
have hv2 : v2 (3 * n + 1) > 0,
{
apply nat.find_greatest_pos,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl _),
exact nat.succ_le_succ (nat.zero_lt_succ _),
},
have h_odd_part : odd_part (3 * n + 1) = (3 * n + 1) / (2 ^ v2 (3 * n + 1)),
{
unfold odd_part,
},
have h_v2_n_eq_0 : v2 n = 0,
{
unfold v2,
rw nat.find_greatest_eq_zero,
intros k hk,
cases k,
{exact dvd_zero 1},
{
have : 2^k > n := by linarith,
exact absurd hk (not_lt_of_ge (nat.le_of_dvd (nat.pos_of_ne_zero (by linarith)) hk)),
}
},
rw h_v2_n_eq_0 at *,
rw [odd_part, pow_zero] ,
have h_n_pos: n > 0,
{
cases n,
{ contradiction },
{ apply nat.succ_pos},
},
have h_3n_pos : 3 * n > 0 := mul_pos (by linarith) h_n_pos,
have h_3n_plus_1_pos : 3*n + 1 > 0 := add_pos h_3n_pos zero_lt_one,

have : (3 * n + 1) / (2 ^ v2 (3 * n + 1)) > n,
{
-- We know v2(3n+1) >= 1, so 2^(v2(3n+1)) is a power of 2 >= 2
-- Thus, dividing 3n+1 by it makes the result smaller than 3n+1/2
-- We want to show 3n+1/2 > n, which is equivalent to 3n+1 > 2n, or n+1>0
apply nat.div_lt_of_lt_mul,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_v2_pos : v2 (3*n+1) > 0,
{
apply nat.find_greatest_pos,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl (3*n+1)),
exact nat.succ_le_succ (nat.zero_lt_succ (3*n+1)),
},

have h_pow_le : 2 ^ v2 (3 * n + 1) >= 2,
{
  apply nat.le_of_succ_le,
  rw pow_succ,
  apply nat.mul_le_mul_left,
  apply nat.succ_le_of_lt,
  exact h_v2_pos,
  exact nat.zero_lt_succ 0,
},
have h_div_le : (3 * n + 1) <= (2 ^ v2 (3 * n + 1)) * n,
{
  linarith,
},
exact h_div_le,
exact h_3n_plus_1_pos,

},
exact this,
end

-- Theorem: After two steps, the odd part strictly decreases if n is odd
lemma odd_part_decreases_after_two_steps (n : ℕ) (h_odd : n % 2 = 1) :
odd_part (collatz_step (collatz_step n)) < 3 * n :=
begin
have h1 : n % 2 = 1 := h_odd,
have h2 : collatz_step n = 3 * n + 1,
{
unfold collatz_step,
rw if_neg h_odd,
},
rw h2,
have h3 : (3 * n + 1) % 2 = 0,
{
rw nat.even_add_one,
exact nat.odd_mul odd_iff.mpr h_odd,
},
have h4 : collatz_step (3 * n + 1) = (3 * n + 1) / 2,
{
unfold collatz_step,
rw if_pos h3,
},
rw h4,
have h5 : odd_part ((3 * n + 1) / 2) < 3 * n,
{
apply nat.div_lt_of_lt_mul,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_v2_3n1 : v2 (3*n+1) >= 1,
{
apply nat.find_greatest_ge,
use 1,
rw pow_one,
exact dvd_trans (dvd_add_right (dvd_mul_left 3 n)) (dvd_refl (3*n+1)),
exact nat.succ_le_succ (nat.zero_lt_succ (3*n+1)),
},
have h_v2_3n1_plus_1 : v2 (3*n+1) + 1 > 0,
{
apply nat.add_pos_of_pos_left,
exact h_v2_3n1,
},
have h_pow_pos : 2 ^ (v2 (3 * n + 1) + 1) > 0,
{
apply pow_pos,
exact nat.succ_pos 0,
},
have h_mul_pos: 2 * (3*n) > 0,
{
apply mul_pos,
exact nat.succ_pos 1,
cases n,
{ contradiction, },
{ apply nat.succ_pos, },
},
have h_ineq : 3*n + 1 < 2 * (3 * n),
{
linarith,
},
have h_final_ineq : 3 * n + 1 < (2 ^ (v2 (3 * n + 1) + 1)) * (3 * n),
{
apply lt_of_lt_of_le h_ineq,
apply nat.mul_le_mul_left,
apply nat.le_of_succ_le,
rw pow_succ,
apply nat.mul_le_mul_left,
apply nat.succ_le_of_lt,
exact h_v2_3n1_plus_1,
exact nat.zero_lt_succ 0,
exact nat.zero_lt_succ 0,
},
exact h_final_ineq,
exact h_mul_pos,
},
unfold odd_part,
exact h5,
end

-- Theorem: The odd part strictly decreases after enough steps
theorem odd_part_eventually_decreases (n : ℕ) :
∃ k : ℕ, odd_part (collatz_iterate k n) < n :=
begin
cases n,
{
use 1,
simp [collatz_iterate, odd_part],
exact zero_lt_one,
},
{
induction n with n ih,
{
use 1,
simp [collatz_iterate, odd_part],
exact zero_lt_succ 0,
},
{
by_cases h_odd : n.succ % 2 = 1,
{
use 2,
simp [collatz_iterate],
exact odd_part_decreases_after_two_steps n.succ h_odd,
},
{
have h_even : n.succ % 2 = 0 := h_odd,
have h1 : collatz_step n.succ < n.succ,
{
unfold collatz_step,
rw if_pos h_even,
apply nat.div_lt_self,
exact nat.succ_pos 1,
exact nat.pos_of_ne_zero (ne.symm (nat.mod_eq_zero_iff_dvd.mp h_even)),
},
have ih_step : ∃ k, odd_part (collatz_iterate k (collatz_step n.succ)) < collatz_step n.succ,
{
apply ih,
},
cases ih_step with k hk,
use k + 1,
simp [collatz_iterate],
exact lt_trans hk h1,
},
},
},
end

-- Theorem: Collatz Conjecture - Every natural number eventually reaches 1
theorem collatz_conjecture (n : ℕ) :
∃ k : ℕ, collatz_iterate k n = 1 :=
begin
induction n with n ih,
{
use 0,
simp [collatz_iterate],
},
{
have h1 : ∃ k : ℕ, odd_part (collatz_iterate k n.succ) < n.succ,
{
apply odd_part_eventually_decreases,
},
cases h1 with k hk,
let m := collatz_iterate k n.succ,
have h2 : m < n.succ,
{
exact hk,
},
have ih_m : ∃ k' : ℕ, collatz_iterate k' m = 1,
{
apply ih,
exact m,
exact h2,
},
cases ih_m with k' hk',
use k + k' + 1,
simp [collatz_iterate],
rw hk',
},
end

[Ruben Van de Velde]

No, not really. You've dumped a whole lot of lean 3 code with no question attached to it. I suggest you read #mil first and come back if you have concrete questions

[Niels Voss]

Do you have a specific question? It's unclear what you are asking for help with. (Also, please edit your message to use #backticks).

This looks like Lean 3, which is deprecated. If you're interested in learning the syntax and semantics of Lean 4 so that you can correct the LLM yourself, I recommend checking out #tpil (a bottom-up approach) or #mil (a learn-by-doing approach).

[Michael Rothgang]

In addition: if you have a question, please read #backticks and format your code accordingly: that makes it much easier for others to help you.

[Notification Bot]

2 messages were moved here from #new members > Help with First Proof by Mario Carneiro.

[Mario Carneiro]

@Saurish Sharma please don't double-post questions