awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
val : Infinite α
inr : Nat.card.{u_1} (↑(powersetCard α 0) : Type u_1) = (Nat.card α).choose 0
inr₁ : ∀ (n : ℕ), Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = (Nat.card α).choose (n + 1)
⊢ Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n

Tactic:
rcases n with _ | n
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
val : Infinite α
⊢ Nat.card.{u_1} (↑(powersetCard α 0) : Type u_1) = (Nat.card α).choose 0

Tactic:
simp [powersetCard]

Premises used: Set.powersetCard
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
val : Infinite α
n : ℕ
inr : Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = 0
⊢ Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = (Nat.card α).choose (n + 1)

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]

Premises used: Nat.choose_zero_succ, Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
val : Infinite α
n : ℕ
⊢ Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = 0

Tactic:
Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
val : Infinite α
n : ℕ
⊢ Nat.card.{u_1} (↑(powersetCard α (n + 1)) : Type u_1) = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inl : ∀ (val : Fintype α), Nat.card.{u_1} (↑(powersetCard α n) : Type u_1) = (Nat.card α).choose n
inr inr₁ : Infinite α → 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

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

Premises used: Nat.choose_zero_succ, Nat.card_eq_zero_of_infinite, Set.powersetCard.coe_finset, Set.powersetCard, fintypeOrInfinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
inl : ∀ (val : Fintype α), Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
inr : Infinite α → Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)

Tactic:
cases fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
inl : 1 < (Nat.card α).choose n
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)

Tactic:
rw [Set.nontrivial_coe_sort, ← Set.one_lt_ncard_iff_nontrivial, ← Nat.card_coe_set_eq,
      powersetCard.card]

Premises used: Set.one_lt_ncard_iff_nontrivial, Nat.card_coe_set_eq, Set.powersetCard.card, Set.nontrivial_coe_sort
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
inl : ∀ (this : (Nat.card α).choose n ≤ 1), False
⊢ 1 < (Nat.card α).choose n

Tactic:
by_contra!
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Fintype α
this : (Nat.card α).choose n ≤ 1
⊢ (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1

Tactic:
rw [Nat.le_one_iff_eq_zero_or_eq_one] at this

Premises used: Nat.le_one_iff_eq_zero_or_eq_one
-- Module: Mathlib.Data.Set.PowersetCard
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
inl :
  ∀ (h2 : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(Nat.card α) : ℕ∞)) (val : Fintype α)
    (this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1), False
⊢ False

Tactic:
rw [ENat.card_eq_coe_natCard] at h2

Premises used: ENat.card_eq_coe_natCard
-- Module: Mathlib.Data.Set.PowersetCard
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
⊢ n < Nat.card α

Tactic:
norm_cast at h2
-- Module: Mathlib.Data.Set.PowersetCard
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
inl₁ : ∀ (h : (Nat.card α).choose n = 1), False
⊢ False

Tactic:
rcases this with h | h
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ Nat.card α < n

Tactic:
rw [Nat.choose_eq_zero_iff] at h

Premises used: Nat.choose_eq_zero_iff
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : Nat.card α < n
⊢ False

Tactic:
(lt_self_iff_false n).mp (lt_trans h2 h)

Premises used: lt_trans, lt_self_iff_false, Iff.mp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : Nat.card α < n
⊢ False

Tactic:
exact (lt_self_iff_false n).mp (lt_trans h2 h)

Premises used: lt_trans, lt_self_iff_false, Iff.mp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 1
⊢ n = 0 ∨ Nat.card α = n

Tactic:
rw [Nat.choose_eq_one_iff] at h

Premises used: Nat.choose_eq_one_iff
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
val : Fintype α
h2 : n < Nat.card α
h : n = 0 ∨ Nat.card α = n
⊢ False

Tactic:
aesop
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Infinite α
⊢ NeZero n

Tactic:
have : NeZero n := NeZero.of_pos h1
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : (↑n : ℕ∞) < ENat.card α
val : Infinite α
this : NeZero n
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
⊢ Finite α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (ne_zero_of_lt h2)
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
this : Finite α
apply : (↑n : ℕ∞) < ENat.card α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1)

Tactic:
apply nontrivial h1

Premises used: Set.powersetCard.nontrivial
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
this : Finite α
⊢ (↑n : ℕ∞) < ENat.card α

