α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x
rw [lt_iff_cons_le]
case mp
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
constructor
case mp.intro
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x
case mp
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
rintro ⟨x', hx'⟩
case mp.intro
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
case mp.intro
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x
have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
no goals
case mp.intro
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
rwa [this, replicate_succ, cons_le_cons_iff] at hx'
case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x
case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
intro h
case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x
rw [replicate_succ]
no goals
case mpr
α : Type u_1
β : Type ?u.93086
γ : Type ?u.93089
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
exact ⟨x, cons_le_cons _ h⟩