English
If t is nonempty, then s × t = s1 × t iff s = s1 ∧ t = t1 or a related emptiness pattern.
Русский
Если t непусто, то равенство произведений имеет форму: s = s1 ∧ t = t1 или другая комбинация пустоты.
LaTeX
$$$ s \times t = s_1 \times t_1 \iff (s = s_1 \land t = t_1) \lor ( (s = \emptyset \lor t = \emptyset) \land (s_1 = \emptyset \lor t_1 = \emptyset) ) $$$
Lean4
theorem prod_eq_prod_iff : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) :=
by
symm
rcases eq_empty_or_nonempty (s ×ˢ t) with h | h
· simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and, or_iff_right_iff_imp]
rintro ⟨rfl, rfl⟩
exact prod_eq_empty_iff.mp h
rw [prod_eq_prod_iff_of_nonempty h]
rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h
simp_rw [h, false_and, or_false]
