awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst : Decidable p
α : p → Type u_4
inst_1 : (hp : p) → Fintype (α hp)
hp : ¬p
h : (hp : p) → α hp
x : p
⊢ h x = ⋯.elim

Tactic:
contradiction
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
s : Multiset α
l : List α
h : ∃ (x : α), x ∈ ⟦l⟧
h_1 : ∃ (x : α), x ∈ ⟦[]⟧
tauto : ∀ w ∈ ⟦l⟧, ∀ w ∈ ⟦[]⟧, False
⊢ False

Tactic:
tauto
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Nonempty α
inst_1 : Fintype α
⊢ ∃ (x : α), Membership.mem (γ := Multiset α) (val univ) x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a : α
⊢ count a (val univ) = 1

Tactic:
count_eq_one_of_mem Finset.univ.nodup (Finset.mem_univ _)

Premises used: Finset.mem_univ, Finset.univ, Finset.nodup, Multiset.count_eq_one_of_mem
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
e : α ≃ β
rw : map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ) = (Finset.map e.toEmbedding univ).val
rw₁ :
  Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
    (map.{u_2, u_1} (α := α) (⇑e.toEmbedding : (a : α) → β) (val univ))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
    (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
⊢ Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ)) (val univ)

Tactic:
rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]

Premises used: Equiv.coe_toEmbedding, Finset.map_univ_equiv, Finset.val, congr_arg, Finset.map_val
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
⊢ Bijective f ↔ map f (val univ) = val univ

Tactic:
⟨fun bij ↦ congr_arg (·.val) (map_univ_equiv <| Equiv.ofBijective f bij),
    fun eq ↦ ⟨
      fun a₁ a₂ ↦ inj_on_of_nodup_map (eq.symm ▸ univ.nodup) _ (mem_univ a₁) _ (mem_univ a₂),
      fun b ↦ have ⟨a, _, h⟩ := mem_map.mp (eq.symm ▸ mem_univ_val b); ⟨a, h⟩⟩⟩

Premises used: Finset.mem_univ, Multiset.inj_on_of_nodup_map, And.intro, Iff.intro
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → P x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
rcases : ∀ (y : α), (P y ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r x y) → Nonempty α
⊢ Nonempty α

Tactic:
rcases h ∅ (by simp) with ⟨y, _⟩

Premises used: EmptyCollection.emptyCollection
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
y : α
h_1 : P y ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r x y
⊢ Nonempty α

Tactic:
⟨y⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
y : α
h_1 : P y ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r x y
⊢ Nonempty α

Tactic:
exact ⟨y⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ Nonempty α

Tactic:
have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
this : Nonempty α
choose! :
  ∀ (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
choose! F hF using h
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
⊢ ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y

Tactic:
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
⊢ let f := seqOfForallFinsetExistsAux P r h';
  f = seqOfForallFinsetExistsAux P r h'

Tactic:
set f := seqOfForallFinsetExistsAux P r h' with hf

Premises used: seqOfForallFinsetExistsAux
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
h : ∀ (n : ℕ) (IH : ∀ m < n, P (f m)), P (f n)
⊢ P (f n)

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
h : ∀ (IH' : ∀ (x : Fin n), P (f (↑x : ℕ))), P (f n)
⊢ P (f n)

Tactic:
have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f (↑x : ℕ))
h :
  P
    (Classical.choose (p := fun (x : α) ↦
      (∀ (x : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
            P x) →
        P x ∧
          ∀ (x_1 : α),
            Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                x_1 →
              r x_1 x)
      ⋯)
⊢ P (f n)

Tactic:
rw [hf, seqOfForallFinsetExistsAux]

Premises used: seqOfForallFinsetExistsAux
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f (↑x : ℕ))
⊢ ∀ (x : α), Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) x → P x

