Theorem: LO.Cumulative.finset_mem (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑u ⊆ T s
Tactic:
haveI := Classical.decEq
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
this : (α : Sort ?u.87136) → DecidableEq α
⊢ ∃ s, ↑u ⊆ T s

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
this : (α : Sort ?u.87136) → DecidableEq α
⊢ ∃ s, ↑u ⊆ T s
Tactic:
induction u using Finset.induction
State after:
case empty
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s

case insert
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
a✝² : F
s✝ : Finset F
a✝¹ : a✝² ∉ s✝
a✝ : ↑s✝ ⊆ ⋃ s, T s → ∃ s, ↑s✝ ⊆ T s
hu : ↑(insert a✝² s✝) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert a✝² s✝) ⊆ T s

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s
Tactic:
case empty => exact ⟨0, by simp⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : ↑(insert f u) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
case insert f u _ ih =>
  simp at hu
  have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
  rcases this with ⟨s, hs⟩
  have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
  rcases this with ⟨s', hs'⟩
  exact ⟨max s s', by
    simp; exact Set.insert_subset
      (subset_of_le H (Nat.le_max_right s s') hs')
      (subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s
Tactic:
exact ⟨0, by simp⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ↑∅ ⊆ T 0
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : ↑(insert f u) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
simp at hu
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
this : ∃ s, ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
this : ∃ s, ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
rcases this with ⟨s, hs⟩
State after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s

State before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
State after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
this : ∃ s', f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s

State before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
this : ∃ s', f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
rcases this with ⟨s', hs'⟩
State after:
case intro.intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s

State before:
case intro.intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
exact ⟨max s s', by
  simp; exact Set.insert_subset
    (subset_of_le H (Nat.le_max_right s s') hs')
    (subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s', f ∈ T s'
Tactic:
simpa using (Set.insert_subset_iff.mp hu).1
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ↑(insert f u) ⊆ T (max s s')
Tactic:
simp
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ insert f ↑u ⊆ T (max s s')

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ insert f ↑u ⊆ T (max s s')
Tactic:
exact Set.insert_subset
(subset_of_le H (Nat.le_max_right s s') hs')
(subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))
State after:
no goals