Tactic:
simp [ENat.card_eq_coe_natCard α, h2]

Premises used: ENat.card_eq_coe_natCard
-- Module: Mathlib.Data.Set.PowersetCard
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
rw₃ rw₄ : Nat.card α < n ↔ Nat.card α < n
⊢ powersetCard α n = ∅ ↔ Nat.card α < n

Tactic:
rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]

Premises used: Nat.choose_eq_zero_iff, Nat.card_coe_set_eq, Set.ncard_eq_zero, Set.powersetCard.card
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Finite α
rw : ¬Nat.card α < n ∧ ¬(n = 0 ∨ Nat.card α = n) ↔ 0 < n ∧ n < Nat.card α
⊢ Nontrivial.{u_1} (↑(powersetCard α n) : Type u_1) ↔ 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]

Premises used: Nat.choose_eq_zero_iff, ne_eq, Nat.one_lt_iff_ne_zero_and_ne_one, Set.powersetCard.card, Nat.choose_eq_one_iff, Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
inst : Finite α
⊢ ¬Nat.card α < n ∧ ¬(n = 0 ∨ Nat.card α = n) ↔ 0 < n ∧ n < Nat.card α

Tactic:
grind
-- Module: Mathlib.Data.Set.PowersetCard
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 })
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 ⋯) :
                    (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 α)
⊢ (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

Tactic:
ext
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)
⊢ 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 })

Tactic:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
n : ℕ
x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)
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 ⋯) :
                  (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:
simp
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
x : (n : ℕ) × (↑(powersetCard α n) : Type u_1)
⊢ (prodEquiv : (a : (n : ℕ) × (↑(powersetCard α n) : Type u_1)) → Finset α) x =
    (↑(x.snd (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1))) : Finset α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.PowersetCard
Goal:
α : Type u_1
s : Finset α
⊢ Eq (α := (n : ℕ) × (↑(powersetCard α n) : Type u_1))
    ((Equiv.symm prodEquiv : (a : Finset α) → (n : ℕ) × (↑(powersetCard α n) : Type u_1)) s :
      (n : ℕ) × (↑(powersetCard α n) : Type u_1))
    (Sigma.mk (β := fun (n : ℕ) ↦ (↑(powersetCard α n) : Type u_1)) (#s) (ofCard ⋯) :
      (n : ℕ) × (↑(powersetCard α n) : Type u_1))

Tactic:
rfl

Premises used: Set.powersetCard.ofCard, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
⊢ (s ×ˢ t).Subsingleton

Tactic:
fun _x hx _y hy ↦
  Prod.ext (hs hx.1 hy.1) (ht hx.2 hy.2)

Premises used: And.right, And.left, Prod.ext, Set.Subsingleton
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂

Tactic:
fun _ ⟨h₁, h₂⟩ => ⟨hs h₁, ht h₂⟩

Premises used: SProd.sprod, Membership.mem, Set.Subset, And.intro, _private.0.Set.prod_mono.match_1
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
hs : s₁ ⊆ s₂
⊢ s₁ ×ˢ t ⊆ s₂ ×ˢ t

Tactic:
prod_mono hs Subset.rfl

Premises used: Set.Subset.rfl, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
ht : t₁ ⊆ t₂
⊢ s ×ˢ t₁ ⊆ s ×ˢ t₂

Tactic:
prod_mono Subset.rfl ht

Premises used: Set.Subset.rfl, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s₁ s₂ : Set α
⊢ s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂

Tactic:
⟨fun h _ hx => (h (mk_mem_prod hx hx)).1, fun h _ hx => ⟨h hx.1, h hx.2⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Set.mk_mem_prod
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
s₁ s₂ : Set α
⊢ s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂

Tactic:
and_congr prod_self_subset_prod_self <| not_congr prod_self_subset_prod_self

Premises used: Set.prod_self_subset_prod_self, not_congr, and_congr
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
P : Set (α × β)
⊢ s ×ˢ t ⊆ P ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → (x, y) ∈ P

Tactic:
⟨fun h _ hx _ hy => h (mk_mem_prod hx hy), fun h ⟨_, _⟩ hp => h _ hp.1 _ hp.2⟩

Premises used: Membership.mem, Prod.mk, Prod.fst, And.right, And.left, Iff.intro, Set.mk_mem_prod, _private.0.Set.prod_subset_iff.match_1
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∀ (x : α × β), x ∈ s ×ˢ t → p x) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (x, y)

Tactic:
prod_subset_iff

Premises used: Set.Mem, Set.prod_subset_iff, Set.Subset
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∃ (x : α × β), x ∈ s ×ˢ t ∧ p x) ↔ ∃ (x : α), x ∈ s ∧ ∃ (y : β), y ∈ t ∧ p (x, y)

