-- Mathlib/Data/Fintype/Sum.lean
theorem Set.MapsTo.exists_equiv_extend_of_card_eq [Fintype α] {t : Finset β}
    (hαt : Fintype.card α = #t) {s : Set α} {f : α → β} (hfst : s.MapsTo f t)
    (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst

Result:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ InjOn f ↑s'

Tactic:
simpa [s'] using hfs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
classical
  let s' : Finset α := s.toFinset
  have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
  have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
  obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
  refine ⟨g, fun i hi => ?_⟩
  apply hg
  simpa [s'] using hi

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Proof state:
case intro.a
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
i : α
hi : i ∈ s
⊢ i ∈ s'

Tactic:
simpa [s'] using hi

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
i : α
hi : i ∈ s
⊢ ↑(g i) = f i

Tactic:
apply hg

Result:
case intro.a
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
i : α
hi : i ∈ s
⊢ i ∈ s'

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
refine ⟨g, fun i hi => ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ { x // x ∈ t }
hg : ∀ i ∈ s', ↑(g i) = f i
i : α
hi : i ∈ s
⊢ ↑(g i) = f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
⊢ Finset.image f s' ⊆ t

Tactic:
simpa [s', ← Finset.coe_subset] using hfst

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
have hfs' : Set.InjOn f s' := by simpa [s'] using hfs

Result:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
let s' : Finset α := s.toFinset

Result:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
s' : Finset α := s.toFinset
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i