Lean4
theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamentalSequence o) :=
by
induction o with
| zero => exact rfl
| oadd a m b iha ihb
rw [fundamentalSequence]
rcases e : b.fundamentalSequence with (⟨_ | b'⟩ | f) <;> simp only [FundamentalSequenceProp] <;>
rw [e, FundamentalSequenceProp] at ihb
· rcases e : a.fundamentalSequence with (⟨_ | a'⟩ | f) <;> rcases e' : m.natPred with - | m' <;> simp only <;>
rw [e, FundamentalSequenceProp] at iha <;>
(try rw [show m = 1 by have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]) <;>
(try
rw [show m = (m' + 1).succPNat by
rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]) <;>
simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left, add_zero,
lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero, Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero,
mul_add_one, PNat.one_coe, succ_zero, _root_.zero_add, zero_def]
· decide
· exact ⟨rfl, inferInstance⟩
· have := opow_pos (repr a') omega0_pos
refine
⟨isSuccLimit_mul this isSuccLimit_omega0, fun i => ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩,
exists_lt_mul_omega0'⟩
rw [← mul_succ, ← natCast_succ]
gcongr
apply nat_lt_omega0
· have := opow_pos (repr a') omega0_pos
refine
⟨isSuccLimit_add _ (isSuccLimit_mul this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩,
exists_lt_add exists_lt_mul_omega0'⟩
· rw [← mul_succ, ← natCast_succ]
gcongr
apply nat_lt_omega0
· refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
rw [repr, ← zero_def, repr, add_zero, iha.1, opow_succ]
gcongr
apply nat_lt_omega0
· rcases iha with ⟨h1, h2, h3⟩
refine ⟨isSuccLimit_opow one_lt_omega0 h1, fun i => ?_, exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩
obtain ⟨h4, h5, h6⟩ := h2 i
exact ⟨h4, h5, fun H => @NF.oadd_zero _ _ (h6 H.fst)⟩
· rcases iha with ⟨h1, h2, h3⟩
refine
⟨isSuccLimit_add _ (isSuccLimit_opow one_lt_omega0 h1), fun i => ?_,
exists_lt_add (exists_lt_omega0_opow' one_lt_omega0 h1 h3)⟩
obtain ⟨h4, h5, h6⟩ := h2 i
refine ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (h6 H.fst)))⟩
rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one, opow_lt_opow_iff_right one_lt_omega0]
· refine ⟨by rw [repr, ihb.1, add_succ, repr], fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩
have := H.snd'.repr_lt
rw [ihb.1] at this
exact (lt_succ _).trans this
· rcases ihb with ⟨h1, h2, h3⟩
simp only [repr]
exact
⟨isSuccLimit_add _ h1, fun i =>
⟨oadd_lt_oadd_3 (h2 i).1, oadd_lt_oadd_3 (h2 i).2.1, fun H =>
H.fst.oadd _ (NF.below_of_lt' (lt_trans (h2 i).2.1 H.snd'.repr_lt) ((h2 i).2.2 H.snd))⟩,
exists_lt_add h3⟩
