α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑x).fst * (↑x).snd
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑y).fst * (↑x).snd
rw [← h]
no goals
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑x).fst * (↑x).snd
exact x.2.2.2.symm
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑x).snd
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑y).snd
rw [← h]
no goals
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑x).snd
exact x.2.2.2.symm