awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have 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
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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n
have 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
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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
have refine : (∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1
Tactic: refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
⊢ s.ncard = t.ncard + 1
have rw : (insert a t).ncard = t.ncard + 1
Tactic: rw [← h, ncard_insert_of_notMem hat (hs.subset ((subset_insert a t).trans_eq h))]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.ncard = t.ncard + 1
have rw₁ : t.ncard + 1 = t.ncard + 1
Tactic: rw [← h, ncard_insert_of_notMem hat (hs.subset ((subset_insert a t).trans_eq h))]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have rw : s.encard.toNat = 2 ↔ s.encard = 2
Tactic: rw [← encard_eq_two, ncard_def]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have rw : s.encard.toNat = 3 ↔ s.encard = 3
Tactic: rw [← encard_eq_three, ncard_def]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have rw : s.encard.toNat = 4 ↔ s.encard = 4
Tactic: rw [← encard_eq_four, ncard_def]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_3
s : Set α
⊢ ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
have pos : ∀ (hs : s.Finite),
  ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
have neg : ∀ (hs : ¬s.Finite),
  ncard.{u_3} (α := α ⊕ α) ((OrderIso.symm sumEquiv : (a : Set α × Set α) → Set (α ⊕ α)) (s, s)) = s.ncard + s.ncard
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
⊢ 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}
have 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})
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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})
⊢ 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}
have 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})
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf
⊢ 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}
have 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}
Tactic: rw [← Set.ncard_range_of_injective (Function.injective_surjInv hf),
    ← Set.ncard_add_ncard_compl (Set.range g), add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
hf : Surjective f
h : Nonempty α
g : (b : β) → α := surjInv hf
⊢ (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}
have hf₁ : ∀ (b : β), f (g b) = b
Tactic: replace hf : ∀ b, f (g b) = b := Function.surjInv_eq hf
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
have 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}
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ (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}
have 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
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
have h₁ : ∃ (x : α), (Set.range g)ᶜ ⊆ {x}
Tactic: rw [Set.ncard_le_one_iff_subset_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
have 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}
Tactic: obtain ⟨x, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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}
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
have hx₁ : ∀ x_1 ∉ Set.range g, Membership.mem (γ := Set α) {x} x_1
Tactic: simp only [Set.subset_def, Set.mem_compl_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → Eq (α := Set α) {a, b} {c, d}
have inr : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: suffices ∀ a b : α, f a = f b → a ≠ b → a = x ∨ a = g (f x) by grind
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have pos : ∀ (ha : a ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases ha : a ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have neg : ∀ (ha : a ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases ha : a ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have pos : ∀ (hb : b ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases hb : b ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have neg : ∀ (hb : b ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases hb : b ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have pos : ∀ (hb : b ∈ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases hb : b ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
have neg : ∀ (hb : b ∉ Set.range g), f a = f b → a ≠ b → a = x ∨ a = g (f x)
Tactic: by_cases hb : b ∈ Set.range g
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ (Set.range g)ᶜ.ncard ≤ 1
have inr : ∀ a ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b
Tactic: rw [Set.ncard_le_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b
have inr : ∀ (a : α), (∀ (x : β), g x ≠ a) → ∀ (b : α), (∀ (x : β), g x ≠ b) → a = b
Tactic: simp only [Set.mem_compl_iff, Set.mem_range, not_exists, ← ne_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S
have refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : Set (Set α)) ∈ S
Tactic: refine Finset.induction_on F (fun _ => ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : Set (Set α)) ∈ S
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S
have 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
Tactic: refine Finset.induction_on F (fun _ => ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ ⋂₀ (↑(insert a s) : Set (Set α)) ∈ S
have refine_2 : a ∩ ⋂₀ (↑s : Set (Set α)) ∈ S
Tactic: suffices a ∩ ⋂₀ ↑s ∈ S by simpa
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S
have refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : 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)
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
refine_1 : (↑∅ : Set (Set α)) ⊆ S → ⋂₀ (↑∅ : Set (Set α)) ∈ S
⊢ (↑F : Set (Set α)) ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S
have 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
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)
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s : Set α
h : s ∈ insert A S
⊢ s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
have basic : s = A → s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
have basic₁ : s ∈ S → s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
have inter : ∀ (h : T1 ∈ S), T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
Tactic: rcases h1 with (h | ⟨Q, hQ, rfl⟩)
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
have 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
Tactic: rcases h1 with (h | ⟨Q, hQ, rfl⟩)
Cleared hypotheses: T1, h, h1
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
have inter : ∀ (i : T2 ∈ S), T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
Tactic: rcases h2 with (i | ⟨R, hR, rfl⟩)
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q
have inter₁ : ∀ (R : Set α) (hR : R ∈ S), finiteInterClosure (insert A S) (A ∩ R) → T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q
Tactic: rcases h2 with (i | ⟨R, hR, rfl⟩)
Cleared hypotheses: T2, h_2, h2
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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)
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
have inter : ∀ (i : T2 ∈ S), A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
Tactic: rcases h2 with (i | ⟨R, hR, rfl⟩)
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
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
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
have 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
Tactic: rcases h2 with (i | ⟨R, hR, rfl⟩)
Cleared hypotheses: T2, h, h2
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)
have h : ∀ (x : α), x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
have h : x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
h_1 : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
h_2 : finiteInterClosure (insert A S) (A ∩ R)
x : α
h : x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
have h₁ : x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q
have basic : ∀ {s : Set α} (h : s ∈ insert A S), s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
Tactic: induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Constructions (goal)
Goal:
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
basic : ∀ {s : Set α} (h : s ∈ insert A S), s ∈ S ∨ ∃ Q ∈ S, s = A ∩ Q
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q
have univ : Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q
Tactic: induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩
Cleared hypotheses: H