awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hfat : f a ∈ t
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
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))

Premises used: Equiv.trans, Equiv.swap, Subtype.mk, DFunLike.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
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
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
⊢ ∀ 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:
simp_rw [mem_insert]

Premises used: Finset.mem_insert
-- 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 α
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 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
i : α
has : i ∉ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f (↑(insert i s) : Set α)
hfat : f i ∈ t
⊢ (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f i) hfat) ((g' : (a : α) → ↥t) i)) : (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 α)
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
h₁ : Ne.{u_2 + 1} (α := ↥t) ((g' : (a : α) → ↥t) i : ↥t) ((g' : (a : α) → ↥t) a : ↥t)
⊢ (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
          i) :
      β) =
    f i

Tactic:
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]

Premises used: Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne
-- 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
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ (g' : (a : α) → ↥t) i ≠ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat

Tactic:
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)

Premises used: Finset.mem_insert_self, ne_of_eq_of_ne, ne_of_apply_ne, ne_of_mem_of_not_mem, Finset.subset_insert, Set.InjOn.ne, Subtype.val
-- 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
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ (g' : (a : α) → ↥t) i ≠ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat

Tactic:
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)

Premises used: ne_of_eq_of_ne, ne_of_apply_ne, Subtype.val
-- 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
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ Ne.{u_2 + 1} (α := ↥t) ((g' : (a : α) → ↥t) i : ↥t) ((g' : (a : α) → ↥t) a : ↥t)

Tactic:
g'.injective.ne (ne_of_mem_of_not_mem hi has)

Premises used: Function.Injective.ne, ne_of_mem_of_not_mem, Equiv.injective
-- 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
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ Ne.{u_2 + 1} (α := ↥t) ((g' : (a : α) → ↥t) i : ↥t) ((g' : (a : α) → ↥t) a : ↥t)

Tactic:
exact g'.injective.ne (ne_of_mem_of_not_mem hi has)

Premises used: Function.Injective.ne, ne_of_mem_of_not_mem, Equiv.injective
-- Module: Mathlib.Data.Fintype.Sum
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
⊢ Finset.image f s' ⊆ t

Tactic:
simpa [s', ← Finset.coe_subset] using hfst

Premises used: Finset.coe_subset
-- Module: Mathlib.Data.Fintype.Sum
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
⊢ Finset.image f s' ⊆ t

Tactic:
have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
-- Module: Mathlib.Data.Fintype.Sum
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
⊢ InjOn f (↑s' : Set α)

Tactic:
simpa [s'] using hfs
-- Module: Mathlib.Data.Fintype.Sum
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
⊢ InjOn f (↑s' : Set α)

Tactic:
have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
-- Module: Mathlib.Data.Fintype.Sum
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 α)
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
⊢ ∃ (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'

Premises used: Finset.exists_equiv_extend_of_card_eq
-- Module: Mathlib.Data.Fintype.Sum
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

Tactic:
⟨g, fun i hi => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Fintype.Sum
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
refine : ∀ (i : α) (hi : 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:
refine ⟨g, fun i hi => ?_⟩
-- Module: Mathlib.Data.Fintype.Sum
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
a : i ∈ s'
⊢ (↑((g : (a : α) → ↥t) i) : β) = f i

Tactic:
apply hg
-- Module: Mathlib.Data.Fintype.Sum
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
⊢ i ∈ s'

Tactic:
simpa [s'] using hi
-- Module: Mathlib.Data.Fintype.Sum
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
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
a :
  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), i ∈ s'
⊢ ∃ (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
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } ≤ card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })

Tactic:
Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)

Premises used: subtypeOrLeftEmbedding, Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
h : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
⊢ card.{u_1} { x : α // p x ∨ q x } ≤ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }

Tactic:
convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)

Premises used: subtypeOrLeftEmbedding, Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
h h₁ :
  card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
⊢ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })

Tactic:
rw [Fintype.card_sum]

Premises used: Fintype.card_sum
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
h : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
⊢ card.{u_1} { x : α // p x ∨ q x } ≤ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }

Tactic:
classical
    convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
    rw [Fintype.card_sum]

Premises used: Fintype.card_sum
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })

Tactic:
Fintype.card_congr (subtypeOrEquiv p q h)

