awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)

Tactic:
le_add_of_le_right hle

Premises used: le_add_of_le_right
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)

Tactic:
exact le_add_of_le_right hle

Premises used: le_add_of_le_right
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), t ⊆ s
suffices₄ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
suffices₅ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)),
    ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
suffices₆ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)),
    ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)

Tactic:
classical
  suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
⊢ StrictMonoOn (α := Set α) (Nat.card ∘ Elem) (setOf Set.Finite)

Tactic:
fun _ _ _ ↦ card_lt_card

Premises used: Set.Finite.card_lt_card, Set.Mem, setOf, Set.Finite, Nat.card, StrictMonoOn
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
⊢ StrictMonoOn (α := Set α) (ENat.card ∘ Elem) (setOf Set.Finite)

Tactic:
fun _ hs _ _ ↦ hs.ecard_lt_ecard

Premises used: Set.Finite.ecard_lt_ecard, StrictMonoOn, ENat.card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊆ t
hcard : Nat.card.{u_1} (↑t : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1)
⊢ s = t

Tactic:
(eq_or_ssubset_of_subset hsub).elim id fun h ↦ absurd hcard <| not_le_of_gt <| ht.card_lt_card h

Premises used: Set.Finite.card_lt_card, id, absurd, eq_or_ssubset_of_subset, not_le_of_gt, Or.elim
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : (⇑e : (a : α) → α) '' s = s
rw rw₁ : s ⊆ s
⊢ (⇑e : (a : α) → α) '' s ⊆ s

Tactic:
rw [h]
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
⊢ StrictMono (α := Set α) (Nat.card ∘ Elem)

Tactic:
fun _ t ↦ t.toFinite.card_lt_card

Premises used: StrictMono, Set.Finite.card_lt_card, Nat.card, Set.toFinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
⊢ StrictMono (α := Set α) (ENat.card ∘ Elem)

Tactic:
fun s _ ↦ s.toFinite.ecard_lt_ecard

Premises used: StrictMono, Set.toFinite, Set.Finite.ecard_lt_ecard, ENat.card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
s : Set α
h : Nat.card α ≤ Nat.card.{u_1} (↑s : Type u_1)
⊢ s = ⊤

Tactic:
Set.Finite.eq_of_subset_of_card_le univ.toFinite (subset_univ s) <|
    Nat.card_congr (Equiv.Set.univ α) ▸ h

Premises used: Set.subset_univ, Set.univ, Eq.rec, Nat.card_congr, Set.toFinite, Set.Finite.eq_of_subset_of_card_le, Eq.symm, Equiv.Set.univ
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
inst : Finite α
have : ∀ (this : Fintype α), l.length ≤ Nat.card α
⊢ l.length ≤ Nat.card α

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
inst : Finite α
this : Fintype α
grw : Fintype.card α ≤ Nat.card α
grw₁ grw₂ : Nat.card α ≤ Nat.card α
⊢ l.length ≤ Nat.card α

Tactic:
grw [h.length_le_card, Fintype.card_eq_nat_card]

Premises used: List.Nodup.length_le_card, Fintype.card_eq_nat_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
inl : Finite α → (↑l.length : ℕ∞) ≤ ENat.card α
inr : Infinite α → (↑l.length : ℕ∞) ≤ ENat.card α
⊢ (↑l.length : ℕ∞) ≤ ENat.card α

Tactic:
cases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Finite α
inl : (↑(Nat.card α) : ℕ∞) ≤ ENat.card α
inl₁ inl₂ : LE.le (α := ℕ∞) (↑(Nat.card α) : ℕ∞) (↑(Nat.card α) : ℕ∞)
⊢ (↑l.length : ℕ∞) ≤ ENat.card α

Tactic:
grw [h.length_le_natCard, ENat.card_eq_coe_natCard]

Premises used: List.Nodup.length_le_natCard, ENat.card_eq_coe_natCard
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Infinite α
inr : LE.le (α := ℕ∞) (↑l.length : ℕ∞) ⊤
⊢ (↑l.length : ℕ∞) ≤ ENat.card α

Tactic:
grw [ENat.card_eq_top_of_infinite]

