[GOAL]
α✝ β✝ : Type u
s✝ : Set α✝
f✝ : α✝ → Set β✝
g : Set (α✝ → β✝)
α β γ : Type u_1
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
ext
[GOAL]
case h
α✝ β✝ : Type u
s✝ : Set α✝
f✝ : α✝ → Set β✝
g : Set (α✝ → β✝)
α β γ : Type u_1
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
simp
[GOAL]
α β : Type u
s : Set α
f : α → Set β
g : Set (α → β)
α✝ β✝ γ✝ : Type ?u.7831
x✝² : Set α✝
x✝¹ : α✝ → Set β✝
x✝ : β✝ → Set γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x => x✝¹ x >>= x✝
[PROOFSTEP]
simp only [bind_def, biUnion_iUnion]
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
⊢ Lean.Internal.coeM γ ⊆ β
[PROOFSTEP]
intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : { val := val✝, property := ha } ∈ γ
right✝ : a✝ ∈ (fun h => (fun a => pure (CoeT.coe a)) { val := val✝, property := ha }) h✝
⊢ a✝ ∈ β
[PROOFSTEP]
convert ha
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Lean.Internal.coeM γ
⊢ { val := a, property := (_ : a ∈ β) } ∈ γ
[PROOFSTEP]
rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h => (fun a => pure (CoeT.coe a)) w✝) ha
⊢ { val := a, property := (_ : a ∈ β) } ∈ γ
[PROOFSTEP]
convert ha


