Theorem: Multiset.find?_eq_none (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false
Tactic:
have ⟨L,hL⟩ := xs.exists_rep
State after:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false

State before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false
Tactic:
cases hL
State after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ find? f ⟦L⟧ h = none ↔ ∀ x ∈ ⟦L⟧, f x = false

State before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ find? f ⟦L⟧ h = none ↔ ∀ x ∈ ⟦L⟧, f x = false
Tactic:
simp only [find?, Quotient.lift_mk, List.find?_eq_none, Bool.not_eq_true]
State after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ (∀ x ∈ L, f x = false) ↔ ∀ x ∈ ⟦L⟧, f x = false

State before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ (∀ x ∈ L, f x = false) ↔ ∀ x ∈ ⟦L⟧, f x = false
Tactic:
simp only [quot_mk_to_coe, mem_coe]
State after:
no goals