Tactic:
simp [IH']
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f (↑x : ℕ))
⊢ P
    (Classical.choose (p := fun (x : α) ↦
      (∀ (x : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
            P x) →
        P x ∧
          ∀ (x_1 : α),
            Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                x_1 →
              r x_1 x)
      ⋯)

Tactic:
exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1

Premises used: Finset.univ, Fin.val, Classical.choose_spec, And.left, Finset.image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∀ (n : ℕ), P (f n)

Tactic:
have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
⟨f, A, fun m n hmn => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
refine : ∀ (m n : ℕ) (hmn : m < n), r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
refine ⟨f, A, fun m n hmn => ?_⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
rw : seqOfForallFinsetExistsAux P r h' n
| f n

Tactic:
rw [hf]
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
conv_rhs : r (f m) (seqOfForallFinsetExistsAux P r h' n)
⊢ r (f m) (f n)

Tactic:
conv_rhs => rw [hf]
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
rw :
  r (f m)
    (Classical.choose (p := fun (x : α) ↦
      (∀ (x : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
            P x) →
        P x ∧
          ∀ (x_1 : α),
            Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                x_1 →
              r x_1 x)
      ⋯)
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)

Tactic:
rw [seqOfForallFinsetExistsAux]

Premises used: seqOfForallFinsetExistsAux
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ ∀ (x : α), Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) x → P x

Tactic:
simp [A]
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
a : Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) (f m)
⊢ r (f m)
    (Classical.choose (p := fun (x : α) ↦
      (∀ (x : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
            P x) →
        P x ∧
          ∀ (x_1 : α),
            Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                x_1 →
              r x_1 x)
      ⋯)

Tactic:
apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2

Premises used: Finset.univ, Fin.val, Classical.choose_spec, And.right, Finset.image
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) (f m)

Tactic:
Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Fin.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) (f m)

Tactic:
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
rcases :
  ∀ (f : ℕ → α) (hf : ∀ (n : ℕ), P (f n)) (hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩

Premises used: exists_seq_of_forall_finset_exists
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
⟨f, hf, fun m n hmn => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
refine : ∀ (m n : ℕ) (hmn : m ≠ n), (r on f) m n
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
refine ⟨f, hf, fun m n hmn => ?_⟩
-- Module: Mathlib.Data.Fintype.Basic
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
⊢ (r on f) m n

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : CommMonoid α
f : Bool → α
⊢ ∏ b : Bool, f b = f true * f false

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_4
inst : Fintype α
⊢ card α = ∑ _a : α, 1

Tactic:
Finset.card_eq_sum_ones _

Premises used: Finset.card_eq_sum_ones, Fintype.card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommMonoid α
s : Finset ι
f : ι → α
rw : Eq.{u_1 + 1} (α := α) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
rw₁ : Eq.{u_1 + 1} (α := α) (∏ a ∈ univ ∩ s, f a) (∏ i ∈ s, f i)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (∏ a ∈ s, f a) (∏ i ∈ s, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)

Tactic:
rw [← prod_filter, filter_mem_eq_inter, univ_inter]

Premises used: Finset.prod_filter, Finset.univ_inter, Finset.filter_mem_eq_inter
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
h : ∀ (a : α), f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a : α, f a) 1

Tactic:
Finset.prod_eq_one fun a _ha => h a

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f g : α → M
h : ∀ (a : α), f a = g a
⊢ Eq.{u_4 + 1} (α := M) (∏ a : α, f a) (∏ a : α, g a)

Tactic:
Finset.prod_congr rfl fun a _ha => h a

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a : α
h : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ x : α, f x = f a

Tactic:
Finset.prod_eq_single a (fun x _ hx => h x hx) fun ha => (ha (Finset.mem_univ a)).elim

Premises used: Finset.mem_univ, False.elim, Finset.prod_eq_single
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
ha : a ∉ Finset.univ → f a = 1
hb : b ∉ Finset.univ → f b = 1
⊢ ∏ x : α, f x = f a * f b

Tactic:
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx

Premises used: Finset.prod_eq_mul
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ a ∉ Finset.univ → f a = 1

Tactic:
fun hc => (hc (Finset.mem_univ _)).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ a ∉ Finset.univ → f a = 1

Tactic:
exact fun hc => (hc (Finset.mem_univ _)).elim
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ b ∉ Finset.univ → f b = 1

