awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : (↑(powersetCard α m) : Type u_1)
⊢ (↑t : Finset α)ᶜ ∈ powersetCard α n
have simp : Fintype.card α - m = n
Tactic: simp [Finset.card_compl, mem_iff.mp t.2]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
⊢ (↑s : Finset α).disjUnion (↑t : Finset α) hst ∈ powersetCard α (m + n)
have rw : #((↑s : Finset α).disjUnion (↑t : Finset α) hst) = m + n
Tactic: rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
rw : #((↑s : Finset α).disjUnion (↑t : Finset α) hst) = m + n
⊢ (↑s : Finset α).disjUnion (↑t : Finset α) hst ∈ powersetCard α (m + n)
have rw₁ : #(↑s : Finset α) + #(↑t : Finset α) = m + n
Tactic: rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
rw : #((↑s : Finset α).disjUnion (↑t : Finset α) hst) = m + n
rw₁ : #(↑s : Finset α) + #(↑t : Finset α) = m + n
⊢ (↑s : Finset α).disjUnion (↑t : Finset α) hst ∈ powersetCard α (m + n)
have rw₂ : m + #(↑t : Finset α) = m + n
Tactic: rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n m : ℕ
s : (↑(powersetCard α m) : Type u_1)
t : (↑(powersetCard α n) : Type u_1)
hst : Disjoint (↑s : Finset α) (↑t : Finset α)
rw : #((↑s : Finset α).disjUnion (↑t : Finset α) hst) = m + n
rw₁ : #(↑s : Finset α) + #(↑t : Finset α) = m + n
rw₂ : m + #(↑t : Finset α) = m + n
⊢ (↑s : Finset α).disjUnion (↑t : Finset α) hst ∈ powersetCard α (m + n)
have rw₃ : m + n = m + n
Tactic: rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
⊢ powersetCard α n = (↑(Finset.powersetCard n Finset.univ) : Set (Finset α))
have h : ∀ (x : Finset α), x ∈ powersetCard α n ↔ x ∈ (↑(Finset.powersetCard n Finset.univ) : Set (Finset α))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Fintype α
⊢ Fintype (↑(powersetCard α n) : Type u_1)
have rw : Fintype (↑(↑(Finset.powersetCard n Finset.univ) : Set (Finset α)) : Type u_1)
Tactic: rw [coe_finset]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
⊢ Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
have have : ∀ (this : Fintype α), Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
Tactic: have : Fintype α := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
⊢ ∃ s ∈ powersetCard α n, a ∈ s
have obtain : ∀ (s : Finset α) (a_mem : {a} ⊆ s) (s_card : #s = n), ∃ s ∈ powersetCard α n, a ∈ s
Tactic: obtain ⟨s, a_mem, s_card⟩ := Infinite.exists_superset_card_eq ({a} : Finset α) n
    (by rw [Finset.card_singleton]; exact h)
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h : 0 < n
inst : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ ∃ s ∈ powersetCard α n, a ∈ s
have h₁ : s ∈ powersetCard α n ∧ a ∈ s
Tactic: use ↑s
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
⊢ Infinite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
have rw : ¬Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
Tactic: rw [← not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ False
have apply : Finite α
Tactic: apply Finite.false (α := α)
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ Finite α
have rw : (⋃₀ (SetLike.coe '' powersetCard α n)).Finite
Tactic: rw [← Set.finite_univ_iff, ← this]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ (⋃₀ (SetLike.coe '' powersetCard α n)).Finite
have apply : ∀ t ∈ SetLike.coe '' powersetCard α n, t.Finite
Tactic: apply Set.Finite.sUnion (Finite.image SetLike.coe finite)
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
⊢ False
have suffices : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
Tactic: suffices ⋃₀ (SetLike.coe '' powersetCard α n) = Set.univ by
    apply Finite.false (α := α)
    rw [← Set.finite_univ_iff, ← this]
    apply Set.Finite.sUnion (Finite.image SetLike.coe finite)
    aesop
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
⊢ ⋃₀ (SetLike.coe '' powersetCard α n) = univ
have rw : ∀ (a : α), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
Tactic: rw [sUnion_eq_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Infinite α
finite : Finite.{u_1 + 1} (↑(powersetCard α n) : Type u_1)
a : α
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
have obtain : ∀ (s : Finset α) (s_mem : s ∈ powersetCard α n) (mem_s : a ∈ s), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
Tactic: obtain ⟨s, s_mem, mem_s⟩ := exist_mem_powersetCard_of_inf α n (Nat.pos_of_neZero n) a
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inr : Infinite α → Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
val : Infinite α
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inr : Nat.card.{u_1} (↑(powersetCard α 0) : Type u_1) = (Nat.card α).choose 0
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
val : Infinite α
inr : Nat.card.{u_1} (↑(powersetCard α 0) : Type u_1) = (Nat.card α).choose 0
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inr₁ : ∀ (n : ℕ), Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = (Nat.card α).choose (n + 1)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
val : Infinite α
n : ℕ
⊢ Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = (Nat.card α).choose (n + 1)
have inr : Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = 0
Tactic: rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
Tactic: classical
  cases fintypeOrInfinite α
  · simp [coe_finset]
  · rcases n with _ | n
    · simp [powersetCard]
    · rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]
      exact Nat.card_eq_zero_of_infinite
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
have inr : Infinite α → Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
Tactic: classical
  cases fintypeOrInfinite α
  · simp [coe_finset]
  · rcases n with _ | n
    · simp [powersetCard]
    · rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]
      exact Nat.card_eq_zero_of_infinite
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have inl : ∀ (val : Fintype α), Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
inl : ∀ (val : Fintype α), Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have inr : Infinite α → Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have inl : 1 < (Nat.card α).choose n
Tactic: rw [Set.nontrivial_coe_sort, ← Set.one_lt_ncard_iff_nontrivial, ← Nat.card_coe_set_eq,
      powersetCard.card]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
⊢ 1 < (Nat.card α).choose n
have inl : ∀ (this : (Nat.card α).choose n ≤ 1), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
this : (Nat.card α).choose n ≤ 1
⊢ False
have this₁ : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
Tactic: rw [Nat.le_one_iff_eq_zero_or_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
⊢ False
have inl : ∀ (h2 : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(Nat.card α) : ℕ∞)) (val : Fintype α)
  (this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1), False
Tactic: rw [ENat.card_eq_coe_natCard] at h2
Cleared hypotheses: h2, val, this
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(Nat.card α) : ℕ∞)
val : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
⊢ False
have h2₁ : n < Nat.card α
Tactic: norm_cast at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
h2 : n < Nat.card α
⊢ False
have inl : ∀ (h : (Nat.card α).choose n = 0), False
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
h2 : n < Nat.card α
inl : ∀ (h : (Nat.card α).choose n = 0), False
⊢ False
have inl₁ : ∀ (h : (Nat.card α).choose n = 1), False
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ False
have h₁ : Nat.card α < n
Tactic: rw [Nat.choose_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 1
⊢ False
have h₁ : n = 0 ∨ Nat.card α = n
Tactic: rw [Nat.choose_eq_one_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Infinite α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have this : NeZero n
Tactic: have : NeZero n := NeZero.of_pos h1
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero (ne_zero_of_lt h2)
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
this : Finite α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
have apply : (↑n : ℕ∞) < ENat.card α
Tactic: apply nontrivial h1
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
⊢ powersetCard α n = ∅ ↔ Nat.card α < n
have rw : (powersetCard α n).ncard = 0 ↔ Nat.card α < n
Tactic: rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
rw : (powersetCard α n).ncard = 0 ↔ Nat.card α < n
⊢ powersetCard α n = ∅ ↔ Nat.card α < n
have rw₁ : Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = 0 ↔ Nat.card α < n
Tactic: rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
rw : (powersetCard α n).ncard = 0 ↔ Nat.card α < n
rw₁ : Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = 0 ↔ Nat.card α < n
⊢ powersetCard α n = ∅ ↔ Nat.card α < n
have rw₂ : (Nat.card α).choose n = 0 ↔ Nat.card α < n
Tactic: rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
rw : (powersetCard α n).ncard = 0 ↔ Nat.card α < n
rw₁ : Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = 0 ↔ Nat.card α < n
rw₂ : (Nat.card α).choose n = 0 ↔ Nat.card α < n
⊢ powersetCard α n = ∅ ↔ Nat.card α < n
have rw₃ : Nat.card α < n ↔ Nat.card α < n
Tactic: rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
inst : Finite α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1) ↔ 0 < n ∧ n < Nat.card α
have rw : ¬Nat.card α < n ∧ ¬(n = 0 ∨ Nat.card α = n) ↔ 0 < n ∧ n < Nat.card α
Tactic: rw [← Finite.one_lt_card_iff_nontrivial, powersetCard.card, Nat.one_lt_iff_ne_zero_and_ne_one,
    ne_eq, Nat.choose_eq_zero_iff, ne_eq, Nat.choose_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)
⊢ (fun (x : Finset α) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#x)
            (Subtype.mk (p := fun (x_1 : Finset α) ↦ x_1 ∈ powersetCard α #x) x ⋯) :
          (n : ℕ) × (↑(powersetCard α n) : Type u_1)))
      ((fun (x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) ↦
          (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α))
        x) =
    x
have a : Sigma.fst (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })
    ((fun (x : Finset α) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#x)
            (Subtype.mk (p := fun (x_1 : Finset α) ↦ x_1 ∈ powersetCard α #x) x sorry) :
          (n : ℕ) × (↑(powersetCard α n) : Type u_1)))
      ((fun (x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) ↦
          (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α))
        x)) =
  x.fst (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)
a :
  Sigma.fst (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })
      ((fun (x : Finset α) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#x)
              (Subtype.mk (p := fun (x_1 : Finset α) ↦ x_1 ∈ powersetCard α #x) x ⋯) :
            (n : ℕ) × (↑(powersetCard α n) : Type u_1)))
        ((fun (x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) ↦
            (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α))
          x)) =
    x.fst (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })
⊢ (fun (x : Finset α) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#x)
            (Subtype.mk (p := fun (x_1 : Finset α) ↦ x_1 ∈ powersetCard α #x) x ⋯) :
          (n : ℕ) × (↑(powersetCard α n) : Type u_1)))
      ((fun (x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) ↦
          (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α))
        x) =
    x
have a₁ : ∀ (a : α),
  Membership.mem (γ := Finset α)
      (↑(Sigma.snd (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })
            ((fun (x : Finset α) ↦
                (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#x)
                    (Subtype.mk (p := fun (x_1 : Finset α) ↦ x_1 ∈ powersetCard α #x) x sorry) :
                  (n : ℕ) × (↑(powersetCard α n) : Type u_1)))
              ((fun (x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) ↦
                  (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α))
                x))) :
        Finset α)
      a ↔
    a ∈ (↑(x.snd (β := fun (a : ℕ) ↦ { x : Finset α // x ∈ powersetCard α a })) : Finset α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
⊢ SProd.sprod (β := Set β) s ∅ = ∅
have h : ∀ (x : α × β), x ∈ SProd.sprod (β := Set β) s ∅ ↔ Membership.mem (γ := Set (α × β)) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
⊢ SProd.sprod (α := Set α) ∅ t = ∅
have h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) ∅ t ↔ Membership.mem (γ := Set (α × β)) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ SProd.sprod (α := Set α) (β := Set β) univ univ = univ
have h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) (β := Set β) univ univ ↔ Membership.mem (γ := Set (α × β)) univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ SProd.sprod (α := Set α) {a} t = Prod.mk a '' t
have h : ∀ (x : α) (y : β), (x, y) ∈ SProd.sprod (α := Set α) {a} t ↔ (x, y) ∈ Prod.mk a '' t
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ SProd.sprod (β := Set β) s {b} = (fun (a : α) ↦ (a, b)) '' s
have h : ∀ (x : α) (y : β),
  (x, y) ∈ SProd.sprod (β := Set β) s {b} ↔ Membership.mem (γ := Set (α × β)) ((fun (a : α) ↦ (a, b)) '' s) (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ SProd.sprod (α := Set α) (β := Set β) {a} {b} = {(a, b)}
have h : ∀ (c : α) (d : β),
  (c, d) ∈ SProd.sprod (α := Set α) (β := Set β) {a} {b} ↔ Membership.mem (γ := Set (α × β)) {(a, b)} (c, d)
Tactic: ext ⟨c, d⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
have h : ∀ (x : α) (y : β), (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
have h : ∀ (x : α) (y : β), (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
have h : ∀ (x : α) (y : β), (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
have h : ∀ (x : α) (y : β), (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
have h : ∀ (x : α) (y : β), (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
have simp_rw : (∀ (a : α) (b : β), a ∈ s₁ ∧ b ∈ t₁ → ¬(a ∈ s₂ ∧ b ∈ t₂)) ↔ (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂
Tactic: simp_rw [disjoint_left, mem_prod, Prod.forall]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)
have h : ∀ (x : β × δ), x ∈ Prod.map f g '' s ×ˢ t ↔ x ∈ (f '' s) ×ˢ (g '' t)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s
have rw : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
Tactic: rw [image_swap_eq_preimage_swap, preimage_swap_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s
have rw₁ : t ×ˢ s = t ×ˢ s
Tactic: rw [image_swap_eq_preimage_swap, preimage_swap_prod]
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have inl : ∀ (h : s ×ˢ t = ∅), s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
Tactic: rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
inl : ∀ (h : s ×ˢ t = ∅), s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have inr : ∀ (h : (s ×ˢ t).Nonempty), s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
Tactic: rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s.Nonempty ∧ t.Nonempty
have rwa : ∀ (h : s.Nonempty ∧ t.Nonempty), s.Nonempty ∧ t.Nonempty
Tactic: rwa [prod_nonempty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have st : s.Nonempty ∧ t.Nonempty
Tactic: have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
-- Lean 4 proof step from Mathlib.Data.Set.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have inr : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), s ⊆ s₁
Tactic: refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