internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_surj
Proof state before:
case inr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ s.potential c z ≤ s.potential c w
Tactic:
apply zm
Proof state after:
case inr.a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ w ∈ u
Theorem: Super.ray_surj
Proof state before:
case inr.a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ w ∈ u
Tactic:
simp only [mem_diff, mem_setOf, u]
Proof state after:
case inr.a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ s.potential c w ≤ p1 ∧ w ∉ i
Theorem: Super.ray_surj
Proof state before:
case inr.a
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ s.potential c w ≤ p1 ∧ w ∉ i
Tactic:
use lt.le, m
Proof state after:
no goals
Theorem: Super.ray_bij
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ BijOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post
Tactic:
refine ⟨fun _ m ↦ s.ray_post m, ?_, ?_⟩
Proof state after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ InjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext

case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ SurjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post
Theorem: Super.ray_bij
Proof state before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ InjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext
Tactic:
intro ⟨c0, x0⟩ m0 ⟨c1, x1⟩ m1 e
Proof state after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : (fun y => (y.1, s.ray y.1 y.2)) (c0, x0) = (fun y => (y.1, s.ray y.1 y.2)) (c1, x1)
⊢ (c0, x0) = (c1, x1)
Theorem: Super.ray_bij
Proof state before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : (fun y => (y.1, s.ray y.1 y.2)) (c0, x0) = (fun y => (y.1, s.ray y.1 y.2)) (c1, x1)
⊢ (c0, x0) = (c1, x1)
Tactic:
simp only [Prod.ext_iff] at e ⊢
Proof state after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : c0 = c1 ∧ s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Theorem: Super.ray_bij
Proof state before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
e : c0 = c1 ∧ s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
rcases e with ⟨ec, ex⟩
Proof state after:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Theorem: Super.ray_bij
Proof state before:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 : ℂ
m0 : (c0, x0) ∈ s.ext
c1 x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c0 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
rw [ec] at m0 ex
Proof state after:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 c1 : ℂ
m0 : (c1, x0) ∈ s.ext
x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c1 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Theorem: Super.ray_bij
Proof state before:
case refine_1.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c0 x0 c1 : ℂ
m0 : (c1, x0) ∈ s.ext
x1 : ℂ
m1 : (c1, x1) ∈ s.ext
ec : c0 = c1
ex : s.ray c1 x0 = s.ray c1 x1
⊢ c0 = c1 ∧ x0 = x1
Tactic:
use ec, s.ray_inj m0 m1 ex
Proof state after:
no goals
Theorem: Super.ray_bij
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ SurjOn (fun y => (y.1, s.ray y.1 y.2)) s.ext s.post
Tactic:
intro ⟨c, x⟩ m
Proof state after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ (c, x) ∈ (fun y => (y.1, s.ray y.1 y.2)) '' s.ext
Theorem: Super.ray_bij
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ (c, x) ∈ (fun y => (y.1, s.ray y.1 y.2)) '' s.ext
Tactic:
simp only [mem_image, Prod.ext_iff]
Proof state after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ ∃ x_1 ∈ s.ext, x_1.1 = c ∧ s.ray x_1.1 x_1.2 = x
Theorem: Super.ray_bij
Proof state before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x : S
m : (c, x) ∈ s.post
⊢ ∃ x_1 ∈ s.ext, x_1.1 = c ∧ s.ray x_1.1 x_1.2 = x
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
Proof state after:
case refine_2.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x✝ : S
m✝ : (c, x✝) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = x✝
⊢ ∃ x ∈ s.ext, x.1 = c ∧ s.ray x.1 x.2 = x✝
Theorem: Super.ray_bij
Proof state before:
case refine_2.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
x✝ : S
m✝ : (c, x✝) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = x✝
⊢ ∃ x ∈ s.ext, x.1 = c ∧ s.ray x.1 x.2 = x✝
Tactic:
use⟨c, x⟩, m, rfl, e
Proof state after:
no goals
Theorem: Color.ext_iff
Proof state before:
α β : Type
x y : Color α
⊢ x = y ↔ x.r = y.r ∧ x.g = y.g ∧ x.b = y.b ∧ x.a = y.a
Tactic:
induction x
Proof state after:
case mk
α β : Type
y : Color α
r✝ g✝ b✝ a✝ : α
⊢ { r := r✝, g := g✝, b := b✝, a := a✝ } = y ↔
    { r := r✝, g := g✝, b := b✝, a := a✝ }.r = y.r ∧
      { r := r✝, g := g✝, b := b✝, a := a✝ }.g = y.g ∧
        { r := r✝, g := g✝, b := b✝, a := a✝ }.b = y.b ∧ { r := r✝, g := g✝, b := b✝, a := a✝ }.a = y.a
Theorem: Color.ext_iff
Proof state before:
case mk
α β : Type
y : Color α
r✝ g✝ b✝ a✝ : α
⊢ { r := r✝, g := g✝, b := b✝, a := a✝ } = y ↔
    { r := r✝, g := g✝, b := b✝, a := a✝ }.r = y.r ∧
      { r := r✝, g := g✝, b := b✝, a := a✝ }.g = y.g ∧
        { r := r✝, g := g✝, b := b✝, a := a✝ }.b = y.b ∧ { r := r✝, g := g✝, b := b✝, a := a✝ }.a = y.a
