awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
a : α
inst : Fintype (↑{a} : Type u_1)
h : ∀ (a_1 : α), Membership.mem (γ := Finset α) (toFinset {a}) a_1 ↔ Membership.mem (γ := Finset α) {a} a_1
⊢ Eq (α := Finset α) (toFinset {a}) {a}

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
a : α
inst : Fintype (↑{a} : Type u_1)
a_1 : α
⊢ Membership.mem (γ := Finset α) (toFinset {a}) a_1 ↔ Membership.mem (γ := Finset α) {a} a_1

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Set α
inst_1 : Fintype (↑(insert a s) : Type u_1)
inst_2 : Fintype (↑s : Type u_1)
h : ∀ (a_1 : α), a_1 ∈ (insert a s).toFinset ↔ a_1 ∈ insert a s.toFinset
⊢ (insert a s).toFinset = insert a s.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Set α
inst_1 : Fintype (↑(insert a s) : Type u_1)
inst_2 : Fintype (↑s : Type u_1)
a_1 : α
⊢ a_1 ∈ (insert a s).toFinset ↔ a_1 ∈ insert a s.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
h : ∀ (a : α), Membership.mem (γ := Finset α) {x : α | x ∈ s} a ↔ a ∈ s.toFinset
⊢ {x : α | x ∈ s} = s.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
h : a ∈ s ↔ a ∈ s.toFinset
h₁ h₂ : a ∈ s ↔ a ∈ s
⊢ Membership.mem (γ := Finset α) {x : α | x ∈ s} a ↔ a ∈ s.toFinset

Tactic:
rw [mem_filter_univ, mem_toFinset]

Premises used: Finset.mem_filter_univ, Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Finset α
inst : Fintype (↑(↑s : Set α) : Type u_1)
⊢ (↑s : Set α).toFinset = s

Tactic:
ext fun _ => Set.mem_toFinset

Premises used: Finset.ext, Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u
s : Finset α
⊢ univ = s.attach

Tactic:
rfl

Premises used: Finset.univ, Finset.attach, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
⊢ (↑(image f univ) : Set β) = Set.range f

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
s : Finset α
⊢ s.attach = univ

Tactic:
rfl

Premises used: Finset.univ, Finset.attach, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Multiset.Nodup (α := Prop) {True, False}

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Prop), x ∈ { val := {True, False}, nodup := fintype._proof_1 : Finset Prop }

Tactic:
simpa using em

Premises used: em
-- Module: Mathlib.Data.Fintype.Sets
Goal:
simp : val univ = True ::ₘ {False}
⊢ Eq (α := Multiset Prop) (val univ) (val {True, False})

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
⊢ val univ = True ::ₘ {False}

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst : DecidablePred p
inst_1 : Fintype α
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
⊢ Set α → Finset α

Tactic:
exact fun s => s.toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
⊢ Set α → Finset α

Tactic:
classical exact fun s => s.toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
s : Finset α
⊢ (↑s : Set α).toFinset = s

Tactic:
Finset.toFinset_coe s

Premises used: Finset.toFinset_coe
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
s : Finset α
⊢ (↑s : Set α).toFinset = s

Tactic:
convert! Finset.toFinset_coe s

Premises used: Finset.toFinset_coe
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
s : Set α
⊢ (↑s.toFinset : Set α) = s

Tactic:
s.coe_toFinset

Premises used: Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
s : Set α
⊢ (↑s.toFinset : Set α) = s

Tactic:
exact s.coe_toFinset

Premises used: Set.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
s : Set α
⊢ (↑s.toFinset : Set α) = s

Tactic:
classical exact s.coe_toFinset
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
⊢ Eq (α := (a : Finset α) → Set α) (⇑finsetEquivSet : (a : Finset α) → Set α) SetLike.coe

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ (finsetEquivSet : (a : Finset α) → Set α) s = (↑s : Set α)

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ (Equiv.symm finsetEquivSet : (a : Set α) → Finset α) s = s.toFinset

Tactic:
simp [finsetEquivSet]

Premises used: Fintype.finsetEquivSet
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
⊢ Eq (α := (a : Finset α) → Set α) (⇑finsetOrderIsoSet : (a : Finset α) → Set α) SetLike.coe

Tactic:
rfl

Premises used: setOf, Multiset.Mem, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_1
inst : Fintype α
⊢ Eq.{u_1 + 1} (α := (a : Set α) → Finset α) (⇑(OrderIso.symm finsetOrderIsoSet) : (a : Set α) → Finset α)
    (⇑(Equiv.symm finsetEquivSet) : (a : Set α) → Finset α)

