awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
a : BijOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)
⊢ (sup (t.preimage (Subtype.val (p := P)) ⋯) fun (x : Subtype P) ↦ (↑x : α)) = t.sup id

Tactic:
apply sup_preimage_self

Premises used: Finset.sup_preimage_self
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
⊢ BijOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)

Tactic:
⟨mapsTo_preimage _ _, injOn_of_injective Subtype.val_injective, ?_⟩

Premises used: Subtype.val_injective, Set.mapsTo_preimage, And.intro, Set.BijOn, Set.injOn_of_injective
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
a : SurjOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)
⊢ BijOn (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α)) (↑t : Set α)

Tactic:
refine ⟨mapsTo_preimage _ _, injOn_of_injective Subtype.val_injective, ?_⟩
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
inst : Lattice α
inst_1 : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot (p := P) Pbot
x : α
hx : x ∈ (↑t : Set α)
⊢ x ∈ Set.image (α := Subtype P) (Subtype.val (p := P)) (Subtype.val (p := P) ⁻¹' (↑t : Set α))

Tactic:
simpa using ⟨hx, ht x hx⟩
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
h :
  ∀ (x : (i : α) × β i),
    Membership.mem (γ := Finset ((i : α) × β i))
        (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) x ↔
      x ∈ {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t}
⊢ (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) =
    {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t}

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ Membership.mem (γ := Finset ((i : α) × β i))
      (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) x ↔
    x ∈ {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t}

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image (Sigma.fst (β := fun (a : α) ↦ β a)) s ⊆ t
rw : {a ∈ s | a.fst (β := fun (a : α) ↦ β a) ∈ t} = s
rw₁ rw₂ : s = s
⊢ (t.sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦ s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) = s

Tactic:
rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]

Premises used: Finset.filter_true_of_mem, Finset.image_subset_iff, Finset.sigma_preimage_mk, Iff.mp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : α → Type u_1
inst : DecidableEq α
s : Finset ((a : α) × β a)
⊢ ((image (Sigma.fst (β := fun (a : α) ↦ β a)) s).sigma (α := fun (a : α) ↦ β a) fun (a : α) ↦
      s.preimage (Sigma.mk (β := fun (a : α) ↦ β a) a) ⋯) =
    s

Tactic:
s.sigma_preimage_mk_of_subset (Subset.refl _)

