-- Mathlib/Data/Finset/SMulAntidiagonal.lean
theorem support_smulAntidiagonal_subset_smul {hs : s.IsPWO} {ht : t.IsPWO} :
    { a | (SMulAntidiagonal hs ht a).Nonempty } ⊆ (s • t) :=
  fun a ⟨b, hb⟩ => by
  rw [mem_smulAntidiagonal] at hb
  rw [Set.mem_smul]
  use b.1
  refine { left := hb.1, right := ?_ }
  use b.2
  exact { left := hb.2.1, right := hb.2.2 }

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b ∈ SMulAntidiagonal hs ht a
⊢ a ∈ s • t

Tactic:
rw [mem_smulAntidiagonal] at hb

Result:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ a ∈ s • t

Proof state:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ b.1 ∈ s ∧ ∃ y ∈ t, b.1 • y = a

Tactic:
refine { left := hb.1, right := ?_ }

Result:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ ∃ y ∈ t, b.1 • y = a

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ a ∈ s • t

Tactic:
rw [Set.mem_smul]

Result:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ ∃ x ∈ s, ∃ y ∈ t, x • y = a

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ ∃ x ∈ s, ∃ y ∈ t, x • y = a

Tactic:
use b.1

Result:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ b.1 ∈ s ∧ ∃ y ∈ t, b.1 • y = a

Proof state:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ b.2 ∈ t ∧ b.1 • b.2 = a

Tactic:
exact { left := hb.2.1, right := hb.2.2 }

Result:
no goals

Proof state:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ ∃ y ∈ t, b.1 • y = a

Tactic:
use b.2

Result:
case h
G : Type u_1
P : Type u_2
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsPWO
ht : t.IsPWO
a : P
x✝ : a ∈ {a | (SMulAntidiagonal hs ht a).Nonempty}
b : G × P
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 • b.2 = a
⊢ b.2 ∈ t ∧ b.1 • b.2 = a