awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
pos : true ∈ t → false ∈ t → s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
neg : true ∈ t → ¬false ∈ t → s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
have pos₁ : ¬true ∈ t → false ∈ t → ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BoolIndicator (goal)
Goal:
α : Type u_1
s : Set α
t : Set Bool
pos : true ∈ t → false ∈ t → s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
neg : true ∈ t → ¬false ∈ t → s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅
pos₁ : ¬true ∈ t → false ∈ t → ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
have neg₁ : ¬true ∈ t →
  ¬false ∈ t → Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Set.BooleanAlgebra (goal)
Goal:
α ι : Type u_1
κ : ι → Type u_1
f : (a : ι) → κ a → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (⨅ (a : ι), ⨆ (b : κ a), f a b) x ↔
    Membership.mem (γ := Set α) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
have inl : ∀ (hs : s.Infinite), ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
Tactic: obtain hs | hs := s.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
inl : ∀ (hs : s.Infinite), ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
have inr : ∀ (hs : s.Finite), ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
Tactic: obtain hs | hs := s.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
have inl : Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
Tactic: rw [hs.ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
have pos : ∀ (h : Eq (α := ℕ) 1 0), Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
Tactic: by_cases h : 1 = 0
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
pos : ∀ (h : Eq (α := ℕ) 1 0), Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
⊢ Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
have neg : ∀ (h : ¬Eq (α := ℕ) 1 0), Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
Tactic: by_cases h : 1 = 0
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have this : Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := h.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1))
have rw : #(↑s : Type u_1) = #((↑s : Type u_1) ⊕ (↑s : Type u_1))
Tactic: rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
rw : #(↑s : Type u_1) = #((↑s : Type u_1) ⊕ (↑s : Type u_1))
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1))
have rw₁ : #(↑s : Type u_1) = #(↑s : Type u_1) + #(↑s : Type u_1)
Tactic: rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
rw : #(↑s : Type u_1) = #((↑s : Type u_1) ⊕ (↑s : Type u_1))
rw₁ : #(↑s : Type u_1) = #(↑s : Type u_1) + #(↑s : Type u_1)
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1))
have rw₂ : #(↑s : Type u_1) = #(↑s : Type u_1)
Tactic: rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have obtain : ∀ (f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)),
  ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: obtain ⟨f⟩ : Nonempty (s ≃ s ⊕ s) := by
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have refine_1 : image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl)) ∪
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr)) =
  s
Tactic: refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)
refine_1 :
  image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
          (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl)) ∪
      image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
          (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr)) =
    s
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have refine_2 : Disjoint (α := Set α)
  (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1))
      (range Sum.inl)))
  (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1))
      (range Sum.inr)))
Tactic: refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)
refine_1 :
  image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
          (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl)) ∪
      image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
          (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr)) =
    s
refine_2 :
  Disjoint (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl)))
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr)))
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have refine_3 : #(↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
          (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
            (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl))) :
      Type u_1) =
  #(↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
          (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
            (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr))) :
      Type u_1)