Premises used: ENat.card_eq_top_of_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Infinite α
⊢ LE.le (α := ℕ∞) (↑l.length : ℕ∞) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Infinite α
⊢ LE.le (α := ℕ∞) (↑l.length : ℕ∞) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_3
⊢ Finite α ↔ ∃ (n : ℕ), Nonempty.{max 1 u_3} (α ≃ Fin n)

Tactic:
⟨fun ⟨e⟩ => ⟨_, ⟨e⟩⟩, fun ⟨_, ⟨e⟩⟩ => ⟨e⟩⟩

Premises used: Finite.intro, Finite, Exists, Equiv, Nonempty.intro, Iff.intro, Exists.intro, Nonempty, Fin, _private.0.finite_iff_exists_equiv_fin.match_1, _private.0.finite_iff_exists_equiv_fin.match_2
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_3
h : Finite α
⊢ ∃ (n : ℕ), Nonempty.{max 1 u_3} (α ≃ Fin n)

Tactic:
finite_iff_exists_equiv_fin.mp h

Premises used: Iff.mp, finite_iff_exists_equiv_fin
-- Module: Mathlib.Data.Finite.Defs
Goal:
β : Sort u_2
α : Sort u_3
h : Finite α
f : α ≃ β
⊢ Finite β

Tactic:
let ⟨e⟩ := h; ⟨f.symm.trans e⟩

Premises used: Finite.intro, Equiv.trans, Finite, Equiv.symm, _private.0.finite_iff_exists_equiv_fin.match_1
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
f : α ≃ β
⊢ Finite α ↔ Finite β

Tactic:
⟨fun _ => Finite.of_equiv _ f, fun _ => Finite.of_equiv _ f.symm⟩

Premises used: Finite.of_equiv, Iff.intro, Equiv.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
h : Bijective f
⊢ Finite α ↔ Finite β

Tactic:
(Equiv.ofBijective f h).finite_iff

Premises used: Equiv.finite_iff, Equiv.ofBijective
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
inst : Finite α
f : α → β
h : Bijective f
⊢ Finite β

Tactic:
h.finite_iff.mp ‹_›

Premises used: Iff.mp, Function.Bijective.finite_iff
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
inst : Finite α
⊢ Nonempty.{max 1 u_1} (DecidableEq α)

Tactic:
let ⟨_n, ⟨e⟩⟩ := Finite.exists_equiv_fin α; ⟨e.decidableEq⟩

Premises used: Equiv.decidableEq, Nonempty.intro, Finite.exists_equiv_fin, Nonempty, _private.0.Finite.nonempty_decidableEq.match_1, DecidableEq
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
inst : Finite α
⊢ Finite.{u_1 + 1} (PLift α)

Tactic:
Finite.of_equiv α Equiv.plift.symm

Premises used: Finite.of_equiv, Equiv.plift, Equiv.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α_1 : Sort u_1
β : Sort u_2
α : Type v
inst : Finite α
⊢ Finite (ULift.{u, v} α)

Tactic:
Finite.of_equiv α Equiv.ulift.symm

Premises used: Finite.of_equiv, Equiv.ulift, Equiv.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
⊢ ¬Finite α ↔ Infinite α

Tactic:
⟨Infinite.mk, fun h => h.1⟩

Premises used: Infinite.mk, Iff.intro, Infinite.not_finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
⊢ ¬Infinite α ↔ Finite α

Tactic:
not_finite_iff_infinite.not_right.symm

Premises used: not_finite_iff_infinite, Iff.not_right, Iff.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Infinite α ↔ Infinite β

Tactic:
not_finite_iff_infinite.symm.trans <| e.finite_iff.not.trans not_finite_iff_infinite

Premises used: not_finite_iff_infinite, Equiv.finite_iff, Iff.not, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
inst : Infinite α
⊢ Infinite.{u_1 + 1} (PLift α)

Tactic:
Equiv.plift.infinite_iff.2 ‹_›

Premises used: Iff.mpr, Equiv.plift, Equiv.infinite_iff
-- Module: Mathlib.Data.Finite.Defs
Goal:
α_1 : Sort u_1
β : Sort u_2
α : Type v
inst : Infinite α
⊢ Infinite (ULift.{u, v} α)

