case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁
intro heq
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty (s₁ ×ˢ t₁)
⊢ s = s₁ ∧ t = t₁
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty s ∧ Set.Nonempty t
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty s₁ ∧ Set.Nonempty t₁
⊢ s = s₁ ∧ t = t₁
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty (s₁ ×ˢ t₁)
⊢ s = s₁ ∧ t = t₁
rw [prod_nonempty_iff] at h h₁
no goals
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty s ∧ Set.Nonempty t
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty s₁ ∧ Set.Nonempty t₁
⊢ s = s₁ ∧ t = t₁
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and_iff, ←
  snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ Set.Nonempty (s₁ ×ˢ t₁)
rwa [← heq]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s ×ˢ t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
rintro ⟨rfl, rfl⟩
no goals
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.88331
δ : Type ?u.88334
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s ×ˢ t
rfl