awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
s : Set α
t : Set β
g : δ → β
⊢ s ×ˢ (g ⁻¹' t) = (fun (p : α × δ) ↦ (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
δ : Type u_4
f : α → β
g : γ → δ
s : Set β
t : Set δ
⊢ Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' 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 : γ → α
g : γ → β
⊢ (fun (x : γ) ↦ (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun (a : α) ↦ (a, b)) ⁻¹' s ×ˢ t = s

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : ¬b ∈ t
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (a : α) ↦ (a, b)) ⁻¹' s ×ˢ t) ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : ¬a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
inst : DecidablePred fun (x : β) ↦ x ∈ t
⊢ (fun (a : α) ↦ (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
b : β
inst : DecidablePred fun (x : β) ↦ x ∈ t
f : γ → α
⊢ (fun (a : γ) ↦ (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
s : Set α
t : Set β
a : α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : δ → β
⊢ (fun (b : δ) ↦ (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
rw : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
rw₁ rw₂ : t ×ˢ s = t ×ˢ s
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s

Tactic:
rw [image_swap_eq_preimage_swap, preimage_swap_prod]

Premises used: Set.image_swap_eq_preimage_swap, Set.preimage_swap_prod
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)

Tactic:
fun _ ⟨hx, hy⟩ ↦ ⟨hy, hx⟩

Premises used: SProd.sprod, Membership.mem, Set.MapsTo, And.intro, _private.0.Set.mapsTo_swap_prod.match_1, Prod.swap
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ),
    x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ Membership.mem (γ := Set (γ × δ)) ((fun (p : α × β) ↦ (m₁ p.1, m₂ p.2)) '' s ×ˢ t) x

Tactic:
simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

Premises used: and_left_comm, and_comm, exists_and_right, and_assoc, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ),
    x ∈ range m₁ ×ˢ range m₂ ↔ Membership.mem (γ := Set (γ × δ)) (range fun (p : α × β) ↦ (m₁ p.1, m₂ p.2)) x

Tactic:
simp [range]

Premises used: Set.range
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m₁ : α → γ
m₂ : β → δ
⊢ range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂

Tactic:
prod_range_range_eq.symm

Premises used: Prod.map, Set.prod_range_range_eq, Eq.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m₁ : α → γ
⊢ ∀ (x : γ × β),
    x ∈ SProd.sprod (β := Set β) (range m₁) univ ↔
      Membership.mem (γ := Set (γ × β)) (range fun (p : α × β) ↦ (m₁ p.1, p.2)) x

Tactic:
simp [range]

Premises used: Set.range
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
m₂ : β → δ
⊢ ∀ (x : α × δ),
    x ∈ SProd.sprod (α := Set α) univ (range m₂) ↔
      Membership.mem (γ := Set (α × δ)) (range fun (p : α × β) ↦ (p.1, m₂ p.2)) x

Tactic:
simp [range]

Premises used: Set.range
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
⊢ (range fun (x : α) ↦ (f x, g x)) ⊆ range f ×ˢ range g

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty

Tactic:
fun ⟨x, hx⟩ ⟨y, hy⟩ =>
  ⟨(x, y), ⟨hx, hy⟩⟩

Premises used: SProd.sprod, Prod.mk, Set.Nonempty, And.intro, Exists.intro, _private.0.Set.Nonempty.prod.match_1
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Nonempty → s.Nonempty

Tactic:
fun ⟨x, hx⟩ => ⟨x.1, hx.1⟩

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

Tactic:
fun ⟨x, hx⟩ => ⟨x.2, hx.2⟩

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

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

Premises used: Set.Nonempty.snd, Set.Nonempty.prod, And.right, And.left, And.intro, Iff.intro, Set.Nonempty.fst
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]

Premises used: Set.not_nonempty_iff_eq_empty, Set.prod_nonempty_iff, not_and_or, Iff.symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W

Tactic:
simp [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
⊢ (fun (x : α) ↦ (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun (a : α) ↦ (a, b)) '' s ⊆ s ×ˢ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a '' t ⊆ s ×ˢ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t ⊆ Prod.fst ⁻¹' s

Tactic:
inter_subset_left

Premises used: Set.Mem, setOf, Set.prod, Set.inter_subset_left, Set.preimage
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst '' s ×ˢ t ⊆ s

Tactic:
image_subset_iff.2 <| prod_subset_preimage_fst s t

Premises used: Iff.mpr, Set.prod_subset_preimage_fst, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set β
t : Set α
ht : t.Nonempty
⊢ Prod.fst '' s ×ˢ t = s

Tactic:
(fst_image_prod_subset _ _).antisymm fun y hy =>
    let ⟨x, hx⟩ := ht
    ⟨(y, x), ⟨hy, hx⟩, rfl⟩

Premises used: SProd.sprod, Membership.mem, Set.fst_image_prod_subset, Prod.mk, Prod.fst, HasSubset.Subset.antisymm, And.intro, Exists.intro, Set.image, _private.0.Set.Nonempty.prod.match_1, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ MapsTo Prod.fst (s ×ˢ t) s

Tactic:
fun _ hx ↦ (mem_prod.1 hx).1

Premises used: Set.mem_prod, And.left, Set.MapsTo, Iff.mp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t ⊆ Prod.snd ⁻¹' t

Tactic:
inter_subset_right

Premises used: Set.Mem, setOf, Set.prod, Set.preimage, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.snd '' s ×ˢ t ⊆ t

Tactic:
image_subset_iff.2 <| prod_subset_preimage_snd s t

Premises used: Iff.mpr, Set.prod_subset_preimage_snd, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
⊢ Prod.snd '' s ×ˢ t = t

Tactic:
(snd_image_prod_subset _ _).antisymm fun y y_in =>
    let ⟨x, x_in⟩ := hs
    ⟨(x, y), ⟨x_in, y_in⟩, rfl⟩

Premises used: Set.snd_image_prod_subset, SProd.sprod, Membership.mem, Prod.mk, HasSubset.Subset.antisymm, And.intro, Exists.intro, Set.image, _private.0.Set.Nonempty.prod.match_1, Prod.snd, rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
x : α × β
p₁ : α
p₂ : β
h : (p₁, p₂) ∈ s
⊢ (p₁, p₂) ∈ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
aesop
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ MapsTo Prod.snd (s ×ˢ t) t

Tactic:
fun _ hx ↦ (mem_prod.1 hx).2

Premises used: Set.mem_prod, And.right, Set.MapsTo, Iff.mp
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
inl : ∀ (h : s ×ˢ t = ∅), s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
inr : ∀ (h : (s ×ˢ t).Nonempty), s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Premises used: SProd.sprod, Set.eq_empty_or_nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
simp [h, prod_eq_empty_iff.1 h]

Premises used: Iff.mp, Set.prod_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : s.Nonempty ∧ t.Nonempty), s.Nonempty ∧ t.Nonempty
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
rwa [prod_nonempty_iff] at h

Premises used: Set.prod_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩

Premises used: And.intro, Iff.intro, Or.inl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
inr : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), s ⊆ s₁
inr₁ : ∀ (H : s ×ˢ t ⊆ s₁ ×ˢ t₁), t ⊆ t₁
inr₂ : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁

Tactic:
have := image_mono (f := Prod.fst) H
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
inr : ∀ (this : s ⊆ Prod.fst '' s₁ ×ˢ t₁), s ⊆ s₁
inr₁ inr₂ inr₃ inr₄ : ∀ (this : s ⊆ s₁), s ⊆ s₁
⊢ s ⊆ s₁

Tactic:
rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this

Premises used: Set.Nonempty.snd, Set.fst_image_prod, Set.Nonempty.mono, And.right
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁

Tactic:
have := image_mono (f := Prod.snd) H
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
inr : ∀ (this : t ⊆ Prod.snd '' s₁ ×ˢ t₁), t ⊆ t₁
inr₁ inr₂ inr₃ inr₄ : ∀ (this : t ⊆ t₁), t ⊆ t₁
⊢ t ⊆ t₁

Tactic:
rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this

Premises used: Set.Nonempty.mono, And.left, Set.snd_image_prod, Set.Nonempty.fst
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ⊆ s₁ ∧ t ⊆ t₁

Tactic:
simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H

Premises used: Set.Nonempty.ne_empty, And.right, And.left, or_false
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
prod_mono H.1 H.2

Premises used: And.right, And.left, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact prod_mono H.1 H.2

Premises used: And.right, And.left, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
rw : ¬(s = ∅ ∨ t = ∅)
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁

Tactic:
rw [prod_subset_prod_iff, or_iff_left]

Premises used: Set.prod_subset_prod_iff, or_iff_left
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
rw : ¬s ×ˢ t = ∅
⊢ ¬(s = ∅ ∨ t = ∅)

Tactic:
rw [← Set.prod_eq_empty_iff]

Premises used: Set.prod_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬s ×ˢ t = ∅

Tactic:
h.ne_empty

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬s ×ˢ t = ∅

Tactic:
exact h.ne_empty

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
h : t.Nonempty
⊢ s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁

Tactic:
simp +contextual [prod_subset_prod_iff, or_iff_left h.ne_empty]

Premises used: Set.prod_subset_prod_iff, Set.Nonempty.ne_empty, or_iff_left
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t t₁ : Set β
h : s.Nonempty
⊢ s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁

Tactic:
simp +contextual [prod_subset_prod_iff, or_comm (a := s = ∅), or_iff_left h.ne_empty]

Premises used: Set.prod_subset_prod_iff, Set.Nonempty.ne_empty, or_iff_left, or_comm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
mp : s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁
mpr : s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Tactic:
constructor
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
rwa rwa₁ rwa₂ rwa₃ : (s ×ˢ t).Nonempty
⊢ (s₁ ×ˢ t₁).Nonempty

Tactic:
rwa [← heq]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ (s₁ ×ˢ t₁).Nonempty

Tactic:
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
rw [prod_nonempty_iff] at h h₁

Premises used: Set.prod_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
h₂ : s.Nonempty ∧ t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rw [prod_nonempty_iff] at h h₁

Premises used: Set.prod_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
h₂ : s.Nonempty ∧ t.Nonempty
heq₁ : s ×ˢ t = s₁ ×ˢ t₁
⊢ s₁.Nonempty ∧ t₁.Nonempty

Tactic:
rw [prod_nonempty_iff] at h h₁

Premises used: Set.prod_nonempty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
mp : Prod.fst '' s ×ˢ t = s₁ ∧ t = t₁
mp₁ : Prod.fst '' s ×ˢ t = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₂ : Prod.fst '' s₁ ×ˢ t₁ = Prod.fst '' s₁ ×ˢ t₁ ∧ t = t₁
mp₃ : True ∧ t = t₁
mp₄ : t = t₁
mp₅ : Prod.snd '' s ×ˢ t = t₁
mp₆ : Prod.snd '' s ×ˢ t = Prod.snd '' s₁ ×ˢ t₁
mp₇ mp₈ : Prod.snd '' s₁ ×ˢ t₁ = Prod.snd '' s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁

Tactic:
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]

Premises used: Set.fst_image_prod, And.right, And.left, Set.snd_image_prod, eq_self_iff_true, true_and
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
symm : s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Tactic:
symm
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
inl : ∀ (h : s ×ˢ t = ∅), s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
inr : ∀ (h : (s ×ˢ t).Nonempty), s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rcases eq_empty_or_nonempty (s ×ˢ t) with h | h

Premises used: SProd.sprod, Set.eq_empty_or_nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
inl : s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
      or_iff_right_iff_imp]

Premises used: eq_comm, or_iff_right_iff_imp, Iff.mp, Set.prod_eq_empty_iff, true_and
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅

Tactic:
prod_eq_empty_iff.mp h

Premises used: Iff.mp, Set.prod_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅

Tactic:
exact prod_eq_empty_iff.mp h

Premises used: Iff.mp, Set.prod_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
inr : s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rw [prod_eq_prod_iff_of_nonempty h]

Premises used: Set.prod_eq_prod_iff_of_nonempty
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬(s = ∅ ∨ t = ∅)

Tactic:
rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h

Premises used: Ne, Set.nonempty_iff_ne_empty, Set.prod_eq_empty_iff
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
inr : s = s₁ ∧ t = t₁ ∨ False ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
inr₁ : s = s₁ ∧ t = t₁ ∨ False ↔ s = s₁ ∧ t = t₁
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
simp_rw [h, false_and, or_false]

Premises used: false_and, or_false
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
simp_rw : s = ∅ ∧ s₁ = ∅ → s = s₁
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true, or_iff_left_iff_imp, or_false]

