[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (x : α ⊕ β), x ∈ disjSum univ univ
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ disjSum univ univ
[PROOFSTEP]
simp
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ disjSum univ univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a : α
h : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)
[PROOFSTEP]
classical exact (Equiv.sumCompl (· = a)).bijective
[GOAL]
α : Type u_1
β : Type u_2
a : α
h : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)
[PROOFSTEP]
exact (Equiv.sumCompl (· = a)).bijective
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ = erase (image b univ) k
[PROOFSTEP]
apply subset_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i => b ↑i) univ ⊆ erase (image b univ) k
[PROOFSTEP]
rw [image_subset_iff]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ (x : { a // b a ≠ k }), x ∈ univ → b ↑x ∈ erase (image b univ) k
[PROOFSTEP]
intro i _
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : { a // b a ≠ k }
a✝ : i ∈ univ
⊢ b ↑i ∈ erase (image b univ) k
[PROOFSTEP]
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ erase (image b univ) k ⊆ image (fun i => b ↑i) univ
[PROOFSTEP]
intro i hi
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ i ∈ image (fun i => b ↑i) univ
[PROOFSTEP]
rw [mem_image]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
[PROOFSTEP]
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ erase (image b univ) k
a : α
left✝ : a ∈ univ
ha : b a = i
⊢ ∃ a, a ∈ univ ∧ b ↑a = i
[PROOFSTEP]
subst ha
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ erase (image b univ) k
⊢ ∃ a_1, a_1 ∈ univ ∧ b ↑a_1 = b a
[PROOFSTEP]
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊂ image b univ
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ image (fun i => b ↑i) univ ⊆ image b univ
[PROOFSTEP]
intro x hx
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
⊢ x ∈ image b univ
[PROOFSTEP]
rcases mem_image.1 hx with ⟨y, _, hy⟩
[GOAL]
case left.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
x : β
hx : x ∈ image (fun i => b ↑i) univ
y : { a // p (b a) }
left✝ : y ∈ univ
hy : b ↑y = x
⊢ x ∈ image b univ
[PROOFSTEP]
exact hy ▸ mem_image_of_mem b (mem_univ (y : α))
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
⊢ ¬image b univ ⊆ image (fun i => b ↑i) univ
[PROOFSTEP]
intro h
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rw [mem_image] at hk 
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
hk : ∃ a, a ∈ univ ∧ b a = k
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rcases hk with ⟨k', _, hk'⟩
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
k : β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
hp : ¬p k
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hk' : b k' = k
⊢ False
[PROOFSTEP]
subst hk'
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
⊢ False
[PROOFSTEP]
have := h (mem_image_of_mem b (mem_univ k'))
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : b k' ∈ image (fun i => b ↑i) univ
⊢ False
[PROOFSTEP]
rw [mem_image] at this 
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝ : k' ∈ univ
hp : ¬p (b k')
this : ∃ a, a ∈ univ ∧ b ↑a = b k'
⊢ False
[PROOFSTEP]
rcases this with ⟨j, _, hj'⟩
[GOAL]
case right.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
b : α → β
p : β → Prop
inst✝ : DecidablePred p
h : image b univ ⊆ image (fun i => b ↑i) univ
k' : α
left✝¹ : k' ∈ univ
hp : ¬p (b k')
j : { a // p (b a) }
left✝ : j ∈ univ
hj' : b ↑j = b k'
⊢ False
[PROOFSTEP]
exact hp (hj' ▸ j.2)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
classical
induction' s using Finset.induction with a s has H generalizing f
· obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
  use e
  simp
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
obtain ⟨g', hg'⟩ := H hfst' hfs'
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
simp_rw [mem_insert]
rintro i (rfl | hi)
· simp
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
·
  exact
    ne_of_apply_ne Subtype.val
      (ne_of_eq_of_ne (hg' _ hi) <| hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
· exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
induction' s using Finset.induction with a s has H generalizing f
[GOAL]
case empty
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ ∃ g, ∀ (i : α), i ∈ ∅ → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Nonempty (α ≃ { x // x ∈ t })
[PROOFSTEP]
rwa [← Fintype.card_eq, Fintype.card_coe]
[GOAL]
case empty.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ { x // x ∈ t }
⊢ ∃ g, ∀ (i : α), i ∈ ∅ → ↑(↑g i) = f i
[PROOFSTEP]
use e
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s : Finset α
f✝ : α → β
hfst✝ : image f✝ s ⊆ t
hfs✝ : Set.InjOn f✝ ↑s
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
e : α ≃ { x // x ∈ t }
⊢ ∀ (i : α), i ∈ ∅ → ↑(↑e i) = f i
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
[GOAL]
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨g', hg'⟩ := H hfst' hfs'
[GOAL]
case insert.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
[GOAL]
case insert.intro
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∃ g, ∀ (i : α), i ∈ insert a s → ↑(↑g i) = f i
[PROOFSTEP]
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∀ (i : α), i ∈ insert a s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
simp_rw [mem_insert]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
⊢ ∀ (i : α), i = a ∨ i ∈ s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
rintro i (rfl | hi)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
s : Finset α
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
i : α
has : ¬i ∈ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f ↑(insert i s)
hfat : f i ∈ t
⊢ ↑(↑(g'.trans (Equiv.swap { val := f i, property := hfat } (↑g' i))) i) = f i
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
[PROOFSTEP]
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
[GOAL]
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑g' i ≠ { val := f a, property := hfat }
[PROOFSTEP]
exact
  ne_of_apply_ne Subtype.val
    (ne_of_eq_of_ne (hg' _ hi) <| hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
[GOAL]
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = card t
s✝ : Finset α
f✝ : α → β
hfst✝ : image f✝ s✝ ⊆ t
hfs✝ : Set.InjOn f✝ ↑s✝
a : α
s : Finset α
has : ¬a ∈ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ { x // x ∈ t }
hg' : ∀ (i : α), i ∈ s → ↑(↑g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑g' i ≠ ↑g' a
[PROOFSTEP]
exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
classical
let s' : Finset α := s.toFinset
have hfst' : s'.image f ⊆ t := by simpa [← Finset.coe_subset] using hfst
have hfs' : Set.InjOn f s' := by simpa using hfs
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
refine' ⟨g, fun i hi => _⟩
apply hg
simpa using hi
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
let s' : Finset α := s.toFinset
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
have hfst' : s'.image f ⊆ t := by simpa [← Finset.coe_subset] using hfst
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
⊢ Finset.image f s' ⊆ t
[PROOFSTEP]
simpa [← Finset.coe_subset] using hfst
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
have hfs' : Set.InjOn f s' := by simpa using hfs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
⊢ InjOn f ↑s'
[PROOFSTEP]
simpa using hfs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
⊢ ∃ g, ∀ (i : α), i ∈ s → ↑(↑g i) = f i
[PROOFSTEP]
refine' ⟨g, fun i hi => _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
i : α
hi : i ∈ s
⊢ ↑(↑g i) = f i
[PROOFSTEP]
apply hg
[GOAL]
case intro.a
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = card t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := toFinset s
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ (i : α), i ∈ s' → ↑(↑g i) = f i
i : α
hi : i ∈ s
⊢ i ∈ s'
[PROOFSTEP]
simpa using hi
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }
[PROOFSTEP]
classical
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
rw [Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }
[PROOFSTEP]
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
[PROOFSTEP]
rw [Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }
[PROOFSTEP]
classical
convert Fintype.card_congr (subtypeOrEquiv p q h)
simp
[GOAL]
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } = card { x // p x } + card { x // q x }
[PROOFSTEP]
convert Fintype.card_congr (subtypeOrEquiv p q h)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
p q : α → Prop
h : Disjoint p q
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
[PROOFSTEP]
refine' ⟨fun H => _, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
[GOAL]
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β
[PROOFSTEP]
contrapose! H
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
haveI := fintypeOfNotInfinite H.1
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
haveI := fintypeOfNotInfinite H.2
[GOAL]
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)
[PROOFSTEP]
exact Infinite.false
