Theorem: Multiset.exists_intermediate (LeanCamCombi/Mathlib/Data/Multiset/Basic.lean)

State before:
α : Type u_1
s t : Multiset α
n : ℕ
hst : s ≤ t
hs : card s ≤ n
ht : n ≤ card t
⊢ ∃ u, s ≤ u ∧ u ≤ t ∧ card u = n
Tactic:
induction' s using Quotient.inductionOn with l₀
State after:
case h
α : Type u_1
s t : Multiset α
n : ℕ
ht : n ≤ card t
l₀ : List α
hst : ⟦l₀⟧ ≤ t
hs : card ⟦l₀⟧ ≤ n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ t ∧ card u = n

State before:
case h
α : Type u_1
s t : Multiset α
n : ℕ
ht : n ≤ card t
l₀ : List α
hst : ⟦l₀⟧ ≤ t
hs : card ⟦l₀⟧ ≤ n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ t ∧ card u = n
Tactic:
induction' t using Quotient.inductionOn with l₂
State after:
case h.h
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n

State before:
case h.h
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Tactic:
obtain ⟨l₁, h⟩ := hst.exists_intermediate hs ht
State after:
case h.h.intro
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
l₁ : List α
h : l₀.Subperm l₁ ∧ l₁.Subperm l₂ ∧ l₁.length = n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n

State before:
case h.h.intro
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
l₁ : List α
h : l₀.Subperm l₁ ∧ l₁.Subperm l₂ ∧ l₁.length = n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
Tactic:
exact ⟨l₁, h⟩
State after:
no goals