Tactic:
induction y
Proof state after:
case mk.mk
α β : Type
r✝¹ g✝¹ b✝¹ a✝¹ r✝ g✝ b✝ a✝ : α
⊢ { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ } = { r := r✝, g := g✝, b := b✝, a := a✝ } ↔
    { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.r = { r := r✝, g := g✝, b := b✝, a := a✝ }.r ∧
      { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.g = { r := r✝, g := g✝, b := b✝, a := a✝ }.g ∧
        { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.b = { r := r✝, g := g✝, b := b✝, a := a✝ }.b ∧
          { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.a = { r := r✝, g := g✝, b := b✝, a := a✝ }.a
Theorem: Color.ext_iff
Proof state before:
case mk.mk
α β : Type
r✝¹ g✝¹ b✝¹ a✝¹ r✝ g✝ b✝ a✝ : α
⊢ { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ } = { r := r✝, g := g✝, b := b✝, a := a✝ } ↔
    { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.r = { r := r✝, g := g✝, b := b✝, a := a✝ }.r ∧
      { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.g = { r := r✝, g := g✝, b := b✝, a := a✝ }.g ∧
        { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.b = { r := r✝, g := g✝, b := b✝, a := a✝ }.b ∧
          { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.a = { r := r✝, g := g✝, b := b✝, a := a✝ }.a
Tactic:
simp only [mk.injEq]
Proof state after:
no goals
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : v.unquantize ≠ nan
⊢ v.unquantize.val = ↑v.toNat / 256 + 1 / 512
Tactic:
rw [unquantize] at n ⊢
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
have lt : 2 * v.toNat + 1 < 2^63 := by have h := v.toNat_lt; norm_num only at h ⊢; omega
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
have e9 : ((-9 : Int64) : ℤ) = -9 := by decide
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ ((Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9)).val = ↑v.toNat / 256 + 1 / 512
Tactic:
simp only [Floating.val_scaleB n, Floating.val_ofNat' lt, e9, Nat.cast_add, Nat.cast_mul,
  Nat.cast_ofNat, Nat.cast_one, Int.reduceNeg, zpow_neg, add_mul, one_mul, one_div]
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ 2 * ↑v.toNat * (2 ^ 9)⁻¹ + (2 ^ 9)⁻¹ = ↑v.toNat / 256 + 512⁻¹
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
e9 : ↑(-9) = -9
⊢ 2 * ↑v.toNat * (2 ^ 9)⁻¹ + (2 ^ 9)⁻¹ = ↑v.toNat / 256 + 512⁻¹
Tactic:
ring_nf
Proof state after:
no goals
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
⊢ 2 * v.toNat + 1 < 2 ^ 63
Tactic:
have h := v.toNat_lt
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 2 ^ 8
⊢ 2 * v.toNat + 1 < 2 ^ 63
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 2 ^ 8
⊢ 2 * v.toNat + 1 < 2 ^ 63
Tactic:
norm_num only at h ⊢
Proof state after:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 256
⊢ 2 * v.toNat + 1 < 9223372036854775808
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
h : v.toNat < 256
⊢ 2 * v.toNat + 1 < 9223372036854775808
Tactic:
omega
Proof state after:
no goals
Theorem: UInt8.val_unquantize
Proof state before:
α β : Type
v : UInt8
n : (Floating.ofNat (2 * v.toNat + 1) false).scaleB (-9) ≠ nan
lt : 2 * v.toNat + 1 < 2 ^ 63
⊢ ↑(-9) = -9
Tactic:
decide
Proof state after:
no goals
Theorem: Floating.val_ofUInt8
Proof state before:
α β : Type
v : UInt8
up : Bool
⊢ 2 ^ 8 < 2 ^ 63
Tactic:
norm_num
Proof state after:
no goals
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈ approx x.quantize
Tactic:
rw [quantize]
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈
    approx
      (let c := x.untrusted_quantize;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
⊢ x' ∈
    approx
      (let c := x.untrusted_quantize;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hc : x.untrusted_quantize = c
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hl : c.unquantize.sub half_color_error.lo true = lo
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
generalize hh : c.unquantize.add half_color_error.lo false = hi
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈
    approx
      (let c := c;
      let m := c.unquantize;
      let lo := m.sub half_color_error.lo true;
      let hi := m.add half_color_error.lo false;
      if lo ≠ nan ∧ hi ≠ nan ∧ lo ≤ x.lo ∧ x.hi ≤ hi then some c else none)
Tactic:
simp only [hl, hh, ne_eq, Floating.val_le_val]
Proof state after:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
by_cases n : lo = nan ∨ hi = nan
Proof state after:
case pos
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : lo = nan ∨ hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)

case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Theorem: Interval.mem_approx_quantize
Proof state before:
case neg
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)
Tactic:
rcases not_or.mp n with ⟨n0,n1⟩
Proof state after:
case neg.intro
α β : Type
x' : ℝ
x : Interval
xm : x' ∈ approx x
c : UInt8
hc : x.untrusted_quantize = c
lo : Floating
hl : c.unquantize.sub half_color_error.lo true = lo
hi : Floating
hh : c.unquantize.add half_color_error.lo false = hi
n : ¬(lo = nan ∨ hi = nan)
n0 : ¬lo = nan
n1 : ¬hi = nan
⊢ x' ∈ approx (if ¬lo = nan ∧ ¬hi = nan ∧ lo.val ≤ x.lo.val ∧ x.hi.val ≤ hi.val then some c else none)