-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem mulAntidiagonal_min_mul_min {α} [LinearOrderedCancelCommMonoid α] {s t : Set α}
    (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
    mulAntidiagonal hs.isPWO ht.isPWO (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}

Proof state:
case h.mk
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ (a, b) ∈ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}

Tactic:
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]

Result:
case h.mk
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt ↔ a = hs.min hns ∧ b = ht.min hnt

Proof state:
case h.mk.mp
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

Tactic:
rintro ⟨has, hat, hst⟩

Result:
case h.mk.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = hs.min hns * ht.min hnt
⊢ a = hs.min hns ∧ b = ht.min hnt

Proof state:
case h.mk
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt ↔ a = hs.min hns ∧ b = ht.min hnt

Tactic:
constructor

Result:
case h.mk.mp
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

case h.mk.mpr
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt

Proof state:
case h.mk.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = hs.min hns * ht.min hnt
⊢ a = hs.min hns ∧ b = ht.min hnt

Tactic:
obtain rfl :=
  (hs.min_le hns has).eq_of_not_lt fun hlt =>
    (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst

Result:
case h.mk.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : α
hat : b ∈ t
has : hs.min hns ∈ s
hst : hs.min hns * b = hs.min hns * ht.min hnt
⊢ hs.min hns = hs.min hns ∧ b = ht.min hnt

Proof state:
case h.mk.mpr.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min hns ∈ s ∧ ht.min hnt ∈ t ∧ hs.min hns * ht.min hnt = hs.min hns * ht.min hnt

Tactic:
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩

Result:
no goals

Proof state:
case h.mk.mp.intro.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : α
hat : b ∈ t
has : hs.min hns ∈ s
hst : hs.min hns * b = hs.min hns * ht.min hnt
⊢ hs.min hns = hs.min hns ∧ b = ht.min hnt

Tactic:
exact ⟨rfl, mul_left_cancel hst⟩

Result:
no goals

Proof state:
case h.mk.mpr
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case h.mk.mpr.intro
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min hns ∈ s ∧ ht.min hnt ∈ t ∧ hs.min hns * ht.min hnt = hs.min hns * ht.min hnt

Proof state:
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ (a, b) ∈ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}