awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have neg : ∀ (h : ¬x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have pos : s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have neg : s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
Tactic: by_cases h : x ∈ s <;> [left; right]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
pos : ∀ (h : x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s ∪ g '' sᶜ
have neg : ∀ (h : ¬x ∈ s), s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ
Tactic: by_cases h : x ∈ s <;> [left; right]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ f '' s
have h₁ : x ∈ s ∧ f x = s.piecewise (β := fun (a : α) ↦ β) f g x
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ∈ g '' sᶜ
have h₁ : x ∈ sᶜ ∧ g x = s.piecewise (β := fun (a : α) ↦ β) f g x
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
⊢ f x ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)
have h : s.piecewise (β := fun (a : α) ↦ β) f g x = f x
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ sᶜ
⊢ g x ∈ range (s.piecewise (β := fun (a : α) ↦ β) f g)
have h : s.piecewise (β := fun (a : α) ↦ β) f g x = g x
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise (β := fun (a : α) ↦ β) f g) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
have rw : (InjOn f s ∧
    InjOn g sᶜ ∧
      ∀ (x : α),
        x ∈ s →
          ∀ (y : α), y ∈ sᶜ → s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y) ↔
  InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
Tactic: rw [← injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
    (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧
      InjOn g sᶜ ∧
        ∀ (x : α),
          x ∈ s →
            ∀ (y : α), y ∈ sᶜ → s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
have refine : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ sᶜ),
  s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
Tactic: refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
have rw : f x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
Tactic: rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_notMem s f g hy]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
rw : f x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x ≠ s.piecewise (β := fun (a : α) ↦ β) f g y ↔ f x ≠ g y
have rw₁ : f x ≠ g y ↔ f x ≠ g y
Tactic: rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_notMem s f g hy]
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
s : Set α
inst : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi (α := δ) t'
hg : g ∈ t.pi (α := δ) t'
i : α
ht : i ∈ t
⊢ s.piecewise (β := δ) f g i ∈ t' i
have pos : ∀ (hs : i ∈ s), s.piecewise (β := δ) f g i ∈ t' i
Tactic: by_cases hs : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Piecewise (goal)
Goal:
α : Type u_1
s : Set α
inst : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi (α := δ) t'
hg : g ∈ t.pi (α := δ) t'
i : α
ht : i ∈ t
pos : ∀ (hs : i ∈ s), s.piecewise (β := δ) f g i ∈ t' i
⊢ s.piecewise (β := δ) f g i ∈ t' i
have neg : ∀ (hs : ¬i ∈ s), s.piecewise (β := δ) f g i ∈ t' i
Tactic: by_cases hs : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Set.Pointwise.Support (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : One γ
c : α
f : β → γ
⊢ (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • mulSupport f
have h : ∀ (x : β),
  Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Pointwise.Support (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
f : β → γ
⊢ (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • support f
have h : ∀ (x : β), Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Pointwise.Support (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : One γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • mulSupport f
have h : ∀ (x : β),
  Membership.mem (γ := Set β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • mulSupport f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Pointwise.Support (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : GroupWithZero α
inst_1 : MulAction α β
inst_2 : Zero γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) = c • support f
have h : ∀ (x : β), Membership.mem (γ := Set β) (support.{u_2, u_3} (M := γ) fun (x : β) ↦ f (c⁻¹ • x)) x ↔ x ∈ c • support f
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ s ∈ powersetCard α n ↔ #s = n
have rw : Membership.mem (γ := Set (Finset α)) {s : Finset α | #s = n} s ↔ #s = n
Tactic: rw [powersetCard, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
rw : Membership.mem (γ := Set (Finset α)) {s : Finset α | #s = n} s ↔ #s = n
⊢ s ∈ powersetCard α n ↔ #s = n
have rw₁ : #s = n ↔ #s = n
Tactic: rw [powersetCard, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑s : Set α).ncard = n
have rw : (↑(↑s : Finset α) : Set α).ncard = n
Tactic: rw [← coe_coe, Set.ncard_coe_finset, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).ncard = n
⊢ (↑s : Set α).ncard = n
have rw₁ : #(↑s : Finset α) = n
Tactic: rw [← coe_coe, Set.ncard_coe_finset, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).ncard = n
rw₁ : #(↑s : Finset α) = n
⊢ (↑s : Set α).ncard = n
have rw₂ : n = n
Tactic: rw [← coe_coe, Set.ncard_coe_finset, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑s : Set α).Nonempty ↔ 1 ≤ n
have rw : (↑(↑s : Finset α) : Set α).Nonempty ↔ 1 ≤ n
Tactic: rw [← Set.powersetCard.coe_coe, Finset.coe_nonempty, ← one_le_card, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nonempty ↔ 1 ≤ n
⊢ (↑s : Set α).Nonempty ↔ 1 ≤ n
have rw₁ : (↑s : Finset α).Nonempty ↔ 1 ≤ n
Tactic: rw [← Set.powersetCard.coe_coe, Finset.coe_nonempty, ← one_le_card, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nonempty ↔ 1 ≤ n
rw₁ : (↑s : Finset α).Nonempty ↔ 1 ≤ n
⊢ (↑s : Set α).Nonempty ↔ 1 ≤ n
have rw₂ : 1 ≤ #(↑s : Finset α) ↔ 1 ≤ n
Tactic: rw [← Set.powersetCard.coe_coe, Finset.coe_nonempty, ← one_le_card, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nonempty ↔ 1 ≤ n
rw₁ : (↑s : Finset α).Nonempty ↔ 1 ≤ n
rw₂ : 1 ≤ #(↑s : Finset α) ↔ 1 ≤ n
⊢ (↑s : Set α).Nonempty ↔ 1 ≤ n
have rw₃ : 1 ≤ n ↔ 1 ≤ n
Tactic: rw [← Set.powersetCard.coe_coe, Finset.coe_nonempty, ← one_le_card, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑s : Set α).Nontrivial ↔ 1 < n
have rw : (↑(↑s : Finset α) : Set α).Nontrivial ↔ 1 < n
Tactic: rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nontrivial ↔ 1 < n
⊢ (↑s : Set α).Nontrivial ↔ 1 < n
have rw₁ : (↑s : Finset α).Nontrivial ↔ 1 < n
Tactic: rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nontrivial ↔ 1 < n
rw₁ : (↑s : Finset α).Nontrivial ↔ 1 < n
⊢ (↑s : Set α).Nontrivial ↔ 1 < n
have rw₂ : 1 < #(↑s : Finset α) ↔ 1 < n
Tactic: rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α n) : Type u_1)
rw : (↑(↑s : Finset α) : Set α).Nontrivial ↔ 1 < n
rw₁ : (↑s : Finset α).Nontrivial ↔ 1 < n
rw₂ : 1 < #(↑s : Finset α) ↔ 1 < n
⊢ (↑s : Set α).Nontrivial ↔ 1 < n
have rw₃ : 1 < n ↔ 1 < n
Tactic: rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
⊢ s = t ↔ (↑s : Finset α) ⊆ (↑t : Finset α)
have rw : s = t ↔ (↑s : Finset α) = (↑t : Finset α)
Tactic: rw [Finset.subset_iff_eq_of_card_le (t.prop.trans_le s.prop.ge), Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
rw : s = t ↔ (↑s : Finset α) = (↑t : Finset α)
⊢ s = t ↔ (↑s : Finset α) ⊆ (↑t : Finset α)
have rw₁ : (↑s : Finset α) = (↑t : Finset α) ↔ (↑s : Finset α) = (↑t : Finset α)
Tactic: rw [Finset.subset_iff_eq_of_card_le (t.prop.trans_le s.prop.ge), Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
have rwa : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b} + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
Tactic: rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
Cleared hypotheses: hα, hab
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
rwa : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b} + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
have rwa₁ : ∀ (hα : (↑n : ℕ∞) < 1 + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
Tactic: rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
Cleared hypotheses: hα, hab
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
rwa : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b} + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₁ : ∀ (hα : (↑n : ℕ∞) < 1 + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
have rwa₂ : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b}ᶜ + 1) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
Tactic: rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
Cleared hypotheses: hα, hab
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
rwa : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b} + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₁ : ∀ (hα : (↑n : ℕ∞) < 1 + encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
rwa₂ : ∀ (hα : (↑n : ℕ∞) < encard (α := α) {b}ᶜ + 1) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
have rwa₃ : ∀ (hα : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ) (hab : a ≠ b), (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
Tactic: rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
Cleared hypotheses: hα, hab
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
⊢ ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s
have ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
Tactic: have ha' : n ≤ Set.encard {b}ᶜ := by
    rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.coe_ne_top n)] at hα
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
⊢ ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s
have obtain : ∀ (s : Set α) (has : {a} ⊆ s) (has' : s ⊆ {b}ᶜ) (hs : s.encard = (↑n : ℕ∞)),
  ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s
Tactic: obtain ⟨s, has, has', hs⟩ :=
    Set.exists_superset_subset_encard_eq (s := {a}) (by simp [Ne.symm hab]) (by simpa) ha'
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (hypothesis)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
⊢ ∃ (s : (↑(powersetCard α n) : Type u_1)), a ∈ s ∧ b ∉ s
have this : s.Finite
Tactic: have : Set.Finite s := Set.finite_of_encard_eq_coe hs
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
⊢ this.toFinset (s := s) ∈ powersetCard α n
have rwa : #(this.toFinset (s := s)) = n
Tactic: rwa [mem_iff, ← ENat.coe_inj, ← this.encard_eq_coe_toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
a b : α
hab : a ≠ b
ha' : (↑n : ℕ∞) ≤ encard (α := α) {b}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = (↑n : ℕ∞)
this : s.Finite
rwa : #(this.toFinset (s := s)) = n
⊢ this.toFinset (s := s) ∈ powersetCard α n
have rwa₁ : Eq (α := ℕ∞) (↑(#(this.toFinset (s := s))) : ℕ∞) (↑n : ℕ∞)
Tactic: rwa [mem_iff, ← ENat.coe_inj, ← this.encard_eq_coe_toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
⊢ s ≠ t ↔ ∃ a ∈ s, a ∉ t
have contrapose! : s = t ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s t : (↑(powersetCard α n) : Type u_1)
⊢ s = t ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t
have rw : (↑s : Finset α) ⊆ (↑t : Finset α) ↔ ∀ (a : α) (_ : a ∈ s), a ∈ t
Tactic: rw [eq_iff_subset]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
⊢ Finset.map f (↑s : Finset α) ∈ powersetCard β n
have rw : #(Finset.map f (↑s : Finset α)) = n
Tactic: rw [mem_iff, card_map, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
rw : #(Finset.map f (↑s : Finset α)) = n
⊢ Finset.map f (↑s : Finset α) ∈ powersetCard β n
have rw₁ : #(↑s : Finset α) = n
Tactic: rw [mem_iff, card_map, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
rw : #(Finset.map f (↑s : Finset α)) = n
rw₁ : #(↑s : Finset α) = n
⊢ Finset.map f (↑s : Finset α) ∈ powersetCard β n
have rw₂ : n = n
Tactic: rw [mem_iff, card_map, s.prop]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
b : β
⊢ b ∈ map n f s ↔ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑s : Set α)) b
have simp : (∃ a ∈ (↑s : Finset α), (f : (a : α) → β) a = b) ↔ ∃ x ∈ s, (f : (a : α) → β) x = b
Tactic: simp [map]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑(map n f s) : Set β) = (⇑f : (a : α) → β) '' (↑s : Set α)
have h : ∀ (x : β), x ∈ (↑(map n f s) : Set β) ↔ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑s : Set α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α 1) : Type u_1)
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ : { x : Finset α // x ∈ powersetCard α 1 }))
      ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s) =
    s
have rw : (↑((fun (a : α) ↦
          (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} sorry :
            { x : Finset α // x ∈ powersetCard α 1 }))
        ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ sorry.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s)) :
    Finset α) =
  (↑s : Finset α)
Tactic: rw [← Subtype.val_inj, (Finset.card_eq_one.mp s.prop).choose_spec]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
s : (↑(powersetCard α 1) : Type u_1)
rw :
  (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ :
              { x : Finset α // x ∈ powersetCard α 1 }))
          ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s)) :
      Finset α) =
    (↑s : Finset α)
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} ⋯ : { x : Finset α // x ∈ powersetCard α 1 }))
      ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ ⋯.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s) =
    s
have rw₁ : Eq (α := Finset α)
  (↑((fun (a : α) ↦
          (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} sorry :
            { x : Finset α // x ∈ powersetCard α 1 }))
        ((fun (s : (↑(powersetCard α 1) : Type u_1)) ↦ sorry.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})) s)) :
    Finset α)
  {sorry.choose (p := fun (a : α) ↦ (↑s : Finset α) = {a})}
Tactic: rw [← Subtype.val_inj, (Finset.card_eq_one.mp s.prop).choose_spec]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ Membership.mem (γ := Set (Finset (Fin n))) (powersetCard (Fin n) n) Finset.univ
have rw : card (α := Fin n) Finset.univ = n
Tactic: rw [mem_iff, Finset.card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
rw : card (α := Fin n) Finset.univ = n
⊢ Membership.mem (γ := Set (Finset (Fin n))) (powersetCard (Fin n) n) Finset.univ
have rw₁ : Fintype.card (Fin n) = n
Tactic: rw [mem_iff, Finset.card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
rw : card (α := Fin n) Finset.univ = n
rw₁ : Fintype.card (Fin n) = n
⊢ Membership.mem (γ := Set (Finset (Fin n))) (powersetCard (Fin n) n) Finset.univ
have rw₂ : n = n
Tactic: rw [mem_iff, Finset.card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ (↑(ofFinEmb n β f) : Set β) = range (ι := Fin n) (⇑f : (a : Fin n) → β)
have h : ∀ (x : β), x ∈ (↑(ofFinEmb n β f) : Set β) ↔ Membership.mem (γ := Set β) (range (ι := Fin n) (⇑f : (a : Fin n) → β)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ Fintype.card (Fin n) = #s
have rw : Fintype.card (Fin n) = n
Tactic: rw [hs, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
rw : Fintype.card (Fin n) = n
⊢ Fintype.card (Fin n) = #s
have rw₁ : n = n
Tactic: rw [hs, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Set.PowersetCard (goal)
Goal:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs
have obtain : ∀ (f : Fin n ↪ β) (hf : Finset.map f Finset.univ = s),
  ∃ (a : Fin n ↪ β), ofFinEmb n β a = Subtype.mk (p := fun (x : Finset β) ↦ x ∈ powersetCard β n) s hs
Tactic: obtain ⟨f : Fin n ↪ β, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])
-- 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 α
s : (↑(powersetCard α n) : Type u_1)
⊢ (↑s : Finset α)ᶜ ∈ powersetCard α m
have simp : Fintype.card α - n = m
Tactic: simp [Finset.card_compl, mem_iff.mp s.2]