[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
⊢ MeasurableSet univᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet t
[PROOFSTEP]
rwa [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ (b : ι), f b)
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ (b : ι), f b)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ (b : ι), f b)
[PROOFSTEP]
rcases exists_surjective_nat ι with ⟨e, he⟩
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (b : ι), f b)
[PROOFSTEP]
rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ (x : ℕ), f (e x))
[PROOFSTEP]
exact m.measurableSet_iUnion _ fun _ => h _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ s), f b)
[PROOFSTEP]
rw [biUnion_eq_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
[PROOFSTEP]
have := hs.to_subtype
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ (x : ↑s), f ↑x)
[PROOFSTEP]
exact MeasurableSet.iUnion (by simpa using h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
this : Countable ↑s
⊢ ∀ (b : ↑s), MeasurableSet (f ↑b)
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋃₀ s)
[PROOFSTEP]
rw [sUnion_eq_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋃ (i : Set α) (_ : i ∈ s), i)
[PROOFSTEP]
exact .biUnion hs h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋂ (b : ι), f b)ᶜ
[PROOFSTEP]
rw [compl_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ (i : ι), (f i)ᶜ)
[PROOFSTEP]
exact .iUnion fun b => (h b).compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋂ (b : β) (_ : b ∈ s), f b)ᶜ
[PROOFSTEP]
rw [compl_iInter₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : Set.Countable s
h : ∀ (b : β), b ∈ s → MeasurableSet (f b)
⊢ MeasurableSet (⋃ (i : β) (_ : i ∈ s), (f i)ᶜ)
[PROOFSTEP]
exact .biUnion hs fun b hb => (h b hb).compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋂₀ s)
[PROOFSTEP]
rw [sInter_eq_biInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : MeasurableSpace α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → MeasurableSet t
⊢ MeasurableSet (⋂ (i : Set α) (_ : i ∈ s), i)
[PROOFSTEP]
exact MeasurableSet.biInter hs h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∪ s₂)
[PROOFSTEP]
rw [union_eq_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ (b : Bool), bif b then s₁ else s₂)
[PROOFSTEP]
exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)
[PROOFSTEP]
rw [inter_eq_compl_compl_union_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
[PROOFSTEP]
exact (h₁.compl.union h₂.compl).compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
⊢ MeasurableSet (if p then s else t)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t✝ u : Set α
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t
[PROOFSTEP]
exacts [hs h, ht h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
i : Bool
⊢ MeasurableSet (bif i then s₁ else s₂)
[PROOFSTEP]
cases i
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif false then s₁ else s₂)
case true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (bif true then s₁ else s₂)
[PROOFSTEP]
exacts [h₂, h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet {_a | p}
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet {_a | p}
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Prop
h : p
⊢ MeasurableSet {_a | p}
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Prop
h : ¬p
⊢ MeasurableSet {_a | p}
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
MeasurableSet'✝¹ : Set α → Prop
measurableSet_empty✝¹ : MeasurableSet'✝¹ ∅
measurableSet_compl✝¹ : ∀ (s : Set α), MeasurableSet'✝¹ s → MeasurableSet'✝¹ sᶜ
measurableSet_iUnion✝¹ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝¹ (f i)) → MeasurableSet'✝¹ (⋃ (i : ℕ), f i)
MeasurableSet'✝ : Set α → Prop
measurableSet_empty✝ : MeasurableSet'✝ ∅
measurableSet_compl✝ : ∀ (s : Set α), MeasurableSet'✝ s → MeasurableSet'✝ sᶜ
measurableSet_iUnion✝ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝ (f i)) → MeasurableSet'✝ (⋃ (i : ℕ), f i)
x✝ : MeasurableSet = MeasurableSet
⊢ { MeasurableSet' := MeasurableSet'✝¹, measurableSet_empty := measurableSet_empty✝¹,
      measurableSet_compl := measurableSet_compl✝¹, measurableSet_iUnion := measurableSet_iUnion✝¹ } =
    { MeasurableSet' := MeasurableSet'✝, measurableSet_empty := measurableSet_empty✝,
      measurableSet_compl := measurableSet_compl✝, measurableSet_iUnion := measurableSet_iUnion✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet s
[PROOFSTEP]
rwa [← insert_eq_of_mem ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Countable s
⊢ MeasurableSet s
[PROOFSTEP]
rw [← biUnion_of_singleton s]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Countable s
⊢ MeasurableSet (⋃ (x : α) (_ : x ∈ s), {x})
[PROOFSTEP]
exact .biUnion hs fun b _ => .singleton b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ p ∅
[PROOFSTEP]
simpa only [h] using m.measurableSet_empty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ ∀ (s : Set α), p s → p sᶜ
[PROOFSTEP]
simpa only [h] using m.measurableSet_compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ ∀ (f : ℕ → Set α), (∀ (i : ℕ), p (f i)) → p (⋃ (i : ℕ), f i)
[PROOFSTEP]
simpa only [h] using m.measurableSet_iUnion
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p tᶜ
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
hs : MeasurableSet s
⊢ p s
[PROOFSTEP]
induction hs
[GOAL]
case basic
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p tᶜ
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s u✝ : Set α
a✝ : u✝ ∈ C
⊢ p u✝
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p tᶜ
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
⊢ p ∅
case compl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p tᶜ
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s t✝ : Set α
a✝ : GenerateMeasurable C t✝
a_ih✝ : p t✝
⊢ p t✝ᶜ
case iUnion
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
p : Set α → Prop
C : Set (Set α)
hC : ∀ (t : Set α), t ∈ C → p t
h_empty : p ∅
h_compl : ∀ (t : Set α), p t → p tᶜ
h_Union : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ (i : ℕ), f i)
s : Set α
f✝ : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable C (f✝ n)
a_ih✝ : ∀ (n : ℕ), p (f✝ n)
⊢ p (⋃ (i : ℕ), f✝ i)
[PROOFSTEP]
exacts [hC _ ‹_›, h_empty, h_compl _ ‹_›, h_Union ‹_› ‹_›]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
S : Set (Set α)
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
[PROOFSTEP]
refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
[PROOFSTEP]
apply generateFrom_induction
[GOAL]
case hC
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
⊢ ∀ (t : Set α), t ∈ S → (x ∈ t ↔ y ∈ t)
[PROOFSTEP]
exact H
[GOAL]
case h_empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅
[PROOFSTEP]
rfl
[GOAL]
case h_compl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
⊢ ∀ (t : Set α), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
[PROOFSTEP]
exact fun _ ↦ Iff.not
[GOAL]
case h_Union
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
⊢ ∀ (f : ℕ → Set α), (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → (x ∈ ⋃ (i : ℕ), f i ↔ y ∈ ⋃ (i : ℕ), f i)
[PROOFSTEP]
intro f hf
[GOAL]
case h_Union
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
S : Set (Set α)
x y : α
H : ∀ (s : Set α), s ∈ S → (x ∈ s ↔ y ∈ s)
s : Set α
f : ℕ → Set α
hf : ∀ (n : ℕ), x ∈ f n ↔ y ∈ f n
⊢ x ∈ ⋃ (i : ℕ), f i ↔ y ∈ ⋃ (i : ℕ), f i
[PROOFSTEP]
simp only [mem_iUnion, hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
⊢ ∀ (t : Set α), t ∈ {∅} → MeasurableSet t
[PROOFSTEP]
simp [@MeasurableSet.empty α ⊥]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
⊢ ∀ (t : Set α), t ∈ {univ} → MeasurableSet t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
S : Set (Set α)
⊢ generateFrom (insert univ S) = generateFrom S
[PROOFSTEP]
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S
[PROOFSTEP]
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u s : Set α
⊢ ∀ (s : Set α), (fun s => s = ∅ ∨ s = univ) s → (fun s => s = ∅ ∨ s = univ) sᶜ
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ s ∈ ⋂₀ ((fun m => {t | MeasurableSet t}) '' ms) ↔ ∀ (m : MeasurableSpace α), m ∈ ms → MeasurableSet s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort u_6
s✝ t u : Set α
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
[PROOFSTEP]
rw [iInf, measurableSet_sInf, forall_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s
[PROOFSTEP]
change GenerateMeasurable (⋃₀ _) _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s | ∃ m, m ∈ ms ∧ MeasurableSet s} s
[PROOFSTEP]
simp [← setOf_exists]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι✝ : Sort u_6
s✝ t u : Set α
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ i, MeasurableSet s} s
[PROOFSTEP]
simp only [iSup, measurableSet_sSup, exists_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : ι → MeasurableSpace α
⊢ ⨆ (n : ι), m n = generateFrom {s | ∃ n, MeasurableSet s}
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s
[PROOFSTEP]
rw [measurableSet_iSup]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s✝ t u : Set α
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
x : R
⊢ MeasurableSet (floor ⁻¹' {⌊x⌋})
[PROOFSTEP]
simpa only [Int.preimage_floor_singleton] using measurableSet_Ico
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
x : R
⊢ MeasurableSet (ceil ⁻¹' {⌈x⌉})
[PROOFSTEP]
simpa only [Int.preimage_ceil_singleton] using measurableSet_Ioc
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
⊢ Measurable Int.fract
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract ⁻¹' s)
[PROOFSTEP]
rw [Int.preimage_fract]
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ (m : ℤ), (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1))
[PROOFSTEP]
exact MeasurableSet.iUnion fun z => measurable_id.sub_const _ (hs.inter measurableSet_Ico)
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract '' s)
[PROOFSTEP]
simp only [Int.image_fract, sub_eq_add_neg, image_add_right']
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ (m : ℤ), (fun x => x + ↑m) ⁻¹' s ∩ Ico 0 1)
[PROOFSTEP]
exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
⊢ MeasurableSet (floor ⁻¹' {⌊n⌋₊})
[PROOFSTEP]
cases' eq_or_ne ⌊n⌋₊ 0 with h h
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
h : ⌊n⌋₊ = 0
⊢ MeasurableSet (floor ⁻¹' {⌊n⌋₊})
[PROOFSTEP]
simp_all [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
h : ⌊n⌋₊ ≠ 0
⊢ MeasurableSet (floor ⁻¹' {⌊n⌋₊})
[PROOFSTEP]
simp_all [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]
[GOAL]
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})
[PROOFSTEP]
cases' eq_or_ne ⌈n⌉₊ 0 with h h
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
h : ⌈n⌉₊ = 0
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})
[PROOFSTEP]
simp_all [h, Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : LinearOrderedSemiring R
inst✝⁴ : FloorSemiring R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
f : α → R
n : R
h : ⌈n⌉₊ ≠ 0
⊢ MeasurableSet (ceil ⁻¹' {⌈n⌉₊})
[PROOFSTEP]
simp_all [h, Nat.preimage_ceil_of_ne_zero, -ceil_eq_zero]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
⊢ MulSalemSpencer (↑f '' s)
[PROOFSTEP]
rintro _ _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ habc
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a✝ : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : ↑f a * ↑f b = ↑f c * ↑f c
⊢ ↑f a = ↑f b
[PROOFSTEP]
rw [h ha hb hc (hf (mul_mem_mul ha hb) (mul_mem_mul hc hc) <| by rwa [map_mul, map_mul])]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
s : Set α
a✝ : α
inst✝ : MulHomClass F α β
f : F
hf : InjOn (↑f) (s * s)
h : MulSalemSpencer s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : ↑f a * ↑f b = ↑f c * ↑f c
⊢ ↑f (a * b) = ↑f (c * c)
[PROOFSTEP]
rwa [map_mul, map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
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)⟩,
    _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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)
[PROOFSTEP]
rintro ⟨hs, ha, ha'⟩ b c d hb hc hd h
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
rw [mem_insert_iff] at hb hc hd
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
obtain rfl | hb := hb
[GOAL]
case intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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 = b ∨ c ∈ s
hd : d = b ∨ d ∈ s
⊢ b = c
[PROOFSTEP]
obtain rfl | hc := hc
[GOAL]
case intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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 : α
hc : c = a ∨ c ∈ s
hd : d = a ∨ d ∈ s
h : b * c = d * d
hb : b ∈ s
⊢ b = c
[PROOFSTEP]
obtain rfl | hc := hc
[GOAL]
case intro.intro.inl.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.inl.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
all_goals obtain rfl | hd := hd
[GOAL]
case intro.intro.inl.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
obtain rfl | hd := hd
[GOAL]
case intro.intro.inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
obtain rfl | hd := hd
[GOAL]
case intro.intro.inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
obtain rfl | hd := hd
[GOAL]
case intro.intro.inl.inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact (mul_left_cancel h).symm
[GOAL]
case intro.intro.inl.inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact ha hc hd h
[GOAL]
case intro.intro.inr.inl.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact mul_right_cancel h
[GOAL]
case intro.intro.inr.inl.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact (ha hb hd <| (mul_comm _ _).trans h).symm
[GOAL]
case intro.intro.inr.inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact ha' hb hc h
[GOAL]
case intro.intro.inr.inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact hs hb hc hd h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ MulSalemSpencer {a, b}
[PROOFSTEP]
rw [mulSalemSpencer_insert]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
refine' ⟨mulSalemSpencer_singleton _, _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → a * b_1 = c * c → a = b_1
[PROOFSTEP]
rintro c d (rfl : c = b) (rfl : d = c)
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a✝ a d : α
⊢ a * d = d * d → a = d
[PROOFSTEP]
exact mul_right_cancel
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a✝ a b : α
⊢ ∀ ⦃b_1 c : α⦄, b_1 ∈ {b} → c ∈ {b} → b_1 * c = a * a → b_1 = c
[PROOFSTEP]
rintro c d (rfl : c = b) (rfl : d = c) _
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a✝¹ a d : α
a✝ : d * d = a * a
⊢ d = d
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
⊢ MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
[PROOFSTEP]
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x x_1 => x * x_1) a b * (fun x x_1 => x * x_1) a c = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [mul_mul_mul_comm, mul_mul_mul_comm a d] at h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : a * a * (b * c) = a * a * (d * d)
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [hs hb hc hd (mul_left_cancel h)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
⊢ MulSalemSpencer ((fun x => x * a) '' s)
[PROOFSTEP]
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => x * a) b * (fun x => x * a) c = (fun x => x * a) d * (fun x => x * a) d
⊢ (fun x => x * a) b = (fun x => x * a) c
[PROOFSTEP]
rw [mul_mul_mul_comm, mul_mul_mul_comm d] at h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * c * (a * a) = d * d * (a * a)
⊢ (fun x => x * a) b = (fun x => x * a) c
[PROOFSTEP]
rw [hs hb hc hd (mul_right_cancel h)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ a * b * (a * c) = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
[PROOFSTEP]
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : MulSalemSpencer ((fun x => x * a) '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ b * a * (c * a) = d * a * (d * a)
[PROOFSTEP]
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
refine' mulSalemSpencer_insert.trans _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
rw [← and_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
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
[PROOFSTEP]
exact and_iff_left fun b c hb hc h => ((mul_lt_mul_of_lt_of_lt (hs _ hb) (hs _ hc)).ne h).elim
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
⊢ MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
[PROOFSTEP]
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x x_1 => x * x_1) a b * (fun x x_1 => x * x_1) a c = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [mul_mul_mul_comm, mul_mul_mul_comm a d] at h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : a * a * (b * c) = a * a * (d * d)
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
[PROOFSTEP]
rw [hs hb hc hd (mul_left_cancel₀ (mul_ne_zero ha ha) h)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
⊢ MulSalemSpencer ((fun x => x * a) '' s)
[PROOFSTEP]
rintro _ _ _ ⟨b, hb, rfl⟩ ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩ h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => x * a) b * (fun x => x * a) c = (fun x => x * a) d * (fun x => x * a) d
⊢ (fun x => x * a) b = (fun x => x * a) c
[PROOFSTEP]
rw [mul_mul_mul_comm, mul_mul_mul_comm d] at h
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : MulSalemSpencer s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * c * (a * a) = d * d * (a * a)
⊢ (fun x => x * a) b = (fun x => x * a) c
[PROOFSTEP]
rw [hs hb hc hd (mul_right_cancel₀ (mul_ne_zero ha ha) h)]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ a * b * (a * c) = (fun x x_1 => x * x_1) a d * (fun x x_1 => x * x_1) a d
[PROOFSTEP]
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : MulSalemSpencer ((fun x => x * a) '' s)
b c d : α
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
h : b * c = d * d
⊢ b * a * (c * a) = d * a * (d * a)
[PROOFSTEP]
rw [mul_mul_mul_comm, h, mul_mul_mul_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
⊢ AddSalemSpencer s ↔ ∀ ⦃a b c : ℕ⦄, a ∈ s → b ∈ s → c ∈ s → a + b = c + c → a = c
[PROOFSTEP]
refine' forall₄_congr fun a b c _ => forall₃_congr fun _ _ habc => ⟨_, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = b → a = c
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : a + a = c + c
⊢ a = c
[PROOFSTEP]
simp_rw [← two_mul] at habc
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
a c : ℕ
x✝² : a ∈ s
x✝¹ : c ∈ s
x✝ : a ∈ s
habc : 2 * a = 2 * c
⊢ a = c
[PROOFSTEP]
exact mul_left_cancel₀ two_ne_zero habc
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
a b c : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : c ∈ s
habc : a + b = c + c
⊢ a = c → a = b
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Set ℕ
a b : ℕ
x✝² : a ∈ s
x✝¹ : b ∈ s
x✝ : a ∈ s
habc : a + b = a + a
⊢ a = b
[PROOFSTEP]
exact (add_left_cancel habc).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
⊢ AddSalemSpencer (frontier s)
[PROOFSTEP]
intro a b c ha hb hc habc
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a b c : E
ha : a ∈ frontier s
hb : b ∈ frontier s
hc : c ∈ frontier s
habc : a + b = c + c
⊢ a = b
[PROOFSTEP]
obtain rfl : (1 / 2 : 𝕜) • a + (1 / 2 : 𝕜) • b = c := by
  rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by norm_num), two_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a b c : E
ha : a ∈ frontier s
hb : b ∈ frontier s
hc : c ∈ frontier s
habc : a + b = c + c
⊢ (1 / 2) • a + (1 / 2) • b = c
[PROOFSTEP]
rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by norm_num), two_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a b c : E
ha : a ∈ frontier s
hb : b ∈ frontier s
hc : c ∈ frontier s
habc : a + b = c + c
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a b : E
ha : a ∈ frontier s
hb : b ∈ frontier s
hc : (1 / 2) • a + (1 / 2) • b ∈ frontier s
habc : a + b = (1 / 2) • a + (1 / 2) • b + ((1 / 2) • a + (1 / 2) • b)
⊢ a = b
[PROOFSTEP]
exact hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hb) one_half_pos one_half_pos (add_halves _) hc.2
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
⊢ AddSalemSpencer (sphere x r)
[PROOFSTEP]
obtain rfl | hr := eq_or_ne r 0
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer (sphere x 0)
[PROOFSTEP]
rw [sphere_zero]
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ AddSalemSpencer {x}
[PROOFSTEP]
exact addSalemSpencer_singleton _
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ AddSalemSpencer (sphere x r)
[PROOFSTEP]
convert addSalemSpencer_frontier isClosed_ball (strictConvex_closedBall ℝ x r)
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)
[PROOFSTEP]
exact (frontier_closedBall _ hr).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ Monotone fun s => Nat.findGreatest (fun m => ∃ t x, card t = m ∧ MulSalemSpencer ↑t) (card s)
[PROOFSTEP]
rintro t u htu
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t u : Finset α
htu : t ≤ u
⊢ (fun s => Nat.findGreatest (fun m => ∃ t x, card t = m ∧ MulSalemSpencer ↑t) (card s)) t ≤
    (fun s => Nat.findGreatest (fun m => ∃ t x, card t = m ∧ MulSalemSpencer ↑t) (card s)) u
[PROOFSTEP]
refine' Nat.findGreatest_mono (fun m => _) (card_le_of_subset htu)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t u : Finset α
htu : t ≤ u
m : ℕ
⊢ (∃ t_1 x, card t_1 = m ∧ MulSalemSpencer ↑t_1) ≤ ∃ t x, card t = m ∧ MulSalemSpencer ↑t
[PROOFSTEP]
rintro ⟨v, hvt, hv⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t u : Finset α
htu : t ≤ u
m : ℕ
v : Finset α
hvt : v ⊆ t
hv : card v = m ∧ MulSalemSpencer ↑v
⊢ ∃ t x, card t = m ∧ MulSalemSpencer ↑t
[PROOFSTEP]
exact ⟨v, hvt.trans htu, hv⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ MulSalemSpencer ↑∅
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ MulSalemSpencer ∅
[PROOFSTEP]
exact mulSalemSpencer_empty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ ↑mulRothNumber {a} = 1
[PROOFSTEP]
refine' MulSalemSpencer.roth_number_eq _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer ↑{a}
[PROOFSTEP]
rw [coe_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer {a}
[PROOFSTEP]
exact mulSalemSpencer_singleton a
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : card u = ↑mulRothNumber (s ∪ t)
hu : MulSalemSpencer ↑u
⊢ card u = card (u ∩ s ∪ u ∩ t)
[PROOFSTEP]
rw [← inter_distrib_left, (inter_eq_left_iff_subset _ _).2 hus]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
[PROOFSTEP]
obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
[PROOFSTEP]
obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ ↑mulRothNumber s * ↑mulRothNumber t ≤ ↑mulRothNumber (s ×ˢ t)
[PROOFSTEP]
rw [← hucard, ← hvcard, ← card_product]
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ card (u ×ˢ v) ≤ ↑mulRothNumber (s ×ˢ t)
[PROOFSTEP]
refine' MulSalemSpencer.le_mulRothNumber _ (product_subset_product hus hvt)
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer ↑(u ×ˢ v)
[PROOFSTEP]
rw [coe_product]
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s : Finset α
t : Finset β
u : Finset α
hus : u ⊆ s
hucard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
v : Finset β
hvt : v ⊆ t
hvcard : card v = ↑mulRothNumber t
hv : MulSalemSpencer ↑v
⊢ MulSalemSpencer (↑u ×ˢ ↑v)
[PROOFSTEP]
exact hu.prod hv
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
⊢ ↑mulRothNumber s < n
[PROOFSTEP]
obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ↑mulRothNumber s < n
[PROOFSTEP]
rw [← hcard, ← not_le]
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
⊢ ¬n ≤ card t
[PROOFSTEP]
intro hn
[GOAL]
case intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ : Finset α
n : ℕ
h : ∀ (t : Finset α), t ∈ powersetLen n s → ¬MulSalemSpencer ↑t
t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
hn : n ≤ card t
⊢ False
[PROOFSTEP]
obtain ⟨u, hut, rfl⟩ := exists_smaller_set t n hn
[GOAL]
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t✝ t : Finset α
hts : t ⊆ s
hcard : card t = ↑mulRothNumber s
ht : MulSalemSpencer ↑t
u : Finset α
hut : u ⊆ t
h : ∀ (t : Finset α), t ∈ powersetLen (card u) s → ¬MulSalemSpencer ↑t
hn : card u ≤ card t
⊢ False
[PROOFSTEP]
exact h _ (mem_powersetLen.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) = ↑mulRothNumber s
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
[PROOFSTEP]
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s.map <| mulLeftEmbedding a)
[GOAL]
case refine'_1.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ map (mulLeftEmbedding a) s
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
[PROOFSTEP]
rw [subset_map_iff] at hus
[GOAL]
case refine'_1.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : ∃ u_1 x, u = map (mulLeftEmbedding a) u_1
hcard : card u = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
[PROOFSTEP]
obtain ⟨u, hus, rfl⟩ := hus
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
[PROOFSTEP]
rw [coe_map] at hu
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ ↑mulRothNumber (map (mulLeftEmbedding a) s) ≤ ↑mulRothNumber s
[PROOFSTEP]
rw [← hcard, card_map]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card (map (mulLeftEmbedding a) u) = ↑mulRothNumber (map (mulLeftEmbedding a) s)
hu : MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
⊢ card u ≤ ↑mulRothNumber s
[PROOFSTEP]
exact (mulSalemSpencer_mul_left_iff.1 hu).le_mulRothNumber hus
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
[PROOFSTEP]
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s
[GOAL]
case refine'_2.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
[PROOFSTEP]
have h : MulSalemSpencer (u.map <| mulLeftEmbedding a : Set α) :=
  by
  rw [coe_map]
  exact hu.mul_left
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
[PROOFSTEP]
rw [coe_map]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
⊢ MulSalemSpencer (↑(mulLeftEmbedding a) '' ↑u)
[PROOFSTEP]
exact hu.mul_left
[GOAL]
case refine'_2.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s ≤ ↑mulRothNumber (map (mulLeftEmbedding a) s)
[PROOFSTEP]
convert h.le_mulRothNumber (map_subset_map.2 hus) using 1
[GOAL]
case h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : card u = ↑mulRothNumber s
hu : MulSalemSpencer ↑u
h : MulSalemSpencer ↑(map (mulLeftEmbedding a) u)
⊢ ↑mulRothNumber s = card (map (mulLeftEmbedding a) u)
[PROOFSTEP]
rw [card_map, hcard]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulRightEmbedding a) s) = ↑mulRothNumber s
[PROOFSTEP]
rw [← mul_left_embedding_eq_mul_right_embedding, mulRothNumber_map_mul_left s a]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n M N : ℕ
⊢ ↑rothNumberNat (M + N) ≤ ↑rothNumberNat M + ↑rothNumberNat N
[PROOFSTEP]
simp_rw [rothNumberNat_def]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range (M + N)) ≤ ↑addRothNumber (range M) + ↑addRothNumber (range N)
[PROOFSTEP]
rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    ↑addRothNumber (range M) + ↑addRothNumber (map (addLeftEmbedding M) (range N))
[PROOFSTEP]
exact addRothNumber_union_le _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
[PROOFSTEP]
obtain h | h := le_total b a
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
h : b ≤ a
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
[PROOFSTEP]
rw [tsub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
[PROOFSTEP]
convert addRothNumber_map_add_left _ a
[GOAL]
case h.e'_2.h.e'_6
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))
[PROOFSTEP]
rw [range_eq_Ico, map_eq_image]
[GOAL]
case h.e'_2.h.e'_6
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = image (↑(addLeftEmbedding a)) (Ico 0 (b - a))
[PROOFSTEP]
convert (image_add_left_Ico 0 (b - a) _).symm
[GOAL]
case h.e'_2.h.e'_5
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)
[PROOFSTEP]
exact (add_tsub_cancel_of_le h).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
𝕜 : Type u_4
E : Type u_5
s : Finset ℕ
k n : ℕ
⊢ ∀ (x : ℕ), ‖↑(↑rothNumberNat x)‖ ≤ ‖↑x‖
[PROOFSTEP]
simpa only [Real.norm_coe_nat, Nat.cast_le] using rothNumberNat_le