Tactic:
Equiv.ulift.infinite_iff.2 ‹_›

Premises used: Iff.mpr, Equiv.ulift, Equiv.infinite_iff
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_3
⊢ Finite α ∨ Infinite α

Tactic:
or_iff_not_imp_left.2 not_finite_iff_infinite.1

Premises used: Iff.mpr, not_finite_iff_infinite, Classical.or_iff_not_imp_left, Iff.mp
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_3
inst : Infinite α
inst_1 : Finite α
⊢ False

Tactic:
@Infinite.not_finite α ‹_› ‹_›

Premises used: Infinite.not_finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
inst : Infinite α
h : Finite α
⊢ False

Tactic:
not_finite α

Premises used: not_finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
inst : Finite α
h : Infinite α
⊢ False

Tactic:
@Infinite.not_finite α ‹_› ‹_›

Premises used: Infinite.not_finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
⊢ Finite Bool

Tactic:
.intro finTwoEquiv.symm

Premises used: Finite.intro, finTwoEquiv, Equiv.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Sort u_1
β : Sort u_2
⊢ Finite Prop

Tactic:
.of_equiv _ Equiv.propEquivBool.symm

Premises used: Equiv.propEquivBool, Finite.of_equiv, Equiv.symm
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ Finite.{u + 1} (↑s : Type u) ↔ s.Finite

Tactic:
.rfl

Premises used: Iff.rfl, Set.Finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
h : s.Finite
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
h

Premises used: Set.Finite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ ¬s.Finite ↔ s.Infinite

Tactic:
.rfl

Premises used: Iff.rfl, Set.Infinite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ ¬s.Infinite ↔ s.Finite

Tactic:
not_not

Premises used: Classical.not_not, Set.Infinite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
hs : s.Infinite
⊢ ¬s.Finite

Tactic:
hs

Premises used: Set.Infinite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ s.Finite ∨ s.Infinite

Tactic:
em _

Premises used: em, Set.Infinite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ s.Infinite ∨ s.Finite

Tactic:
em' _

Premises used: em', Set.Infinite
-- Module: Mathlib.Data.Finite.Defs
Goal:
α : Type u
s : Set α
⊢ Infinite.{u + 1} (↑s : Type u) ↔ s.Infinite

Tactic:
not_finite_iff_infinite.symm.trans finite_coe_iff.not

Premises used: not_finite_iff_infinite, Iff.not, Set.finite_coe_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
have : ∀ (this : Fintype α), Nat.card.{u_1} (Perm α) = (Nat.card α)!
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
rw : Fintype.card.{u_1} (Perm α) = (Nat.card α)!
rw₁ : Fintype.card.{u_1} (Perm α) = (Fintype.card α)!
rw₂ rw₃ : (Fintype.card α)! = (Fintype.card α)!
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!

Tactic:
rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

Premises used: Fintype.card_perm, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
have have₁ have₂ : ∀ (this : Fintype α), Nat.card.{u_1} (Perm α) = (Nat.card α)!
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!

Tactic:
classical
  have := Fintype.ofFinite α
  rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

Premises used: Fintype.card_perm, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
hα : Nat.card α ≤ 2
apply : Nat.card.{u_1} (Perm α) ∣ 2
⊢ IsCyclic.{u_1} (Perm α)

Tactic:
apply isCyclic_of_card_dvd_prime (p := 2)

Premises used: isCyclic_of_card_dvd_prime
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
hα : Nat.card α ≤ 2
⊢ Nat.card.{u_1} (Perm α) ∣ 2

Tactic:
simpa [card_perm] using factorial_dvd_factorial hα

Premises used: Nat.card_perm, Nat.factorial_dvd_factorial
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
⊢ IsMulCommutative.{u_1} (Perm α) ↔ Nat.card α ≤ 2

Tactic:
⟨?_, fun h ↦ (isCyclic_of_card_le_two h).isMulCommutative⟩

Premises used: IsCyclic.isMulCommutative, Iff.intro
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
refine : IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
⊢ IsMulCommutative.{u_1} (Perm α) ↔ Nat.card α ≤ 2

