Theorem: Aux.conv_lambda_sq_larger_sum (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
apply sum_congr rfl
State after:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then f d1 d2 x else 0) =
      ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then f d1 d2 x else 0

State before:
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then f d1 d2 x else 0) =
      ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then f d1 d2 x else 0
Tactic:
intro d hd
State after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∈ n.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

State before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∈ n.divisors
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
rw [mem_divisors] at hd
State after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

State before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
simp_rw [←Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ←ite_and, ite_sum_zero, ←ite_and]
State after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

State before:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr with d1
State after:
case e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 : ℕ
⊢ (∑ x ∈ n.divisors, if d1 ∣ d ∧ x ∣ d ∧ d = d1.lcm x then f d1 x d else 0) =
    ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

State before:
case e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 : ℕ
⊢ (∑ x ∈ n.divisors, if d1 ∣ d ∧ x ∣ d ∧ d = d1.lcm x then f d1 x d else 0) =
    ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr with d2
State after:
case e_f.h.e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (if d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 then f d1 d2 d else 0) = if d = d1.lcm d2 then f d1 d2 d else 0

State before:
case e_f.h.e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (if d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 then f d1 d2 d else 0) = if d = d1.lcm d2 then f d1 d2 d else 0
Tactic:
congr
State after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)

State before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
Tactic:
rw [eq_iff_iff]
State after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 ↔ d = d1.lcm d2

State before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 ↔ d = d1.lcm d2
Tactic:
refine ⟨fun ⟨_, _, h⟩ ↦ h, ?_⟩
State after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d = d1.lcm d2 → d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2

State before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d = d1.lcm d2 → d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2
Tactic:
rintro rfl
State after:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d1 d2 : ℕ
hd : d1.lcm d2 ∣ n ∧ n ≠ 0
⊢ d1 ∣ d1.lcm d2 ∧ d2 ∣ d1.lcm d2 ∧ d1.lcm d2 = d1.lcm d2

State before:
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d1 d2 : ℕ
hd : d1.lcm d2 ∣ n ∧ n ≠ 0
⊢ d1 ∣ d1.lcm d2 ∧ d2 ∣ d1.lcm d2 ∧ d1.lcm d2 = d1.lcm d2
Tactic:
exact ⟨Nat.dvd_lcm_left d1 d2, Nat.dvd_lcm_right d1 d2, rfl⟩
State after:
no goals