Tactic:
rfl

Premises used: Finset.map, Set.toFinset, rfl
-- Module: Mathlib.Data.Fintype.Sets
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
b : β
⊢ b ∈ image f univ ↔ b ∈ Set.range f

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Shrink
Goal:
α_1 : Type u
inst : Fintype α_1
α : Type u
inst_1 : Finite α
⊢ Finite.{v + 1} (Shrink.{v, u} α)

Tactic:
.of_equiv _ (equivShrink _)

Premises used: Finite.of_equiv, equivShrink
-- Module: Mathlib.Data.Fintype.Shrink
Goal:
α : Type u
inst : Fintype α
inst_1 : Fintype (Shrink.{v, u} α)
⊢ card.{v} (Shrink.{v, u} α) = card α

Tactic:
card_congr (equivShrink _).symm

Premises used: Fintype.card_congr, Equiv.symm, equivShrink
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ Eq.{u_2 + 1} (α := Set α)
    (⋃ (ij : (i : ι) × κ i),
      ⋃ (_ : Membership.mem (γ := Finset ((i : ι) × κ i)) (s.sigma (α := κ) fun (x : ι) ↦ Finset.univ) ij), f ij)
    (⋃ i ∈ s, ⋃ (j : κ i), f (Sigma.mk (β := κ) i j))

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ s, ⋃ (j : κ i), f i j)
    (⋃ (ij : (i : ι) × κ i),
      ⋃ (_ : Membership.mem (γ := Finset ((i : ι) × κ i)) (s.sigma (α := κ) fun (x : ι) ↦ Finset.univ) ij),
        f (ij.fst (β := fun (i : ι) ↦ κ i)) (ij.snd (β := fun (i : ι) ↦ κ i)))

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ Eq.{u_2 + 1} (α := Set α)
    (⋂ (ij : (i : ι) × κ i),
      ⋂ (_ : Membership.mem (γ := Finset ((i : ι) × κ i)) (s.sigma (α := κ) fun (x : ι) ↦ Finset.univ) ij), f ij)
    (⋂ i ∈ s, ⋂ (j : κ i), f (Sigma.mk (β := κ) i j))

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ s, ⋂ (j : κ i), f i j)
    (⋂ (ij : (i : ι) × κ i),
      ⋂ (_ : Membership.mem (γ := Finset ((i : ι) × κ i)) (s.sigma (α := κ) fun (x : ι) ↦ Finset.univ) ij),
        f (ij.fst (β := fun (i : ι) ↦ κ i)) (ij.snd (β := fun (i : ι) ↦ κ i)))

Tactic:
aesop
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
inst_1 : Fintype ι
⊢ ∀ (x : (i : ι) × κ i), Membership.mem (γ := Finset ((i : ι) × κ i)) (Finset.sigma (α := κ) univ fun (x : ι) ↦ univ) x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sigma
Goal:
ι : Type u_1
κ : ι → Type u_3
inst : (i : ι) → Fintype (κ i)
inst_1 : Fintype ι
⊢ Eq (α := Finset ((i : ι) × κ i)) (Finset.sigma (α := κ) univ fun (x : ι) ↦ univ) univ

Tactic:
rfl

