α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
intro b hb
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
⊢ ∃ a ha, b = f a ha
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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ ∃ a ha, b = f a ha
have finj : f'.Injective := by
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  simp only [Subtype.mk.injEq] at hxy ⊢
  apply hinj _ _ hx hy hxy
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
⊢ ∃ a ha, b = f a ha
have hft := ht.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
⊢ ∃ a ha, b = f a ha
have hft' := Fintype.ofInjective f' finj
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
⊢ ∃ a ha, b = f a ha
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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∃ a ha, b = f a ha
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
⊢ ∃ a ha, b = f a ha
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
case h.e'_2.h.h.e'_1.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ toFinset s

case convert_1
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a : α) (ha : a ∈ toFinset s), f'' a ha ∈ toFinset t

case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ toFinset s) (ha₂ : a₂ ∈ toFinset s), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂

case convert_3
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∃ a ha, b = f a ha
convert @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ (by simpa) (by simpa)
no goals
case convert_3
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
rwa [←ncard_eq_toFinset_card', ←ncard_eq_toFinset_card']
case mk.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' { val := x, property := hx } = f' { val := y, property := hy }
⊢ { val := x, property := hx } = { 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Injective f'
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
case mk.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x (_ : ↑{ val := x, property := hx } ∈ s) = f y (_ : ↑{ val := y, property := hy } ∈ s)
⊢ x = y
case mk.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' { val := x, property := hx } = f' { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
simp only [Subtype.mk.injEq] at hxy ⊢
no goals
case mk.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x (_ : ↑{ val := x, property := hx } ∈ s) = f y (_ : ↑{ val := y, property := hy } ∈ s)
⊢ x = y
apply hinj _ _ hx hy hxy
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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ b ∈ toFinset t
simpa
no goals
case h.e'_2.h.h.e'_1.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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ toFinset s
simp
no goals
case convert_1
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a : α) (ha : a ∈ toFinset s), f'' a ha ∈ toFinset t
simp [hf]
case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁ : a₁ ∈ toFinset s
ha₂ : a₂ ∈ toFinset s
h : f'' a₁ ha₁ = f'' a₂ ha₂
⊢ a₁ = a₂
case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ toFinset s) (ha₂ : a₂ ∈ toFinset s), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
intros a₁ a₂ ha₁ ha₂ h
case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁✝ : a₁ ∈ toFinset s
ha₁ : a₁ ∈ s
ha₂✝ : a₂ ∈ toFinset s
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁✝ = f'' a₂ ha₂✝
⊢ a₁ = a₂
case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁ : a₁ ∈ toFinset s
ha₂ : a₂ ∈ toFinset s
h : f'' a₁ ha₁ = f'' a₂ ha₂
⊢ a₁ = a₂
rw [mem_toFinset] at ha₁ ha₂
no goals
case convert_2
α : 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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁✝ : a₁ ∈ toFinset s
ha₁ : a₁ ∈ s
ha₂✝ : a₂ ∈ toFinset s
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁✝ = f'' a₂ ha₂✝
⊢ a₁ = a₂
exact hinj _ _ ha₁ ha₂ h