[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
⊢ Finite ↑s ↔ Set.Finite s
[PROOFSTEP]
rw [finite_iff_nonempty_fintype, finite_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ Finite.toFinset h = toFinset s
[PROOFSTEP]
have : h.fintype = ‹_› := Subsingleton.elim _ _
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
this : Finite.fintype h = inst✝
⊢ Finite.toFinset h = toFinset s
[PROOFSTEP]
rw [Finite.toFinset, this]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Finite s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
[PROOFSTEP]
cases h
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
a✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
[PROOFSTEP]
exact ⟨s.toFinset, fun _ => mem_toFinset⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Finite s
⊢ ∃ s', ↑s' = s
[PROOFSTEP]
cases h
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
a✝ : Fintype ↑s
⊢ ∃ s', ↑s' = s
[PROOFSTEP]
exact ⟨s.toFinset, s.coe_toFinset⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite s
⊢ Finset.Nonempty (Finite.toFinset h) ↔ Set.Nonempty s
[PROOFSTEP]
rw [← Finset.coe_nonempty, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite s
⊢ { x // x ∈ Finite.toFinset h } = ↑s
[PROOFSTEP]
rw [← Finset.coe_sort_coe _, h.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t✝ : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t✝
t : Finset α
⊢ Finite.toFinset hs ⊆ t ↔ s ⊆ ↑t
[PROOFSTEP]
rw [← Finset.coe_subset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t✝ : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t✝
t : Finset α
⊢ Finite.toFinset hs ⊂ t ↔ s ⊂ ↑t
[PROOFSTEP]
rw [← Finset.coe_ssubset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ t : Set α
a : α
hs : Set.Finite s✝
ht : Set.Finite t
s : Finset α
⊢ s ⊆ Finite.toFinset ht ↔ ↑s ⊆ t
[PROOFSTEP]
rw [← Finset.coe_subset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ t : Set α
a : α
hs : Set.Finite s✝
ht : Set.Finite t
s : Finset α
⊢ s ⊂ Finite.toFinset ht ↔ ↑s ⊂ t
[PROOFSTEP]
rw [← Finset.coe_ssubset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
⊢ Finite.toFinset hs ⊆ Finite.toFinset ht ↔ s ⊆ t
[PROOFSTEP]
simp only [← Finset.coe_subset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
⊢ Finite.toFinset hs ⊂ Finite.toFinset ht ↔ s ⊂ t
[PROOFSTEP]
simp only [← Finset.coe_ssubset, Finite.coe_toFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
h : Set.Finite {x | p x}
⊢ Finite.toFinset h = Finset.filter p Finset.univ
[PROOFSTEP]
ext
  -- porting note: `simp` doesn't use the `simp` lemma `Set.toFinset_setOf` without the `_`
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
h : Set.Finite {x | p x}
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finset.filter p Finset.univ
[PROOFSTEP]
simp [Set.toFinset_setOf _]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∩ t)
⊢ Finite.toFinset h = Finite.toFinset hs ∩ Finite.toFinset ht
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∩ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs ∩ Finite.toFinset ht
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∪ t)
⊢ Finite.toFinset h = Finite.toFinset hs ∪ Finite.toFinset ht
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∪ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs ∪ Finite.toFinset ht
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s \ t)
⊢ Finite.toFinset h = Finite.toFinset hs \ Finite.toFinset ht
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s \ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs \ Finite.toFinset ht
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∆ t)
⊢ Finite.toFinset h = Finite.toFinset hs ∆ Finite.toFinset ht
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∆ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs ∆ Finite.toFinset ht
[PROOFSTEP]
simp [mem_symmDiff, Finset.mem_symmDiff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht : Set.Finite t
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : Set.Finite s
h : Set.Finite sᶜ
⊢ Finite.toFinset h = (Finite.toFinset hs)ᶜ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht : Set.Finite t
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : Set.Finite s
h : Set.Finite sᶜ
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ (Finite.toFinset hs)ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
inst✝ : Fintype α
h : Set.Finite univ
⊢ Finite.toFinset h = Finset.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht : Set.Finite t
inst✝ : DecidableEq β
f : α → β
hs : Set.Finite s
h : Set.Finite (f '' s)
⊢ Finite.toFinset h = Finset.image f (Finite.toFinset hs)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht : Set.Finite t
inst✝ : DecidableEq β
f : α → β
hs : Set.Finite s
h : Set.Finite (f '' s)
a✝ : β
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finset.image f (Finite.toFinset hs)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : Set.Finite (range f)
⊢ Finite.toFinset h = Finset.image f Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs : Set.Finite s
ht : Set.Finite t
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : Set.Finite (range f)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finset.image f Finset.univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ toFinset s ∪ toFinset t ↔ x ∈ s ∪ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ Finset.filter p (toFinset s) ↔ x ∈ {a | a ∈ s ∧ p a}
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ toFinset s ∩ toFinset t ↔ x ∈ s ∩ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ t
⊢ ∀ (x : α), x ∈ Finset.filter (fun x => x ∈ t) (toFinset s) ↔ x ∈ s ∩ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑t
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : α), x ∈ Finset.filter (fun x => x ∈ s) (toFinset t) ↔ x ∈ s ∩ t
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ t
h : t ⊆ s
⊢ Fintype ↑t
[PROOFSTEP]
rw [← inter_eq_self_of_subset_right h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ t
h : t ⊆ s
⊢ Fintype ↑(s ∩ t)
[PROOFSTEP]
apply Set.fintypeInterOfLeft
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α), x ∈ toFinset s \ toFinset t ↔ x ∈ s \ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
inst✝¹ : Fintype (PLift ι)
f : ι → Set α
inst✝ : (i : ι) → Fintype ↑(f i)
⊢ ∀ (x : α), (x ∈ Finset.biUnion Finset.univ fun i => toFinset (f i.down)) ↔ x ∈ ⋃ (i : ι), f i
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
s : Set (Set α)
inst✝ : Fintype ↑s
H : (t : ↑s) → Fintype ↑↑t
⊢ Fintype ↑(⋃₀ s)
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
s : Set (Set α)
inst✝ : Fintype ↑s
H : (t : ↑s) → Fintype ↑↑t
⊢ Fintype ↑(⋃ (i : ↑s), ↑i)
[PROOFSTEP]
exact @Set.fintypeiUnion _ _ _ _ _ H
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝¹ : DecidableEq α
ι : Type u_1
s : Set ι
inst✝ : Fintype ↑s
t : ι → Set α
H : (i : ι) → i ∈ s → Fintype ↑(t i)
this : (i : { x // x ∈ toFinset s }) → Fintype ↑(t ↑i)
x : α
⊢ (x ∈ Finset.biUnion (Finset.attach (toFinset s)) fun x => toFinset (t ↑x)) ↔ x ∈ ⋃ (x : ι) (_ : x ∈ s), t x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝² : DecidableEq α
ι : Type u_1
s : Set ι
inst✝¹ : Fintype ↑s
t : ι → Set α
inst✝ : (i : ι) → Fintype ↑(t i)
⊢ ∀ (x : α), (x ∈ Finset.biUnion (toFinset s) fun x => toFinset (t x)) ↔ x ∈ ⋃ (x : ι) (_ : x ∈ s), t x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ ∀ (x : α), x ∈ ∅ ↔ x ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
⊢ ∀ (x : α), x ∈ {a} ↔ x ∈ {a}
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ ∀ (x : α), x ∈ insert a (toFinset s) ↔ x ∈ insert a s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ ¬a ∈ (toFinset s).val
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ ∀ (x : α),
    x ∈ { val := a ::ₘ (toFinset s).val, nodup := (_ : Multiset.Nodup (a ::ₘ (toFinset s).val)) } ↔ x ∈ insert a s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∈ s
⊢ ∀ (x : α), x ∈ toFinset s ↔ x ∈ insert a s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
s : Set α
f : α → β
inst✝ : Fintype ↑s
⊢ ∀ (x : β), x ∈ Finset.image f (toFinset s) ↔ x ∈ f '' s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
⊢ a ∈
      { val := Multiset.filterMap g (toFinset (f '' s)).val,
        nodup := (_ : Multiset.Nodup (Multiset.filterMap g (toFinset (f '' s)).val)) } ↔
    a ∈ s
[PROOFSTEP]
suffices (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s by
  simpa [exists_and_left.symm, and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
this : (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s
⊢ a ∈
      { val := Multiset.filterMap g (toFinset (f '' s)).val,
        nodup := (_ : Multiset.Nodup (Multiset.filterMap g (toFinset (f '' s)).val)) } ↔
    a ∈ s
[PROOFSTEP]
simpa [exists_and_left.symm, and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
⊢ (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s
[PROOFSTEP]
rw [exists_swap]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
⊢ (∃ y x, f y = x ∧ g x = some a ∧ y ∈ s) ↔ a ∈ s
[PROOFSTEP]
suffices (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s by simpa [and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
this : (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s
⊢ (∃ y x, f y = x ∧ g x = some a ∧ y ∈ s) ↔ a ∈ s
[PROOFSTEP]
simpa [and_comm, and_left_comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
a : α
⊢ (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s
[PROOFSTEP]
simp [I _, (injective_of_isPartialInv I).eq_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
f : ι → α
inst✝ : Fintype (PLift ι)
⊢ ∀ (x : α), x ∈ Finset.image (f ∘ PLift.down) Finset.univ ↔ x ∈ range f
[PROOFSTEP]
simp [Equiv.plift.exists_congr_left]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ ∀ (x : ℕ), x ∈ Finset.range n ↔ x ∈ {i | i < n}
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
n : ℕ
⊢ Fintype ↑{i | i ≤ n}
[PROOFSTEP]
simpa [Nat.lt_succ_iff] using Set.fintypeLTNat (n + 1)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α × β), x ∈ toFinset s ×ˢ toFinset t ↔ x ∈ s ×ˢ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
s : Set α
inst✝ : Fintype ↑s
⊢ ∀ (x : α × α), x ∈ Finset.offDiag (toFinset s) ↔ x ∈ offDiag s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)
[PROOFSTEP]
rw [← image_prod]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x => f x.fst x.snd) '' s ×ˢ t)
[PROOFSTEP]
apply Set.fintypeImage
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq β
f : Set (α → β)
s : Set α
inst✝¹ : Fintype ↑f
inst✝ : Fintype ↑s
⊢ Fintype ↑(seq f s)
[PROOFSTEP]
rw [seq_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq β
f : Set (α → β)
s : Set α
inst✝¹ : Fintype ↑f
inst✝ : Fintype ↑s
⊢ Fintype ↑(⋃ (f_1 : α → β) (_ : f_1 ∈ f), f_1 '' s)
[PROOFSTEP]
apply Set.fintypeBiUnion'
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ Set.Finite s ↔ Set.Finite t
[PROOFSTEP]
simp_rw [← Set.finite_coe_iff, hst.finite_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Finset α
⊢ Finite.toFinset (_ : Set.Finite ↑s) = s
[PROOFSTEP]
rw [toFinite_toFinset, toFinset_coe]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Multiset α
⊢ Set.Finite {x | x ∈ s}
[PROOFSTEP]
classical simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Multiset α
⊢ Set.Finite {x | x ∈ s}
[PROOFSTEP]
simpa only [← Multiset.mem_toFinset] using s.toFinset.finite_toSet
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Multiset α
⊢ Finite.toFinset (_ : Set.Finite {x | x ∈ s}) = toFinset s
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ Finite.toFinset (_ : Set.Finite {x | x ∈ s}) ↔ x ∈ toFinset s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(s ∪ t)
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝ : Fintype ↑s
⊢ Finite ↑(s ∪ t)
[PROOFSTEP]
cases nonempty_fintype t
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
val✝¹ : Fintype ↑s
val✝ : Fintype ↑t
⊢ Finite ↑(s ∪ t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t
[PROOFSTEP]
rw [← sep_eq_of_subset h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
⊢ Finite ↑(range f)
[PROOFSTEP]
haveI := Fintype.ofFinite (PLift ι)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
this : Fintype (PLift ι)
⊢ Finite ↑(range f)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
⊢ Finite ↑(⋃ (i : ι), f i)
[PROOFSTEP]
rw [iUnion_eq_range_psigma]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
⊢ Finite ↑(range fun a => ↑a.snd)
[PROOFSTEP]
apply Set.finite_range
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst✝ : Finite ↑s
H : ∀ (t : ↑s), Finite ↑↑t
⊢ Finite ↑(⋃₀ s)
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
inst✝ : Finite ↑s
H : ∀ (t : ↑s), Finite ↑↑t
⊢ Finite ↑(⋃ (i : ↑s), ↑i)
[PROOFSTEP]
exact @Finite.Set.finite_iUnion _ _ _ _ H
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
⊢ Finite ↑(⋃ (x : ι) (_ : x ∈ s), t x)
[PROOFSTEP]
rw [biUnion_eq_iUnion]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
[PROOFSTEP]
haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ (i : ι), i ∈ s → Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ (x : ↑s), t ↑x)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
⊢ Finite ↑(f '' s)
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑(f '' s)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)
[PROOFSTEP]
rw [← image_prod]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x => f x.fst x.snd) '' s ×ˢ t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(seq f s)
[PROOFSTEP]
rw [seq_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(⋃ (f_1 : α → β) (_ : f_1 ∈ f), f_1 '' s)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite (s ∪ t)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (s ∪ t)
[PROOFSTEP]
cases ht
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a✝¹ : Fintype ↑s
a✝ : Fintype ↑t
⊢ Set.Finite (s ∪ t)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
hsc : Set.Finite sᶜ
⊢ Finite α
[PROOFSTEP]
rw [← finite_univ_iff, ← union_compl_self s]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
hsc : Set.Finite sᶜ
⊢ Set.Finite (s ∪ sᶜ)
[PROOFSTEP]
exact hs.union hsc
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
p : α → Prop
⊢ Set.Finite {a | a ∈ s ∧ p a}
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
a✝ : Fintype ↑s
⊢ Set.Finite {a | a ∈ s ∧ p a}
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
t : Set α
⊢ Set.Finite (s ∩ t)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a✝ : Fintype ↑s
⊢ Set.Finite (s ∩ t)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
t : Set α
⊢ Set.Finite (t ∩ s)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a✝ : Fintype ↑s
⊢ Set.Finite (t ∩ s)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
t : Set α
ht : t ⊆ s
⊢ Set.Finite t
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
⊢ Set.Finite t
[PROOFSTEP]
haveI := Finite.Set.subset _ ht
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
ht : t ⊆ s
a✝ : Fintype ↑s
this : Finite ↑t
⊢ Set.Finite t
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
t : Set α
⊢ Set.Finite (s \ t)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a✝ : Fintype ↑s
⊢ Set.Finite (s \ t)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Finite ι
f : ι → Set α
H : ∀ (i : ι), Set.Finite (f i)
⊢ Set.Finite (⋃ (i : ι), f i)
[PROOFSTEP]
haveI := fun i => (H i).fintype
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Finite ι
f : ι → Set α
H : ∀ (i : ι), Set.Finite (f i)
this : (i : ι) → Fintype ↑(f i)
⊢ Set.Finite (⋃ (i : ι), f i)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
hs : Set.Finite s
H : ∀ (t : Set α), t ∈ s → Set.Finite t
⊢ Set.Finite (⋃₀ s)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (⋃₀ s)
[PROOFSTEP]
haveI := fun i : s => (H i i.2).to_subtype
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set (Set α)
H : ∀ (t : Set α), t ∈ s → Set.Finite t
a✝ : Fintype ↑s
this : ∀ (i : ↑s), Finite ↑↑i
⊢ Set.Finite (⋃₀ s)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
[PROOFSTEP]
classical
cases hs
haveI := fintypeBiUnion s t fun i hi => (ht i hi).fintype
apply toFinite
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
[PROOFSTEP]
haveI := fintypeBiUnion s t fun i hi => (ht i hi).fintype
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : ι → Set α
ht : ∀ (i : ι), i ∈ s → Set.Finite (t i)
a✝ : Fintype ↑s
this : Fintype ↑(⋃ (x : ι) (_ : x ∈ s), t x)
⊢ Set.Finite (⋃ (i : ι) (_ : i ∈ s), t i)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
hs : Set.Finite s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
⊢ Set.Finite (⋃ (i : ι) (h : i ∈ s), t i h)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (i : ι) (h : i ∈ s), t i h)
[PROOFSTEP]
rw [biUnion_eq_iUnion]
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : Set ι
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), Set.Finite (t i hi)
a✝ : Fintype ↑s
⊢ Set.Finite (⋃ (x : ↑s), t ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
apply finite_iUnion fun i : s => ht i.1 i.2
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
⊢ Set.Finite (⋃ (i : ι), s i)
[PROOFSTEP]
suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
this : ⋃ (i : ι), s i ⊆ ⋃ (i : ι) (_ : i ∈ t), s i
⊢ Set.Finite (⋃ (i : ι), s i)
[PROOFSTEP]
exact (ht.biUnion hs).subset this
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
⊢ ⋃ (i : ι), s i ⊆ ⋃ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
refine' iUnion_subset fun i x hx => _
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
by_cases hi : i ∈ t
[GOAL]
case pos
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
exact mem_biUnion hi hx
[GOAL]
case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
rw [he i hi, mem_empty_iff_false] at hx
[GOAL]
case neg
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set ι
ht : Set.Finite t
hs : ∀ (i : ι), i ∈ t → Set.Finite (s i)
he : ∀ (i : ι), ¬i ∈ t → s i = ∅
i : ι
x : α
hx : False
hi : ¬i ∈ t
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Infinite s
⊢ s ≠ ∅
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Set.Infinite ∅
⊢ False
[PROOFSTEP]
exact h finite_empty
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
hs : Set.Finite s
⊢ Set.Finite (insert a s)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
a✝ : Fintype ↑s
⊢ Set.Finite (insert a s)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
hs : Set.Finite s
⊢ Set.Finite (f '' s)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
a✝ : Fintype ↑s
⊢ Set.Finite (f '' s)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
F : (i : α) → i ∈ s → β
⊢ Set.Finite {y | ∃ x hx, y = F x hx}
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
F : (i : α) → i ∈ s → β
a✝ : Fintype ↑s
⊢ Set.Finite {y | ∃ x hx, y = F x hx}
[PROOFSTEP]
simpa [range, eq_comm] using finite_range fun x : s => F x x.2
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
h : Set.Finite (f '' s)
hi : InjOn f s
⊢ Set.Finite s
[PROOFSTEP]
cases h
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
hi : InjOn f s
a✝ : Fintype ↑(f '' s)
⊢ Set.Finite s
[PROOFSTEP]
exact
  ⟨Fintype.ofInjective (fun a => (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s)) fun a b eq =>
      Subtype.eq <| hi a.2 b.2 <| Subtype.ext_iff_val.1 eq⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set β
h : Set.Finite (f ⁻¹' s)
hs : s ⊆ range f
⊢ Set.Finite s
[PROOFSTEP]
rw [← image_preimage_eq_of_subset hs]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set β
h : Set.Finite (f ⁻¹' s)
hs : s ⊆ range f
⊢ Set.Finite (f '' (f ⁻¹' s))
[PROOFSTEP]
exact Finite.image f h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite (s ×ˢ t)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
ht : Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (s ×ˢ t)
[PROOFSTEP]
cases ht
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
a✝¹ : Fintype ↑s
a✝ : Fintype ↑t
⊢ Set.Finite (s ×ˢ t)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Infinite (s ×ˢ t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
[PROOFSTEP]
simp_rw [Set.Infinite, @and_comm ¬_, ← not_imp]
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
⊢ ¬(Set.Nonempty t → Set.Finite s) ∨ ¬(Set.Nonempty s → Set.Finite t)
[PROOFSTEP]
by_contra'
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite (s ×ˢ t)
this : (Set.Nonempty t → Set.Finite s) ∧ (Set.Nonempty s → Set.Finite t)
⊢ False
[PROOFSTEP]
exact h ((this.1 h.nonempty.snd).prod $ this.2 h.nonempty.fst)
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (s ×ˢ t)
[PROOFSTEP]
rintro (h | h)
[GOAL]
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite s ∧ Set.Nonempty t
⊢ Set.Infinite (s ×ˢ t)
[PROOFSTEP]
exact h.1.prod_left h.2
[GOAL]
case refine'_2.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
h : Set.Infinite t ∧ Set.Nonempty s
⊢ Set.Infinite (s ×ˢ t)
[PROOFSTEP]
exact h.1.prod_right h.2
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
⊢ Set.Finite (s ×ˢ t) ↔ (Set.Finite s ∨ t = ∅) ∧ (Set.Finite t ∨ s = ∅)
[PROOFSTEP]
simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ : Set α
t : Set β
s : Set α
hs : Set.Finite s
⊢ Set.Finite (offDiag s)
[PROOFSTEP]
classical
cases hs
apply Set.toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ : Set α
t : Set β
s : Set α
hs : Set.Finite s
⊢ Set.Finite (offDiag s)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ : Set α
t : Set β
s : Set α
a✝ : Fintype ↑s
⊢ Set.Finite (offDiag s)
[PROOFSTEP]
apply Set.toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β → γ
hs : Set.Finite s
ht : Set.Finite t
⊢ Set.Finite (image2 f s t)
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β → γ
ht : Set.Finite t
a✝ : Fintype ↑s
⊢ Set.Finite (image2 f s t)
[PROOFSTEP]
cases ht
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β → γ
a✝¹ : Fintype ↑s
a✝ : Fintype ↑t
⊢ Set.Finite (image2 f s t)
[PROOFSTEP]
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
hf : Set.Finite f
hs : Set.Finite s
⊢ Set.Finite (Set.seq f s)
[PROOFSTEP]
classical
cases hf
cases hs
apply toFinite
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
hf : Set.Finite f
hs : Set.Finite s
⊢ Set.Finite (Set.seq f s)
[PROOFSTEP]
cases hf
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
hs : Set.Finite s
a✝ : Fintype ↑f
⊢ Set.Finite (Set.seq f s)
[PROOFSTEP]
cases hs
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
a✝¹ : Fintype ↑f
a✝ : Fintype ↑s
⊢ Set.Finite (Set.seq f s)
[PROOFSTEP]
apply toFinite
[GOAL]
α✝ : Type u
β : Type v
ι : Sort w
γ : Type x
α : Type u
a : Set α
h : Set.Finite a
s : Set α
⊢ s ∈ Finset.map Finset.coeEmb.toEmbedding (Finset.powerset (Finite.toFinset h)) ↔ s ∈ {b | b ⊆ a}
[PROOFSTEP]
simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset, ← and_assoc, Finset.coeEmb] using
  h.subset
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
t : (d : δ) → Set (κ d)
ht : ∀ (d : δ), Set.Finite (t d)
⊢ Set.Finite (Set.pi univ t)
[PROOFSTEP]
cases _root_.nonempty_fintype δ
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
t : (d : δ) → Set (κ d)
ht : ∀ (d : δ), Set.Finite (t d)
val✝ : Fintype δ
⊢ Set.Finite (Set.pi univ t)
[PROOFSTEP]
lift t to ∀ d, Finset (κ d) using ht
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite (Set.pi univ fun i => ↑(t i))
[PROOFSTEP]
classical
rw [← Fintype.coe_piFinset]
apply Finset.finite_toSet
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite (Set.pi univ fun i => ↑(t i))
[PROOFSTEP]
rw [← Fintype.coe_piFinset]
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
δ : Type u_1
inst✝ : Finite δ
κ : δ → Type u_2
val✝ : Fintype δ
t : (i : δ) → Finset (κ i)
⊢ Set.Finite ↑(Fintype.piFinset fun i => t i)
[PROOFSTEP]
apply Finset.finite_toSet
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → Finset β
h : Set.Finite (range f)
⊢ Set.Finite (⋃ (a : α), ↑(f a))
[PROOFSTEP]
rw [← biUnion_range]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → Finset β
h : Set.Finite (range f)
⊢ Set.Finite (⋃ (x : Finset β) (_ : x ∈ range fun a => f a), ↑x)
[PROOFSTEP]
exact h.biUnion fun y _ => y.finite_toSet
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq α
s : Set α
a : α
hs : Set.Finite (insert a s)
⊢ ∀ (a_1 : α), a_1 ∈ Finite.toFinset hs ↔ a_1 ∈ insert a (Finite.toFinset (_ : Set.Finite s))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
hs : Set.Finite s
ht : Set.Finite t
⊢ ∀ (a : α × β), a ∈ Finite.toFinset hs ×ˢ Finite.toFinset ht ↔ a ∈ Finite.toFinset (_ : Set.Finite (s ×ˢ t))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : DecidableEq α
hs : Set.Finite s
⊢ ∀ (a : α × α), a ∈ Finite.toFinset (_ : Set.Finite (offDiag s)) ↔ a ∈ Finset.offDiag (Finite.toFinset hs)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
h : Set.Finite s
⊢ range ↑(Equiv.asEmbedding (Fintype.equivFin ↑↑(Finite.toFinset h)).symm) = s
[PROOFSTEP]
simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, setOf_mem_eq]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
[PROOFSTEP]
cases hs
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
[PROOFSTEP]
choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
⊢ ∀ (x : ↑s), ∃ i, ↑x ∈ t i
[PROOFSTEP]
simpa [subset_def] using h
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, Set.Finite I ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ I), t i
[PROOFSTEP]
refine' ⟨range f, finite_range f, fun x hx => _⟩
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ range f), t i
[PROOFSTEP]
rw [biUnion_range, mem_iUnion]
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
s : Set α
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ (i : ι), t i
a✝ : Fintype ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)
[PROOFSTEP]
exact ⟨⟨x, hx⟩, hf _⟩
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
⊢ t = ⋃ (i : ↑{i | i ∈ I}), (fun x => s ↑x ∩ t) i
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
⊢ x ∈ t ↔ x ∈ ⋃ (i : ↑{i | i ∈ I}), (fun x => s ↑x ∩ t) i
[PROOFSTEP]
rw [mem_iUnion]
[GOAL]
case h
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
⊢ x ∈ t ↔ ∃ i, x ∈ (fun x => s ↑x ∩ t) i
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
⊢ x ∈ t → ∃ i, x ∈ (fun x => s ↑x ∩ t) i
[PROOFSTEP]
intro x_in
[GOAL]
case h.mp
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
x_in : x ∈ t
⊢ ∃ i, x ∈ (fun x => s ↑x ∩ t) i
[PROOFSTEP]
rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
x_in : x ∈ t
i : ι
hi : i ∈ I
H : x ∈ (fun h => s i) hi
⊢ ∃ i, x ∈ (fun x => s ↑x ∩ t) i
[PROOFSTEP]
refine' ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩
[GOAL]
case h.mpr
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
⊢ (∃ i, x ∈ (fun x => s ↑x ∩ t) i) → x ∈ t
[PROOFSTEP]
rintro ⟨i, -, H⟩
[GOAL]
case h.mpr.intro.intro
α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
s : ι → Set α
t : Set α
tfin : Set.Finite t
h : t ⊆ ⋃ (i : ι), s i
I : Set ι
Ifin : Set.Finite I
hI : t ⊆ ⋃ (i : ι) (_ : i ∈ I), s i
x : α
i : ↑{i | i ∈ I}
H : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exact H
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
s : Set α
h : Set.Finite s
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
⊢ C s
[PROOFSTEP]
lift s to Finset α using h
[GOAL]
case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
s : Finset α
⊢ C ↑s
[PROOFSTEP]
induction' s using Finset.cons_induction_on with a s ha hs
[GOAL]
case intro.h₁
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
⊢ C ↑∅
[PROOFSTEP]
rwa [Finset.coe_empty]
[GOAL]
case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C ↑(Finset.cons a s ha)
[PROOFSTEP]
rw [Finset.coe_cons]
[GOAL]
case intro.h₂
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → C s → C (insert a s)
a : α
s : Finset α
ha : ¬a ∈ s
hs : C ↑s
⊢ C (insert a ↑s)
[PROOFSTEP]
exact @H1 a s ha (Set.toFinite _) hs
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
⊢ C S
[PROOFSTEP]
refine' @Set.Finite.induction_on α (fun s => s ⊆ S → C s) S h (fun _ => H0) _ Subset.rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
⊢ ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → (fun s => s ⊆ S → C s) s → (fun s => s ⊆ S → C s) (insert a s)
[PROOFSTEP]
intro a s has _ hCs haS
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : insert a s ⊆ S
⊢ C (insert a s)
[PROOFSTEP]
rw [insert_subset_iff] at haS
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : a ∈ S ∧ s ⊆ S
⊢ C (insert a s)
[PROOFSTEP]
exact H1 haS.1 haS.2 has (hCs haS.2)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), Set.Finite t → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
[PROOFSTEP]
haveI : Nonempty γ := (h ∅ finite_empty).nonempty
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), Set.Finite t → ∃ c, P c t
this : Nonempty γ
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
[PROOFSTEP]
choose! c hc using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
[PROOFSTEP]
set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k (_ : ↑k ∈ Iio n))
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
[PROOFSTEP]
set u : ℕ → γ := fun n => Nat.strongRecOn' n f
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k (_ : ↑k ∈ Iio n))
u : ℕ → γ := fun n => Nat.strongRecOn' n f
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
[PROOFSTEP]
refine' ⟨u, fun n => _⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k (_ : ↑k ∈ Iio n))
u : ℕ → γ := fun n => Nat.strongRecOn' n f
n : ℕ
⊢ P (u n) (u '' Iio n)
[PROOFSTEP]
convert hc (u '' Iio n) ((finite_lt_nat _).image _)
[GOAL]
case h.e'_1
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k (_ : ↑k ∈ Iio n))
u : ℕ → γ := fun n => Nat.strongRecOn' n f
n : ℕ
⊢ u n = c (u '' Iio n)
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
case h.e'_1
α : Type u
β : Type v
ι : Sort w
γ✝ : Type x
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), Set.Finite t → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k (_ : ↑k ∈ Iio n))
u : ℕ → γ := fun n => Nat.strongRecOn' n f
n : ℕ
⊢ u n = c (range fun x => u ↑x)
[PROOFSTEP]
exact Nat.strongRecOn'_beta
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Fintype ↑∅
⊢ Fintype.card ↑∅ = Fintype.card ↑∅
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
h : Fintype ↑∅
⊢ h = fintypeEmpty
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
[PROOFSTEP]
rw [fintypeInsertOfNotMem, Fintype.card_ofFinset]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ Finset.card { val := a ::ₘ (toFinset s).val, nodup := (_ : Multiset.Nodup (a ::ₘ (toFinset s).val)) } =
    Fintype.card ↑s + 1
[PROOFSTEP]
simp only [Finset.card, toFinset, Finset.map_val, Embedding.coe_subtype, Multiset.card_cons, Multiset.card_map,
  add_left_inj]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
⊢ ↑Multiset.card Finset.univ.val = Fintype.card ↑s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
[PROOFSTEP]
rw [← card_fintypeInsertOfNotMem s h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : ¬a ∈ s
d : Fintype ↑(insert a s)
⊢ d = fintypeInsertOfNotMem s h
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝¹ : Fintype ↑s
f : α → β
inst✝ : Fintype ↑(f '' s)
H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y → x = y
this : (a : Prop) → Decidable a
⊢ ∀ (x : β), x ∈ Finset.image f (toFinset s) ↔ x ∈ f '' s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
[PROOFSTEP]
rw [← toFinset_card, toFinset_setOf, Finset.filter_ne', Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
⊢ Set.Infinite univ ↔ Infinite α
[PROOFSTEP]
rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Infinite s
n : ℕ
⊢ ↑(Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) ⊆ s ∧
    Finset.card (Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set α
hs : Set.Finite sᶜ
h : Set.Finite s
⊢ Set.Finite univ
[PROOFSTEP]
simpa using hs.union h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set α
hs : Set.Finite s
h : Set.Finite sᶜ
⊢ Set.Finite univ
[PROOFSTEP]
simpa using hs.union h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
⊢ Set.Infinite (s ∪ t) ↔ Set.Infinite s ∨ Set.Infinite t
[PROOFSTEP]
simp only [Set.Infinite, finite_union, not_and_or]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
⊢ Set.Infinite (image2 f s t) ↔ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s
[PROOFSTEP]
refine' ⟨fun h => Set.infinite_prod.1 _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (image2 f s t)
⊢ Set.Infinite (s ×ˢ t)
[PROOFSTEP]
rw [← image_uncurry_prod] at h
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
h : Set.Infinite (uncurry f '' s ×ˢ t)
⊢ Set.Infinite (s ×ˢ t)
[PROOFSTEP]
exact h.of_image _
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
⊢ Set.Infinite s ∧ Set.Nonempty t ∨ Set.Infinite t ∧ Set.Nonempty s → Set.Infinite (image2 f s t)
[PROOFSTEP]
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
[GOAL]
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a : α
b✝ : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
hs : Set.Infinite s
b : β
hb : b ∈ t
⊢ Set.Infinite (image2 f s t)
[PROOFSTEP]
exact hs.image2_left hb (hfs _ hb)
[GOAL]
case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b : β
hfs : ∀ (b : β), b ∈ t → InjOn (fun a => f a b) s
hft : ∀ (a : α), a ∈ s → InjOn (f a) t
ht : Set.Infinite t
a : α
ha : a ∈ s
⊢ Set.Infinite (image2 f s t)
[PROOFSTEP]
exact ht.image2_right ha (hft _ ha)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β
hs : Set.Infinite s
hf : MapsTo f s t
ht : Set.Finite t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
contrapose! ht
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
t : Set β
f : α → β
hs : Set.Infinite s
hf : MapsTo f s t
ht : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ¬Set.Finite t
[PROOFSTEP]
exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite (range f)
[PROOFSTEP]
rw [← image_univ, infinite_image_iff (injOn_of_injective hi _)]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ Set.Infinite univ
[PROOFSTEP]
exact infinite_univ
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ Set.Infinite s
[PROOFSTEP]
rw [← range_subset_iff] at hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : (range fun x => f x) ⊆ s
⊢ Set.Infinite s
[PROOFSTEP]
exact (infinite_range_of_injective hi).mono hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
⊢ ¬InjOn f s
[PROOFSTEP]
have : Finite (f '' s) := finite_coe_iff.mpr h_fin
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this : Finite ↑(f '' s)
⊢ ¬InjOn f s
[PROOFSTEP]
have : Infinite s := infinite_coe_iff.mpr h_inf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
⊢ ¬InjOn f s
[PROOFSTEP]
have h := not_injective_infinite_finite ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
⊢ ¬InjOn f s
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
s : Set α
h_inf : Set.Infinite s
h_fin : Set.Finite (f '' s)
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (restrict s f) (f '' s) (_ : ∀ (x : ↑s), ∃ a, a ∈ s ∧ f a = restrict s f x))
[PROOFSTEP]
rwa [injective_codRestrict, ← injOn_iff_injective]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
⊢ Set.Infinite s
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
⊢ Set.Infinite s
[PROOFSTEP]
set f : ℕ → α := fun n => Nat.recOn n (h default).choose fun _ a => (h a).choose
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun x a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ Set.Infinite s
[PROOFSTEP]
have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun x a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ ∀ (n : ℕ), f n ∈ s
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case zero
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun x a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
⊢ f Nat.zero ∈ s
[PROOFSTEP]
exact (h _).choose_spec.1
[GOAL]
case succ
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun x a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
n✝ : ℕ
⊢ f (Nat.succ n✝) ∈ s
[PROOFSTEP]
exact (h _).choose_spec.1
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Preorder α
inst✝ : Nonempty α
s : Set α
h : ∀ (a : α), ∃ b, b ∈ s ∧ a < b
inhabited_h : Inhabited α
f : ℕ → α :=
  fun n => Nat.recOn n (Exists.choose (_ : ∃ b, b ∈ s ∧ default < b)) fun x a => Exists.choose (_ : ∃ b, b ∈ s ∧ a < b)
hf : ∀ (n : ℕ), f n ∈ s
⊢ Set.Infinite s
[PROOFSTEP]
exact infinite_of_injective_forall_mem (strictMono_nat_of_lt_succ fun n => (h _).choose_spec.2).injective hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : ∀ (a : α), f a ∈ t
ht : Set.Finite t
⊢ ∃ a b, a < b ∧ f a = f b
[PROOFSTEP]
rw [← maps_univ_to] at hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
⊢ ∃ a b, a < b ∧ f a = f b
[PROOFSTEP]
obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : LinearOrder α
inst✝ : Infinite α
t : Set β
f : α → β
hf : MapsTo (fun a => f a) univ t
ht : Set.Finite t
a b : α
h : a < b ∧ f a = f b
⊢ ∃ a b, a < b ∧ f a = f b
[PROOFSTEP]
exact ⟨a, b, h⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : Set.Finite s
x : α
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ ∀ (b : α), b ∈ s → f a ≤ f b
[PROOFSTEP]
simpa only [exists_prop, Finite.mem_toFinset] using h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : Set.Finite s
x : α
hx : x ∈ s
⊢ ∃ a, a ∈ s ∧ ∀ (b : α), b ∈ s → f b ≤ f a
[PROOFSTEP]
simpa only [exists_prop, Finite.mem_toFinset] using h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | hs
[GOAL]
case inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : Set.Finite ∅
⊢ ∃ a, ∀ (b : α), b ∈ ∅ → f a ≤ f b
[PROOFSTEP]
exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
[GOAL]
case inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
[PROOFSTEP]
rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : Set.Finite s
hs : Set.Nonempty s
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ (b : α), b ∈ s → f x₀ ≤ f b
⊢ ∃ a, ∀ (b : α), b ∈ s → f a ≤ f b
[PROOFSTEP]
exact ⟨x₀, fun x hx => hx₀ x hx⟩
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s : Set ι
hs : Set.Finite s
f : ι → ι' → α
hf : ∀ (i : ι), i ∈ s → Monotone (f i)
⊢ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
[PROOFSTEP]
induction' s, hs using Set.Finite.dinduction_on with a s _ _ ihs hf
[GOAL]
case H0
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s → Monotone (f i)
hf : ∀ (i : ι), i ∈ ∅ → Monotone (f i)
⊢ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ ∅), f i j = ⨅ (i : ι) (_ : i ∈ ∅), ⨆ (j : ι'), f i j
[PROOFSTEP]
simp [iSup_const]
[GOAL]
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : ∀ (i : ι), i ∈ insert a s → Monotone (f i)
⊢ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
[PROOFSTEP]
rw [ball_insert_iff] at hf
[GOAL]
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ insert a s), f i j = ⨅ (i : ι) (_ : i ∈ insert a s), ⨆ (j : ι'), f i j
[PROOFSTEP]
simp only [iInf_insert, ← ihs hf.2]
[GOAL]
case H1
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
s✝ : Set ι
f : ι → ι' → α
hf✝ : ∀ (i : ι), i ∈ s✝ → Monotone (f i)
a : ι
s : Set ι
a✝ : ¬a ∈ s
h✝ : Set.Finite s
ihs :
  (∀ (i : ι), i ∈ s → Monotone (f i)) →
    ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j = ⨅ (i : ι) (_ : i ∈ s), ⨆ (j : ι'), f i j
hf : Monotone (f a) ∧ ∀ (x : ι), x ∈ s → Monotone (f x)
⊢ ⨆ (j : ι'), f a j ⊓ ⨅ (x : ι) (_ : x ∈ s), f x j = (⨆ (j : ι'), f a j) ⊓ ⨆ (j : ι'), ⨅ (i : ι) (_ : i ∈ s), f i j
[PROOFSTEP]
exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ ⨆ (j : ι'), ⨅ (i : ι), f i j = ⨅ (i : ι), ⨆ (j : ι'), f i j
[PROOFSTEP]
simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
⊢ (⋃ (j : ι'), pi I fun i => s i j) = pi I fun i => ⋃ (j : ι'), s i j
[PROOFSTEP]
simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
⊢ ⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
[PROOFSTEP]
haveI := hI.fintype.finite
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
⊢ ⋃ (j : ι'), ⋂ (x : ↑I), eval ↑x ⁻¹' s (↑x) j = ⋂ (x : ↑I), ⋃ (i : ι'), eval ↑x ⁻¹' s (↑x) i
[PROOFSTEP]
refine' iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => _)
[GOAL]
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : Set.Finite I
hs : ∀ (i : ι), i ∈ I → Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂
[PROOFSTEP]
exact preimage_mono <| hs i i.2 h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
hs : Set.Nonempty s
⊢ ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
[PROOFSTEP]
induction s, h using Set.Finite.dinduction_on with
| H0 => exact absurd hs not_nonempty_empty
| @H1 a s his _ ih =>
  cases' s.eq_empty_or_nonempty with h h
  · use a
    simp [h]
  rcases ih h with ⟨b, hb, ih⟩
  by_cases h : f b ≤ f a
  · refine' ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · rfl
    · rwa [← ih c hcs (le_trans h hac)]
  · refine' ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · exact (h hbc).elim
    · exact ih c hcs hbc
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
hs : Set.Nonempty s
⊢ ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
[PROOFSTEP]
induction s, h using Set.Finite.dinduction_on with
| H0 => exact absurd hs not_nonempty_empty
| @H1 a s his _ ih =>
  cases' s.eq_empty_or_nonempty with h h
  · use a
    simp [h]
  rcases ih h with ⟨b, hb, ih⟩
  by_cases h : f b ≤ f a
  · refine' ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · rfl
    · rwa [← ih c hcs (le_trans h hac)]
  · refine' ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · exact (h hbc).elim
    · exact ih c hcs hbc
[GOAL]
case H0
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
hs : Set.Nonempty ∅
⊢ ∃ a, a ∈ ∅ ∧ ∀ (a' : α), a' ∈ ∅ → f a ≤ f a' → f a = f a'
[PROOFSTEP]

| H0 => exact absurd hs not_nonempty_empty
[GOAL]
case H0
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
hs : Set.Nonempty ∅
⊢ ∃ a, a ∈ ∅ ∧ ∀ (a' : α), a' ∈ ∅ → f a ≤ f a' → f a = f a'
[PROOFSTEP]
exact absurd hs not_nonempty_empty
[GOAL]
case H1
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]

| @H1 a s his _ ih =>
  cases' s.eq_empty_or_nonempty with h h
  · use a
    simp [h]
  rcases ih h with ⟨b, hb, ih⟩
  by_cases h : f b ≤ f a
  · refine' ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · rfl
    · rwa [← ih c hcs (le_trans h hac)]
  · refine' ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => _⟩
    rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
    · exact (h hbc).elim
    · exact ih c hcs hbc
[GOAL]
case H1
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
cases' s.eq_empty_or_nonempty with h h
[GOAL]
case H1.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h : s = ∅
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h : s = ∅
⊢ a ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a ≤ f a' → f a = f a'
[PROOFSTEP]
simp [h]
[GOAL]
case H1.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h : Set.Nonempty s
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
rcases ih h with ⟨b, hb, ih⟩
[GOAL]
case H1.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
by_cases h : f b ≤ f a
[GOAL]
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
refine' ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac _⟩
[GOAL]
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
⊢ f c ≤ f a
[PROOFSTEP]
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
[GOAL]
case pos.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
his : ¬c ∈ s
hs : Set.Nonempty (insert c s)
h : f b ≤ f c
hc : c ∈ insert c s
hac : f c ≤ f c
⊢ f c ≤ f c
[PROOFSTEP]
rfl
[GOAL]
case pos.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
hcs : c ∈ s
⊢ f c ≤ f a
[PROOFSTEP]
rwa [← ih c hcs (le_trans h hac)]
[GOAL]
case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
[PROOFSTEP]
refine' ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => _⟩
[GOAL]
case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
⊢ f b = f c
[PROOFSTEP]
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
[GOAL]
case neg.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
hbc : f b ≤ f c
his : ¬c ∈ s
hs : Set.Nonempty (insert c s)
h : ¬f b ≤ f c
hc : c ∈ insert c s
⊢ f b = f c
[PROOFSTEP]
exact (h hbc).elim
[GOAL]
case neg.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : ¬a ∈ s
h✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
hs : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
hcs : c ∈ s
⊢ f b = f c
[PROOFSTEP]
exact ih c hcs hbc
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite (f '' s)
hs : Set.Nonempty s
⊢ ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
[PROOFSTEP]
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximal_wrt id (f '' s) h (hs.image f)
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite (f '' s)
hs : Set.Nonempty s
a : α
ha : a ∈ s
hmax : ∀ (a' : β), a' ∈ f '' s → id (f a) ≤ id a' → id (f a) = id a'
⊢ ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
[PROOFSTEP]
exact ⟨a, ha, fun a' ha' hf ↦ hmax _ (mem_image_of_mem f ha') hf⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
s : Set α
I : Set β
S : β → Set α
H : Set.Finite I
⊢ BddAbove (⋃ (i : β) (_ : i ∈ ∅), S i) ↔ ∀ (i : β), i ∈ ∅ → BddAbove (S i)
[PROOFSTEP]
simp only [biUnion_empty, bddAbove_empty, ball_empty_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
s : Set α
I : Set β
S : β → Set α
H : Set.Finite I
a✝ : β
s✝ : Set β
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
hs : BddAbove (⋃ (i : β) (_ : i ∈ s✝), S i) ↔ ∀ (i : β), i ∈ s✝ → BddAbove (S i)
⊢ BddAbove (⋃ (i : β) (_ : i ∈ insert a✝ s✝), S i) ↔ ∀ (i : β), i ∈ insert a✝ s✝ → BddAbove (S i)
[PROOFSTEP]
simp only [biUnion_insert, ball_insert_iff, bddAbove_union, hs]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ ¬BddBelow s → Set.Infinite s
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ ¬Set.Infinite s → BddBelow s
[PROOFSTEP]
rw [not_infinite]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ Set.Finite s → BddBelow s
[PROOFSTEP]
exact Finite.bddBelow
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s : Set α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s : Set α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
✝ : Nontrivial α
⊢ Finite α
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x, y, hne⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s : Set α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α
[PROOFSTEP]
refine' @Finite.of_fintype α ⟨{ x, y }, fun z => _⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s : Set α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}
[PROOFSTEP]
simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s : Set α
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∀ (z : α), z ∈ s → x < y → y < z → False
⊢ ∀ ⦃x y z : ↑s⦄, x < y → y < z → False
[PROOFSTEP]
simpa only [SetCoe.forall'] using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : LinearOrder α
s✝ s : Set α
⊢ Set.Finite (s \ ⋃ (x : ↑s × ↑s), Ioo ↑x.fst ↑x.snd)
[PROOFSTEP]
simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioo a b) (Ioo (f a) (f b))
[PROOFSTEP]
intro p hp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
p : β
hp : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ioo a b
[PROOFSTEP]
rcases h_surj p with ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ f x ∈ f '' Ioo a b
[PROOFSTEP]
refine' ⟨x, mem_Ioo.2 _, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ a < x ∧ x < b
[PROOFSTEP]
contrapose! hp
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : a < x → b ≤ x
⊢ ¬f x ∈ Ioo (f a) (f b)
[PROOFSTEP]
exact fun h => h.2.not_le (h_mono <| hp <| h_mono.reflect_lt h.1)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))
[PROOFSTEP]
obtain hab | hab := lt_or_le a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))
[PROOFSTEP]
intro p hp
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
⊢ p ∈ f '' Ico a b
[PROOFSTEP]
rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
hp : f a ∈ Ico (f a) (f b)
⊢ f a ∈ f '' Ico a b
[PROOFSTEP]
exact mem_image_of_mem f (left_mem_Ico.mpr hab)
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ico a b
[PROOFSTEP]
have := surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
this : p ∈ f '' Ioo a b
⊢ p ∈ f '' Ico a b
[PROOFSTEP]
exact image_subset f Ioo_subset_Ico_self this
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))
[PROOFSTEP]
rw [Ico_eq_empty (h_mono hab).not_lt]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
⊢ SurjOn f (Ico a b) ∅
[PROOFSTEP]
exact surjOn_empty f _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioc a b) (Ioc (f a) (f b))
[PROOFSTEP]
simpa using surjOn_Ico_of_monotone_surjective h_mono.dual h_surj (toDual b) (toDual a)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
⊢ SurjOn f (Icc a b) (Icc (f a) (f b))
[PROOFSTEP]
intro p hp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
⊢ p ∈ f '' Icc a b
[PROOFSTEP]
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f a ∈ Icc (f a) (f b)
⊢ f a ∈ f '' Icc a b
[PROOFSTEP]
exact ⟨a, left_mem_Icc.mpr hab, rfl⟩
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f b ∈ Icc (f a) (f b)
⊢ f b ∈ f '' Icc a b
[PROOFSTEP]
exact ⟨b, right_mem_Icc.mpr hab, rfl⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Icc a b
[PROOFSTEP]
have := surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
this : p ∈ f '' Ioo a b
⊢ p ∈ f '' Icc a b
[PROOFSTEP]
exact image_subset f Ioo_subset_Icc_self this
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a) (Ioi (f a))
[PROOFSTEP]
rw [← compl_Iic, ← compl_compl (Ioi (f a))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
[PROOFSTEP]
refine' MapsTo.surjOn_compl _ h_surj
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ MapsTo f (Iic a) (Ioi (f a))ᶜ
[PROOFSTEP]
exact fun x hx => (h_mono hx).not_lt
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))
[PROOFSTEP]
rw [← Ioi_union_left, ← Ioi_union_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})
[PROOFSTEP]
exact (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union (@image_singleton _ _ f a ▸ surjOn_image _ _)