F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
⊢ (MulSalemSpencer s ∧
      (∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b) ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c) →
    MulSalemSpencer (insert a s)
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
⊢ MulSalemSpencer (insert a s) ↔
    MulSalemSpencer s ∧
      (∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b) ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
refine' ⟨fun hs => ⟨hs.mono (subset_insert _ _),
  fun b c hb hc => hs (Or.inl rfl) (Or.inr hb) (Or.inr hc),
  fun b c hb hc => hs (Or.inr hb) (Or.inr hc) (Or.inl rfl)⟩, _⟩
case intro.intro
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hb : b ∈ insert a s
hc : c ∈ insert a s
hd : d ∈ insert a s
h : b * c = d * d
⊢ b = c
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
⊢ (MulSalemSpencer s ∧
      (∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b) ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c) →
    MulSalemSpencer (insert a s)
rintro ⟨hs, ha, ha'⟩ b c d hb hc hd h
case intro.intro
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hb : b = a ∨ b ∈ s
hc : c = a ∨ c ∈ s
hd : d = a ∨ d ∈ s
h : b * c = d * d
⊢ b = c
case intro.intro
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hb : b ∈ insert a s
hc : c ∈ insert a s
hd : d ∈ insert a s
h : b * c = d * d
⊢ b = c
rw [mem_insert_iff] at hb hc hd
case intro.intro.inl.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
c d : α
h : c * c = d * d
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d = c ∨ d ∈ s
⊢ c = c

case intro.intro.inl.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
ha : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b * b_1 = c * c → b = b_1
ha' : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b_1 * c = b * b → b_1 = c
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c

case intro.intro.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d = c ∨ d ∈ s
⊢ b = c

case intro.intro.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hd : d = a ∨ d ∈ s
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
⊢ b = c
case intro.intro
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hb : b = a ∨ b ∈ s
hc : c = a ∨ c ∈ s
hd : d = a ∨ d ∈ s
h : b * c = d * d
⊢ b = c
obtain rfl | hb := hb <;> obtain rfl | hc := hc
case intro.intro.inl.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
c d : α
hc : c ∈ s
h : d * c = d * d
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ d = c

case intro.intro.inl.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
ha : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b * b_1 = c * c → b = b_1
ha' : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b_1 * c = b * b → b_1 = c
hc : c ∈ s
hd : d ∈ s
⊢ b = c

case intro.intro.inr.inl.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ b = d

case intro.intro.inr.inl.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d ∈ s
⊢ b = c

case intro.intro.inr.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ b = c

case intro.intro.inr.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
case intro.intro.inl.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
ha : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b * b_1 = c * c → b = b_1
ha' : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b_1 * c = b * b → b_1 = c
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c

case intro.intro.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d = c ∨ d ∈ s
⊢ b = c

case intro.intro.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hd : d = a ∨ d ∈ s
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
⊢ b = c
all_goals obtain rfl | hd := hd
no goals
case intro.intro.inl.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
c d : α
h : c * c = d * d
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d = c ∨ d ∈ s
⊢ c = c
rfl
case intro.intro.inr.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ b = c

case intro.intro.inr.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
case intro.intro.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
hd : d = a ∨ d ∈ s
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
⊢ b = c
obtain rfl | hd := hd
no goals
case intro.intro.inl.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
c d : α
hc : c ∈ s
h : d * c = d * d
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ d = c
exact (mul_left_cancel h).symm
no goals
case intro.intro.inl.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
ha : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b * b_1 = c * c → b = b_1
ha' : ∀ ⦃b_1 c : α⦄, b_1 ∈ s → c ∈ s → b_1 * c = b * b → b_1 = c
hc : c ∈ s
hd : d ∈ s
⊢ b = c
exact ha hc hd h
no goals
case intro.intro.inr.inl.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ b = d
exact mul_right_cancel h
no goals
case intro.intro.inr.inl.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
ha : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → c * b = c_1 * c_1 → c = b
ha' : ∀ ⦃b c_1 : α⦄, b ∈ s → c_1 ∈ s → b * c_1 = c * c → b = c_1
hd : d ∈ s
⊢ b = c
exact (ha hb hd <| (mul_comm _ _).trans h).symm
no goals
case intro.intro.inr.inr.inl
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
hs : MulSalemSpencer s
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → d * b = c * c → d = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = d * d → b = c
⊢ b = c
exact ha' hb hc h
no goals
case intro.intro.inr.inr.inr
F : Type ?u.68556
α : Type u_1
β : Type ?u.68562
𝕜 : Type ?u.68565
E : Type ?u.68568
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
ha : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
ha' : ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → b * c = a * a → b = c
b c d : α
h : b * c = d * d
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
exact hs hb hc hd h