Tactic:
refine ⟨?_, fun h ↦ (isCyclic_of_card_le_two h).isMulCommutative⟩
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
rw :
  ¬∃ (a : α) (b : α) (c : α),
      Membership.mem (γ := Set α) _root_.Set.univ a ∧
        Membership.mem (γ := Set α) _root_.Set.univ b ∧
          Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ Nat.card α ≤ 2

Tactic:
rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]

Premises used: Set.two_lt_ncard_iff, not_lt, Set.ncard_univ
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left : Membership.mem (γ := Set α) _root_.Set.univ a
left_1 : Membership.mem (γ := Set α) _root_.Set.univ b
left_2 : Membership.mem (γ := Set α) _root_.Set.univ c
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
apply : b = c
⊢ False

Tactic:
apply hbc
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left : Membership.mem (γ := Set α) _root_.Set.univ a
left_1 : Membership.mem (γ := Set α) _root_.Set.univ b
left_2 : Membership.mem (γ := Set α) _root_.Set.univ c
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∀ (a b : Perm α) (x : α), Eq (α := α) ((a * b : (a : α) → α) x : α) ((b * a : (a : α) → α) x : α)

Tactic:
simp_rw [Perm.ext_iff] at h

Premises used: Equiv.Perm.ext_iff
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
a b c : α
left : Membership.mem (γ := Set α) _root_.Set.univ a
left_1 : Membership.mem (γ := Set α) _root_.Set.univ b
left_2 : Membership.mem (γ := Set α) _root_.Set.univ c
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
h : ∀ (a b : Perm α) (x : α), Eq (α := α) ((a * b : (a : α) → α) x : α) ((b * a : (a : α) → α) x : α)
⊢ b = c

Tactic:
simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a

Premises used: Equiv.swap, Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
rintro₁ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a),
    ¬∃ (a : α) (b : α) (c : α),
        Membership.mem (γ := Set α) _root_.Set.univ a ∧
          Membership.mem (γ := Set α) _root_.Set.univ b ∧
            Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