Premises used: and_true, or_iff_left_iff_imp, Set.Nonempty.ne_empty, Set.prod_eq_prod_iff, or_false
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ Eq.{u_1 + 1} (α := Set α) ∅ ∅

Tactic:
rfl
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
⊢ s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
fun _ hp ↦ mem_prod.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩

Premises used: Iff.mpr, Set.Subset, Prod.fst, Set.mem_prod, Set.mem_image_of_mem, And.intro, Prod.snd
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Set β
g : α → Set γ
hf : Monotone f
hg : Monotone g
⊢ Monotone (β := Set (β × γ)) fun (x : α) ↦ f x ×ˢ g x

Tactic:
fun _ _ h => prod_mono (hf h) (hg h)

Premises used: Monotone, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Set β
g : α → Set γ
hf : Antitone f
hg : Antitone g
⊢ Antitone (β := Set (β × γ)) fun (x : α) ↦ f x ×ˢ g x

Tactic:
fun _ _ h => prod_mono (hf h) (hg h)

Premises used: Antitone, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst : Preorder α
f : α → Set β
g : α → Set γ
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn (β := Set (β × γ)) (fun (x : α) ↦ f x ×ˢ g x) s

Tactic:
fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)

Premises used: MonotoneOn, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst : Preorder α
f : α → Set β
g : α → Set γ
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn (β := Set (β × γ)) (fun (x : α) ↦ f x ×ˢ g x) s