Tactic:
fun hc => (hc (Finset.mem_univ _)).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ b ∉ Finset.univ → f b = 1

Tactic:
exact fun hc => (hc (Finset.mem_univ _)).elim
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
M : Type u_4
inst : CommMonoid M
ι : Type u_5
inst_1 : Subsingleton ι
s : Finset ι
f : ι → M
b : M
h : ∏ i ∈ s, f i = b
⊢ ∀ i ∈ s, f i = b

Tactic:
Finset.eq_of_card_le_one_of_prod_eq (Finset.card_le_one_of_subsingleton s) h

Premises used: Finset.eq_of_card_le_one_of_prod_eq, Finset.card_le_one_of_subsingleton
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : Option α → M
⊢ ∏ i : Option α, f i = f none * ∏ i : α, f (some i)

Tactic:
Finset.prod_insertNone f univ

Premises used: Finset.univ, Finset.prod_insertNone
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
inst_2 : DecidableEq α
f : α → M
a : α
simp_rw :
  ∏ i : Option { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) i) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
simp_rw₁ :
  f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) none) *
      ∏ i : { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some i)) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
simp_rw₂ :
  f a * ∏ i : { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some i)) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
⊢ ∏ i : α, f i = f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)

Tactic:
simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]

Premises used: Fintype.prod_option, Equiv.prod_comp, Equiv.optionSubtypeNe, Equiv.optionSubtypeNe_some, Equiv.optionSubtypeNe_none
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ #(s.pi (β := α) t) = ∏ i ∈ s, #(t i)

Tactic:
Multiset.card_pi _ _

Premises used: Multiset.card_pi, Set.Mem, setOf, Multiset.recOn, Finset.prod, Multiset.Mem, Multiset.rec, Multiset.pi, Finset.card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
s : (i : ι) → Finset (α i)
⊢ #(piFinset (δ := α) s) = ∏ i : ι, #(s i)

Tactic:
simp [piFinset, card_map]

Premises used: Finset.card_map, Fintype.piFinset
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_7
s : Finset α
n : ℕ
⊢ Finset.card.{u_7} (α := (a : Fin n) → α) (piFinset (δ := fun (x : Fin n) ↦ α) fun (x : Fin n) ↦ s) = #s ^ n

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Fintype (α i)
⊢ card ((i : ι) → α i) = ∏ i : ι, card.{u_6} (α i)

Tactic:
card_piFinset _

Premises used: Finset.univ, Finset.map, Fintype.card_piFinset, Fintype.card, Fintype.piFinset
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_7
inst : Fintype α
n : ℕ
⊢ card.{u_7} (Fin n → α) = card α ^ n

Tactic:
card_piFinset_const _ _

Premises used: Finset.univ, Fintype.card_piFinset_const, Finset.map, Fintype.card, Fintype.piFinset
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_9
α : ι → Type u_7
M : Type u_8
inst : Fintype ι
inst_1 : (i : ι) → Fintype (α i)
inst_2 : CommMonoid M
f : Sigma α → M
⊢ Eq.{u_8 + 1} (α := M) (∏ x : Sigma α, f x) (∏ x : ι, ∏ y : α x, f (Sigma.mk (β := α) x y))

Tactic:
Finset.prod_sigma ..

Premises used: Finset.univ, Finset.sigma, Finset.prod_sigma
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_9
α : ι → Type u_7
M : Type u_8
inst : Fintype ι
inst_1 : (i : ι) → Fintype (α i)
inst_2 : CommMonoid M
f : (i : ι) → α i → M
⊢ Eq.{u_8 + 1} (α := M) (∏ x : Sigma α, f (x.fst (β := α)) (x.snd (β := α))) (∏ x : ι, ∏ y : α x, f x y)

Tactic:
prod_sigma ..

Premises used: Fintype.prod_sigma
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_8
α : ι → Type u_7
inst : Fintype ι
inst_1 : (i : ι) → Fintype (α i)
⊢ card (Sigma α) = ∑ i : ι, card.{u_7} (α i)

Tactic:
card_sigma _ _

Premises used: Finset.univ, Fintype.card, Finset.sigma, Finset.card_sigma