case empty
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s t✝
t : Multiset α
h : Rel r 0 t
⊢ countp (r x) 0 = countp (r x) t

case cons
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t✝
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
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
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
induction' s using Multiset.induction_on with y s ih generalizing t
no goals
case empty
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s t✝
t : Multiset α
h : Rel r 0 t
⊢ countp (r x) 0 = countp (r x) t
rw [rel_zero_left.mp h]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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)
case cons
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t✝
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
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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)
rw [countp_cons, countp_cons, ih hb2]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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
simp only [decide_eq_true_eq, add_right_inj]
no goals
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476873
γ : Type ?u.476876
δ : Type ?u.476879
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
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
refine' (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)