awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
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 : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁ : a₁ ∈ s.toFinset
ha₂ : a₂ ∈ s.toFinset
h : f'' a₁ ha₁ = f'' a₂ ha₂
ha₃ : a₁ ∈ s
ha₄ : a₂ ∈ s.toFinset
ha₅ : a₂ ∈ s
⊢ f'' a₁ ha₁ = f'' a₂ ha₄

Tactic:
rw [mem_toFinset] at ha₁ ha₂

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
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 : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁_1 : a₁ ∈ s.toFinset
ha₁ : a₁ ∈ s
ha₂_1 : a₂ ∈ s.toFinset
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁_1 = f'' a₂ ha₂_1
⊢ a₁ = a₂

Tactic:
hinj _ _ ha₁ ha₂ h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
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 : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁_1 : a₁ ∈ s.toFinset
ha₁ : a₁ ∈ s
ha₂_1 : a₂ ∈ s.toFinset
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁_1 = f'' a₂ ha₂_1
⊢ a₁ = a₂

Tactic:
exact hinj _ _ ha₁ ha₂ h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
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 : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
convert_3 : t.ncard ≤ s.toFinset.card
convert_3₁ convert_3₂ convert_3₃ convert_3₄ : t.ncard ≤ s.ncard
⊢ t.toFinset.card ≤ s.toFinset.card

Tactic:
rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']

