awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
by_contra! : ∀ (this : ∀ (b : α) (_ : b ∈ s), b = a), False
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra!
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this_1 : Nonempty α
this : ∀ (b : α) (_ : b ∈ s), b = a
⊢ False

Tactic:
hs.not_ge (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

Premises used: Iff.mpr, Finset.card_le_one_iff_subset_singleton, Exists.intro, Finset.subset_singleton_iff', LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this_1 : Nonempty α
this : ∀ (b : α) (_ : b ∈ s), b = a
⊢ False

Tactic:
exact hs.not_ge (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

Premises used: Iff.mpr, Finset.card_le_one_iff_subset_singleton, Exists.intro, Finset.subset_singleton_iff', LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : Subsingleton α
s : Finset α
⊢ #s ≤ 1

Tactic:
Finset.card_le_one_iff.2 fun {_ _ _ _} => Subsingleton.elim _ _

Premises used: Iff.mpr, Finset.card_le_one_iff, Subsingleton.elim
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
contrapose! : #s ≤ 1 ↔ ∀ (a : α) (_ : a ∈ s) (b : α) (_ : b ∈ s), a = b
⊢ 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ (a : α) (_ : a ∈ s) (b : α) (_ : b ∈ s), a = b

Tactic:
card_le_one

Premises used: Finset.card_le_one
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ (a : α) (_ : a ∈ s) (b : α) (_ : b ∈ s), a = b

Tactic:
exact card_le_one

Premises used: Finset.card_le_one
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
rw : (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
⊢ 1 < #s ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [one_lt_card]

Premises used: Finset.one_lt_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_and_left]

Premises used: exists_and_left
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
rw₃ : #s ≤ 1 ↔ ¬Nontrivial.{u_1} (↑(↑s : Set α) : Type u_1)
rw₄ : #s ≤ 1 ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
rw₅ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
rw₆ rw₇ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} ↥s
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]

