no goals
α : 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
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
α : 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
α : 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
let s' : Finset α := s.toFinset
α : 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
α : 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
have hfst' : s'.image f ⊆ t := by simpa [← Finset.coe_subset] using hfst
α : 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
α : 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
have hfs' : Set.InjOn f s' := by simpa using hfs
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
α : 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
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
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
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
refine' ⟨g, fun i hi => _⟩
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'
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
apply hg
no goals
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'
simpa using hi
no goals
α : 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
simpa [← Finset.coe_subset] using hfst
no goals
α : 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'
simpa using hfs