Tactic: refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have inl : ∀ (hs : s.Infinite), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: obtain hs | hs := s.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
inl : ∀ (hs : s.Infinite), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have inr : ∀ (hs : s.Finite), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: obtain hs | hs := s.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (hypothesis)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have he₁ : Even #(hs.toFinset (s := s))
Tactic: rw [ncard_eq_toFinset_card s hs] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
he : Even #(hs.toFinset (s := s))
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have inr : ∀ (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u) (hctu : #t = #u),
  ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
he : Even #(hs.toFinset (s := s))
t u : Finset α
hutu : t ∪ u = hs.toFinset (s := s)
hdtu : Disjoint t u
hctu : #t = #u
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have h : (↑t : Set α) ∪ (↑u : Set α) = s ∧
  Disjoint (↑t : Set α) (↑u : Set α) ∧ #(↑(↑t : Set α) : Type u_1) = #(↑(↑u : Set α) : Type u_1)
Tactic: use t, u
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have inr : ∀ (he : Even #(hs.toFinset (s := s))),
  ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
inr inr₁ inr₂ :
  ∀ (he : Even #(hs.toFinset (s := s))),
    ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have inr₃ : ∀ (he : Even #(hs.toFinset (s := s))) (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u)
  (hctu : #t = #u), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
Tactic: classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
inr inr₁ inr₂ :
  ∀ (he : Even #(hs.toFinset (s := s))),
    ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
inr₃ :
  ∀ (he : Even #(hs.toFinset (s := s))) (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u)
    (hctu : #t = #u), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have h : ∀ (he : Even #(hs.toFinset (s := s))) (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u)
  (hctu : #t = #u),
  (↑t : Set α) ∪ (↑u : Set α) = s ∧
    Disjoint (↑t : Set α) (↑u : Set α) ∧ #(↑(↑t : Set α) : Type u_1) = #(↑(↑u : Set α) : Type u_1)
Tactic: classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
have obtain : ∀ (t u : Set α) (hutu : t ∪ u = s) (hdtu : Disjoint t u) (hctu : #(↑t : Type u_1) = #(↑u : Type u_1)),
  ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
Tactic: obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
s : Set α
⊢ Even s.ncard ↔ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
have mpr : (∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)) → Even s.ncard
Tactic: use exists_union_disjoint_cardinal_eq_of_even
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ Even (t ∪ u).ncard
have mpr : ∀ (hfin : (t ∪ u).Finite), Even (t ∪ u).ncard
Tactic: obtain hfin | hnfin := (t ∪ u).finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
mpr : ∀ (hfin : (t ∪ u).Finite), Even (t ∪ u).ncard
⊢ Even (t ∪ u).ncard
have mpr₁ : ∀ (hnfin : (t ∪ u).Infinite), Even (t ∪ u).ncard
Tactic: obtain hfin | hnfin := (t ∪ u).finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (hypothesis)
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard
have hfin₁ : t.Finite ∧ u.Finite
Tactic: rw [finite_union] at hfin
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (hypothesis)
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard
have hn : t.ncard = u.ncard
Tactic: have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (t ∪ u).ncard
have mpr : Even (u.ncard + u.ncard)
Tactic: rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
⊢ ncard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
have rw : Eq (α := ℕ) (∑ᶠ (i : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, s i) i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
Tactic: rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
rw :
  Eq (α := ℕ) (∑ᶠ (i : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, s i) i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
⊢ ncard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
have rw₁ : Eq (α := ℕ) (∑ᶠ (i : ι) (_ : i ∈ t) (j : α) (_ : j ∈ s i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
Tactic: rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
rw :
  Eq (α := ℕ) (∑ᶠ (i : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, s i) i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
rw₁ : Eq (α := ℕ) (∑ᶠ (i : ι) (_ : i ∈ t) (j : α) (_ : j ∈ s i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
⊢ ncard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
have rw₂ : Eq (α := ℕ) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
Tactic: rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ ncard.{u_1} (α := α) (⋃ (i : ι), s i) = ∑ᶠ (i : ι), (s i).ncard
have rw : ncard.{u_1} (α := α) (⋃ (i : ι), s i) =
  ncard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)
Tactic: rw [← finsum_mem_univ, ← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: by_cases! h : ∀ i ∈ t, (s i).Finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have neg : ∀ (h : ∃ i ∈ t, (s i).Infinite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: by_cases! h : ∀ i ∈ t, (s i).Finite
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
Tactic: have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos : Eq (α := ℕ∞) (↑(ncard.{u_1} (α := α) (⋃ i ∈ t, s i)) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
Tactic: rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
pos : Eq (α := ℕ∞) (↑(ncard.{u_1} (α := α) (⋃ i ∈ t, s i)) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos₁ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
Tactic: rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
pos : Eq (α := ℕ∞) (↑(ncard.{u_1} (α := α) (⋃ i ∈ t, s i)) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
pos₁ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos₂ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (↑(s i).ncard : ℕ∞))
Tactic: rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
pos : Eq (α := ℕ∞) (↑(ncard.{u_1} (α := α) (⋃ i ∈ t, s i)) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
pos₁ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
pos₂ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (↑(s i).ncard : ℕ∞))
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have pos₃ : Eq (α := ℕ∞) (∑ᶠ (x : ι) (_ : x ∈ t), (↑(s x).ncard : ℕ∞)) (∑ᶠ (i : ι) (_ : i ∈ t), (↑(s i).ncard : ℕ∞))
Tactic: rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∃ i ∈ t, (s i).Infinite
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have neg : ∀ (i : ι) (hi : i ∈ t) (hn : (s i).Infinite),
  encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Tactic: obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card.Arithmetic (goal)
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
have neg : encard.{u_1} (α := α) (⋃ i_1 ∈ insert i (t \ {i}), s i_1) =
  (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard
Tactic: rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]