Tactic:
fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)

Premises used: AntitoneOn, Set.prod_mono
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
γ : Type u_3
δ : Type u_4
s : Set α
a b : α → γ × δ
⊢ EqOn a b s ↔ EqOn (Prod.fst ∘ a) (Prod.fst ∘ b) s ∧ EqOn (Prod.snd ∘ a) (Prod.snd ∘ b) s

Tactic:
grind [EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
ht : t.Nonempty
obtain : ∀ (x : β) (hxt : x ∈ t), EqOn f f' s
⊢ EqOn f f' s

Tactic:
obtain ⟨x, hxt⟩ := ht
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : β
hxt : x_1 ∈ t
x : α
hxs : x ∈ s
⊢ Prod.map f g (x, x_1) = Prod.map f' g' (x, x_1)

Tactic:
have h' := h <| mk_mem_prod hxs hxt
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : β
hxt : x_1 ∈ t
x : α
hxs : x ∈ s
h' : Prod.map f g (x, x_1) = Prod.map f' g' (x, x_1)
⊢ f x = f' x

Tactic:
grind
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
hs : s.Nonempty
obtain : ∀ (x : α) (hxs : x ∈ s), EqOn g g' t
⊢ EqOn g g' t

Tactic:
obtain ⟨x, hxs⟩ := hs
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : α
hxs : x_1 ∈ s
x : β
hxt : x ∈ t
⊢ Prod.map f g (x_1, x) = Prod.map f' g' (x_1, x)

Tactic:
have h' := h <| mk_mem_prod hxs hxt
-- Module: Mathlib.Data.Set.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x_1 : α
hxs : x_1 ∈ s
x : β
hxt : x ∈ t
h' : Prod.map f g (x_1, x) = Prod.map f' g' (x_1, x)
⊢ g x = g' x

Tactic:
grind