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

State before:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ countelements A (n - 1) = countelements A n
Tactic:
repeat rw [countelements]
State after:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = (filter (fun x => x ∈ A) (Icc 1 n)).card

State before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 n)).card ≤ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card
Tactic:
refine card_le_card fun x hx ↦ ?_
State after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ filter (fun x => x ∈ A) (Icc 1 (n - 1))

State before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ filter (fun x => x ∈ A) (Icc 1 (n - 1))
Tactic:
rw [mem_filter]
State after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A

State before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Tactic:
rw [mem_filter, mem_Icc] at hx
State after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A

State before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Tactic:
refine ⟨mem_Icc.2 ⟨hx.1.1, Nat.le_pred_of_lt $ hx.1.2.lt_of_ne ?_⟩, hx.2⟩
State after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ≠ n

State before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ≠ n
Tactic:
rintro rfl
State after:
case refine_2
A B : Set ℕ
x : ℕ
hn : x ∉ A
hx : (1 ≤ x ∧ x ≤ x) ∧ x ∈ A
⊢ False

State before:
case refine_2
A B : Set ℕ
x : ℕ
hn : x ∉ A
hx : (1 ≤ x ∧ x ≤ x) ∧ x ∈ A
⊢ False
Tactic:
exact hn hx.2
State after:
no goals

State before:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = countelements A n
Tactic:
rw [countelements]
State after:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = (filter (fun x => x ∈ A) (Icc 1 n)).card

State before:
case refine_1
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ n - 1 ≤ n
Tactic:
simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one]
State after:
no goals