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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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✝

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
State after:
no goals

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
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

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
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✝

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
State after:
no goals

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, _⟩
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

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
State after:
no goals

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
State after:
no goals

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
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✝)

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
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✝

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
State after:
no goals

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
State after:
no goals

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
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✝

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]
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

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
State after:
no goals

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
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✝

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
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✝

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
State after:
no goals