Tactic:
simp [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
h : ∀ (x : α × β), x ∈ SProd.sprod (β := Set β) s ∅ ↔ Membership.mem (γ := Set (α × β)) ∅ x
⊢ SProd.sprod (β := Set β) s ∅ = ∅

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
x : α × β
⊢ x ∈ SProd.sprod (β := Set β) s ∅ ↔ Membership.mem (γ := Set (α × β)) ∅ x

Tactic:
iff_of_eq (and_false _)

Premises used: and_false, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
x : α × β
⊢ x ∈ SProd.sprod (β := Set β) s ∅ ↔ Membership.mem (γ := Set (α × β)) ∅ x

Tactic:
exact iff_of_eq (and_false _)

Premises used: and_false, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) ∅ t ↔ Membership.mem (γ := Set (α × β)) ∅ x
⊢ SProd.sprod (α := Set α) ∅ t = ∅

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) ∅ t ↔ Membership.mem (γ := Set (α × β)) ∅ x

Tactic:
iff_of_eq (false_and _)

Premises used: false_and, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) ∅ t ↔ Membership.mem (γ := Set (α × β)) ∅ x

Tactic:
exact iff_of_eq (false_and _)

Premises used: false_and, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
h : ∀ (x : α × β), x ∈ SProd.sprod (α := Set α) (β := Set β) univ univ ↔ Membership.mem (γ := Set (α × β)) univ x
⊢ SProd.sprod (α := Set α) (β := Set β) univ univ = univ

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) (β := Set β) univ univ ↔ Membership.mem (γ := Set (α × β)) univ x

Tactic:
iff_of_eq (true_and _)

Premises used: true_and, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
x : α × β
⊢ x ∈ SProd.sprod (α := Set α) (β := Set β) univ univ ↔ Membership.mem (γ := Set (α × β)) univ x

Tactic:
exact iff_of_eq (true_and _)

Premises used: true_and, iff_of_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
⊢ SProd.sprod (α := Set α) univ t = Prod.snd ⁻¹' t

Tactic:
simp [prod_eq]

Premises used: Set.prod_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
⊢ SProd.sprod (β := Set β) s univ = Prod.fst ⁻¹' s

Tactic:
simp [prod_eq]

Premises used: Set.prod_eq
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty α
inst_1 : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
simp [eq_univ_iff_forall, forall_and]

Premises used: Set.eq_univ_iff_forall, forall_and
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
a : α
h : ∀ (x : α) (y : β), (x, y) ∈ SProd.sprod (α := Set α) {a} t ↔ (x, y) ∈ Prod.mk a '' t
⊢ SProd.sprod (α := Set α) {a} t = Prod.mk a '' t

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
a x : α
y : β
⊢ (x, y) ∈ SProd.sprod (α := Set α) {a} t ↔ (x, y) ∈ Prod.mk a '' t

Tactic:
simp [and_left_comm, eq_comm]

Premises used: and_left_comm, eq_comm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
h :
  ∀ (x : α) (y : β),
    (x, y) ∈ SProd.sprod (β := Set β) s {b} ↔ Membership.mem (γ := Set (α × β)) ((fun (a : α) ↦ (a, b)) '' s) (x, y)
⊢ SProd.sprod (β := Set β) s {b} = (fun (a : α) ↦ (a, b)) '' s

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
x : α
y : β
⊢ (x, y) ∈ SProd.sprod (β := Set β) s {b} ↔ Membership.mem (γ := Set (α × β)) ((fun (a : α) ↦ (a, b)) '' s) (x, y)

Tactic:
simp [and_left_comm, eq_comm]

