@@ -54,7 +54,7 @@ def tate_big_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) :
5454 let ⟨vpj, k, integralInv⟩ :=
5555 match 3 * (primeEVR hp).valtn c4 with
5656 | ⊤ => (0 , n, true )
57- | ofN v_c4_3 => if v_c4_3 < n then ((v_c4_3 : ℤ) - (n : ℤ), v_c4_3, false ) else (v_c4_3 - n, n, true )
57+ | some v_c4_3 => if v_c4_3 < n then ((v_c4_3 : ℤ) - (n : ℤ), v_c4_3, false ) else (v_c4_3 - n, n, true )
5858 let ⟨u, r, s, t⟩ :=
5959 if k < 12 then (1 , 0 , 0 , 0 ) else
6060 let u' := p ^ (k / 12 )
@@ -113,6 +113,7 @@ def tate_big_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) :
113113
114114open SurjVal
115115
116+ -- TODO move
116117macro "simp_wf'" : tactic =>
117118 `(tactic| simp (config := { zeta := false }) only [invImage, InvImage, Prod.lex, sizeOfWFRel,
118119 measure, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf_nat, Nat.lt_eq] )
@@ -135,8 +136,7 @@ def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0
135136 else
136137 have hdr : has_double_root 1 a3q (-a6q2) hp := by
137138 apply And.intro (val_of_one surjvalp) _
138- apply ENat.pos_of_ne_zero
139- rw [mul_one, ←neg_mul_eq_mul_neg, sub_eq_add_neg, neg_neg]
139+ rw [mul_one, ←neg_mul_eq_mul_neg, sub_eq_add_neg, neg_neg, pos_iff_ne_zero]
140140 exact discr_1
141141 let a := double_root 1 a3q (-a6q2) p
142142
@@ -149,29 +149,34 @@ def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0
149149 Nat.cast_pow, ←mul_add, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer]
150150 apply add_le_add (le_of_eq rfl)
151151 rw [add_comm, ←mul_one 2 ]
152- exact succ_le_of_lt (val_poly_of_double_root hp 1 a3q (-a6q2) hdr).2
152+ rw [one_le_iff_pos]
153+ exact (val_poly_of_double_root hp 1 a3q (-a6q2) hdr).2
153154 have h4' : surjvalp e1.a4 ≥ q + 1 := by
154155 rw [t_of_a4]
155156 apply le_trans _ (surjvalp.v_add_ge_min_v _ _)
156157 apply le_min h4
157- rw [mul_assoc, val_neg, surjvalp.v_mul_eq_add_v, add_comm, surjvalp.v_mul_eq_add_v,
158- Nat.cast_pow, val_of_pow_uniformizer]
159- conv =>
160- rhs
161- rw [add_comm, add_assoc]
162- rw [add_comm]
163- apply add_le_add (le_of_eq rfl)
164- exact le_trans h1 (le_add_right (surjvalp e.a1) _)
158+ simp (config := {zeta := false })
159+ -- rw [mul_assoc, val_neg, surjvalp.v_mul_eq_add_v, add_comm, surjvalp.v_mul_eq_add_v,
160+ -- Nat.cast_pow, val_of_pow_uniformizer]
161+ elinarith
162+ -- conv =>
163+ -- rhs
164+ -- rw [add_comm, add_assoc]
165+ -- rw [ add_comm ]
166+ -- apply add_le_add (le_of_eq rfl) -- TOOD simplify
167+ -- exact le_trans h1 le_self_add
165168 have h6' : (primeEVR hp).valtn e1.a6 ≥ 2 * q + 1 := by
166- rw [t_of_a6, factor_p_of_le_val evrp h6, factor_p_of_le_val evrp h3, rw_a6, ←val_neg,
167- sub_eq_add_neg, sub_eq_add_neg, neg_add, neg_add, neg_neg, neg_neg,
168- Nat.cast_pow, pow_two]
169- erw [ add_assoc (-((↑p : ℤ) ^ (2 * q) * a6q2) : ℤ)]
170- rw [neg_mul_eq_mul_neg _ a6q2, factorize1 a a3q ↑p q, ←pow_add, add_self_eq_mul_two,
171- ←mul_add, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer, add_mul, ←pow_two a,
172- ←one_mul (a ^ 2 ), add_comm (-a6q2)]
173- push_cast
174- exact add_le_add (le_of_eq rfl) (succ_le_of_lt (val_poly_of_double_root hp 1 a3q (-a6q2) hdr).1 )
169+ rw [t_of_a6]
170+ sorry
171+ -- rw [factor_p_of_le_val evrp h6, factor_p_of_le_val evrp h3, rw_a6, ←val_neg,
172+ -- sub_eq_add_neg, sub_eq_add_neg, neg_add, neg_add, neg_neg, neg_neg,
173+ -- Nat.cast_pow, pow_two]
174+ -- erw [ add_assoc (-((↑p : ℤ) ^ (2 * q) * a6q2) : ℤ)]
175+ -- rw [neg_mul_eq_mul_neg _ a6q2, factorize1 a a3q ↑p q, ←pow_add, add_self_eq_mul_two,
176+ -- ←mul_add, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer, add_mul, ←pow_two a,
177+ -- ←one_mul (a ^ 2), add_comm (-a6q2)]
178+ -- push_cast
179+ -- exact add_le_add (le_of_eq rfl) (succ_le_of_lt (val_poly_of_double_root hp 1 a3q (-a6q2) hdr).1)
175180 let t := t + u0 ^ 3 * a * (p ^ q : ℕ)
176181 let a2p := sub_val evrp 1 e1.a2
177182 let a4pq := sub_val evrp (q + 1 ) e1.a4
@@ -188,11 +193,10 @@ def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0
188193 else
189194 have hdr' : has_double_root a2p a4pq a6pq2 hp := by
190195 have v_a2p : surjvalp a2p = 0 := by
191- rw [←rw_a2', val_sub_val_eq evrp e1.a2 1 h2']
196+ rw [← rw_a2', val_sub_val_eq evrp e1.a2 1 h2']
192197 simp
193198 apply And.intro v_a2p _
194- apply ENat.pos_of_ne_zero
195- assumption
199+ rwa [pos_iff_ne_zero]
196200 let a' := double_root a2p a4pq a6pq2 p
197201 have rw_a' : double_root a2p a4pq a6pq2 p = a' := rfl
198202 --if p = 2 then modulo a6pq2 2 else modulo (2 * a2p * -a4pq) 3
@@ -202,49 +206,54 @@ def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0
202206 have h2'' : surjvalp e2.a2 = 1 := by
203207 rwa [r_of_a2, v_add_eq_min_v surjvalp]
204208 rw [h2']
205- apply lt_of_succ_le
209+ have : ¬IsMax (1 : ℕ∞)
210+ · norm_num
211+ rw [← Order.succ_le_iff_of_not_isMax this] -- TODO this is asking for better abstraction
206212 apply val_mul_ge_of_right_ge surjvalp
207213 apply val_mul_ge_of_right_ge surjvalp
208214 rw [Nat.cast_pow, val_of_pow_uniformizer surjvalp]
209- rw [← lt_ofN 1 q] at hq
210- exact succ_le_of_lt hq
215+ rw [Order.succ_le_iff_of_not_isMax this]
216+ exact_mod_cast hq
211217 have h3'' : surjvalp e2.a3 ≥ q + 1 := by
212218 rw [r_of_a3]
213219 apply le_trans _ (surjvalp.v_add_ge_min_v _ _)
214220 apply le_min h3'
215221 rw [mul_comm a', mul_assoc, surjvalp.v_mul_eq_add_v, Nat.cast_pow, val_of_pow_uniformizer]
216222 exact add_le_add (le_of_eq rfl) (val_mul_ge_of_right_ge surjvalp h1')
217223 have h4'' : surjvalp e2.a4 ≥ q + 2 := by
218- rw [r_of_a4, factor_p_of_le_val evrp h4', rw_a4', factor_p_of_le_val evrp (le_of_eq h2'.symm),
219- rw_a2', Nat.cast_pow, factorize2 a' a2p (↑p) q, ←pow_add, ←mul_add, add_comm a4pq]
220- apply le_trans (le_min _ _) (surjvalp.v_add_ge_min_v _ _)
221- . rw [Nat.add_succ q, Nat.succ_eq_add_one, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer]
222- rw [Nat.cast_add, Nat.cast_one, add_assoc]
223- rw [show (2 : ℕ∞) = 1 + 1 by norm_num, ← add_assoc, ← add_assoc]
224- apply add_le_add (le_of_eq rfl)
225- exact (succ_le_of_lt (val_poly_of_double_root hp a2p a4pq a6pq2 hdr').2 )
226- . rw [pow_two, factorize3 a' p q, ←pow_add]
227- apply val_mul_ge_of_left_ge surjvalp _
228- rw [val_of_pow_uniformizer]
229- exact (le_ofN _ _).2 (Nat.add_le_add (le_of_eq rfl) (Nat.succ_le_of_lt hq))
224+ sorry
225+ -- rw [r_of_a4, factor_p_of_le_val evrp h4', rw_a4', factor_p_of_le_val evrp (le_of_eq h2'.symm),
226+ -- rw_a2', Nat.cast_pow, factorize2 a' a2p (↑p) q, ←pow_add, ←mul_add, add_comm a4pq]
227+ -- apply le_trans (le_min _ _) (surjvalp.v_add_ge_min_v _ _)
228+ -- . rw [Nat.add_succ q, Nat.succ_eq_add_one, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer]
229+ -- rw [Nat.cast_add, Nat.cast_one, add_assoc]
230+ -- rw [show (2 : ℕ∞) = 1 + 1 by norm_num, ← add_assoc, ← add_assoc]
231+ -- apply add_le_add (le_of_eq rfl)
232+ -- exact (succ_le_of_lt (val_poly_of_double_root hp a2p a4pq a6pq2 hdr').2)
233+ -- . rw [pow_two, factorize3 a' p q, ←pow_add]
234+ -- apply val_mul_ge_of_left_ge surjvalp _
235+ -- rw [ val_of_pow_uniformizer ]
236+ -- exact (le_ofN _ _).2 (Nat.add_le_add (le_of_eq rfl) (Nat.succ_le_of_lt hq))
230237 have h6'' : surjvalp e2.a6 ≥ 2 * (q + 1 ) := by
231238 rw [r_of_a6, Nat.cast_pow]
232239 apply le_trans (le_min _ _) (surjvalp.v_add_ge_min_v _ _)
233- . rw [factor_p_of_le_val evrp h6', rw_a6', factor_p_of_le_val evrp h4', rw_a4',
234- factor_p_of_eq_val evrp h2', rw_a2', factorize4 a' a2p a4pq a6pq2 p q, ←pow_add, ←pow_add,
235- ←pow_add, ←Nat.add_assoc, add_self_eq_mul_two q, ←mul_add, ←mul_add, mul_add,
236- ←add_self_eq_mul_two 1 , ←add_assoc, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer]
237- push_cast
238- apply add_le_add (le_of_eq rfl)
239- rw [show 1 = ENat.succ 0 by rfl]
240- apply succ_le_of_lt
241- have := (val_poly_of_double_root hp a2p a4pq a6pq2 hdr').1
242- push_cast at this
243- exact this
244- . rw [mul_pow a' _ 3 , ←pow_mul, mul_add, mul_one, Nat.mul_succ] -- TODO why did this break
245- apply val_mul_ge_of_right_ge surjvalp
246- rw [val_of_pow_uniformizer, mul_comm q]
247- exact (le_ofN _ _).2 (Nat.add_le_add (le_of_eq rfl) (Nat.succ_le_of_lt hq))
240+ sorry
241+ sorry
242+ -- . rw [factor_p_of_le_val evrp h6', rw_a6', factor_p_of_le_val evrp h4', rw_a4',
243+ -- factor_p_of_eq_val evrp h2', rw_a2', factorize4 a' a2p a4pq a6pq2 p q, ←pow_add, ←pow_add,
244+ -- ←pow_add, ←Nat.add_assoc, add_self_eq_mul_two q, ←mul_add, ←mul_add, mul_add,
245+ -- ←add_self_eq_mul_two 1, ←add_assoc, surjvalp.v_mul_eq_add_v, val_of_pow_uniformizer]
246+ -- push_cast
247+ -- apply add_le_add (le_of_eq rfl)
248+ -- rw [show 1 = ENat.succ 0 by rfl]
249+ -- apply succ_le_of_lt
250+ -- have := (val_poly_of_double_root hp a2p a4pq a6pq2 hdr').1
251+ -- push_cast at this
252+ -- exact this
253+ -- . rw [mul_pow a' _ 3, ←pow_mul, mul_add, mul_one, Nat.mul_succ] -- TODO why did this break
254+ -- apply val_mul_ge_of_right_ge surjvalp
255+ -- rw [val_of_pow_uniformizer, mul_comm q]
256+ -- exact (le_ofN _ _).2 (Nat.add_le_add (le_of_eq rfl) (Nat.succ_le_of_lt hq))
248257 let r := r + u0 ^ 2 + a' * (p ^ q : ℕ) -- TODO check these
249258 let t := t + u0 ^ 2 * s0 * a' * (p ^ q : ℕ)
250259 kodaira_type_Is p hp e2 u0 r s0 t (m + 2 ) (q + 1 ) (Nat.lt_succ_of_lt hq) h1'' h2'' h3'' h4'' h6''
@@ -255,8 +264,11 @@ decreasing_by
255264 simp only [Nat.cast_pow, rst_iso_a2, zero_mul, sub_zero, mul_zero, add_zero, rst_iso_a4,
256265 rst_iso_a6, iso_rst_val_discr_to_nat, ge_iff_le, Nat.lt_eq]
257266 apply Nat.sub_lt_sub_left _ _
258- . rw [← lt_ofN, ofN_val_discr_to_nat]
259- exact lt_of_succ_le (v_discr_of_v_ai surjvalp e hq h1 h2 h3 h4 h6)
267+ . rw [← Nat.succ_le_iff]
268+ suffices : 2 * q + 3 ≤ (primeEVR hp).valtn e.discr
269+ · rw [← ofN_val_discr_to_nat] at this
270+ exact_mod_cast this
271+ exact v_discr_of_v_ai surjvalp e hq h1 h2 h3 h4 h6
260272 . exact Nat.add_lt_add_right (Nat.mul_lt_mul_of_pos_left q.lt_succ_self (Nat.zero_lt_succ 1 )) 2
261273
262274
@@ -280,7 +292,7 @@ def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ
280292 let n := val_discr_to_nat navp e
281293 if testΔ : n = 0 then (I 0 , 0 , 1 , .Good, (u, r, s, t)) else -- TODO check
282294 have hΔ : navp e.discr ≥ 1 := by
283- rw [show ¬n = 0 ↔ 0 < n by simp [Nat.pos_iff_ne_zero], ← lt_ofN, ofN_val_discr_to_nat] at testΔ
295+ rw [show ¬n = 0 ↔ 0 < n by simp [Nat.pos_iff_ne_zero], ofN_val_discr_to_nat] at testΔ
284296 exact succ_le_of_lt testΔ
285297
286298 if test_b2 : navp e.b2 < 1 then
0 commit comments