Theorem: sum_schnirelmannDensity_ge_one_sumset_nat (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ A + B = Set.univ
Tactic:
refine Set.eq_univ_of_forall $ fun n ↦ sumset_contains_n hA hB ?_
State after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
⊢ n ≤ countelements A n + countelements B n

State before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
⊢ n ≤ countelements A n + countelements B n
Tactic:
obtain rfl | hn := eq_or_ne n 0
State after:
case inl
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ≤ countelements A 0 + countelements B 0

case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n

State before:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n
Tactic:
rw [← Nat.cast_le (α := ℝ), ← one_le_div (by positivity)]
State after:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑(countelements A n + countelements B n) / ↑n

State before:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑(countelements A n + countelements B n) / ↑n
Tactic:
calc
  _ ≤ _ := hAB
  _ ≤ _ := add_le_add (schnirelmannDensity_le_div hn) (schnirelmannDensity_le_div hn)
  _ = _ := by push_cast; rw [add_div]; rfl
State after:
no goals

State before:
case inl
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ≤ countelements A 0 + countelements B 0
Tactic:
exact countelements_nonneg A 0
State after:
no goals

State before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n
Tactic:
positivity
State after:
no goals

State before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n + countelements B n) / ↑n
Tactic:
push_cast
State after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    (↑(countelements A n) + ↑(countelements B n)) / ↑n

State before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    (↑(countelements A n) + ↑(countelements B n)) / ↑n
Tactic:
rw [add_div]
State after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n) / ↑n + ↑(countelements B n) / ↑n

State before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n) / ↑n + ↑(countelements B n) / ↑n
Tactic:
rfl
State after:
no goals