Premises used: Finset.Subset.refl, Finset.sigma_preimage_mk_of_subset
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
h : ∀ (x : α), x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft
⊢ s.preimage Sum.inl ⋯ = s.toLeft

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
h : ∀ (x : β), x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight
⊢ s.preimage Sum.inr ⋯ = s.toRight

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
b : ↥s
⊢ Membership.mem (α := α) (s.preimage (⇑e : (a : α) → β) ⋯) ((e.symm : (a : β) → α) (↑b : β) : α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x : ↥(s.preimage (⇑e : (a : α) → β) ⋯)
⊢ (fun (b : ↥s) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s.preimage (⇑e : (a : α) → β) ⋯) ((e.symm : (a : β) → α) (↑b : β)) ⋯ :
          ↥(s.preimage (⇑e : (a : α) → β) ⋯)))
      ((fun (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) ↦
          (Subtype.mk (p := fun (x : β) ↦ x ∈ s) ((e : (a : α) → β) (↑a : α)) ⋯ : ↥s))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x : ↥s
⊢ (fun (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ s) ((e : (a : α) → β) (↑a : α)) ⋯ : ↥s))
      ((fun (b : ↥s) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s.preimage (⇑e : (a : α) → β) ⋯) ((e.symm : (a : β) → α) (↑b : β)) ⋯ :
            ↥(s.preimage (⇑e : (a : α) → β) ⋯)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq α
e : α ≃ β
s : Finset β
⊢ Finset.image (⇑e.symm : (a : β) → α) s = s.preimage (⇑e : (a : α) → β) ⋯

Tactic:
grind [Finset.mem_preimage]

Premises used: Finset.mem_preimage
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
inst : DecidableEq β
e : α ≃ β
s : Finset α
⊢ Finset.image (⇑e : (a : α) → β) s = s.preimage (⇑e.symm : (a : β) → α) ⋯

Tactic:
e.symm.image_symm_eq_preimage_of_finset s

Premises used: Equiv.image_symm_eq_preimage_of_finset, Equiv.symm
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
h :
  ∀ (x : (a : α) → π ((e : (a : α) → β) a)) (b : ↥s),
    Eq.{u_1 + 1} (α := π (↑b : β))
      ((s.restrict (π := π) ∘ (⇑(Equiv.piCongrLeft π e) : (a : (a : α) → π ((e : (a : α) → β) a)) → (b : β) → π b)) x
          b :
        π (↑b : β))
      (((⇑(Equiv.piCongrLeft.{u_1 + 1, u + 1, v + 1} (fun (b : ↥s) ↦ π (↑b : β)) (e.restrictPreimageFinset s) :
                  ((a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                      π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) ≃
                    ((b : ↥s) → π (↑b : β))) :
              (a :
                  (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                    π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) →
                (b : ↥s) → π (↑b : β)) ∘
            (s.preimage (⇑e : (a : α) → β) ⋯).restrict (π := fun (i : α) ↦ π ((e : (a : α) → β) i)))
          x b :
        π (↑b : β))
⊢ Eq (α := ((a : α) → π ((e : (a : α) → β) a)) → (i : ↥s) → π (↑i : β))
    (s.restrict (π := π) ∘ (⇑(Equiv.piCongrLeft π e) : (a : (a : α) → π ((e : (a : α) → β) a)) → (b : β) → π b))
    ((⇑(Equiv.piCongrLeft.{u_1 + 1, u + 1, v + 1} (fun (b : ↥s) ↦ π (↑b : β)) (e.restrictPreimageFinset s) :
            ((a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) ≃
              ((b : ↥s) → π (↑b : β))) :
        (a :
            (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
              π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) →
          (b : ↥s) → π (↑b : β)) ∘
      (s.preimage (⇑e : (a : α) → β) ⋯).restrict (π := fun (i : α) ↦ π ((e : (a : α) → β) i)))

Tactic:
ext x b
-- Module: Mathlib.Data.Finset.Preimage
Goal:
α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
x : (a : α) → π ((e : (a : α) → β) a)
b : ↥s
⊢ Eq.{u_1 + 1} (α := π (↑b : β))
    ((s.restrict (π := π) ∘ (⇑(Equiv.piCongrLeft π e) : (a : (a : α) → π ((e : (a : α) → β) a)) → (b : β) → π b)) x b :
      π (↑b : β))
    (((⇑(Equiv.piCongrLeft.{u_1 + 1, u + 1, v + 1} (fun (b : ↥s) ↦ π (↑b : β)) (e.restrictPreimageFinset s) :
                ((a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                    π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) ≃
                  ((b : ↥s) → π (↑b : β))) :
            (a :
                (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) →
                  π (↑((e.restrictPreimageFinset s : (a : ↥(s.preimage (⇑e : (a : α) → β) ⋯)) → ↥s) a) : β)) →
              (b : ↥s) → π (↑b : β)) ∘
          (s.preimage (⇑e : (a : α) → β) ⋯).restrict (π := fun (i : α) ↦ π ((e : (a : α) → β) i)))
        x b :
      π (↑b : β))

Tactic:
simp only [comp_apply, restrict, Equiv.piCongrLeft_apply_eq_cast,
    Equiv.restrictPreimageFinset_symm_apply_coe]

Premises used: Equiv.restrictPreimageFinset_symm_apply_coe, Finset.restrict, Equiv.piCongrLeft_apply_eq_cast, Function.comp_apply
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.product t = s ×ˢ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).val = s.val ×ˢ t.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α × β
⊢ p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t

Tactic:
Multiset.mem_product

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
a : α
b : β
ha : a ∈ s
hb : b ∈ t
⊢ (a, b) ∈ s ×ˢ t

Tactic:
mem_product.2 ⟨ha, hb⟩

Premises used: Iff.mpr, And.intro, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
Set.ext fun _ => Finset.mem_product

Premises used: Set.ext, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s

Tactic:
simp +contextual [mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t

Tactic:
simp +contextual [mem_image]

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq α
ht : t.Nonempty
h : ∀ (i : α), i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq α
ht : t.Nonempty
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s

Tactic:
simp [mem_image, ht.exists_mem]

Premises used: Finset.Nonempty.exists_mem, Finset.mem_image
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq β
ht : s.Nonempty
h : ∀ (i : β), i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst : DecidableEq β
ht : s.Nonempty
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t

Tactic:
simp [mem_image, ht.exists_mem]

Premises used: Finset.Nonempty.exists_mem, Finset.mem_image
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
s : Finset (α × β)
⊢ s ⊆ image Prod.fst s ×ˢ image Prod.snd s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ s ×ˢ t ⊆ s' ×ˢ t'

Tactic:
fun ⟨_, _⟩ h =>
  mem_product.2 ⟨hs (mem_product.1 h).1, ht (mem_product.1 h).2⟩

Premises used: Iff.mpr, SProd.sprod, Membership.mem, And.right, And.left, And.intro, Iff.mp, Finset.mem_product, _private.0.Finset.product_subset_product.match_1
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
hs : s ⊆ s'
⊢ s ×ˢ t ⊆ s' ×ˢ t

Tactic:
product_subset_product hs (Subset.refl _)

Premises used: Finset.Subset.refl, Finset.product_subset_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
ht : t ⊆ t'
⊢ s ×ˢ t ⊆ s ×ˢ t'

Tactic:
product_subset_product (Subset.refl _) ht

Premises used: Finset.Subset.refl, Finset.product_subset_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : DecidableEq β
inst_1 : DecidableEq δ
f : α → β
g : γ → δ
s : Finset α
t : Finset γ
⊢ image (Prod.map f g) (s ×ˢ t) = image f s ×ˢ image g t

Tactic:
mod_cast Set.prodMap_image_prod f g s t

Premises used: SProd.sprod, congrArg, SetLike.coe_set_eq._simp_1, Set.prodMap_image_prod, cast, Finset.coe_image._simp_1, Prod.map, SetLike.coe, congr, Finset.coe_product._simp_1, Set.image, Eq, Finset.image, Eq.trans
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

Tactic:
simpa [← coe_inj] using Set.prodMap_image_prod f g s t

Premises used: Set.prodMap_image_prod, Finset.coe_inj, SetLike.coe, DFunLike.coe
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
push_cast :
  (⇑{ toFun := Prod.swap, inj' := ⋯ } : (a : β × α) → α × β) '' (↑t : Set β) ×ˢ (↑s : Set α) =
    (↑s : Set α) ×ˢ (↑t : Set β)
⊢ (↑(map { toFun := Prod.swap, inj' := ⋯ : β × α ↪ α × β } (t ×ˢ s)) : Set (α × β)) = (↑(s ×ˢ t) : Set (α × β))

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (⇑{ toFun := Prod.swap, inj' := ⋯ } : (a : β × α) → α × β) '' (↑t : Set β) ×ˢ (↑s : Set α) =
    (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
Set.image_swap_prod _ _

Premises used: Set.image_swap_prod, Prod.swap
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (⇑{ toFun := Prod.swap, inj' := ⋯ } : (a : β × α) → α × β) '' (↑t : Set β) ×ˢ (↑s : Set α) =
    (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
exact Set.image_swap_prod _ _

Premises used: Set.image_swap_prod
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
push_cast : Prod.swap '' (↑t : Set β) ×ˢ (↑s : Set α) = (↑s : Set α) ×ˢ (↑t : Set β)
⊢ (↑(image Prod.swap (t ×ˢ s)) : Set (α × β)) = (↑(s ×ˢ t) : Set (α × β))

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' (↑t : Set β) ×ˢ (↑s : Set α) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
Set.image_swap_prod _ _

Premises used: Set.image_swap_prod
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' (↑t : Set β) ×ˢ (↑s : Set α) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
exact Set.image_swap_prod _ _

Premises used: Set.image_swap_prod
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = s.biUnion fun (a : α) ↦ image (fun (b : β) ↦ (a, b)) t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ s ×ˢ t = t.biUnion fun (b : β) ↦ image (fun (a : α) ↦ (a, b)) s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ (s ×ˢ t).biUnion f = s.biUnion fun (a : α) ↦ t.biUnion fun (b : β) ↦ f (a, b)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ #(s ×ˢ t) = #s * #t

Tactic:
Multiset.card_product _ _

Premises used: Multiset.card_product, Finset.card
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
simp_rw : 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]

Premises used: Finset.one_lt_card_iff_nontrivial, Finset.card_product, Finset.card_pos
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)

Tactic:
apply Nat.one_lt_mul_iff

Premises used: Nat.one_lt_mul_iff
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = filter p s ×ˢ filter q t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst : DecidablePred p
⊢ {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t

Tactic:
simpa using filter_product p fun _ => true

Premises used: Bool.true, Eq, Finset.filter_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

Tactic:
simpa using filter_product (fun _ : α => true) q

Premises used: Bool.true, Eq, Finset.filter_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₁ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]

Premises used: Finset.card_product, Finset.card_union_of_disjoint, Finset.filter_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : {x ∈ s ×ˢ t | p x.1 = q x.2} = {x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2}
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ {x ∈ s ×ˢ t | p x.1 = q x.2} = {x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : Disjoint (α := α × β → Prop) (fun (x : α × β) ↦ p x.1 ∧ q x.2) fun (x : α × β) ↦ ¬p x.1 ∧ ¬q x.2
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
apply Finset.disjoint_filter_filter'

Premises used: Finset.disjoint_filter_filter'
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint (α := α × β → Prop) (fun (x : α × β) ↦ p x.1 ∧ q x.2) fun (x : α × β) ↦ ¬p x.1 ∧ ¬q x.2

Tactic:
(disjoint_compl_right.inf_left _).inf_right _

Premises used: disjoint_compl_right, Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
⊢ Disjoint (α := α × β → Prop) (fun (x : α × β) ↦ p x.1 ∧ q x.2) fun (x : α × β) ↦ ¬p x.1 ∧ ¬q x.2

Tactic:
exact (disjoint_compl_right.inf_left _).inf_right _

Premises used: disjoint_compl_right, Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
rw : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
rw₁ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₂ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
rw₃ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₄ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₅ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₆ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₇ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₈ : #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
rw₉ rw₁₀ : Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    grind
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

Premises used: Finset.card_product, congr_arg, Finset.disjoint_filter_filter', disjoint_compl_right, Finset.card_union_of_disjoint, Finset.filter_product, Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
t : Finset β
⊢ SProd.sprod (α := Finset α) ∅ t = ∅

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.empty, Multiset.join, Multiset.product, List.foldr, Multiset.bind, Finset.product, rfl
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ SProd.sprod (β := Finset β) s ∅ = ∅

Tactic:
eq_empty_of_forall_notMem fun _ h => notMem_empty _ (Finset.mem_product.1 h).2

Premises used: Finset.eq_empty_of_forall_notMem, Finset.notMem_empty, And.right, Iff.mp, Prod.snd, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ (s ×ˢ t).Nonempty

Tactic:
let ⟨x, hx⟩ := hs
  let ⟨y, hy⟩ := ht
  ⟨(x, y), mem_product.2 ⟨hx, hy⟩⟩

Premises used: Iff.mpr, SProd.sprod, Prod.mk, And.intro, Exists.intro, Finset.Nonempty, _private.0.Finset.Nonempty.product.match_1, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
h : (s ×ˢ t).Nonempty
⊢ s.Nonempty

Tactic:
let ⟨xy, hxy⟩ := h
  ⟨xy.1, (mem_product.1 hxy).1⟩

Premises used: _private.0.Finset.Nonempty.fst.match_1, Prod.fst, And.left, Exists.intro, Iff.mp, Finset.Nonempty, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
h : (s ×ˢ t).Nonempty
⊢ t.Nonempty

Tactic:
let ⟨xy, hxy⟩ := h
  ⟨xy.2, (mem_product.1 hxy).2⟩

Premises used: _private.0.Finset.Nonempty.fst.match_1, And.right, Exists.intro, Iff.mp, Finset.Nonempty, Prod.snd, Finset.mem_product
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.product h.2⟩

Premises used: Finset.Nonempty.product, Finset.Nonempty.snd, Finset.Nonempty.fst, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Data.Finset.Prod
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
contrapose! : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
contrapose!