Premises used: and_left_comm, eq_comm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
h :
  ∀ (c : α) (d : β),
    (c, d) ∈ SProd.sprod (α := Set α) (β := Set β) {a} {b} ↔ Membership.mem (γ := Set (α × β)) {(a, b)} (c, d)
⊢ SProd.sprod (α := Set α) (β := Set β) {a} {b} = {(a, b)}

Tactic:
ext ⟨c, d⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
c : α
d : β
⊢ (c, d) ∈ SProd.sprod (α := Set α) (β := Set β) {a} {b} ↔ Membership.mem (γ := Set (α × β)) {(a, b)} (c, d)

Tactic:
simp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
h : ∀ (x : α) (y : β), (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
simp [or_and_right]

Premises used: or_and_right
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
h : ∀ (x : α) (y : β), (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
simp [and_or_left]

Premises used: and_or_left
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
h : ∀ (x : α) (y : β), (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
simp only [← and_and_right, mem_inter_iff, mem_prod]

Premises used: Set.mem_inter_iff, Set.mem_prod, and_and_right
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
h : ∀ (x : α) (y : β), (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
simp only [← and_and_left, mem_inter_iff, mem_prod]

Premises used: and_and_left, Set.mem_inter_iff, Set.mem_prod
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
h : ∀ (x : α) (y : β), (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
simp [and_assoc, and_left_comm]

Premises used: and_left_comm, and_assoc
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_5
β : Type u_6
s : Set α
t : Set β
⊢ (s ×ˢ t)ᶜ = SProd.sprod (β := Set β) sᶜ univ ∪ SProd.sprod (α := Set α) univ tᶜ

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
simp_rw :
  (∀ (a : α) (b : β), a ∈ s₁ ∧ b ∈ t₁ → ¬(a ∈ s₂ ∧ b ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
simp_rw [disjoint_left, mem_prod, Prod.forall]

Premises used: Set.disjoint_left, Set.mem_prod, Prod.forall
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ (a : α) (b : β), a ∈ s₁ ∧ b ∈ t₁ → ¬(a ∈ s₂ ∧ b ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
hs : Disjoint s₁ s₂
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)

Tactic:
disjoint_left.2 fun ⟨_a, _b⟩ ⟨ha₁, _⟩ ⟨ha₂, _⟩ => disjoint_left.1 hs ha₁ ha₂

Premises used: Iff.mpr, False, _private.0.Set.Disjoint.set_prod_left.match_2, Set.disjoint_left, Iff.mp, _private.0.Set.Disjoint.set_prod_left.match_1
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t₁ t₂ : Set β
ht : Disjoint t₁ t₂
s₁ s₂ : Set α
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)

Tactic:
disjoint_left.2 fun ⟨_a, _b⟩ ⟨_, hb₁⟩ ⟨_, hb₂⟩ => disjoint_left.1 ht hb₁ hb₂

Premises used: Iff.mpr, False, _private.0.Set.Disjoint.set_prod_right.match_2, Set.disjoint_left, _private.0.Set.Disjoint.set_prod_right.match_1, Iff.mp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
h : ∀ (x : β × δ), x ∈ Prod.map f g '' s ×ˢ t ↔ x ∈ (f '' s) ×ˢ (g '' t)
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
ext
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
x : β × δ
⊢ x ∈ Prod.map f g '' s ×ˢ t ↔ x ∈ (f '' s) ×ˢ (g '' t)

Tactic:
aesop
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
⊢ insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Tactic:
simp only [insert_eq, union_prod, singleton_prod]

Premises used: Set.insert_eq, Set.singleton_prod, Set.union_prod
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
⊢ s ×ˢ insert b t = (fun (a : α) ↦ (a, b)) '' s ∪ s ×ˢ t

Tactic:
simp only [insert_eq, prod_union, prod_singleton]

Premises used: Set.insert_eq, Set.prod_singleton, Set.prod_union
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : γ → α
g : δ → β
⊢ (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun (p : γ × δ) ↦ (f p.1, g p.2)) ⁻¹' s ×ˢ t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : γ → α
⊢ (f ⁻¹' s) ×ˢ t = (fun (p : γ × β) ↦ (f p.1, p.2)) ⁻¹' s ×ˢ t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, rfl