F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ MulSalemSpencer {b} ∧
    (∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → a * b_1 = c * c → a = b_1) ∧
      ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → b_1 * c = a * a → b_1 = c
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ MulSalemSpencer {a, b}
rw [mulSalemSpencer_insert]
case refine'_1
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → a * b_1 = c * c → a = b_1

case refine'_2
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → b_1 * c = a * a → b_1 = c
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ MulSalemSpencer {b} ∧
    (∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → a * b_1 = c * c → a = b_1) ∧
      ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → b_1 * c = a * a → b_1 = c
refine' ⟨mulSalemSpencer_singleton _, _, _⟩
case refine'_1
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a d : α
⊢ a * d = d * d → a = d
case refine'_1
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → a * b_1 = c * c → a = b_1
rintro c d (rfl : c = b) (rfl : d = c)
no goals
case refine'_1
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a d : α
⊢ a * d = d * d → a = d
exact mul_right_cancel
case refine'_2
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝¹ a d : α
a✝ : d * d = a * a
⊢ d = d
case refine'_2
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → b_1 * c = a * a → b_1 = c
rintro c d (rfl : c = b) (rfl : d = c) _
no goals
case refine'_2
F : Type ?u.75150
α : Type u_1
β : Type ?u.75156
𝕜 : Type ?u.75159
E : Type ?u.75162
inst✝ : CancelCommMonoid α
s : Set α
a✝¹ a d : α
a✝ : d * d = a * a
⊢ d = d
rfl