awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
have have₁ have₂ : ∀ (hsf : s.Finite), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have₃ :
  ∀ (hsf : s.Finite) (h : ∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = hsf.toFinset (s := s) ∧ t.card = n),
    ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have₄ :
  ∀ (hsf : s.Finite) (a : α) (t : Finset α) (hat : a ∉ t) (hts : insert a t = hsf.toFinset (s := s)),
    ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card
have₅ :
  ∀ (hsf : s.Finite) (a : α) (t : Finset α) (hat : a ∉ t) (hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s),
    ∃ (a : α) (t_1 : Set α), a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card
refine_1 :
  ∀ (hsf : s.Finite) (a : α) (t : Finset α) (hat : a ∉ t) (hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s),
    insert a (↑t : Set α) = s
refine_2 refine_2₁ :
  ∀ (hsf : s.Finite) (a : α) (t : Finset α) (hat : a ∉ t) (hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s),
    (↑t : Set α).ncard = t.card
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp

Premises used: Set.Finite.mem_toFinset, Finset.mem_insert, Finset.ext_iff, Finset.card_eq_succ, Set.ext_iff, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ s.ncard = n + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
⟨eq_insert_of_ncard_eq_succ, ?_⟩

Premises used: Set.eq_insert_of_ncard_eq_succ, Iff.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
refine : (∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1
⊢ s.ncard = n + 1 ↔ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
rw : (insert a t).ncard = t.ncard + 1
rw₁ rw₂ : t.ncard + 1 = t.ncard + 1
⊢ s.ncard = t.ncard + 1

Tactic:
rw [← h, ncard_insert_of_notMem hat (hs.subset ((subset_insert a t).trans_eq h))]

Premises used: LE.le.trans_eq, Set.Finite.subset, Set.ncard_insert_of_notMem, Set.subset_insert
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard.toNat = 2 ↔ s.encard = 2
⊢ s.ncard = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
rw [← encard_eq_two, ncard_def]

Premises used: Set.ncard_def, Set.encard_eq_two
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 2 ↔ s.encard = 2

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard.toNat = 3 ↔ s.encard = 3
⊢ s.ncard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [← encard_eq_three, ncard_def]

Premises used: Set.ncard_def, Set.encard_eq_three
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 3 ↔ s.encard = 3

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard.toNat = 4 ↔ s.encard = 4
⊢ s.ncard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [← encard_eq_four, ncard_def]

Premises used: Set.ncard_def, Set.encard_eq_four
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 4 ↔ s.encard = 4

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
s : Set α
pos :
  ∀ (hs : s.Finite),
    ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
neg :
  ∀ (hs : ¬s.Finite),
    ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
⊢ ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
s : Set α
hs : s.Finite
⊢ ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard

Tactic:
simp [(ncard_union_eq_iff (.image _ hs) (.image _ hs)).2 disjoint_image_inl_image_inr,
      ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective]

Premises used: Iff.mpr, Sum.inr_injective, Sum.inl_injective, Set.Finite.image, Set.disjoint_image_inl_image_inr, Set.ncard_union_eq_iff, Set.ncard_image_of_injective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
s : Set α
hs : ¬s.Finite
⊢ ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard

Tactic:
simp [(infinite_union.2 <| .inl <| .image Sum.inl_injective.injOn hs).ncard, Infinite.ncard hs]

Premises used: Iff.mpr, Set.Infinite.ncard, Set.Infinite.image, Function.Injective.injOn, Sum.inl_injective, Or.inl, Set.infinite_union
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
inl :
  IsEmpty α →
    (Nat.card α ≤ Nat.card β + 1 ↔
      ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d})
inr :
  Nonempty α →
    (Nat.card α ≤ Nat.card β + 1 ↔
      ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d})
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
rcases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
h : IsEmpty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf
inr : (Set.range g)ᶜ.ncard ≤ 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
rw [← Set.ncard_range_of_injective (Function.injective_surjInv hf),
    ← Set.ncard_add_ncard_compl (Set.range g), add_le_add_iff_left]

Premises used: add_le_add_iff_left, Set.ncard_add_ncard_compl, Set.range, Function.injective_surjInv, Set.ncard_range_of_injective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf
⊢ ∀ (b : β), f (g b) = b

Tactic:
replace hf : ∀ b, f (g b) = b := Function.surjInv_eq hf
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
⊢ (Set.range g)ᶜ.ncard ≤ 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
inr :
  ∀ (h : (Set.range g)ᶜ.ncard ≤ 1) (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
inr₁ :
  ∀ (h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}),
    (Set.range g)ᶜ.ncard ≤ 1
