Theorem: finiteExhaustion (Fine/Util/util.lean)

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
⊢ Monotone fam → ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
Tactic:
intros h₁
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
Tactic:
apply @Finset.induction_on α (λfs => ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } → ∃n : β, ↑fs ⊆ fam n) instDec fin
State after:
case empty
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n

case insert
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n
Tactic:
case empty =>
  intros _
  refine ⟨default,?_⟩
  intros h₂ h₃
  contradiction
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n
Tactic:
case insert => 
  intros x fs _ h₃ h₄
  have l₁ : x ∈ {x : α | ∃n : β, x ∈ fam n } := h₄ $ Finset.mem_insert_self x fs
  have ⟨n, l₂⟩ := l₁
  have l₃ : ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } := by
    intros y h₅
    exact h₄ $ Finset.mem_insert_of_mem (Finset.mem_coe.mp h₅)
  have ⟨m, l₄⟩ := h₃ l₃
  cases le_total n m
  case inl leqthan => 
    have l₅ := (h₁ leqthan) l₂
    refine ⟨m,?_⟩
    intros y h₄
    cases Finset.mem_insert.mp h₄
    case inl h₅ => rw [h₅]; assumption
    case inr h₅ => exact l₄ h₅
  case inr geqthan =>
    have l₅ := le_trans l₄ (h₁ geqthan) 
    refine ⟨n,?_⟩
    intros y h₄
    cases Finset.mem_insert.mp h₄
    case inl h₅ => rw [h₅]; assumption
    case inr h₅ => exact l₅ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n
Tactic:
intros _
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑∅ ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑∅ ⊆ fam n
Tactic:
refine ⟨default,?_⟩
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ↑∅ ⊆ fam default

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ↑∅ ⊆ fam default
Tactic:
intros h₂ h₃
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
h₂ : α
h₃ : h₂ ∈ ↑∅
⊢ h₂ ∈ fam default

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
h₂ : α
h₃ : h₂ ∈ ↑∅
⊢ h₂ ∈ fam default
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n
Tactic:
intros x fs _ h₃ h₄
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have l₁ : x ∈ {x : α | ∃n : β, x ∈ fam n } := h₄ $ Finset.mem_insert_self x fs
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have ⟨n, l₂⟩ := l₁
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have l₃ : ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } := by
  intros y h₅
  exact h₄ $ Finset.mem_insert_of_mem (Finset.mem_coe.mp h₅)
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have ⟨m, l₄⟩ := h₃ l₃
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
cases le_total n m
State after:
case inl
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
h✝ : n ≤ m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

case inr
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
h✝ : m ≤ n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
case inl leqthan => 
  have l₅ := (h₁ leqthan) l₂
  refine ⟨m,?_⟩
  intros y h₄
  cases Finset.mem_insert.mp h₄
  case inl h₅ => rw [h₅]; assumption
  case inr h₅ => exact l₄ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
case inr geqthan =>
  have l₅ := le_trans l₄ (h₁ geqthan) 
  refine ⟨n,?_⟩
  intros y h₄
  cases Finset.mem_insert.mp h₄
  case inl h₅ => rw [h₅]; assumption
  case inr h₅ => exact l₅ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
⊢ ↑fs ⊆ { x | ∃ n, x ∈ fam n }
Tactic:
intros y h₅
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
y : α
h₅ : y ∈ ↑fs
⊢ y ∈ { x | ∃ n, x ∈ fam n }

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
y : α
h₅ : y ∈ ↑fs
⊢ y ∈ { x | ∃ n, x ∈ fam n }
Tactic:
exact h₄ $ Finset.mem_insert_of_mem (Finset.mem_coe.mp h₅)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have l₅ := (h₁ leqthan) l₂
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
refine ⟨m,?_⟩
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
⊢ ↑(insert x fs) ⊆ fam m

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
⊢ ↑(insert x fs) ⊆ fam m
Tactic:
intros y h₄
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
⊢ y ∈ fam m

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
⊢ y ∈ fam m
Tactic:
cases Finset.mem_insert.mp h₄
State after:
case inl
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h✝ : y = x
⊢ y ∈ fam m

case inr
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h✝ : y ∈ fs
⊢ y ∈ fam m

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ y ∈ fam m
Tactic:
case inl h₅ => rw [h₅]; assumption
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y ∈ fs
⊢ y ∈ fam m
Tactic:
case inr h₅ => exact l₄ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ y ∈ fam m
Tactic:
rw [h₅]
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ x ∈ fam m

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ x ∈ fam m
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y ∈ fs
⊢ y ∈ fam m
Tactic:
exact l₄ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
have l₅ := le_trans l₄ (h₁ geqthan)
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
⊢ ∃ n, ↑(insert x fs) ⊆ fam n
Tactic:
refine ⟨n,?_⟩
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
⊢ ↑(insert x fs) ⊆ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
⊢ ↑(insert x fs) ⊆ fam n
Tactic:
intros y h₄
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
⊢ y ∈ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
⊢ y ∈ fam n
Tactic:
cases Finset.mem_insert.mp h₄
State after:
case inl
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h✝ : y = x
⊢ y ∈ fam n

case inr
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h✝ : y ∈ fs
⊢ y ∈ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ y ∈ fam n
Tactic:
case inl h₅ => rw [h₅]; assumption
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y ∈ fs
⊢ y ∈ fam n
Tactic:
case inr h₅ => exact l₅ h₅
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ y ∈ fam n
Tactic:
rw [h₅]
State after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ x ∈ fam n

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y = x
⊢ x ∈ fam n
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
geqthan : m ≤ n
l₅ : ↑fs ≤ fam n
y : α
h₄ : y ∈ ↑(insert x fs)
h₅ : y ∈ fs
⊢ y ∈ fam n
Tactic:
exact l₅ h₅
State after:
no goals