Premises used: Finset.univ, Finset.sigma, rfl
-- Module: Mathlib.Data.Fintype.Sort
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : LinearOrder α
m n : ℕ
s : Finset α
hm : #s = m
hn : #sᶜ = n
i : Fin m
⊢ Eq (α := α) ((finSumEquivOfFinset hm hn : (a : Fin m ⊕ Fin n) → α) (Sum.inl i) : α)
    ((s.orderEmbOfFin hm : (a : Fin m) → α) i : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fintype.Sort
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : LinearOrder α
m n : ℕ
s : Finset α
hm : #s = m
hn : #sᶜ = n
i : Fin n
⊢ Eq (α := α) ((finSumEquivOfFinset hm hn : (a : Fin m ⊕ Fin n) → α) (Sum.inr i) : α)
    ((sᶜ.orderEmbOfFin hn : (a : Fin n) → α) i : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u
β : Type v
inst : Fintype α
inst_1 : Fintype β
val : α
⊢ Membership.mem (γ := Finset (α ⊕ β)) (disjSum univ univ) (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u
β : Type v
inst : Fintype α
inst_1 : Fintype β
val : β
⊢ Membership.mem (γ := Finset (α ⊕ β)) (disjSum univ univ) (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
u : Finset (α ⊕ β)
⊢ u.toLeft = univ ↔ map Function.Embedding.inl univ ⊆ u

Tactic:
simp [map_inl_subset_iff_subset_toLeft]

Premises used: Finset.map_inl_subset_iff_subset_toLeft
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
u : Finset (α ⊕ β)
⊢ u.toRight = ∅ ↔ u ⊆ map Function.Embedding.inl univ

Tactic:
simp [subset_map_inl]

Premises used: Finset.subset_map_inl
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
u : Finset (α ⊕ β)
⊢ u.toRight = univ ↔ map Function.Embedding.inr univ ⊆ u

Tactic:
simp [map_inr_subset_iff_subset_toRight]

Premises used: Finset.map_inr_subset_iff_subset_toRight
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
u : Finset (α ⊕ β)
⊢ u.toLeft = ∅ ↔ u ⊆ map Function.Embedding.inr univ

Tactic:
simp [subset_map_inr]

Premises used: Finset.subset_map_inr
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
⊢ Eq (α := Finset (α ⊕ β)) (disjSum univ univ) univ

Tactic:
rfl

Premises used: Finset.univ, Finset.disjSum, rfl
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
h :
  ∀ (a : α), Membership.mem (γ := Finset α) (toLeft.{u_3, u_4} (β := β) univ) a ↔ Membership.mem (γ := Finset α) univ a
⊢ Eq.{u_3 + 1} (α := Finset α) (toLeft.{u_3, u_4} (β := β) univ) univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
a : α
⊢ Membership.mem (γ := Finset α) (toLeft.{u_3, u_4} (β := β) univ) a ↔ Membership.mem (γ := Finset α) univ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
h :
  ∀ (a : β), Membership.mem (γ := Finset β) (toRight.{u_3, u_4} (α := α) univ) a ↔ Membership.mem (γ := Finset β) univ a
⊢ Eq.{u_4 + 1} (α := Finset β) (toRight.{u_3, u_4} (α := α) univ) univ

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
β : Type u_4
inst : Fintype α
inst_1 : Fintype β
a : β
⊢ Membership.mem (γ := Finset β) (toRight.{u_3, u_4} (α := α) univ) a ↔ Membership.mem (γ := Finset β) univ a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
⊢ card (α ⊕ β) = card α + card β

Tactic:
card_disjSum _ _

Premises used: Finset.univ, Fintype.card, Finset.disjSum, Finset.card_disjSum
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
a : α
x : Fintype { b : α // b ≠ a }
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := { b : α // b = a } ⊕ { b : α // b ≠ a })
    (Sum.elim (Subtype.val (p := fun (b : α) ↦ b = a)) (Subtype.val (p := fun (b : α) ↦ b ≠ a)))

Tactic:
(Equiv.sumCompl (· = a)).bijective

Premises used: Equiv.bijective, Equiv.sumCompl, Eq, Sum.elim
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
a : α
x : Fintype { b : α // b ≠ a }
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := { b : α // b = a } ⊕ { b : α // b ≠ a })
    (Sum.elim (Subtype.val (p := fun (b : α) ↦ b = a)) (Subtype.val (p := fun (b : α) ↦ b ≠ a)))

Tactic:
exact (Equiv.sumCompl (· = a)).bijective

Premises used: Equiv.bijective, Equiv.sumCompl, Eq
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
a : α
x : Fintype { b : α // b ≠ a }
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := { b : α // b = a } ⊕ { b : α // b ≠ a })
    (Sum.elim (Subtype.val (p := fun (b : α) ↦ b = a)) (Subtype.val (p := fun (b : α) ↦ b ≠ a)))

Tactic:
classical exact (Equiv.sumCompl (· = a)).bijective
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
a : image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ ⊆ (image b univ).erase k
a₁ : (image b univ).erase k ⊆ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ
⊢ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ = (image b univ).erase k

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
a :
  ∀ (x : { a : α // b a ≠ k }),
    Membership.mem (γ := Finset { a : α // b a ≠ k }) univ x → b (↑x : α) ∈ (image b univ).erase k
⊢ image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ ⊆ (image b univ).erase k

Tactic:
rw [image_subset_iff]

Premises used: Finset.image_subset_iff
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : { a : α // b a ≠ k }
a : Membership.mem (γ := Finset { a : α // b a ≠ k }) univ i → b (↑i : α) ∈ (image b univ).erase k
⊢ Membership.mem (γ := Finset { a : α // b a ≠ k }) univ i → b (↑i : α) ∈ (image b univ).erase k

Tactic:
_
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : { a : α // b a ≠ k }
h : Membership.mem (γ := Finset { a : α // b a ≠ k }) univ i
⊢ b (↑i : α) ∈ (image b univ).erase k

Tactic:
apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))

Premises used: Finset.mem_univ, Finset.mem_erase_of_ne_of_mem, Finset.mem_image_of_mem, Subtype.property
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
⊢ Membership.mem (γ := Finset β) (image (fun (i : { a : α // b a ≠ k }) ↦ b (↑i : α)) univ) i

Tactic:
rw [mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a :
  ∀ (a : α),
    Membership.mem (γ := Finset α) univ a →
      ∀ (ha : b a = i),
        ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i
⊢ ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i

Tactic:
rcases mem_image.1 (erase_subset _ _ hi) with ⟨a, _, ha⟩

Premises used: Finset.mem_image, Iff.mp, Finset.erase_subset
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
a : α
left : Membership.mem (γ := Finset α) univ a
ha : b a = i
a₁ :
  ∀ (hi : b a ∈ (image b univ).erase k),
    ∃ (a_1 : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a_1 ∧ b (↑a_1 : α) = b a
⊢ ∃ (a : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a ∧ b (↑a : α) = i

Tactic:
subst ha
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
a : α
left : Membership.mem (γ := Finset α) univ a
hi : b a ∈ (image b univ).erase k
⊢ ∃ (a_1 : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a_1 ∧ b (↑a_1 : α) = b a

Tactic:
⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

Premises used: Finset.mem_univ, Finset.ne_of_mem_erase, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
a : α
left : Membership.mem (γ := Finset α) univ a
hi : b a ∈ (image b univ).erase k
⊢ ∃ (a_1 : { a : α // b a ≠ k }), Membership.mem (γ := Finset { a : α // b a ≠ k }) univ a_1 ∧ b (↑a_1 : α) = b a

Tactic:
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
k : β
b : α → β
hk : k ∈ image b univ
p : β → Prop
inst_2 : DecidablePred p
hp : ¬p k
⊢ image (fun (i : { a : α // p (b a) }) ↦ b (↑i : α)) univ ⊂ image b univ

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
rwa : Fintype.card α = Fintype.card.{u_2} ↥t
rwa₁ rwa₂ rwa₃ rwa₄ : Fintype.card α = #t
⊢ Nonempty (Equiv.{u_1 + 1, u_2 + 1} α ↥t)

Tactic:
rwa [← Fintype.card_eq, Fintype.card_coe]

Premises used: Fintype.card_eq, Fintype.card_coe
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
empty :
  ∀ (e : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
      ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]

Premises used: Membership.mem, Equiv, Subtype, Nonempty
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
e : Equiv.{u_1 + 1, u_2 + 1} α ↥t
h : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((e : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
use e
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f (↑∅ : Set α)
e : Equiv.{u_1 + 1, u_2 + 1} α ↥t
⊢ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((e : (a : α) → ↥t) i) : β) = f i

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H :
  ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f (↑(insert a s) : Set α)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
?_
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f (↑s : Set α)
insert :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (H :
      ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
        ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i)
    {f : α → β} (hfst : image f (Insert.insert a s) ⊆ t) (hfs : Set.InjOn f (↑(Insert.insert a s) : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
induction s using Finset.induction generalizing f with
    | empty =>
      obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp
    | insert a s has H => ?_

Premises used: Membership.mem, Equiv, Subtype, Insert.insert, Nonempty
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H :
  ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f (↑(insert a s) : Set α)
⊢ image f s ⊆ t

Tactic:
have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H :
  ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f (↑(insert a s) : Set α)
hfst' : image f s ⊆ t
⊢ Set.InjOn f (↑s : Set α)

Tactic:
have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H :
  ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
f : α → β
hfst : image f (Insert.insert a s) ⊆ t
hfs : Set.InjOn f (↑(Insert.insert a s) : Set α)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f (↑s : Set α)
insert :
  ∀ (g' : Equiv.{u_1 + 1, u_2 + 1} α ↥t) (hg' : ∀ i ∈ s, (↑((g' : (a : α) → ↥t) i) : β) = f i),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
obtain ⟨g', hg'⟩ := H hfst' hfs'
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H :
  ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f (↑(insert a s) : Set α)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f (↑s : Set α)
g' : Equiv.{u_1 + 1, u_2 + 1} α ↥t
hg' : ∀ i ∈ s, (↑((g' : (a : α) → ↥t) i) : β) = f i
⊢ f a ∈ t

Tactic:
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))