-- Mathlib/Data/Multiset/Count.lean
theorem Rel.countP_eq (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t : Multiset α} (x : α)
    [DecidablePred (r x)] (h : Rel r s t) : countP (r x) s = countP (r x) t

Proof state:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0

Tactic:
simp only [decide_eq_true_eq, Nat.add_right_inj]

Result:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (if r x y then 1 else 0) = if r x b then 1 else 0

Proof state:
case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) t

Tactic:
rw [rel_zero_left.mp h]

Result:
no goals

Proof state:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (if r x y then 1 else 0) = if r x b then 1 else 0

Tactic:
exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h : Rel r s t
⊢ countP (r x) s = countP (r x) t

Tactic:
induction' s using Multiset.induction_on with y s ih generalizing t

Result:
case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) t

case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
⊢ countP (r x) (y ::ₘ s) = countP (r x) t

Proof state:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
⊢ countP (r x) (y ::ₘ s) = countP (r x) t

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h

Result:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)

Proof state:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)

Tactic:
rw [countP_cons, countP_cons, ih hb2]

Result:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0