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

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
α : 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
induction' s using Finset.induction with a s has H generalizing f
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
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
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
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
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
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
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
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
obtain ⟨g', hg'⟩ := H hfst' hfs'
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
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
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
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
⊢ ∀ (i : α), i ∈ insert a s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
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
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
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
⊢ ∀ (i : α), i = a ∨ i ∈ s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
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
⊢ ∀ (i : α), i ∈ insert a s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
simp_rw [mem_insert]
case insert.intro.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

case insert.intro.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
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
⊢ ∀ (i : α), i = a ∨ i ∈ s → ↑(↑(g'.trans (Equiv.swap { val := f a, property := hfat } (↑g' a))) i) = f i
rintro i (rfl | hi)
case insert.intro.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 }

case insert.intro.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
case insert.intro.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
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
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
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
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
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 }
⊢ ∀ (i : α), i ∈ ∅ → ↑(↑e i) = f i
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
use e
no goals
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 }
⊢ ∀ (i : α), i ∈ ∅ → ↑(↑e i) = f i
simp
no goals
α : 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 })
rwa [← Fintype.card_eq, Fintype.card_coe]
no goals
case insert.intro.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
simp
no goals
case insert.intro.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 }
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)
no goals
case insert.intro.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
exact g'.injective.ne (ne_of_mem_of_not_mem hi has)