-- Mathlib/Data/Nat/Count.lean
theorem count_add (a b : ℕ) : count p (a + b) = count p a + count (fun k ↦ p (a + k)) b

Proof state:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) (range b))

Tactic:
rw [Finset.disjoint_left]

Result:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → a_1 ∉ map (addLeftEmbedding a) (range b)

Proof state:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 < b, a + a_3 = a_1

Tactic:
rintro x hx ⟨c, _, rfl⟩

Result:
case a.intro.intro
p : ℕ → Prop
inst✝ : DecidablePred p
a b c : ℕ
left✝ : c < b
hx : a + c < a
⊢ False

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b

Tactic:
have : Disjoint {x ∈ range a | p x} {x ∈ (range b).map <| addLeftEmbedding a | p x} := by
  apply disjoint_filter_filter
  rw [Finset.disjoint_left]
  simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
  rintro x hx ⟨c, _, rfl⟩
  exact (self_le_add_right _ _).not_lt hx

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter (fun x => p x) (range a)) (filter (fun x => p x) (map (addLeftEmbedding a) (range b)))
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter (fun x => p x) (range a)) (filter (fun x => p x) (map (addLeftEmbedding a) (range b)))
⊢ #(filter (fun x => p x) (range a)) + #(filter ((fun x => p x) ∘ ⇑{ toFun := fun h => a + h, inj' := ⋯ }) (range b)) =
    #(filter (fun x => p x) (range a)) + #(filter (fun x => p (a + x)) (range b))

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter (fun x => p x) (range a)) (filter (fun x => p x) (map (addLeftEmbedding a) (range b)))
⊢ count p (a + b) = count p a + count (fun k => p (a + k)) b

Tactic:
simp_rw [count_eq_card_filter_range, range_add, filter_union, card_union_of_disjoint this,
  filter_map, addLeftEmbedding, card_map]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
this : Disjoint (filter (fun x => p x) (range a)) (filter (fun x => p x) (map (addLeftEmbedding a) (range b)))
⊢ #(filter (fun x => p x) (range a)) + #(filter ((fun x => p x) ∘ ⇑{ toFun := fun h => a + h, inj' := ⋯ }) (range b)) =
    #(filter (fun x => p x) (range a)) + #(filter (fun x => p (a + x)) (range b))

Proof state:
case a.intro.intro
p : ℕ → Prop
inst✝ : DecidablePred p
a b c : ℕ
left✝ : c < b
hx : a + c < a
⊢ False

Tactic:
exact (self_le_add_right _ _).not_lt hx

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (filter (fun x => p x) (range a)) (filter (fun x => p x) (map (addLeftEmbedding a) (range b)))

Tactic:
apply disjoint_filter_filter

Result:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) (range b))

Proof state:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → a_1 ∉ map (addLeftEmbedding a) (range b)

Tactic:
simp_rw [mem_map, mem_range, addLeftEmbedding_apply]

Result:
case a
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 < b, a + a_3 = a_1