Premises used: Finset.coe_sort_coe, not_iff_not, Finset.card_le_one_iff_subsingleton_coe, not_nontrivial_iff_subsingleton, not_lt, Finset.Nontrivial, Set.nontrivial_coe_sort
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
simp_rw :
  ∀ (h : ∃ (a : (i : ι) → α i) (b : (i : ι) → α i), a ∈ s ∧ b ∈ s ∧ ∃ (a_1 : ι), a a_1 ≠ b a_1),
    ∃ (i : ι),
      (∃ (a : α i) (b : α i),
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
            Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
        ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
⊢ ∃ (i : ι), 1 < card.{u_5} (α := α i) (image (fun (x : (i : ι) → α i) ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
simp_rw [one_lt_card_iff, Function.ne_iff] at h ⊢

Premises used: Finset.one_lt_card_iff, Function.ne_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : ∃ (a : (i : ι) → α i) (b : (i : ι) → α i), a ∈ s ∧ b ∈ s ∧ ∃ (a_1 : ι), a a_1 ≠ b a_1
obtain :
  ∀ (a1 a2 : (i : ι) → α i) (h1 : a1 ∈ s) (h2 : a2 ∈ s) (i : ι) (hne : a1 i ≠ a2 i),
    ∃ (i : ι),
      (∃ (a : α i) (b : α i),
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
            Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
        ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
⊢ ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
obtain ⟨a1, a2, h1, h2, i, hne⟩ := h
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩

Premises used: And.intro, Exists.intro, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
refine : ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
⊢ ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
refine ⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
rw : ∃ x ∈ s, ¬x i = ai
⊢ {x ∈ s | x i = ai} ⊂ s

Tactic:
rw [filter_ssubset]

Premises used: Finset.filter_ssubset
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
inl : ∃ x ∈ s, ¬x i = a2 i
inr : ∀ (hne : a2 i ≠ ai), ∃ x ∈ s, ¬x i = ai
⊢ ∃ x ∈ s, ¬x i = ai

Tactic:
obtain rfl | hne := eq_or_ne (a2 i) ai

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ x ∈ s, ¬x i = a2 i

Tactic:
⟨a1, h1, hne⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne_1 : a1 i ≠ a2 i
ai : α i
hne : a2 i ≠ ai
⊢ ∃ x ∈ s, ¬x i = ai

Tactic:
⟨a2, h2, hne⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Finset.Card
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ x ∈ s, ¬x i = a2 i

Tactic:
exacts [⟨a1, h1, hne⟩, ⟨a2, h2, hne⟩]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
⊢ card.{u_1} (α := α) ∅ = n + 1 → ∃ (a : α) (t : Finset α) (h : a ∉ t), cons a t h = ∅ ∧ #t = n

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s_1 : Finset α
n : ℕ
a : α
s : Finset α
h : a ∉ s
h_1 : #s = n + 1 → ∃ (a : α) (t : Finset α) (h : a ∉ t), cons a t h = s ∧ #t = n
h_2 : #(cons a s h) = n + 1
⊢ ∃ (h_3 : a ∉ s), cons a s h_3 = cons a s h ∧ #s = n

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
h : ∃ (a : α) (t : Finset α) (h : a ∉ t), cons a t h = s ∧ #t = n
a : α
t : Finset α
w : a ∉ t
hs : cons a t w = s
right : #t = n
⊢ #s = n + 1

Tactic:
simpa [← hs]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
inst : DecidableEq α
h : #s = n + 1
a : α
has : a ∈ s
⊢ #(s.erase a) = n

Tactic:
simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Finset.card_erase_of_mem
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 2 → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
mpr : (∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}) → #s = 2
⊢ #s = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
⊢ #s = 2 → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
rw [card_eq_succ]

Premises used: Finset.card_eq_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
grind [card_eq_one]

Premises used: Finset.card_eq_one
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}) → #s = 2

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 3 → ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
mpr : (∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3
⊢ #s = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp :
  (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 2) →
    ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
⊢ #s = 3 → ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [card_eq_succ]

Premises used: Finset.card_eq_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 2) →
    ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
grind [card_eq_two]

Premises used: Finset.card_eq_two
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 4 → ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
mpr : (∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4
⊢ #s = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp :
  (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 3) →
    ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
⊢ #s = 4 → ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [card_eq_succ]

Premises used: Finset.card_eq_succ
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 3) →
    ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
grind [card_eq_three]

Premises used: Finset.card_eq_three
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ (∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw :
  (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < #s ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]

Premises used: exists_and_left, Nat.reduceAdd, Nat.lt_iff_add_one_le, Finset.le_card_iff_exists_subset_card, exists_comm, Finset.card_eq_three
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
mp :
  (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
mpr :
  (∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}
⊢ (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_all [insert_subset_iff]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ {a, b, c} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}

Tactic:
simp_all [insert_subset_iff]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw : HAdd.hAdd (α := ℕ) 2 1 ≤ #s ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₁ :
  (∃ t ⊆ s, #t = HAdd.hAdd (α := ℕ) 2 1) ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₂ : (∃ t ⊆ s, #t = 3) ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₃ :
  (∃ t ⊆ s, ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ t = {x, y, z}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₄ :
  (∃ (t : Finset α) (x : α) (x_1 : α) (x_2 : α), t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x_1 ≠ x_2 ∧ t = {x, x_1, x_2}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₅ :
  (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
mp :
  (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
mpr mpr₁ :
  (∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}
⊢ 2 < #s ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩
      exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
      exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

Premises used: exists_and_left, Nat.reduceAdd, Nat.lt_iff_add_one_le, Finset.le_card_iff_exists_subset_card, exists_comm, Finset.card_eq_three, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw :
  (∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [two_lt_card_iff, exists_and_left]

Premises used: exists_and_left, Finset.two_lt_card_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw :
  (∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
⊢ 3 < #s ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four,
      ← exists_and_left, exists_comm (α := Finset α)]

Premises used: exists_and_left, Nat.reduceAdd, Nat.lt_iff_add_one_le, Finset.card_eq_four, Finset.le_card_iff_exists_subset_card, exists_comm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
mp :
  (∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
mpr :
  (∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}
⊢ (∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_all [insert_subset_iff]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c d : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
⊢ {a, b, c, d} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧ Eq (α := Finset α) {a, b, c, d} {a, b, c, d}

Tactic:
simp_all [insert_subset_iff]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
a b c d : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
⊢ ∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
    ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}

Tactic:
exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw :
  HAdd.hAdd (α := ℕ) 3 1 ≤ #s ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₁ :
  (∃ t ⊆ s, #t = HAdd.hAdd (α := ℕ) 3 1) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₂ :
  (∃ t ⊆ s, #t = 4) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₃ :
  (∃ t ⊆ s, ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ t = {x, y, z, w}) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₄ :
  (∃ (t : Finset α) (x : α) (x_1 : α) (x_2 : α) (x_3 : α),
      t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x ≠ x_3 ∧ x_1 ≠ x_2 ∧ x_1 ≠ x_3 ∧ x_2 ≠ x_3 ∧ t = {x, x_1, x_2, x_3}) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
simp_rw₅ :
  (∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
mp :
  (∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
mpr mpr₁ :
  (∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ (b : α) (b_1 : α) (b_2 : α) (b_3 : α),
      ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}
⊢ 3 < #s ↔
    ∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
      exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

Premises used: exists_and_left, Nat.reduceAdd, Nat.lt_iff_add_one_le, Finset.card_eq_four, Finset.le_card_iff_exists_subset_card, exists_comm, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
simp_rw :
  (∃ (a : α) (b : α) (c : α) (d : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
⊢ 3 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_rw [three_lt_card_iff, exists_and_left]

Premises used: exists_and_left, Finset.three_lt_card_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
rw rw₁ :
  (H s fun (t : Finset α) (h : t ⊂ s) ↦
      have this := ⋯;
      strongInduction (p := p) H t) =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := p) H t
⊢ strongInduction (p := p) H s = H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := p) H t

Tactic:
rw [strongInduction]

Premises used: Finset.strongInduction
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
dsimp :
  strongInduction (p := fun (x : Finset α) ↦ p x) H s =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t
⊢ s.strongInductionOn (p := fun (x : Finset α) ↦ p x) H =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ t.strongInductionOn (p := fun (x : Finset α) ↦ p x) H

Tactic:
dsimp only [strongInductionOn]