α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
⊢ s = t
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
⊢ s = t
have htfin := ht.fintype
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ s = t
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
⊢ s = t
have hft := (ht.subset h).fintype
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s = toFinset t
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ s = t
rw [← @toFinset_inj]
case h
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s ⊆ toFinset t

case h₂
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s = toFinset t
apply Finset.eq_of_subset_of_card_le
case h₂
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
case h₂
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
rw [ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ (ht.subset h)] at h'
case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset t = Finite.toFinset ht

case h.e'_4.h.e'_2
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s = Finite.toFinset (_ : Set.Finite s)
case h₂
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
convert h'
case h.e'_4.h.e'_2.a
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset s ↔ a✝ ∈ Finite.toFinset (_ : Set.Finite s)
case h.e'_4.h.e'_2
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s = Finite.toFinset (_ : Set.Finite s)
ext
no goals
case h.e'_4.h.e'_2.a
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset s ↔ a✝ ∈ Finite.toFinset (_ : Set.Finite s)
simp
no goals
case h
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset s ⊆ toFinset t
simpa
case h.e'_3.h.e'_2.a
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset t ↔ a✝ ∈ Finite.toFinset ht
case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
⊢ toFinset t = Finite.toFinset ht
ext
no goals
case h.e'_3.h.e'_2.a
α : Type u_1
β : Type ?u.49880
s t : Set α
a b x y : α
f : α → β
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
h' : Finset.card (Finite.toFinset ht) ≤ Finset.card (Finite.toFinset (_ : Set.Finite s))
htfin : Fintype ↑t
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset t ↔ a✝ ∈ Finite.toFinset ht
simp