Theorem: Finset.mem_fold_union_iff (FormalSystems/Preliminaries/Fold.lean)

State before:
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ e ∈ fold Union.union ∅ f s ↔ ∃ x ∈ s, e ∈ f x
Tactic:
constructor
State after:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ e ∈ fold Union.union ∅ f s → ∃ x ∈ s, e ∈ f x

case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s

State before:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ e ∈ fold Union.union ∅ f s → ∃ x ∈ s, e ∈ f x

case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s
Tactic:
. have ⟨s, _⟩ := s
  revert s
  apply Quot.ind
  intro l _ h
  dsimp [Finset.fold] at h
  have ⟨_, h, _⟩ := List.mem_fold_union_iff.mp h
  simp at h
  have ⟨x, _, h⟩ := h
  exists x; simp [h]
  constructor; repeat { assumption }
State after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s

State before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s
Tactic:
. intro ⟨x, h₁, h₂⟩
  have ⟨s, _⟩ := s
  revert s
  apply Quot.ind
  intro l _ h
  simp [Finset.fold, Multiset.fold]
  apply List.mem_fold_union_iff.mpr
  exists f x
  simp; constructor
  exists x
  assumption
State after:
no goals

State before:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ e ∈ fold Union.union ∅ f s → ∃ x ∈ s, e ∈ f x
Tactic:
have ⟨s, _⟩ := s
State after:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
s : Multiset α
nodup✝ : Multiset.Nodup s
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ } → ∃ x ∈ { val := s, nodup := nodup✝ }, e ∈ f x

State before:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
s : Multiset α
nodup✝ : Multiset.Nodup s
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ } → ∃ x ∈ { val := s, nodup := nodup✝ }, e ∈ f x
Tactic:
revert s
State after:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    e ∈ fold Union.union ∅ f { val := s, nodup := nodup } → ∃ x ∈ { val := s, nodup := nodup }, e ∈ f x

State before:
case mp
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    e ∈ fold Union.union ∅ f { val := s, nodup := nodup } → ∃ x ∈ { val := s, nodup := nodup }, e ∈ f x
Tactic:
apply Quot.ind
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup } →
      ∃ x ∈ { val := Quot.mk Setoid.r a, nodup := nodup }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup } →
      ∃ x ∈ { val := Quot.mk Setoid.r a, nodup := nodup }, e ∈ f x
Tactic:
intro l _ h
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
Tactic:
dsimp [Finset.fold] at h
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : e ∈ List.foldr Union.union ∅ (List.map f l)
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : e ∈ List.foldr Union.union ∅ (List.map f l)
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
Tactic:
have ⟨_, h, _⟩ := List.mem_fold_union_iff.mp h
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
h : w✝ ∈ List.map f l
right✝ : e ∈ w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
h : w✝ ∈ List.map f l
right✝ : e ∈ w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
Tactic:
simp at h
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h : ∃ a ∈ l, f a = w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h : ∃ a ∈ l, f a = w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
Tactic:
have ⟨x, _, h⟩ := h
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
Tactic:
exists x
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ } ∧ e ∈ f x

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ } ∧ e ∈ f x
Tactic:
simp [h]
State after:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ l ∧ e ∈ w✝

State before:
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ l ∧ e ∈ w✝
Tactic:
constructor
State after:
case mp.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ l

case mp.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ e ∈ w✝

State before:
case mp.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ x ∈ l

case mp.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ e ∈ w✝
Tactic:
repeat { assumption }
State after:
no goals

State before:
case mp.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝¹ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
right✝ : e ∈ w✝
h✝ : ∃ a ∈ l, f a = w✝
x : α
left✝ : x ∈ l
h : f x = w✝
⊢ e ∈ w✝
Tactic:
assumption
State after:
no goals

State before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
⊢ (∃ x ∈ s, e ∈ f x) → e ∈ fold Union.union ∅ f s
Tactic:
intro ⟨x, h₁, h₂⟩
State after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₁ : x ∈ s
h₂ : e ∈ f x
⊢ e ∈ fold Union.union ∅ f s

State before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₁ : x ∈ s
h₂ : e ∈ f x
⊢ e ∈ fold Union.union ∅ f s
Tactic:
have ⟨s, _⟩ := s
State after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
s : Multiset α
nodup✝ : Multiset.Nodup s
h₁ : x ∈ { val := s, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ }

State before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
s : Multiset α
nodup✝ : Multiset.Nodup s
h₁ : x ∈ { val := s, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ }
Tactic:
revert s
State after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    x ∈ { val := s, nodup := nodup } → e ∈ fold Union.union ∅ f { val := s, nodup := nodup }

State before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    x ∈ { val := s, nodup := nodup } → e ∈ fold Union.union ∅ f { val := s, nodup := nodup }
Tactic:
apply Quot.ind
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    x ∈ { val := Quot.mk Setoid.r a, nodup := nodup } →
      e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup }

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    x ∈ { val := Quot.mk Setoid.r a, nodup := nodup } →
      e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup }
Tactic:
intro l _ h
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }
Tactic:
simp [Finset.fold, Multiset.fold]
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ List.foldr Union.union ∅ (List.map f l)

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ List.foldr Union.union ∅ (List.map f l)
Tactic:
apply List.mem_fold_union_iff.mpr
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ s ∈ List.map f l, e ∈ s

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ s ∈ List.map f l, e ∈ s
Tactic:
exists f x
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ f x ∈ List.map f l ∧ e ∈ f x

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ f x ∈ List.map f l ∧ e ∈ f x
Tactic:
simp
State after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ (∃ a ∈ l, f a = f x) ∧ e ∈ f x

State before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ (∃ a ∈ l, f a = f x) ∧ e ∈ f x
Tactic:
constructor
State after:
case mpr.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ a ∈ l, f a = f x

case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x

State before:
case mpr.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ a ∈ l, f a = f x

case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Tactic:
exists x
State after:
case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x

State before:
case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Tactic:
assumption
State after:
no goals