case empty
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t u✝ : Multiset α
r1✝ : Rel r s✝ t
r2✝ : Rel r t u✝
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u

case cons
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t✝ u✝ : Multiset α
r1✝ : Rel r s✝ t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u
induction' t using Multiset.induction_on with x t ih generalizing s u
no goals
case empty
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t u✝ : Multiset α
r1✝ : Rel r s✝ t
r2✝ : Rel r t u✝
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u
rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u✝ : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u
case cons
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t✝ u✝ : Multiset α
r1✝ : Rel r s✝ t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
case cons.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)
case cons.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u✝ : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
no goals
case cons.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.476292
γ : Type ?u.476295
δ : Type ?u.476298
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)