Premises used: Set.ncard_eq_toFinset_card'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
y : β
hy : y ∈ t
obtain :
  ∀ (a : α) (ha : a ∈ s) (hy : f a ha ∈ t),
    ∃ (a_1 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
⊢ ∃ (a : (↑s : Type u_1)), f' a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy

Tactic:
obtain ⟨a, ha, rfl⟩ := hsurj y hy

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
simp :
  ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
⊢ ∃ (a_1 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
simp only [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
⟨_, ha, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
exact ⟨_, ha, rfl⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
⊢ Function.Surjective f'

Tactic:
have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
haveI : ∀ (this : Fintype (↑s : Type u_1)), a₁ = a₂
⊢ a₁ = a₂

Tactic:
haveI := hs.fintype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this : Fintype (↑s : Type u_1)
haveI : ∀ (this : Fintype (↑t : Type u_2)), a₁ = a₂
⊢ a₁ = a₂

Tactic:
haveI := Fintype.ofSurjective _ hsurj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
a : α
h : a ∈ s.toFinset
⊢ a ∈ s

Tactic:
simpa using h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
rw : ∀ (ha_1 : a ∈ s), f'' a ha ∈ t
⊢ f'' a ha ∈ t.toFinset

Tactic:
rw [mem_toFinset] at ha ⊢

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha_1 : a ∈ s.toFinset
ha : a ∈ s
⊢ f'' a ha_1 ∈ t

Tactic:
hf a ha

Premises used: Set.Mem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha_1 : a ∈ s.toFinset
ha : a ∈ s
⊢ f'' a ha_1 ∈ t

Tactic:
exact hf a ha
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
rw rw₁ rw₂ rw₃ : ∀ (ha_1 : a ∈ s), f'' a ha ∈ t
⊢ f'' a ha ∈ t.toFinset

Tactic:
{ rw [mem_toFinset] at ha ⊢; exact hf a ha }

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ ∀ b ∈ t.toFinset, ∃ (a : α) (ha : a ∈ s.toFinset), f'' a ha = b

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
rwa : s.ncard ≤ t.toFinset.card
rwa₁ rwa₂ rwa₃ rwa₄ : s.ncard ≤ t.ncard
⊢ s.toFinset.card ≤ t.toFinset.card

Tactic:
rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']

Premises used: Set.ncard_eq_toFinset_card'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
rwa : s.ncard ≤ t.toFinset.card
rwa₁ rwa₂ rwa₃ rwa₄ : s.ncard ≤ t.ncard
⊢ s.toFinset.card ≤ t.toFinset.card

Tactic:
{ rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }

Premises used: Set.ncard_eq_toFinset_card'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ a₁ ∈ s.toFinset

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ a₂ ∈ s.toFinset

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ f'' a₁ ⋯ = f'' a₂ ⋯

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ a₁ = a₂

Tactic:
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₁
      (by simpa) a₂ (by simpa) (by simpa)

Premises used: Finset.inj_on_of_surj_on_of_card_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
set set₁ : a₁ = a₂
set₂ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f'), a₁ = a₂
set₃ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f') (this : Fintype (↑s : Type u_1)), a₁ = a₂
set₄ set₅ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f') (this : Fintype (↑s : Type u_1)) (this : Fintype (↑t : Type u_2)), a₁ = a₂
⊢ a₁ = a₂

Tactic:
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.exists]
    exact ⟨_, ha, rfl⟩
  haveI := hs.fintype
  haveI := Fintype.ofSurjective _ hsurj
  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₁
      (by simpa) a₂ (by simpa) (by simpa)
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
s : Set α
⊢ ncard.{u_3} (α := (↑s : Type u_3)) univ = s.ncard

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
rw : (Prod.fst '' graphOn f s).ncard = s.ncard
rw₁ rw₂ : s.ncard = s.ncard
⊢ (graphOn f s).ncard = s.ncard

Tactic:
rw [← fst_injOn_graph.ncard_image, image_fst_graphOn]

Premises used: Set.fst_injOn_graph, Set.InjOn.ncard_image, Set.image_fst_graphOn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
to_encard_tac :
  HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
⊢ (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
rw₂ : (s ∪ t).encard + (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
rw₃ : (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
rw₄ rw₅ : s.encard + t.encard = s.encard + t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)

Tactic:
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]

Premises used: Set.Finite.union, Set.encard_union_add_encard_inter, Set.inter_subset_left, Set.Finite.subset, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
rw₁ rw₂ : s.ncard + t.ncard = s.ncard + t.ncard
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]

Premises used: add_comm, Set.ncard_union_add_ncard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
inl : ∀ (h : (s ∪ t).Finite), (s ∪ t).ncard ≤ s.ncard + t.ncard
inr : ∀ (h : (s ∪ t).Infinite), (s ∪ t).ncard ≤ s.ncard + t.ncard
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
obtain (h | h) := (s ∪ t).finite_or_infinite

Premises used: Set.finite_or_infinite, Union.union
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
inl : (↑(s ∪ t).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
inl : (s ∪ t).encard ≤ s.encard + t.encard
⊢ (↑(s ∪ t).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)

Tactic:
rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]

Premises used: Set.subset_union_right, Set.Finite.subset, Set.subset_union_left, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
apply encard_union_le

Premises used: Set.encard_union_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
inr : 0 ≤ s.ncard + t.ncard
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
rw [h.ncard]

Premises used: Set.Infinite.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ 0 ≤ s.ncard + t.ncard

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
to_encard_tac : (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
⊢ (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
rw : (↑(s ∪ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : (↑(s ∪ t).ncard : ℕ∞) = s.encard + t.encard
rw₂ : (s ∪ t).encard = s.encard + t.encard
rw₃ rw₄ : s.encard + t.encard = s.encard + t.encard
⊢ (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)

Tactic:
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]

Premises used: Set.Finite.union, Set.encard_union_eq, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∪ t).ncard = (s ∪ t).ncard + (s ∩ t).ncard ↔ Disjoint s t
rw₁ : (s ∩ t).ncard = 0 ↔ Disjoint s t
rw₂ : s ∩ t = ∅ ↔ Disjoint s t
rw₃ rw₄ : s ∩ t = ∅ ↔ s ∩ t = ∅
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t

Tactic:
rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]

Premises used: left_eq_add, Set.Finite.inter_of_left, Set.ncard_eq_zero, Set.disjoint_iff_inter_eq_empty, Set.ncard_union_add_ncard_inter
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
h : ¬Disjoint s t
⊢ (s ∪ t).ncard < s.ncard + t.ncard

Tactic:
(ncard_union_le s t).lt_of_ne (mt (ncard_union_eq_iff hs ht).mp h)

Premises used: mt, Set.ncard_union_le, LE.le.lt_of_ne, Set.ncard_union_eq_iff, Iff.mp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
to_encard_tac : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
⊢ (t \ s).ncard + s.ncard = t.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = t.encard
rw₁ : (↑(t \ s).ncard : ℕ∞) + s.encard = t.encard
rw₂ : (t \ s).encard + s.encard = t.encard
rw₃ rw₄ : t.encard = t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)

Tactic:
rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
    encard_diff_add_encard_of_subset h]

Premises used: Set.encard_diff_add_encard_of_subset, Set.Finite.subset, Set.Finite.diff, Set.Finite.cast_ncard_eq