awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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 α)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have 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 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: 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 => ?_
Cleared hypotheses: s, f, hfst, hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
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
have hfst' : image f s ⊆ t
Tactic: have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
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
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
have hfs' : Set.InjOn f (↑s : Set α)
Tactic: have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
have 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 a s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: obtain ⟨g', hg'⟩ := H hfst' hfs'
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
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
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
have hfat : f a ∈ t
Tactic: have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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
hfat : f a ∈ t
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
have h : ∀ i ∈ insert a s,
  (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
          i) :
      β) =
    f i
Tactic: use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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
hfat : f a ∈ t
⊢ ∀ i ∈ insert a s,
    (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
            i) :
        β) =
      f i
have h : ∀ (i : α),
  i = a ∨ i ∈ s →
    (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
            i) :
        β) =
      f i
Tactic: simp_rw [mem_insert]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
          i) :
      β) =
    f i
have h : (g' : (a : α) → ↥t) i ≠ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat
Tactic: rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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
hfat : f a ∈ t
i : α
hi : i ∈ s
h : (g' : (a : α) → ↥t) i ≠ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat
⊢ (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
          i) :
      β) =
    f i
have h₁ : Ne.{u_2 + 1} (α := ↥t) ((g' : (a : α) → ↥t) i : ↥t) ((g' : (a : α) → ↥t) a : ↥t)
Tactic: rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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 α)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have empty : ∀ {f : α → β} (hfst : image f ∅ ⊆ t) (hfs : Set.InjOn f (↑∅ : Set α)),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
    ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    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 => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
Cleared hypotheses: s, f, hfst, hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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 α)
empty :
  ∀ {f : α → β} (hfst : image f ∅ ⊆ t) (hfs : Set.InjOn f (↑∅ : Set α)),
    ∃ (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 ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have 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 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: classical
    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 => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
Cleared hypotheses: s, f, hfst, hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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 α)
empty :
  ∀ {f : α → β} (hfst : image f ∅ ⊆ t) (hfs : Set.InjOn f (↑∅ : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
      ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
insert 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
have 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 α))
  (hfst' : image f s ⊆ t),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    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 => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
Cleared hypotheses: s, f, hfst, hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
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 α)
empty :
  ∀ {f : α → β} (hfst : image f ∅ ⊆ t) (hfs : Set.InjOn f (↑∅ : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
      ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
insert 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
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 α))
    (hfst' : image f s ⊆ t),
    ∃ (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
have 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 α))
  (hfst' : image f s ⊆ t) (hfs' : Set.InjOn f (↑s : Set α)),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    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 => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
Cleared hypotheses: s, f, hfst, hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
s' : Finset α := s.toFinset
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have hfst' : Finset.image f s' ⊆ t
Tactic: have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have hfs' : InjOn f (↑s' : Set α)
Tactic: have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f (↑s' : Set α)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have obtain : ∀ (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 ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f (↑s' : Set α)
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 ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have refine : ∀ (i : α) (hi : i ∈ s), (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: refine ⟨g, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f (↑s' : Set α)
g : Equiv.{u_1 + 1, u_2 + 1} α ↥t
hg : ∀ i ∈ s', (↑((g : (a : α) → ↥t) i) : β) = f i
i : α
hi : i ∈ s
⊢ (↑((g : (a : α) → ↥t) i) : β) = f i
have a : i ∈ s'
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
let let₁ let₂ : ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have let₃ : let s' := s.toFinset;
∀ (hfst' : Finset.image f s' ⊆ t), ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
let let₁ let₂ : ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₃ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t), ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have let₄ : let s' := s.toFinset;
∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
let let₁ let₂ : ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₃ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t), ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₄ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have let₅ : let s' := s.toFinset;
∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (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 ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
let let₁ let₂ : ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₃ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t), ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₄ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₅ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (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 ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have let₆ : let s' := s.toFinset;
∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t)
  (hg : ∀ i ∈ s', (↑((g : (a : α) → ↥t) i) : β) = f i) (i : α) (hi : i ∈ s), (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi