-- Mathlib/Data/Finset/SMulAntidiagonal.lean
theorem smulAntidiagonal_min_smul_min [LinearOrder G] [LinearOrder P] [SMul G P]
    [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty)
    (hnt : t.Nonempty) :
    SMulAntidiagonal hs.isPWO ht.isPWO (hs.min hns • ht.min hnt) = {(hs.min hns, ht.min hnt)}

Proof state:
case h.mk.mp.intro.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : P
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, IsCancelSMul.left_cancel _ _ _ hst⟩

Result:
no goals

Proof state:
case h.mk.mpr
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ 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
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
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:
case h.mk.mp
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ 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
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
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.mpr.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
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
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ (a, b) ∈ SMulAntidiagonal ⋯ ⋯ (hs.min hns • ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}

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

Result:
case h.mk
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ 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.intro.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
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 =>
    (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst

Result:
case h.mk.mp.intro.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : P
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:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ SMulAntidiagonal ⋯ ⋯ (hs.min hns • ht.min hnt) = {(hs.min hns, ht.min hnt)}

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ (a, b) ∈ SMulAntidiagonal ⋯ ⋯ (hs.min hns • ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}

Proof state:
case h.mk
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ 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
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

case h.mk.mpr
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt