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

State before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
xs : Multiset α
⊢ find? f xs h = some x ↔ x ∈ xs ∧ f x = true
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
x : α
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = some x ↔ x ∈ xs ∧ f x = true

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

State before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ find? f ⟦L⟧ h = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Tactic:
simp [-quot_mk_to_coe, find?]
State after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ ⟦L⟧ ∧ f x = true

State before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Tactic:
simp
State after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ L ∧ f x = true

State before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ L ∧ f x = true
Tactic:
constructor
State after:
case refl.mp
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x → x ∈ L ∧ f x = true

case refl.mpr
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ x ∈ L ∧ f x = true → List.find? f L = some x

State before:
case refl.mp
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x → x ∈ L ∧ f x = true
Tactic:
intro h
State after:
case refl.mp
α : Type u_1
f : α → Bool
h✝ : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h : List.find? f L = some x
⊢ x ∈ L ∧ f x = true

State before:
case refl.mp
α : Type u_1
f : α → Bool
h✝ : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h : List.find? f L = some x
⊢ x ∈ L ∧ f x = true
Tactic:
simp [List.find?_some h, List.find?_mem h]
State after:
no goals

State before:
case refl.mpr
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ x ∈ L ∧ f x = true → List.find? f L = some x
Tactic:
rintro ⟨h1,h2⟩
State after:
case refl.mpr.intro
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h1 : x ∈ L
h2 : f x = true
⊢ List.find? f L = some x

State before:
case refl.mpr.intro
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h1 : x ∈ L
h2 : f x = true
⊢ List.find? f L = some x
Tactic:
induction h1 <;> simp [List.find?, *]
State after:
case refl.mpr.intro.tail
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
⊢ (match f b✝ with
    | true => some b✝
    | false => some x) =
    some x

State before:
case refl.mpr.intro.tail
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
⊢ (match f b✝ with
    | true => some b✝
    | false => some x) =
    some x
Tactic:
split
State after:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ some b✝ = some x

case refl.mpr.intro.tail.h_2
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = false
⊢ some x = some x

State before:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ some b✝ = some x
Tactic:
simp
State after:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ b✝ = x

State before:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ b✝ = x
Tactic:
apply h <;> assumption
State after:
no goals

State before:
case refl.mpr.intro.tail.h_2
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = false
⊢ some x = some x
Tactic:
rfl
State after:
no goals