internlm/Lean-Github huggingface dataset:
Theorem: List.mem_fold_union_iff
Proof state before:
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l ↔ ∃ s ∈ l, e ∈ s
Tactic:
constructor
Proof state after:
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l → ∃ s ∈ l, e ∈ s

case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Theorem: List.mem_fold_union_iff
Proof state before:
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l → ∃ s ∈ l, e ∈ s

case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Tactic:
. intro h
  induction l with
  | nil => contradiction
  | cons _ _ ih =>
    simp at h
    cases h <;> simp
    . apply Or.inl
      assumption
    . apply Or.inr
      apply ih
      assumption
Proof state after:
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Tactic:
. intro ⟨s, h, _⟩
  induction l with
  | nil => contradiction
  | cons _ _ ih =>
    simp at h
    cases h <;> simp
    case inl h =>
      apply Or.inl; rw [<- h]
      assumption
    case inr _ =>
      apply Or.inr
      apply ih
      assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l → ∃ s ∈ l, e ∈ s
Tactic:
intro h
Proof state after:
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
h : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
⊢ ∃ s ∈ l, e ∈ s
Theorem: List.mem_fold_union_iff
Proof state before:
case mp
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
h : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
⊢ ∃ s ∈ l, e ∈ s
Tactic:
induction l with
| nil => contradiction
| cons _ _ ih =>
  simp at h
  cases h <;> simp
  . apply Or.inl
    assumption
  . apply Or.inr
    apply ih
    assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.nil
β : Type u_1
inst✝ : DecidableEq β
e : β
h : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ []
⊢ ∃ s ∈ [], e ∈ s
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)
⊢ ∃ s ∈ head✝ :: tail✝, e ∈ s
Tactic:
simp at h
Proof state after:
case mp.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h : e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ s ∈ head✝ :: tail✝, e ∈ s
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h : e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ s ∈ head✝ :: tail✝, e ∈ s
Tactic:
cases h <;> simp
Proof state after:
case mp.cons.inl
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ head✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a

case mp.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inl
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ head✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a

case mp.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Tactic:
. apply Or.inl
  assumption
Proof state after:
case mp.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Tactic:
. apply Or.inr
  apply ih
  assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inl
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ head✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Tactic:
apply Or.inl
Proof state after:
case mp.cons.inl.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ head✝
⊢ e ∈ head✝
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inl.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ head✝
⊢ e ∈ head✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ head✝ ∨ ∃ a ∈ tail✝, e ∈ a
Tactic:
apply Or.inr
Proof state after:
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ a ∈ tail✝, e ∈ a
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ ∃ a ∈ tail✝, e ∈ a
Tactic:
apply ih
Proof state after:
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Theorem: List.mem_fold_union_iff
Proof state before:
case mp.cons.inr.h
β : Type u_1
inst✝ : DecidableEq β
e : β
head✝ : Finset β
tail✝ : List (Finset β)
ih : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝ → ∃ s ∈ tail✝, e ∈ s
h✝ : e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
⊢ (∃ s ∈ l, e ∈ s) → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Tactic:
intro ⟨s, h, _⟩
Proof state after:
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
s : Finset β
h : s ∈ l
right✝ : e ∈ s
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_1
inst✝ : DecidableEq β
e : β
l : List (Finset β)
s : Finset β
h : s ∈ l
right✝ : e ∈ s
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ l
Tactic:
induction l with
| nil => contradiction
| cons _ _ ih =>
  simp at h
  cases h <;> simp
  case inl h =>
    apply Or.inl; rw [<- h]
    assumption
  case inr _ =>
    apply Or.inr
    apply ih
    assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr.nil
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
h : s ∈ []
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ []
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s ∈ head✝ :: tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)
Tactic:
simp at h
Proof state after:
case mpr.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝ ∨ s ∈ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)
Theorem: List.mem_fold_union_iff
Proof state before:
case mpr.cons
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝ ∨ s ∈ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ (head✝ :: tail✝)
Tactic:
cases h <;> simp
Proof state after:
case mpr.cons.inl
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s = head✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝

case mpr.cons.inr
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Theorem: List.mem_fold_union_iff
Proof state before:
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
case inl h =>
  apply Or.inl; rw [<- h]
  assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
case inr _ =>
  apply Or.inr
  apply ih
  assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
apply Or.inl
Proof state after:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ head✝
Theorem: List.mem_fold_union_iff
Proof state before:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ head✝
Tactic:
rw [<- h]
Proof state after:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ s
Theorem: List.mem_fold_union_iff
Proof state before:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h : s = head✝
⊢ e ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fold_union_iff
Proof state before:
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ e ∈ head✝ ∨ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
apply Or.inr
Proof state after:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Theorem: List.mem_fold_union_iff
Proof state before:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
Tactic:
apply ih
Proof state after:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ s ∈ tail✝
Theorem: List.mem_fold_union_iff
Proof state before:
case h
β : Type u_1
inst✝ : DecidableEq β
e : β
s : Finset β
right✝ : e ∈ s
head✝ : Finset β
tail✝ : List (Finset β)
ih : s ∈ tail✝ → e ∈ foldr (fun x x_1 => x ∪ x_1) ∅ tail✝
h✝ : s ∈ tail✝
⊢ s ∈ tail✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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 }
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof state after:
no goals
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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
Theorem: Finset.mem_fold_union_iff
Proof 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]
Proof 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✝
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof 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✝
Theorem: Finset.mem_fold_union_iff
Proof 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 }
Proof state after:
no goals
Theorem: Finset.mem_fold_union_iff
Proof 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
Proof state after:
no goals
Theorem: Finset.mem_fold_union_iff
Proof 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₂⟩
Proof 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