Premises used: Fintype.card_congr, subtypeOrEquiv
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
h₁ : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
⊢ card.{u_1} { x : α // p x ∨ q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }

Tactic:
convert! Fintype.card_congr (subtypeOrEquiv p q h)

Premises used: Fintype.card_congr, subtypeOrEquiv
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
h₁ : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
⊢ card.{u_1} { x : α // p x ∨ q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }

Tactic:
classical
    convert! Fintype.card_congr (subtypeOrEquiv p q h)
    simp
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_3
inst : Fintype α
inst_1 : DecidableEq α
a b : α
h : a ≠ b
⊢ card.{u_3} { c : α // c = a ∨ c = b } = 2

Tactic:
Fintype.card_subtype_or_disjoint _ _ fun _ ha hb _ hc ↦ ha _ hc ▸ hb _ hc ▸ h <| rfl

Premises used: Fintype.card, Multiset.cons, Fintype.card_subtype_or_disjoint, Multiset.ofList, Finset.card, Multiset.card
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Tactic:
⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩

Premises used: Sum.infinite_of_left, Sum.infinite_of_right, Iff.intro, Or.elim
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
refine : ∀ (H : Infinite (α ⊕ β)), Infinite α ∨ Infinite β
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Tactic:
refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
contrapose! : ∀ (H : Finite α ∧ Finite β), Finite (α ⊕ β)
⊢ Infinite α ∨ Infinite β

Tactic:
contrapose! H
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
H : Finite α ∧ Finite β
⊢ Finite α

Tactic:
cases H
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
H : Finite α ∧ Finite β
left : Finite α
⊢ Finite β

Tactic:
cases H
-- Module: Mathlib.Data.Fintype.Sum
Goal:
α : Type u_1
β : Type u_2
left : Finite α
right : Finite β
⊢ Finite (α ⊕ β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
x : ℤˣ
inl : x = 1 → Membership.mem (γ := Finset ℤˣ) {1, -1} x
inr : x = -1 → Membership.mem (γ := Finset ℤˣ) {1, -1} x
⊢ Membership.mem (γ := Finset ℤˣ) {1, -1} x

Tactic:
cases Int.units_eq_one_or x

Premises used: Int.units_eq_one_or
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
x : ℤˣ
h : x = 1
⊢ Membership.mem (γ := Finset ℤˣ) {1, -1} x

Tactic:
simp [*]
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
x : ℤˣ
h : x = -1
⊢ Membership.mem (γ := Finset ℤˣ) {1, -1} x

Tactic:
simp [*]
-- Module: Mathlib.Data.Fintype.Units
Goal:
⊢ Eq (α := Finset ℤˣ) Finset.univ {1, -1}

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Units
Goal:
⊢ card ℤˣ = 2

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : Finite α
⊢ Finite.{u_1 + 1} αˣ

Tactic:
.of_injective _ Units.val_injective

Premises used: Units.val_injective, Finite.of_injective
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1

Tactic:
rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]

Premises used: eq_comm, Nat.card_congr, unitsEquivNeZero, Equiv.sumCompl, OfNat.ofNat, Eq
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
inl :
  Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inr :
  Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }

Tactic:
rcases finite_or_infinite {a : α // a ≠ 0}

Premises used: finite_or_infinite, Subtype, Ne, OfNat.ofNat
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
h : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inl : Nat.card.{u_1} { a : α // a = 0 } + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inl₁ : 1 + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inl₂ inl₃ : Nat.card.{u_1} { a : α // ¬a = 0 } = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }

Tactic:
rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]

Premises used: Nat.card_sum, add_tsub_cancel_left, Nat.card_unique
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
h : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inr : HSub.hSub (α := ℕ) 0 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inr₁ : HSub.hSub (α := ℕ) 0 1 = 0
inr₂ inr₃ : Eq (α := ℕ) 0 0
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

Premises used: Nat.card_eq_zero_of_infinite, zero_tsub
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
rw₁ : Nat.card α - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
rw₂ rw₃ rw₄ : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inl :
  Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inr inr₁ :
  Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1

Tactic:
classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

Premises used: Nat.card_eq_zero_of_infinite, Nat.card_sum, finite_or_infinite, add_tsub_cancel_left, Subtype, Ne, eq_comm, Nat.card_congr, unitsEquivNeZero, Nat.card_unique, OfNat.ofNat, zero_tsub
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Finite α
rw : Nat.card α = Nat.card α - 1 + 1
rw₁ rw₂ : Nat.card α = Nat.card α
⊢ Nat.card α = Nat.card.{u_1} αˣ + 1

Tactic:
rw [Nat.card_units, tsub_add_cancel_of_le Nat.card_pos]

Premises used: Nat.card_units, tsub_add_cancel_of_le
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
rw : Nat.card.{u_1} αˣ = card α - 1
rw₁ : Nat.card α - 1 = card α - 1
rw₂ rw₃ : card α - 1 = card α - 1
⊢ card.{u_1} αˣ = card α - 1

Tactic:
rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]

Premises used: Nat.card_units, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Fintype.Units
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
rw : card α = card α - 1 + 1
rw₁ rw₂ : card α = card α
⊢ card α = card.{u_1} αˣ + 1

Tactic:
rw [Fintype.card_units, tsub_add_cancel_of_le Fintype.card_pos]

Premises used: Fintype.card_units, tsub_add_cancel_of_le
-- Module: Mathlib.Data.Fintype.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Vector α n)

Tactic:
Finite.of_equiv _ (Equiv.vectorEquivFin _ _).symm

Premises used: Finite.of_equiv, Equiv.vectorEquivFin, Equiv.symm
-- Module: Mathlib.Data.Fintype.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Sym' α n)

Tactic:
inferInstanceAs <| Finite (Quotient _)

Premises used: _private.0.Sym.Sym'.instFinite._proof_1
-- Module: Mathlib.Data.Fintype.Vector
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Sym α n)

Tactic:
Finite.of_equiv _ Sym.symEquivSym'.symm

Premises used: Finite.of_equiv, Sym.symEquivSym', Equiv.symm