internlm/Lean-Github huggingface dataset:
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
Proof state after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [hz]
Proof state after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x y
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x y
Tactic:
exact le_max_right x y
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)
Tactic:
have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
  rw [Set.eq_singleton_iff_unique_mem]
  constructor
  . simpa
  . intro x hx
    simp at hx
    exact hx.2.symm
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Tactic:
have : sSup {f z} = f z := by apply csSup_singleton
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Tactic:
simp at hx
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
have : f z ≤ x := hx z h
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : f z ≤ x
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : f z ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [hz] at this
Proof state after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : y ≤ x
⊢ y ≤ max x (sSup ∅)
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : y ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
apply le_max_of_le_left this
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (Set.range fun x => f z) = {f z}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
Proof state after:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (f z ∈ Set.range fun x => f z) ∧ ∀ x ∈ Set.range fun x => f z, x = f z
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (f z ∈ Set.range fun x => f z) ∧ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z

case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z

case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
. simpa
Proof state after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
. intro x hx
  simp at hx
  exact hx.2.symm
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z
Tactic:
simpa
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
intro x hx
Proof state after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : x ∈ Set.range fun x => f z
⊢ x = f z
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : x ∈ Set.range fun x => f z
⊢ x = f z
Tactic:
simp at hx
Proof state after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : z ∈ s ∧ f z = x
⊢ x = f z
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : z ∈ s ∧ f z = x
⊢ x = f z
Tactic:
exact hx.2.symm
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ sSup {f z} = f z
Tactic:
apply csSup_singleton
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ (Set.range fun x => f z) = ∅
Tactic:
simpa
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i
Tactic:
simp
Proof state after:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ i ∈ s ∧ f i = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ i ∈ s ∧ f i = a
Tactic:
use hi, fia
Proof state after:
no goals
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
intro x hx
Proof state after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : x ∈ Set.range fun h => f i
⊢ x = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : x ∈ Set.range fun h => f i
⊢ x = a
Tactic:
simp at hx
Proof state after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : i ∈ s ∧ f i = x
⊢ x = a
Theorem: ConditionallyCompleteLattice.le_biSup
Proof state before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : i ∈ s ∧ f i = x
⊢ x = a
Tactic:
rwa [hx.2] at fia
Proof state after:
no goals
Theorem: localOscillation_of_same
Proof state before:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ localOscillation E f f = 0
Tactic:
rw [localOscillation]
Proof state after:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ ⨆ z ∈ E ×ˢ E, ‖f z.1 - f z.1 - f z.2 + f z.2‖ = 0
Theorem: localOscillation_of_same
Proof state before:
X : Type
inst✝ : PseudoMetricSpace X
E : Set X
f : C(X, ℂ)
⊢ ⨆ z ∈ E ×ˢ E, ‖f z.1 - f z.1 - f z.2 + f z.2‖ = 0
Tactic:
simp only [Set.mem_prod, sub_self, zero_sub, add_left_neg, norm_zero, Real.ciSup_const_zero]
Proof state after:
no goals
Theorem: localOscillation_of_integer_linear
Proof state before:
x R : ℝ
R_nonneg : 0 ≤ R
⊢ ∀ (n m : ℤ), localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
intro n m
Proof state after:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
by_cases n_ne_m : n = m
Proof state after:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case pos
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|

case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
. rw [n_ne_m]
  simp
  apply localOscillation_of_same
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : ¬n = m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
push_neg at n_ne_m
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have norm_n_sub_m_pos : 0 < |(n : ℝ) - m| := by
  simp
  rwa [sub_eq_zero, Int.cast_inj]
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have norm_integer_linear_eq {n m : ℤ} {z : ℝ × ℝ} : ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ := by
  rw [←Complex.norm_real, integer_linear, integer_linear]
  congr 1
  simp
  ring
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
have localOscillation_eq : localOscillation (Metric.ball x R) (θ n) (θ m) = ⨆ z ∈ (Metric.ball x R) ×ˢ (Metric.ball x R), ‖(n - m) * (z.1 - x) - (n - m) * (z.2 - x)‖ := by
    rw [localOscillation]
    congr
    ext z
    rw [norm_integer_linear_eq]
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |↑n - ↑m|
Tactic:
rw [localOscillation_eq]
Proof state after:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ = 2 * R * |↑n - ↑m|
Theorem: localOscillation_of_integer_linear
Proof state before:
case neg
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ = 2 * R * |↑n - ↑m|
Tactic:
apply le_antisymm
Proof state after:
case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖ ≤ 2 * R * |↑n - ↑m|

case neg.a
x R : ℝ
R_nonneg : 0 ≤ R
n m : ℤ
n_ne_m : n ≠ m
norm_n_sub_m_pos : 0 < |↑n - ↑m|
norm_integer_linear_eq :
  ∀ {n m : ℤ} {z : ℝ × ℝ},
    ‖(θ n) z.1 - (θ m) z.1 - (θ n) z.2 + (θ m) z.2‖ = ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
localOscillation_eq :
  localOscillation (Metric.ball x R) (θ n) (θ m) =
    ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖
⊢ 2 * R * |↑n - ↑m| ≤ ⨆ z ∈ Metric.ball x R ×ˢ Metric.ball x R, ‖(↑n - ↑m) * (z.1 - x) - (↑n - ↑m) * (z.2 - x)‖