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

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ fold (fun x x_1 => x ∪ x_1) ∅ f qa ⊆ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
apply Finset.subset_iff.mpr
State after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ ∀ ⦃x : β⦄, x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa → x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ ∀ ⦃x : β⦄, x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa → x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
intro _ h
State after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
apply Finset.mem_fold_union_iff.mpr
State after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ ∃ x ∈ qb, x✝ ∈ f x

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ ∃ x ∈ qb, x✝ ∈ f x
Tactic:
have ⟨x, _, _⟩ := Finset.mem_fold_union_iff.mp h
State after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ∃ x ∈ qb, x✝ ∈ f x

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ∃ x ∈ qb, x✝ ∈ f x
Tactic:
exists x
State after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb ∧ x✝ ∈ f x

State before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb ∧ x✝ ∈ f x
Tactic:
constructor
State after:
case left
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x

State before:
case left
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
apply Finset.mem_of_subset
State after:
case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ?left.s₁ ⊆ qb

case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ ?left.s₁

case left.s₁
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ Finset α

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x

State before:
case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ?left.s₁ ⊆ qb

case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ ?left.s₁

case left.s₁
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ Finset α

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
repeat { assumption }
State after:
no goals

State before:
case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
assumption
State after:
no goals