no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
⊢ a₁ = a₂
classical
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
have hsurj : f'.Surjective := by
  rintro ⟨y, hy⟩
  obtain ⟨a, ha, rfl⟩ := hsurj y hy
  simp only [Subtype.mk.injEq, Subtype.exists]
  exact ⟨_, ha, rfl⟩
haveI := hs.fintype
haveI := Fintype.ofSurjective _ hsurj
simp_rw [ncard_eq_toFinset_card] at hst
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
exact
  @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
    (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
    (by { rwa [←ncard_eq_toFinset_card', ←ncard_eq_toFinset_card'] }) a₁ a₂
    (by simpa) (by simpa) (by simpa)
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
⊢ a₁ = a₂
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ a₁ = a₂
have hsurj : f'.Surjective := by
  rintro ⟨y, hy⟩
  obtain ⟨a, ha, rfl⟩ := hsurj y hy
  simp only [Subtype.mk.injEq, Subtype.exists]
  exact ⟨_, ha, rfl⟩
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this : Fintype ↑s
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
⊢ a₁ = a₂
haveI := hs.fintype
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this : Fintype ↑s
⊢ a₁ = a₂
haveI := Fintype.ofSurjective _ hsurj
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
⊢ a₁ = a₂
simp_rw [ncard_eq_toFinset_card] at hst
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
⊢ a₁ = a₂
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₁ = a₂
exact
  @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
    (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
    (by { rwa [←ncard_eq_toFinset_card', ←ncard_eq_toFinset_card'] }) a₁ a₂
    (by simpa) (by simpa) (by simpa)
case mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
y : β
hy : y ∈ t
⊢ ∃ a, f' a = { val := y, property := hy }
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Surjective f'
rintro ⟨y, hy⟩
case mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = { val := f a ha, property := hy }
case mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
y : β
hy : y ∈ t
⊢ ∃ a, f' a = { val := y, property := hy }
obtain ⟨a, ha, rfl⟩ := hsurj y hy
case mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1 h, f a_1 (_ : ↑{ val := a_1, property := (_ : a_1 ∈ s) } ∈ s) = f a ha
case mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = { val := f a ha, property := hy }
simp only [Subtype.mk.injEq, Subtype.exists]
no goals
case mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1 h, f a_1 (_ : ↑{ val := a_1, property := (_ : a_1 ∈ s) } ∈ s) = f a ha
exact ⟨_, ha, rfl⟩
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
a : α
h : a ∈ toFinset s
⊢ a ∈ s
simpa using h
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (b : β), b ∈ toFinset t → ∃ a ha, b = f'' a ha
simpa
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₁ ∈ toFinset s
simpa
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₂ ∈ toFinset s
simpa
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ f'' a₁ (_ : a₁ ∈ toFinset s) = f'' a₂ (_ : a₂ ∈ toFinset s)
simpa