case refine'_1
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

case refine'_2
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m
refine' m.induction_on _ _
case refine'_1
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0
case refine'_1
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0
intros
no goals
case refine'_1
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0
apply Rel.zero
case refine'_2
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)
case refine'_2
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
intro a m ih h
no goals
case refine'_2
α : Type u_1
β : Type ?u.438879
γ : Type ?u.438882
δ : Type ?u.438885
r✝ : α → β → Prop
p : γ → δ → Prop
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)
exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))