α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ ncard s = ncard t
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = ncard t
set f' : s → t := fun x ↦ ⟨f x.1 x.2, h₁ _ _⟩
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this : Finite ↑s
⊢ ncard s = ncard t
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
⊢ ncard s = ncard t
haveI := hs.to_subtype
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this✝ : Finite ↑s
this : Fintype ↑t
⊢ ncard s = ncard t
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this : Finite ↑s
⊢ ncard s = ncard t
haveI := @Fintype.ofFinite _ (Finite.ofBijective hbij)
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this✝¹ : Finite ↑s
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ ncard s = ncard t
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this✝ : Finite ↑s
this : Fintype ↑t
⊢ ncard s = ncard t
haveI := Fintype.ofFinite s
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
this✝¹ : Finite ↑s
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ ncard s = ncard t
convert Fintype.card_of_bijective hbij
<;> rw [ncard_def, Nat.card_eq_fintype_card]
case left
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Injective f'

case right
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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'
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Bijective f'
constructor
case right.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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 }
case right
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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 right.mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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 right.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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⟩ := h₃ y hy
case right.mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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 right.mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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 right.mk.intro.intro
α : Type u_2
β : Type u_1
s t✝ : Set α
a✝ b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
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⟩
case left.mk.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x✝ y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
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 }
case left
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
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 left.mk.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x✝ y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
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 left.mk.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x✝ y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
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 left.mk.mk
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x✝ y✝ : α
f✝ : α → β
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
hs : autoParam (Set.Finite s) _auto✝
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
exact h₂ _ _ hx hy hxy