Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Table4Ext.allCells_checked

PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext · PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:38 to 57

Mathematical statement

Exact Lean statement

theorem allCells_checked : ∀ c ∈ allCells, checkCell c = true

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem allCells_checked : ∀ c ∈ allCells, checkCell c = true := by  intro c hc  simp only [allCells, List.mem_append] at hc  rcases hc with    ((((((((((((hc | hc) | hc) | hc) | hc) | hc) | hc) | hc) | hc) | hc) |      hc) | hc) | hc) | hc  · exact List.all_eq_true.mp cells_00_checked c hc  · exact List.all_eq_true.mp cells_01_checked c hc  · exact List.all_eq_true.mp cells_02_checked c hc  · exact List.all_eq_true.mp cells_03_checked c hc  · exact List.all_eq_true.mp cells_04_checked c hc  · exact List.all_eq_true.mp cells_05_checked c hc  · exact List.all_eq_true.mp cells_06_checked c hc  · exact List.all_eq_true.mp cells_07_checked c hc  · exact List.all_eq_true.mp cells_08_checked c hc  · exact List.all_eq_true.mp cells_09_checked c hc  · exact List.all_eq_true.mp cells_10_checked c hc  · exact List.all_eq_true.mp cells_11_checked c hc  · exact List.all_eq_true.mp cells_12_checked c hc  · exact List.all_eq_true.mp cells_13_checked c hc