⊢ (Set.range g)ᶜ.ncard ≤ 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h_1 : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
h : (Set.range g)ᶜ.ncard ≤ 1
⊢ ∃ (x : α), (Set.range g)ᶜ ⊆ {x}

Tactic:
rw [Set.ncard_le_one_iff_subset_singleton] at h

Premises used: Set.ncard_le_one_iff_subset_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h_1 : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
h : ∃ (x : α), (Set.range g)ᶜ ⊆ {x}
inr :
  ∀ (x : α) (hx : (Set.range g)ᶜ ⊆ {x}) (a b c d : α),
    f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
obtain ⟨x, hx⟩ := h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : (Set.range g)ᶜ ⊆ {x}
⊢ ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1

Tactic:
simp only [Set.subset_def, Set.mem_compl_iff] at hx

Premises used: Set.subset_def, Set.mem_compl_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
this : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
inr : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
suffices ∀ a b : α, f a = f b → a ≠ b → a = x ∨ a = g (f x) by grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
pos : ∀ (ha : a ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
neg : ∀ (ha : a ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases ha : a ∈ Set.range g

Premises used: Set.range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∈ Set.range g
pos : ∀ (hb : b ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
neg : ∀ (hb : b ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases hb : b ∈ Set.range g

Premises used: Set.range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∉ Set.range g
pos : ∀ (hb : b ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
neg : ∀ (hb : b ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases hb : b ∈ Set.range g

Premises used: Set.range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∈ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∈ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∉ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
a b : α
ha : a ∉ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h_1 : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
inr : ∀ a ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b
⊢ (Set.range g)ᶜ.ncard ≤ 1

Tactic:
rw [Set.ncard_le_one]

Premises used: Set.ncard_le_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h_1 : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
inr : ∀ (a : α), (∀ (x : β), g x ≠ a) → ∀ (b : α), (∀ (x : β), g x ≠ b) → a = b
⊢ ∀ a ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b

Tactic:
simp only [Set.mem_compl_iff, Set.mem_range, not_exists, ← ne_eq]

Premises used: Set.mem_range, not_exists, ne_eq, Set.mem_compl_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf_1 : Surjective f
h_1 : Nonempty α
g : (b : β) → α := surjInv hf_1
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
hb : ∀ (x : β), g x ≠ b
⊢ a = b

Tactic:
simpa [(ha (f b)).symm] using congrArg (a ∈ ·) (h a (g (f a)) b (g (f b))
      (hf (f a)).symm (hf (f b)).symm (ha (f a)).symm (hb (f b)).symm)

Premises used: congrArg, Membership.mem, Ne.symm, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
f : α → β
⊢ s.ncard ≤ (f '' s).ncard + 1 ↔
    ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, ∀ d ∈ s, f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}

Tactic:
simpa [Subtype.ext_iff, ← (Set.image_injective.mpr Subtype.val_injective).eq_iff,
     Set.image_insert_eq, Set.image_singleton] using
      (Set.surjective_mapsTo_image_restrict f s).card_le_card_add_one_iff

Premises used: Iff.mpr, Set.image_injective, Set.image_singleton, Subtype.val_injective, Function.Injective.eq_iff, Set.surjective_mapsTo_image_restrict, Subtype.ext_iff, Function.Surjective.card_le_card_add_one_iff, Set.image_insert_eq
-- Module: Mathlib.Data.Set.CoeSort
Goal:
σ : Type u_1
α : Type u_2
inst : Membership σ α
S : α
⊢ (↑{x : σ | x ∈ S} : Type u_1) = { x : σ // x ∈ S }

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
⊢ FiniteInter (finiteInterClosure S)

Tactic:
{ univ_mem := finiteInterClosure.univ
    inter_mem := fun _ h _ => finiteInterClosure.inter h }

Premises used: FiniteInter.finiteInterClosure.univ, FiniteInter.mk, FiniteInter.finiteInterClosure.inter
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S

Tactic:
Finset.induction_on F (fun _ => ?_) ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : Set (Set α)) ∈ S
refine_2 :
  ∀ (a : Set α) (s : Finset (Set α)),
    a ∉ s →
      ((↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S) →
        (↑(insert a s) : Set (Set α)) ⊆ S → ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S

Tactic:
refine Finset.induction_on F (fun _ => ?_) ?_
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
h : (↑∅ : Set (Set α)) ⊆ S
⊢ ⋂₀ (↑∅ : Set (Set α)) ∈ S

Tactic:
simp [cond.univ_mem]

Premises used: FiniteInter.univ_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
refine_2 :
  a ∉ s →
    ((↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S) →
      (↑(insert a s) : Set (Set α)) ⊆ S → ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S
⊢ a ∉ s →
    ((↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S) →
      (↑(insert a s) : Set (Set α)) ⊆ S → ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S

Tactic:
_
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
h : a ∉ s
h1 : (↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S
h2 : (↑(insert a s) : Set (Set α)) ⊆ S
this : a ∩ ⋂₀ (↑s : Set (Set α)) ∈ S
⊢ ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S

Tactic:
simpa
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
h : a ∉ s
h1 : (↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S
h2 : (↑(insert a s) : Set (Set α)) ⊆ S
refine_2 : a ∩ ⋂₀ (↑s : Set (Set α)) ∈ S
⊢ ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S

Tactic:
suffices a ∩ ⋂₀ ↑s ∈ S by simpa
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
h : a ∉ s
h1 : (↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S
h2 : (↑(insert a s) : Set (Set α)) ⊆ S
⊢ a ∩ ⋂₀ (↑s : Set (Set α)) ∈ S

Tactic:
cond.inter_mem (h2 (Finset.mem_insert_self a s))
          (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, FiniteInter.inter_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
h : a ∉ s
h1 : (↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S
h2 : (↑(insert a s) : Set (Set α)) ⊆ S
⊢ a ∩ ⋂₀ (↑s : Set (Set α)) ∈ S

Tactic:
exact
        cond.inter_mem (h2 (Finset.mem_insert_self a s))
          (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, FiniteInter.inter_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : Set (Set α)) ∈ S
refine_2 refine_2₁ :
  ∀ (a : Set α) (s : Finset (Set α)),
    a ∉ s →
      ((↑s : Set (Set α)) ⊆ S → ⋂₀ (↑s : Set (Set α)) ∈ S) →
        (↑(insert a s) : Set (Set α)) ⊆ S → ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S

Tactic:
classical
    refine Finset.induction_on F (fun _ => ?_) ?_
    · simp [cond.univ_mem]
    · intro a s _ h1 h2
      suffices a ∩ ⋂₀ ↑s ∈ S by simpa
      exact
        cond.inter_mem (h2 (Finset.mem_insert_self a s))
          (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Premises used: FiniteInter.univ_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s ∈ insert A S
basic : s = A → s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
basic₁ : s ∈ S → s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
⊢ s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q

Tactic:
cases h
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s = A
⊢ s = A ∩ Set.univ

Tactic:
simpa
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s = A
⊢ s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q

Tactic:
exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s ∈ S
⊢ s ∈ S

Tactic:
assumption
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s ∈ S
⊢ s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q

Tactic:
exact Or.inl (by assumption)

Premises used: Or.inl
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q

Tactic:
Or.inl cond.univ_mem

Premises used: Or.inl, FiniteInter.univ_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q

Tactic:
exact Or.inl cond.univ_mem

Premises used: Or.inl, FiniteInter.univ_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
h : finiteInterClosure (insert A S) T1
h_1 : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q ∈ S, T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
inter : ∀ (h : T1 ∈ S), T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
inter₁ :
  ∀ (Q : Set α) (hQ : Q ∈ S), finiteInterClosure (insert A S) (A ∩ Q) → A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
rcases h1 with (h | ⟨Q, hQ, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
h_1 : finiteInterClosure (insert A S) T1
h_2 : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
h : T1 ∈ S
inter : ∀ (i : T2 ∈ S), T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
inter₁ :
  ∀ (R : Set α) (hR : R ∈ S), finiteInterClosure (insert A S) (A ∩ R) → T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
rcases h2 with (i | ⟨R, hR, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
h : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
inter : ∀ (i : T2 ∈ S), A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
inter₁ :
  ∀ (R : Set α) (hR : R ∈ S),
    finiteInterClosure (insert A S) (A ∩ R) → A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

Tactic:
rcases h2 with (i | ⟨R, hR, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
h_1 : finiteInterClosure (insert A S) T1
h_2 : finiteInterClosure (insert A S) T2
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
Or.inl (cond.inter_mem h i)

Premises used: Or.inl, FiniteInter.inter_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
h_1 : finiteInterClosure (insert A S) T1
h_2 : finiteInterClosure (insert A S) T2
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
exact Or.inl (cond.inter_mem h i)

Premises used: Or.inl, FiniteInter.inter_mem
-- Module: Mathlib.Data.Set.Constructions
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
h_1 : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
h_2 : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)

Tactic:
simp only [← Set.inter_assoc, Set.inter_comm _ A]

Premises used: Set.inter_comm, Set.inter_assoc