F : Type ?u.90423
α : Type u_1
β : Type ?u.90429
𝕜 : Type ?u.90432
E : Type ?u.90435
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ (i : α), i ∈ s → i < 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 s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
F : Type ?u.90423
α : Type u_1
β : Type ?u.90429
𝕜 : Type ?u.90432
E : Type ?u.90435
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ (i : α), i ∈ s → i < a
⊢ MulSalemSpencer (insert a s) ↔ MulSalemSpencer s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
refine' mulSalemSpencer_insert.trans _
F : Type ?u.90423
α : Type u_1
β : Type ?u.90429
𝕜 : Type ?u.90432
E : Type ?u.90435
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ (i : α), i ∈ s → i < 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 s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
F : Type ?u.90423
α : Type u_1
β : Type ?u.90429
𝕜 : Type ?u.90432
E : Type ?u.90435
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ (i : α), i ∈ s → i < 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 s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
rw [← and_assoc]
no goals
F : Type ?u.90423
α : Type u_1
β : Type ?u.90429
𝕜 : Type ?u.90432
E : Type ?u.90435
inst✝ : OrderedCancelCommMonoid α
s : Set α
a : α
hs : ∀ (i : α), i ∈ s → i < 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 s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b
exact and_iff_left fun b c hb hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim