The proof
f n / n exists and, if so, whether it is
irrational. Read explanation (PDF)Source
Main.lean · 74209 lines · 5.0 MB
Showing the first 500 of 74209 lines. The whole file is 5.0 MB; download it to read the rest.
end Bounty
/- One-file Erdős 1062(ii) proof candidate.
The submission body is independent of local modules and data files. -/
/- Component PolicyCombinatorialFrontFast; SHA256 9f1109298a4d819400a9ca244751c04849e7fee75492eae7fa39e0a2f8219316. -/
section PolicySubmissionPart0
/- Ordinary combinatorial front: compact finite base, normalization, depth-5 closure, and both input families. -/
/- Frozen source PolicyBaseExactCompact; SHA256 e2225388355ddc67c206ff2e1867c675da6447335cd4360f12ac0457d05386a2. -/
section PolicyCombinatorialFront_PolicyBaseExactCompact
/- One-file proof candidate assembled from the actual local import graph.
A complete ordinary-kernel check and target axiom audit are still required. -/
/- Component Solution; SHA256 dd1b2e49c0e97dfe5eb14a613957f604da4aacacc129697486e6add57caf69ab -/
section SubmissionComponent_Solution
/- Combinatorial and arithmetic lemmas for Erdős 1062(ii). -/
open Filter
open scoped Topology
namespace Bounty
def forkFree_iff (A : Set ℕ) :
Erdos1062.ForkFree A ↔
∀ a b c, a ∈ A → b ∈ A → c ∈ A →
a ≠ b → a ≠ c → a ∣ b → a ∣ c → b = c := by
simp only [Erdos1062.ForkFree, Set.Subsingleton, Set.mem_ofPred_eq,
Set.mem_sdiff, Set.mem_singleton_iff]
aesop
def forkFree_mono {A B : Set ℕ} (hAB : A ⊆ B)
(hB : Erdos1062.ForkFree B) : Erdos1062.ForkFree A := by
rw [forkFree_iff] at *
exact fun a b c ha hb hc hab hac habd hacd =>
hB a b c (hAB ha) (hAB hb) (hAB hc) hab hac habd hacd
def forkFree_empty : Erdos1062.ForkFree ∅ := by
simp [Erdos1062.ForkFree]
def exists_maximizer (n : ℕ) :
∃ A ⊆ Set.Icc 1 n, Erdos1062.ForkFree A ∧ A.ncard = Erdos1062.f n := by
classical
exact Nat.findGreatest_spec
(P := fun k => ∃ A ⊆ Set.Icc 1 n, Erdos1062.ForkFree A ∧ A.ncard = k)
(m := 0) (Nat.zero_le n)
⟨∅, Set.empty_subset _, forkFree_empty, by simp⟩
def card_le_f {n : ℕ} {A : Set ℕ} (hA : A ⊆ Set.Icc 1 n)
(hfork : Erdos1062.ForkFree A) : A.ncard ≤ Erdos1062.f n := by
classical
apply Nat.le_findGreatest
· calc
A.ncard ≤ (Set.Icc 1 n).ncard := Set.ncard_le_ncard hA
_ = n := by simp
· exact ⟨A, hA, hfork, rfl⟩
def window_multiple {A : Set ℕ} {P : ℕ → Prop} {r a b : ℕ}
(hpos : ∀ x ∈ A, 0 < x)
(hwindow : ∀ x ∈ A,
(P x ∧ r < 4 * x ∧ x ≤ r) ∨ (¬P x ∧ r < 6 * x ∧ 2 * x ≤ r))
(hdouble : ∀ x ∈ A, P (2 * x) ↔ ¬P x)
(htriple : ∀ x ∈ A, P (3 * x) ↔ P x)
(hfour : ∀ x ∈ A, P (4 * x) ↔ P x)
(hfive : ∀ x ∈ A, 5 * x ∉ A)
(ha : a ∈ A) (hb : b ∈ A) (hne : a ≠ b) (hdvd : a ∣ b) :
(P a ∧ b = 3 * a) ∨ (¬P a ∧ b = 2 * a) := by
have ha0 := hpos a ha
have haw := hwindow a ha
have hbw := hwindow b hb
have halow : r < 6 * a := by rcases haw with h | h <;> omega
have hbhigh : b ≤ r := by rcases hbw with h | h <;> omega
obtain ⟨k, rfl⟩ := hdvd
have hk : k < 6 := by
by_contra h
have hle : 6 ≤ k := by omega
have hm := Nat.mul_le_mul_left a hle
omega
interval_cases k
· simp_all
· simp_all
· have hp := hdouble a ha
have haw := hwindow a ha
have hbw := hwindow (a * 2) hb
simp only [Nat.mul_comm a 2] at *
rcases haw with h | h
· rcases hbw with hb' | hb'
· exact False.elim (hp.mp hb'.1 h.1)
· omega
· exact Or.inr ⟨h.1, trivial⟩
· have hp := htriple a ha
have haw := hwindow a ha
have hbw := hwindow (a * 3) hb
simp only [Nat.mul_comm a 3] at *
rcases haw with h | h
· exact Or.inl ⟨h.1, trivial⟩
· rcases hbw with hb' | hb'
· exact False.elim (h.1 (hp.mp hb'.1))
· omega
· have hp := hfour a ha
have haw := hwindow a ha
have hbw := hwindow (a * 4) hb
simp only [Nat.mul_comm a 4] at *
rcases haw with h | h
· omega
· rcases hbw with hb' | hb'
· exact False.elim (h.1 (hp.mp hb'.1))
· omega
· exact False.elim (hfive a ha (by simpa [Nat.mul_comm] using hb))
def forkFree_window {A : Set ℕ} {P : ℕ → Prop} {r : ℕ}
(hpos : ∀ x ∈ A, 0 < x)
(hwindow : ∀ x ∈ A,
(P x ∧ r < 4 * x ∧ x ≤ r) ∨ (¬P x ∧ r < 6 * x ∧ 2 * x ≤ r))
(hdouble : ∀ x ∈ A, P (2 * x) ↔ ¬P x)
(htriple : ∀ x ∈ A, P (3 * x) ↔ P x)
(hfour : ∀ x ∈ A, P (4 * x) ↔ P x)
(hfive : ∀ x ∈ A, 5 * x ∉ A) :
Erdos1062.ForkFree A := by
rw [forkFree_iff]
intro a b c ha hb hc hab hac habd hacd
have h₁ := window_multiple hpos hwindow hdouble htriple hfour hfive ha hb hab habd
have h₂ := window_multiple hpos hwindow hdouble htriple hfour hfive ha hc hac hacd
aesop
def Smooth23 (n : ℕ) : Prop := ∃ a b : ℕ, n = 2 ^ a * 3 ^ b
def smooth23_pos {n : ℕ} (hn : Smooth23 n) : 0 < n := by
obtain ⟨a, b, rfl⟩ := hn
positivity
def smooth23_not_dvd_five {n : ℕ} (hn : Smooth23 n) : ¬5 ∣ n := by
obtain ⟨a, b, rfl⟩ := hn
intro h
have hp : Nat.Prime 5 := by decide
rcases hp.dvd_mul.mp h with h | h
· have h' := hp.dvd_of_dvd_pow h
norm_num at h'
· have h' := hp.dvd_of_dvd_pow h
norm_num at h'
def factorization_two_double {n : ℕ} (hn : 0 < n) :
(2 * n).factorization 2 = 1 + n.factorization 2 := by
rw [Nat.factorization_mul (by decide) (Nat.ne_of_gt hn), Finsupp.add_apply]
rw [Nat.prime_two.factorization_self]
def factorization_two_triple {n : ℕ} (hn : 0 < n) :
(3 * n).factorization 2 = n.factorization 2 := by
rw [Nat.factorization_mul (by decide) (Nat.ne_of_gt hn), Finsupp.add_apply]
have h : (3 : ℕ).factorization 2 = 0 :=
Nat.factorization_eq_zero_of_not_dvd (by decide)
omega
def factorization_two_four {n : ℕ} (hn : 0 < n) :
(4 * n).factorization 2 = 2 + n.factorization 2 := by
rw [Nat.factorization_mul (by decide) (Nat.ne_of_gt hn), Finsupp.add_apply]
have h : (4 : ℕ).factorization 2 = 2 := by
change (2 ^ 2).factorization 2 = 2
exact Nat.factorization_pow_self Nat.prime_two
omega
def cutoffWindow (p r : ℕ) : Set ℕ :=
{n | Smooth23 n ∧
((n.factorization 2 % 2 = p ∧ r < 4 * n ∧ n ≤ r) ∨
(n.factorization 2 % 2 ≠ p ∧ r < 6 * n ∧ 2 * n ≤ r))}
def cutoffWindow_forkFree {p : ℕ} (hp : p < 2) (r : ℕ) :
Erdos1062.ForkFree (cutoffWindow p r) := by
apply forkFree_window (P := fun n => n.factorization 2 % 2 = p) (r := r)
· intro n hn
exact smooth23_pos hn.1
· intro n hn
exact hn.2
· intro n hn
rw [factorization_two_double (smooth23_pos hn.1)]
omega
· intro n hn
rw [factorization_two_triple (smooth23_pos hn.1)]
· intro n hn
rw [factorization_two_four (smooth23_pos hn.1)]
omega
· intro n _ h
exact smooth23_not_dvd_five h.1 (dvd_mul_right 5 n)
def cutoffWindow_subset (p r : ℕ) : cutoffWindow p r ⊆ Set.Icc 1 r := by
intro n hn
have hpos := smooth23_pos hn.1
have hwin := hn.2
constructor
· omega
· rcases hwin with h | h <;> omega
def cutoffWindow_finite (p r : ℕ) : (cutoffWindow p r).Finite :=
(Set.finite_Icc 1 r).subset (cutoffWindow_subset p r)
def cutoffWindow_disjoint {p q r s : ℕ}
(hcutoff : (if p = q then 4 else 6) * s ≤ r) :
Disjoint (cutoffWindow p r) (cutoffWindow q s) := by
apply Set.disjoint_left.mpr
intro n hn hm
have h₁ := hn.2
have h₂ := hm.2
by_cases hpq : p = q
· simp only [hpq, if_true] at hcutoff
subst q
rcases h₁ with h₁ | h₁ <;> rcases h₂ with h₂ | h₂ <;> omega
· simp only [hpq, if_false] at hcutoff
rcases h₁ with h₁ | h₁ <;> rcases h₂ with h₂ | h₂ <;> omega
def cutoffWindow_lower {p r n : ℕ} (hn : n ∈ cutoffWindow p r) :
r < 6 * n := by
have hpos := smooth23_pos hn.1
rcases hn.2 with h | h <;> omega
def coefficient4 (n : ℕ) : ℤ :=
let x := 4 ^ n
let y := 3 ^ Nat.log 3 x
if 15 * x < 16 * y then 78
else if 9 * x < 10 * y then 30
else if 3 * x < 4 * y then -30
else if 2 * x < 3 * y then 30
else if x < 2 * y then 0
else if 3 * x < 8 * y then -60
else -12
def coefficient3 (n : ℕ) : ℤ :=
let x := 3 ^ n
let y := 4 ^ Nat.log 4 x
if 3 * x < 4 * y then 30
else if 5 * x < 8 * y then 35
else if 3 * x < 5 * y then 29
else if x < 2 * y then 24
else -60
def coefficient4_bound (n : ℕ) : |(coefficient4 n : ℝ)| ≤ 78 := by
unfold coefficient4
dsimp only
split_ifs <;> norm_num
def coefficient3_bound (n : ℕ) : |(coefficient3 n : ℝ)| ≤ 60 := by
unfold coefficient3
dsimp only
split_ifs <;> norm_num
def weighted_summable {a : ℕ → ℝ} {b M : ℝ} (hb : 1 < b)
(ha : ∀ n, |a n| ≤ M) : Summable (fun n => a n / b ^ n) := by
have hb0 : 0 < b := lt_trans zero_lt_one hb
have hgeo := (summable_geometric_of_lt_one (inv_nonneg.mpr hb0.le)
(inv_lt_one_of_one_lt₀ hb)).mul_left M
apply hgeo.of_norm_bounded
intro n
rw [Real.norm_eq_abs, abs_div, abs_of_pos (pow_pos hb0 n),
div_eq_mul_inv, ← inv_pow]
exact mul_le_mul_of_nonneg_right (ha n) (pow_nonneg (inv_nonneg.mpr hb0.le) n)
def coefficient4_summable :
Summable (fun n => (coefficient4 n : ℝ) / (4 : ℝ) ^ n) :=
weighted_summable (by norm_num) coefficient4_bound
noncomputable def explicitDensity : ℝ :=
(32 + (∑' n, (coefficient4 n : ℝ) / (4 : ℝ) ^ n) +
(∑' n, (coefficient3 n : ℝ) / (3 : ℝ) ^ n)) / 0xb4
def weighted_shift_identity {a : ℕ → ℝ} {b M : ℝ} (hb : 1 < b)
(ha : ∀ n, |a n| ≤ M) (q : ℕ) :
(b ^ q - 1) * (∑' n, a n / b ^ n) =
b ^ q * (∑ n ∈ Finset.range q, a n / b ^ n) +
(∑' n, (a (n + q) - a n) / b ^ n) := by
have hb0 : b ≠ 0 := ne_of_gt (lt_trans zero_lt_one hb)
have h₁ := weighted_summable hb ha
have h₂ := weighted_summable hb (fun n => ha (n + q))
have hsplit := h₁.sum_add_tsum_nat_add q
have htail :
b ^ q * (∑' n, a (n + q) / b ^ (n + q)) =
∑' n, a (n + q) / b ^ n := by
rw [← tsum_mul_left]
apply tsum_congr
intro n
rw [pow_add]
field_simp
have hscaled := congrArg (fun x : ℝ => b ^ q * x) hsplit
rw [mul_add, htail] at hscaled
have hdiff :
(∑' n, (a (n + q) - a n) / b ^ n) =
(∑' n, a (n + q) / b ^ n) - (∑' n, a n / b ^ n) := by
simp only [sub_div]
exact h₂.tsum_sub h₁
rw [hdiff]
nlinarith
def integerPrefix (a : ℕ → ℤ) (b q : ℕ) : ℤ :=
∑ n ∈ Finset.range q, a n * (b : ℤ) ^ (q - n)
def integerPrefix_cast (a : ℕ → ℤ) {b : ℕ} (hb : 0 < b) (q : ℕ) :
(integerPrefix a b q : ℝ) =
(b : ℝ) ^ q * (∑ n ∈ Finset.range q, (a n : ℝ) / (b : ℝ) ^ n) := by
unfold integerPrefix
push_cast
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro n hn
have hle : n ≤ q := Nat.le_of_lt (Finset.mem_range.mp hn)
have hb0 : (b : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hb)
have hp : (b : ℝ) ^ q = (b : ℝ) ^ n * (b : ℝ) ^ (q - n) := by
rw [← pow_add, Nat.add_sub_of_le hle]
rw [hp]
field_simp
def integer_weighted_shift {a : ℕ → ℤ} {b : ℕ} {M : ℝ}
(hb : 1 < b) (ha : ∀ n, |(a n : ℝ)| ≤ M) (q : ℕ) :
((b : ℝ) ^ q - 1) * (∑' n, (a n : ℝ) / (b : ℝ) ^ n) =
(integerPrefix a b q : ℝ) +
(∑' n, ((a (n + q) - a n : ℤ) : ℝ) / (b : ℝ) ^ n) := by
rw [integerPrefix_cast a (by omega) q]
push_cast
exact weighted_shift_identity (by exact_mod_cast hb) ha q
def irrational_log_four_div_log_three :
Irrational (Real.log 4 / Real.log 3) := by
rintro ⟨q, hq⟩
have hlog4 : 0 < Real.log 4 := Real.log_pos (by norm_num)
have hlog3 : 0 < Real.log 3 := Real.log_pos (by norm_num)
have hqpos : 0 < q := by
have hreal : (0 : ℝ) < q := by
rw [hq]
exact div_pos hlog4 hlog3
exact_mod_cast hreal
have hnum : 0 < q.num := Rat.num_pos.mpr hqpos
have habsI : (q.num.natAbs : ℤ) = q.num := by
rw [Int.natCast_natAbs, abs_of_pos hnum]
have habs : (q.num.natAbs : ℝ) = (q.num : ℝ) := by
simpa only [Int.cast_natCast] using congrArg (fun z : ℤ => (z : ℝ)) habsI
have hden : (q.den : ℝ) ≠ 0 := by
exact_mod_cast q.den_nz
have hratio :
Real.log 4 / Real.log 3 = (q.num : ℝ) / (q.den : ℝ) := by
rw [← hq, Rat.cast_def]
have hcross := (div_eq_div_iff (ne_of_gt hlog3) hden).mp hratio
have hlogs : Real.log ((4 : ℝ) ^ q.den) = Real.log ((3 : ℝ) ^ q.num.natAbs) := by
rw [Real.log_pow, Real.log_pow, habs]
nlinarith
have hrealpow : (4 : ℝ) ^ q.den = (3 : ℝ) ^ q.num.natAbs :=
Real.log_injOn_pos (by exact pow_pos (by norm_num : (0 : ℝ) < 4) q.den)
(by exact pow_pos (by norm_num : (0 : ℝ) < 3) q.num.natAbs) hlogs
have hpow : (4 : ℕ) ^ q.den = (3 : ℕ) ^ q.num.natAbs := by
exact_mod_cast hrealpow
have hdiv : 2 ∣ (4 : ℕ) ^ q.den := by
obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero q.den_nz
rw [hk, pow_succ]
exact ⟨2 * 4 ^ k, by ring⟩
rw [hpow] at hdiv
have hbad := Nat.prime_two.dvd_of_dvd_pow hdiv
norm_num at hbad
end Bounty
end SubmissionComponent_Solution
/- Component GridWork; SHA256 f152ca58e05da7e36dc3f63f1fb16436c60d2532669012b1b49e753b86708bb9 -/
section SubmissionComponent_GridWork
/- A row-counting proof of the two-dimensional fork-free bound. -/
namespace Bounty
def GridForkFree (A : Finset (ℕ × ℕ)) : Prop :=
∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a ≠ b → a ≠ c →
a.1 ≤ b.1 → a.2 ≤ b.2 → a.1 ≤ c.1 → a.2 ≤ c.2 → b = c
def gridRow (A : Finset (ℕ × ℕ)) (y : ℕ) : Finset (ℕ × ℕ) :=
A.filter (fun a => a.2 = y)
def gridRow_card_le_two {A : Finset (ℕ × ℕ)} (hA : GridForkFree A) (y : ℕ) :
(gridRow A y).card ≤ 2 := by
classical
by_cases hr : (gridRow A y).Nonempty
· let X := (gridRow A y).image Prod.fst
have hX : X.Nonempty := hr.image Prod.fst
obtain ⟨a, ha, hamin⟩ := Finset.mem_image.mp (Finset.min'_mem X hX)
have hay : a.2 = y := (Finset.mem_filter.mp ha).2
have hamin' : ∀ b ∈ gridRow A y, a.1 ≤ b.1 := by
intro b hb
rw [hamin]
exact Finset.min'_le X b.1 (Finset.mem_image_of_mem Prod.fst hb)
have he : ((gridRow A y).erase a).card ≤ 1 := by
apply Finset.card_le_one.mpr
intro b hb c hc
obtain ⟨hba, hbr⟩ := Finset.mem_erase.mp hb
obtain ⟨hca, hcr⟩ := Finset.mem_erase.mp hc
have hby : b.2 = y := (Finset.mem_filter.mp hbr).2
have hcy : c.2 = y := (Finset.mem_filter.mp hcr).2
exact hA a (Finset.mem_filter.mp ha).1 b (Finset.mem_filter.mp hbr).1
c (Finset.mem_filter.mp hcr).1 hba.symm hca.symm
(hamin' b hbr) (by omega) (hamin' c hcr) (by omega)
have hcard := Finset.card_erase_add_one ha
omega
· have hempty : gridRow A y = ∅ := Finset.not_nonempty_iff_eq_empty.mp hr
simp [hempty]
def grid_forbidden_upper {A : Finset (ℕ × ℕ)} (hA : GridForkFree A)
{a b c : ℕ × ℕ} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A)
(habrow : a.2 = b.2) (habcol : a.1 < b.1)
(haccol : a.1 ≤ c.1) (hacrow : a.2 < c.2) : False := by
have hab : a ≠ b := by
intro h
subst b
omega
have hac : a ≠ c := by
intro h
subst c
omega
have hbc := hA a ha b hb c hc hab hac habcol.le
(by omega) haccol hacrow.le
have := congrArg Prod.snd hbc
omega
def grid_above_pair_left {A : Finset (ℕ × ℕ)} (hA : GridForkFree A)
{a b c : ℕ × ℕ} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A)
(hab : a ≠ b) (habrow : a.2 = b.2) (hacrow : a.2 < c.2) :
c.1 < a.1 ∧ c.1 < b.1 := by
have habcol : a.1 ≠ b.1 := by
intro h
exact hab (Prod.ext h habrow)
by_cases hlt : a.1 < b.1
· have h : c.1 < a.1 := by
by_contra hh
exact grid_forbidden_upper hA ha hb hc habrow hlt (by omega) hacrow
omega
· have h : c.1 < b.1 := by
by_contra hh
exact grid_forbidden_upper hA hb ha hc habrow.symm (by omega) (by omega) (by omega)
omega
def gridRows (A : Finset (ℕ × ℕ)) : Finset ℕ := A.image Prod.snd
def gridDoubleRows (A : Finset (ℕ × ℕ)) : Finset ℕ :=
(gridRows A).filter (fun y => (gridRow A y).card = 2)
def gridDoubles (A : Finset (ℕ × ℕ)) : Finset (ℕ × ℕ) :=
A.filter (fun a => (gridRow A a.2).card = 2)
def gridDoubles_fst_injective {A : Finset (ℕ × ℕ)} (hA : GridForkFree A) :
Set.InjOn Prod.fst (gridDoubles A : Set (ℕ × ℕ)) := by
intro a ha b hb hfst
have haA := (Finset.mem_filter.mp ha).1
have hbA := (Finset.mem_filter.mp hb).1
by_cases hrow : a.2 = b.2
· exact Prod.ext hfst hrow
· by_cases hlt : a.2 < b.2
· have hcard := (Finset.mem_filter.mp ha).2
obtain ⟨c, hc, hca⟩ := Finset.exists_mem_ne (show 1 < (gridRow A a.2).card by omega) a
have hcA := (Finset.mem_filter.mp hc).1
have hcy := (Finset.mem_filter.mp hc).2
have h := grid_above_pair_left hA haA hcA hbA hca.symm (by omega) hlt
omega
· have hcard := (Finset.mem_filter.mp hb).2
obtain ⟨c, hc, hcb⟩ := Finset.exists_mem_ne (show 1 < (gridRow A b.2).card by omega) b
have hcA := (Finset.mem_filter.mp hc).1
have hcy := (Finset.mem_filter.mp hc).2
have h := grid_above_pair_left hA hbA hcA haA hcb.symm (by omega) (by omega)
omega
def grid_card_decomposition {A : Finset (ℕ × ℕ)} (hA : GridForkFree A) :
A.card = (gridRows A).card + (gridDoubleRows A).card := by
have hcard : A.card = ∑ y ∈ gridRows A, (gridRow A y).card := by
simpa [gridRows, gridRow] using Finset.card_eq_sum_card_image Prod.snd A
rw [hcard]
calc
(∑ y ∈ gridRows A, (gridRow A y).card) =
∑ y ∈ gridRows A, (1 + if (gridRow A y).card = 2 then 1 else 0) := by
apply Finset.sum_congr rfl
intro y hy
have hupper := gridRow_card_le_two hA y
have hlower : 0 < (gridRow A y).card := by
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hy
apply Finset.card_pos.mpr
exact ⟨a, Finset.mem_filter.mpr ⟨ha, rfl⟩⟩
split_ifs <;> omega
_ = (gridRows A).card + (gridDoubleRows A).card := by
simp [Finset.sum_add_distrib, gridDoubleRows]
def gridDoubles_card (A : Finset (ℕ × ℕ)) :
(gridDoubles A).card = 2 * (gridDoubleRows A).card := by
have hfilter :
A.filter (fun a => a.2 ∈ gridDoubleRows A) = gridDoubles A := by
ext a
simp only [Finset.mem_filter, gridDoubleRows, gridDoubles]
constructor
· intro h
exact ⟨h.1, h.2.2⟩
· intro h
exact ⟨h.1, Finset.mem_image_of_mem Prod.snd h.1, h.2⟩
have hsum := Finset.sum_card_fiberwise_eq_card_filter A (gridDoubleRows A) Prod.snd
rw [hfilter] at hsum
calc
(gridDoubles A).card = ∑ y ∈ gridDoubleRows A, (gridRow A y).card := hsum.symm
_ = ∑ _y ∈ gridDoubleRows A, 2 := by
apply Finset.sum_congr rfl
intro y hy
exact (Finset.mem_filter.mp hy).2
_ = 2 * (gridDoubleRows A).card := by simp [Nat.mul_comm]Provenance