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

State before:
l m : ℕ
hm : Squarefree m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
have hm_pos : 0 < m := Nat.pos_of_ne_zero $ Squarefree.ne_zero hm
State after:
l m : ℕ
hm : Squarefree m
hm_pos : 0 < m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0

State before:
l m : ℕ
hm : Squarefree m
hm_pos : 0 < m
⊢ (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
revert hm
State after:
l m : ℕ
hm_pos : 0 < m
⊢ Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0

State before:
l m : ℕ
hm_pos : 0 < m
⊢ Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
revert m
State after:
l : ℕ
⊢ ∀ (m : ℕ), 0 < m → Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0

State before:
l : ℕ
⊢ ∀ (m : ℕ), 0 < m → Squarefree m → (∑ d ∈ m.divisors, if l ∣ d then μ d else 0) = if l = m then μ l else 0
Tactic:
apply (ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on {n | Squarefree n} (fun _ _ => Squarefree.squarefree_of_dvd)).mpr
State after:
l : ℕ
⊢ ∀ n > 0,
    n ∈ {n | Squarefree n} →
      (∑ x ∈ n.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ n then μ n else 0

State before:
l : ℕ
⊢ ∀ n > 0,
    n ∈ {n | Squarefree n} →
      (∑ x ∈ n.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ n then μ n else 0
Tactic:
intro m hm_pos hm
State after:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ x ∈ m.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ m then μ m else 0

State before:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ x ∈ m.divisorsAntidiagonal, μ x.1 • if l = x.2 then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [sum_divisorsAntidiagonal' (f:= fun x y => μ x • if l=y then μ l else 0)]
State after:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0

State before:
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
by_cases hl : l ∣ m
State after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0

case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0

State before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [if_pos hl, sum_eq_single l]
State after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m

case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ ∀ b ∈ m.divisors, b ≠ l → (μ (m / b) • if l = b then μ l else 0) = 0

case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ l ∉ m.divisors → (μ (m / l) • if l = l then μ l else 0) = 0

State before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m
Tactic:
have hmul : m / l * l = m := Nat.div_mul_cancel hl
State after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m

State before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (μ (m / l) • if l = l then μ l else 0) = μ m
Tactic:
rw [if_pos rfl, smul_eq_mul, ←isMultiplicative_moebius.map_mul_of_coprime,
  hmul]
State after:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (m / l).Coprime l

State before:
case pos
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ (m / l).Coprime l
Tactic:
apply coprime_of_squarefree_mul
State after:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree (m / l * l)

State before:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree (m / l * l)
Tactic:
rw [hmul]
State after:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree m

State before:
case pos.h
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
hmul : m / l * l = m
⊢ Squarefree m
Tactic:
exact hm
State after:
no goals

State before:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ ∀ b ∈ m.divisors, b ≠ l → (μ (m / b) • if l = b then μ l else 0) = 0
Tactic:
intro d _ hdl
State after:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
d : ℕ
a✝ : d ∈ m.divisors
hdl : d ≠ l
⊢ (μ (m / d) • if l = d then μ l else 0) = 0

State before:
case pos.h₀
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
d : ℕ
a✝ : d ∈ m.divisors
hdl : d ≠ l
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Tactic:
rw[if_neg $ hdl.symm, smul_zero]
State after:
no goals

State before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
⊢ l ∉ m.divisors → (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
intro h
State after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : l ∉ m.divisors
⊢ (μ (m / l) • if l = l then μ l else 0) = 0

State before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : l ∉ m.divisors
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
rw[mem_divisors] at h
State after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ (μ (m / l) • if l = l then μ l else 0) = 0

State before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ (μ (m / l) • if l = l then μ l else 0) = 0
Tactic:
exfalso
State after:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ False

State before:
case pos.h₁
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : l ∣ m
h : ¬(l ∣ m ∧ m ≠ 0)
⊢ False
Tactic:
exact h ⟨hl, (Nat.ne_of_lt hm_pos).symm⟩
State after:
no goals

State before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ (∑ i ∈ m.divisors, μ (m / i) • if l = i then μ l else 0) = if l ∣ m then μ m else 0
Tactic:
rw [if_neg hl, sum_eq_zero]
State after:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ ∀ x ∈ m.divisors, (μ (m / x) • if l = x then μ l else 0) = 0

State before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
⊢ ∀ x ∈ m.divisors, (μ (m / x) • if l = x then μ l else 0) = 0
Tactic:
intro d hd
State after:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ (μ (m / d) • if l = d then μ l else 0) = 0

State before:
case neg
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ (μ (m / d) • if l = d then μ l else 0) = 0
Tactic:
rw [if_neg, smul_zero]
State after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ ¬l = d

State before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
⊢ ¬l = d
Tactic:
by_contra h
State after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
h : l = d
⊢ False

State before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : d ∈ m.divisors
h : l = d
⊢ False
Tactic:
rw [←h] at hd
State after:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : l ∈ m.divisors
h : l = d
⊢ False

State before:
case neg.hnc
l m : ℕ
hm_pos : m > 0
hm : m ∈ {n | Squarefree n}
hl : ¬l ∣ m
d : ℕ
hd : l ∈ m.divisors
h : l = d
⊢ False
Tactic:
exact hl (dvd_of_mem_divisors hd)
State after:
no goals