rintro₂ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), False
rintro₃ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), b = c
rintro₄ :
  ∀ (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c →
          ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
            (h : ∀ (a b : Perm α) (x : α), Eq (α := α) ((a * b : (a : α) → α) x : α) ((b * a : (a : α) → α) x : α)),
            b = c
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2

Tactic:
classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a

Premises used: Equiv.Perm.ext_iff, Set.two_lt_ncard_iff, not_lt, Set.ncard_univ
-- Module: Mathlib.Data.Finite.Perm
Goal:
α : Type u_1
inst : Finite α
⊢ IsCyclic.{u_1} (Perm α) ↔ Nat.card α ≤ 2

Tactic:
⟨fun h ↦ isMulCommutative_iff_card_le_two.mp h.isMulCommutative, isCyclic_of_card_le_two⟩

Premises used: Equiv.Perm.isCyclic_of_card_le_two, IsCyclic.isMulCommutative, Iff.intro, Iff.mp, Equiv.Perm.isMulCommutative_iff_card_le_two
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
haveI : ∀ (this : Fintype α), Finite (α × β)
⊢ Finite (α × β)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
haveI : ∀ (this : Fintype β), Finite (α × β)
⊢ Finite (α × β)

Tactic:
haveI := Fintype.ofFinite β
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this_1 : Fintype α
this : Fintype β
⊢ Finite (α × β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite α
inst_1 : Finite β
⊢ Finite (α ×' β)

Tactic:
of_equiv _ Equiv.pprodEquivProdPLift.symm

Premises used: Finite.of_equiv, Equiv.pprodEquivProdPLift, Equiv.symm
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_3
inst : Finite (α × β)
inst_1 : Nonempty β
⊢ Finite α

Tactic:
of_surjective (Prod.fst : α × β → α) Prod.fst_surjective

Premises used: Prod.fst_surjective, Prod.fst, Finite.of_surjective
-- Module: Mathlib.Data.Finite.Prod
Goal:
β : Type u_2
α : Type u_3
inst : Finite (α × β)
inst_1 : Nonempty α
⊢ Finite β

Tactic:
of_surjective (Prod.snd : α × β → β) Prod.snd_surjective

Premises used: Prod.snd_surjective, Prod.snd, Finite.of_surjective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
haveI : ∀ (this : Fintype (PLift α)), Finite ((a : α) → β a)
⊢ Finite ((a : α) → β a)

Tactic:
haveI := Fintype.ofFinite (PLift α)
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
this : Fintype (PLift α)
haveI : ∀ (this : (a : α) → Fintype (PLift (β a))), Finite ((a : α) → β a)
⊢ Finite ((a : α) → β a)

Tactic:
haveI := fun a => Fintype.ofFinite (PLift (β a))
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
this_1 : Fintype (PLift α)
this : (a : α) → Fintype (PLift (β a))
⊢ Finite ((a : α) → β a)

Tactic:
Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Premises used: Finite.of_equiv, Equiv.plift, Equiv.piCongr
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
this_1 : Fintype (PLift α)
this : (a : α) → Fintype (PLift (β a))
⊢ Finite ((a : α) → β a)

Tactic:
exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Premises used: Finite.of_equiv, Equiv.plift, Equiv.piCongr
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
haveI haveI₁ haveI₂ : ∀ (this : Fintype (PLift α)), Finite ((a : α) → β a)
haveI₃ : ∀ (this : Fintype (PLift α)) (this : (a : α) → Fintype (PLift (β a))), Finite ((a : α) → β a)
⊢ Finite ((a : α) → β a)

Tactic:
classical
  haveI := Fintype.ofFinite (PLift α)
  haveI := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)

Premises used: Finite.of_equiv, Equiv.plift, Equiv.piCongr
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
inl : IsEmpty (α ↪ β) → Finite (α ↪ β)
inr : ∀ (h : Nonempty (α ↪ β)), Finite (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
rcases isEmpty_or_nonempty (α ↪ β) with _ | h

Premises used: isEmpty_or_nonempty, Function.Embedding
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : IsEmpty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
h.elim fun f => ?_

Premises used: Nonempty.elim
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
inr : ∀ (f : α ↪ β), Finite (α ↪ β)
⊢ Finite (α ↪ β)

Tactic:
refine h.elim fun f => ?_

Premises used: Nonempty.elim
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite α

Tactic:
haveI : Finite α := Finite.of_injective _ f.injective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)

Tactic:
Finite.of_injective _ DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Finite.of_injective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)

Tactic:
exact Finite.of_injective _ DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Finite.of_injective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
e₁ e₂ : α ≃ β
h : e₁.toEmbedding = e₂.toEmbedding
⊢ ∀ (x : α), Eq.{u_4} (α := β) ((e₁.toEmbedding : (a : α) → β) x : β) ((e₂.toEmbedding : (a : α) → β) x : β)

Tactic:
DFunLike.congr_fun h

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
e₁ e₂ : α ≃ β
h : e₁.toEmbedding = e₂.toEmbedding
⊢ ∀ (x : α), Eq.{u_4} (α := β) ((e₁ : (a : α) → β) x : β) ((e₂ : (a : α) → β) x : β)

Tactic:
convert! DFunLike.congr_fun h using 0

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite α
⊢ Finite (α ≃ β)

Tactic:
Finite.of_equiv _ ⟨Equiv.symm, Equiv.symm, Equiv.symm_symm, Equiv.symm_symm⟩

Premises used: Finite.of_equiv, Equiv.mk, Equiv.symm_symm, Equiv.symm
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : Mul β
inst_2 : Finite α
⊢ Finite (α ≃* β)

Tactic:
Finite.of_injective toEquiv toEquiv_injective

Premises used: MulEquiv.toEquiv, MulEquiv.toEquiv_injective, Finite.of_injective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : Mul β
inst_2 : Finite β
⊢ Finite (α ≃* β)

Tactic:
Finite.of_injective toEquiv toEquiv_injective

Premises used: MulEquiv.toEquiv, MulEquiv.toEquiv_injective, Finite.of_injective
-- Module: Mathlib.Data.Finite.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_2)
⊢ ∀ (x : α × β), x ∈ s.toFinset ×ˢ t.toFinset ↔ x ∈ s ×ˢ t

Tactic:
simp