case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = b → a = c

case refine'_2
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = c → a = b
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
⊢ AddSalemSpencer s ↔ ∀ ⦃a b c : ℕ⦄, a ∈ s → b ∈ s → c ∈ s → a + b = c + c → a = c
refine' forall₄_congr fun a b c _ => forall₃_congr fun _ _ habc => ⟨_, _⟩
case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : a + a = c + c
⊢ a = c
case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = b → a = c
rintro rfl
case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : 2 * a = 2 * c
⊢ a = c
case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : a + a = c + c
⊢ a = c
simp_rw [← two_mul] at habc
no goals
case refine'_1
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : 2 * a = 2 * c
⊢ a = c
exact mul_left_cancel₀ two_ne_zero habc
case refine'_2
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : a ∈ s
habc : a + b = a + a
⊢ a = b
case refine'_2
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = c → a = b
rintro rfl
no goals
case refine'_2
F : Type ?u.109851
α : Type ?u.109854
β : Type ?u.109857
𝕜 : Type ?u.109860
E : Type ?u.109863
s : Set ℕ
a b : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : a ∈ s
habc : a + b = a + a
⊢ a = b
exact (add_left_cancel habc).symm