awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h

Tactic:
⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

Premises used: _private.0.Set.mem_dite_empty_left.match_1, And, And.right, And.left, And.intro, Iff.intro, Exists.intro, Not
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ (h : ¬p), x ∈ t h

Tactic:
exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
p : Prop
inst : Decidable p
t : Set α
x : α
⊢ (∃ (h : ¬p), x ∈ t) ↔ ¬p ∧ x ∈ t

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
β : Type u_2
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
rw : f s ≠ ∅ ↔ s.Nonempty
rw₁ : f s ≠ f ∅ ↔ s.Nonempty
rw₂ : f s ≠ f ∅ ↔ s ≠ ∅
rw₃ rw₄ : s ≠ ∅ ↔ s ≠ ∅
⊢ (f s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

Premises used: Function.Injective.ne_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
inst : Subsingleton α
s : Set α
⊢ s.Nonempty → s = univ

Tactic:
fun ⟨x, hx⟩ =>
  eq_univ_of_forall fun y => Subsingleton.elim x y ▸ hx

Premises used: _private.0.Set.Nonempty.to_type.match_1, Set.univ, Eq.rec, Set.eq_univ_of_forall, Subsingleton.elim, Eq
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
inst : Subsingleton α
p : Set α → Prop
h0 : p ∅
h1 : p univ
s : Set α
⊢ p s

Tactic:
(s.eq_empty_or_nonempty.elim fun h => h.symm ▸ h0) fun h => (eq_univ_of_nonempty h).symm ▸ h1

Premises used: Eq.rec, Set.eq_empty_or_nonempty, Subsingleton.eq_univ_of_nonempty, Or.elim, Eq.symm
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_2
inst : Subsingleton α
s : Set α
x : α
⊢ x ∈ s ↔ s.Nonempty

Tactic:
⟨fun hx => ⟨x, hx⟩, fun ⟨y, hy⟩ => Subsingleton.elim y x ▸ hy⟩

Premises used: _private.0.Set.Nonempty.to_type.match_1, Membership.mem, Eq.rec, Iff.intro, Exists.intro, Subsingleton.elim
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
a b : α
⊢ ¬Membership.mem (γ := Set α) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
a b : α
⊢ Membership.mem (γ := Set α) univ a

Tactic:
simp
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u
s t : Set α
a b : α
p : α → Prop
inst : Decidable (p a)
⊢ Decidable (Membership.mem (γ := Set α) {a : α | p a} a)

Tactic:
assumption
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : Set { a : α // p a }
h :
  ∀ (a : { a : α // p a }),
    Membership.mem (γ := Set { a : α // p a })
        ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
            ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
          ((fun (s : Set { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                  {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
                { s : Set α // ∀ (a : α), a ∈ s → p a }))
            s))
        a ↔
      a ∈ s
⊢ (fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
        ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
      ((fun (s : Set { a : α // p a }) ↦
          (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
              {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
            { s : Set α // ∀ (a : α), a ∈ s → p a }))
        s) =
    s

Tactic:
ext a
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : Set { a : α // p a }
a : { a : α // p a }
⊢ Membership.mem (γ := Set { a : α // p a })
      ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
          ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
        ((fun (s : Set { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
              { s : Set α // ∀ (a : α), a ∈ s → p a }))
          s))
      a ↔
    a ∈ s

Tactic:
⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩

Premises used: Iff.intro, Exists.intro, Subtype.property
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : Set { a : α // p a }
a : { a : α // p a }
⊢ Membership.mem (γ := Set { a : α // p a })
      ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
          ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
        ((fun (s : Set { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
              { s : Set α // ∀ (a : α), a ∈ s → p a }))
          s))
      a ↔
    a ∈ s

Tactic:
exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : { s : Set α // ∀ (a : α), a ∈ s → p a }
a :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (↑((fun (s : Set { a : α // p a }) ↦
                (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                    {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
                  { s : Set α // ∀ (a : α), a ∈ s → p a }))
              ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
                  ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
                s)) :
          Set α)
        x ↔
      x ∈ (↑s : Set α)
⊢ (fun (s : Set { a : α // p a }) ↦
        (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
            {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
          { s : Set α // ∀ (a : α), a ∈ s → p a }))
      ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
          ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
        s) =
    s

Tactic:
ext
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : { s : Set α // ∀ (a : α), a ∈ s → p a }
x : α
⊢ Membership.mem (γ := Set α)
      (↑((fun (s : Set { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                  {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
                { s : Set α // ∀ (a : α), a ∈ s → p a }))
            ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
                ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
              s)) :
        Set α)
      x ↔
    x ∈ (↑s : Set α)

Tactic:
⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩

Premises used: Iff.intro, Exists.intro, Subtype.property
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
s_1 t u : Set α
p : α → Prop
s : { s : Set α // ∀ (a : α), a ∈ s → p a }
x : α
⊢ Membership.mem (γ := Set α)
      (↑((fun (s : Set { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
                  {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
                { s : Set α // ∀ (a : α), a ∈ s → p a }))
            ((fun (s : { s : Set α // ∀ (a : α), a ∈ s → p a }) ↦
                ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a }))
              s)) :
        Set α)
      x ↔
    x ∈ (↑s : Set α)

Tactic:
exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
p : α → Prop
s : Set { a : α // p a }
⊢ Eq (α := { s : Set α // ∀ (a : α), a ∈ s → p a })
    ((Equiv.setSubtypeComm p : (a : Set { a : α // p a }) → { s : Set α // ∀ (a : α), a ∈ s → p a }) s :
      { s : Set α // ∀ (a : α), a ∈ s → p a })
    (Subtype.mk (p := fun (s : Set α) ↦ ∀ (a : α), a ∈ s → p a)
        {a : α | ∃ (h : p a), Subtype.mk (p := fun (a : α) ↦ p a) a h ∈ s} ⋯ :
      { s : Set α // ∀ (a : α), a ∈ s → p a })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Basic
Goal:
α : Type u_1
p : α → Prop
s : { s : Set α // ∀ (a : α), a ∈ s → p a }
⊢ Eq (α := Set { a : α // p a })
    (((Equiv.setSubtypeComm p).symm : (a : { s : Set α // ∀ (a : α), a ∈ s → p a }) → Set { a : α // p a }) s :
      Set { a : α // p a })
    ({a : { a : α // p a } | (↑a : α) ∈ (↑s : Set α)} : Set { a : α // p a })

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
pos : ∀ (h : x ∈ s), x ∈ s ↔ true = true
neg : ∀ (h : ¬x ∈ s), x ∈ s ↔ False
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
pos : ∀ (h : x ∈ s), ¬x ∈ s ↔ False
neg : ∀ (h : ¬x ∈ s), ¬x ∈ s ↔ false = false
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
⊢ s.boolIndicator ⁻¹' {true} = s

Tactic:
ext fun x ↦ (s.mem_iff_boolIndicator x).symm

Premises used: Set.ext, Set.mem_iff_boolIndicator, Iff.symm
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
⊢ s.boolIndicator ⁻¹' {false} = sᶜ

Tactic:
ext fun x ↦ (s.notMem_iff_boolIndicator x).symm

Premises used: Set.ext, Set.notMem_iff_boolIndicator, Iff.symm
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
h : ∀ (x : α), x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
⊢ s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
ext x
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
⊢ x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
simp only [boolIndicator, mem_preimage]

Premises used: Set.boolIndicator, Set.mem_preimage
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
pos : x ∈ s → true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ s ∪ sᶜ)
neg : x ∈ s → true ∈ t → ¬false ∈ t → (true ∈ t ↔ x ∈ s ∪ ∅)
pos₁ : x ∈ s → ¬true ∈ t → false ∈ t → (true ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₁ : x ∈ s → ¬true ∈ t → ¬false ∈ t → (true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
pos₂ : ¬x ∈ s → true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ s ∪ sᶜ)
neg₂ : ¬x ∈ s → true ∈ t → ¬false ∈ t → (false ∈ t ↔ x ∈ s ∪ ∅)
pos₃ : ¬x ∈ s → ¬true ∈ t → false ∈ t → (false ∈ t ↔ x ∈ ∅ ∪ sᶜ)
neg₃ : ¬x ∈ s → ¬true ∈ t → ¬false ∈ t → (false ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x)
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
split_ifs
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : x ∈ s
h_1 : true ∈ t
h_2 : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : x ∈ s
h_1 : true ∈ t
h_2 : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : x ∈ s
h_1 : ¬true ∈ t
h_2 : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : x ∈ s
h_1 : ¬true ∈ t
h_2 : ¬false ∈ t
⊢ true ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : ¬x ∈ s
h_1 : true ∈ t
h_2 : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : ¬x ∈ s
h_1 : true ∈ t
h_2 : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : ¬x ∈ s
h_1 : ¬true ∈ t
h_2 : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
x : α
h : ¬x ∈ s
h_1 : ¬true ∈ t
h_2 : ¬false ∈ t
⊢ false ∈ t ↔ Membership.mem (γ := Set α) (∅ ∪ ∅) x

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
simp :
  ((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 ∅) = ∅
⊢ s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅

Tactic:
simp only [preimage_boolIndicator_eq_union]

Premises used: Set.preimage_boolIndicator_eq_union
-- Module: Mathlib.Data.Set.BoolIndicator
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ᶜ = ∅
neg₁ :
  ¬true ∈ t →
    ¬false ∈ t → Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) ∅
⊢ ((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 ∅) = ∅

Tactic:
split_ifs
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
h : true ∈ t
h_1 : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅

Tactic:
simp [s.union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
h : true ∈ t
h_1 : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅

Tactic:
simp [s.union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
h : ¬true ∈ t
h_1 : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅

Tactic:
simp [s.union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.Data.Set.BoolIndicator
Goal:
α : Type u_1
s : Set α
t : Set Bool
h : ¬true ∈ t
h_1 : ¬false ∈ t
⊢ Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ Eq.{u_1 + 1} (α := Set α) (∅ ∪ ∅) ∅

Tactic:
simp [s.union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.Data.Set.BooleanAlgebra
Goal:
α ι : Type u_1
κ : ι → Type u_1
f : (a : ι) → κ a → Set α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⨅ (a : ι), ⨆ (b : κ a), f a b) x ↔
      Membership.mem (γ := Set α) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)) x
⊢ Eq.{u_1 + 1} (α := Set α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
ext
-- Module: Mathlib.Data.Set.BooleanAlgebra
Goal:
α ι : Type u_1
κ : ι → Type u_1
f : (a : ι) → κ a → Set α
x : α
⊢ Membership.mem (γ := Set α) (⨅ (a : ι), ⨆ (b : κ a), f a b) x ↔
    Membership.mem (γ := Set α) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)) x

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Data.Set.BooleanAlgebra
Goal:
α : Type u_1
⊢ ∀ (a : Set α), a ≤ univ

Tactic:
simp
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
he : Even #s
n : ℕ
hn : #s = n + n
⊢ n ≤ #s

Tactic:
lia
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
he : Even #s
n : ℕ
hn : #s = n + n
t : Finset α
ht : t ⊆ s
ht' : #t = n
⊢ t ∪ s \ t = s ∧ Disjoint t (s \ t) ∧ #t = #(s \ t)

Tactic:
simp [card_sdiff_of_subset, disjoint_sdiff, *]

Premises used: Finset.card_sdiff_of_subset, Finset.disjoint_sdiff
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
inst : DecidableEq α
t u : Finset α
hdtu : Disjoint t u
hctu : #t = #u
⊢ Even #(t ∪ u)

Tactic:
simp_all
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
inl : ∀ (hs : s.Infinite), ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
inr : ∀ (hs : s.Finite), ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
obtain hs | hs := s.infinite_or_finite

Premises used: Set.infinite_or_finite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
inl : Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
rw [hs.ncard]

Premises used: Set.Infinite.ncard
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
pos : ∀ (h : Eq (α := ℕ) 1 0), Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
neg : ∀ (h : ¬Eq (α := ℕ) 1 0), Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0
⊢ Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0

Tactic:
by_cases h : 1 = 0
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
h : Eq (α := ℕ) 1 0
⊢ Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬Eq (α := ℕ) 1 0
⊢ (s ∩ Function.support (M := ℕ) fun (i : α) ↦ 1).Infinite

Tactic:
simpa [Function.support_const h]

Premises used: Function.support_const
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬Eq (α := ℕ) 1 0
⊢ Eq (α := ℕ) (∑ᶠ (i : α) (_ : i ∈ s), 1) 0

Tactic:
exact finsum_mem_eq_zero_of_infinite (by simpa [Function.support_const h])

Premises used: finsum_mem_eq_zero_of_infinite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
simp [finsum_mem_eq_finite_toFinset_sum _ hs, Set.ncard_eq_toFinset_card s hs]

Premises used: finsum_mem_eq_finite_toFinset_sum, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ Set.ncard.{u_1} (α := α) ∅ = 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ Set.encard.{u_1} (α := α) ∅ = 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
h : s.Infinite
⊢ Infinite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := h.to_subtype
-- Module: Mathlib.Data.Set.Card.Arithmetic
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)
rw₂ rw₃ : #(↑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))

Tactic:
rw [← Cardinal.eq, ← add_def, add_mk_eq_self]

Premises used: Cardinal.eq, Cardinal.add_mk_eq_self, Cardinal.add_def
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
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)
⊢ ∃ (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]

Premises used: Set.Elem, Sum, Equiv, Nonempty
-- Module: Mathlib.Data.Set.Card.Arithmetic
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)

Tactic:
⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩

Premises used: Sum.inl, Set.preimage, Sum.inr, And.intro, Exists.intro, Set.image, Set.range, Subtype.val, DFunLike.coe
-- Module: Mathlib.Data.Set.Card.Arithmetic
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)))
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)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
refine ⟨Subtype.val '' f ⁻¹' (range .inl), Subtype.val '' f ⁻¹' (range .inr), ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Set.Card.Arithmetic
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)
⊢ 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:
simp [← image_union, ← preimage_union]

Premises used: Set.preimage_union, Set.image_union
-- Module: Mathlib.Data.Set.Card.Arithmetic
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)
⊢ 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:
disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)

Premises used: Subtype.val_injective, Set.isCompl_range_inl_range_inr, DFunLike.coe, IsCompl.disjoint, Disjoint.preimage, Set.disjoint_image_of_injective