internlm/Lean-Github huggingface dataset:
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ (let b := base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y;
    let_fun lt := ⋯;
    { r := (ofFn w h chunk f).data[b], g := (ofFn w h chunk f).data[b + 1], b := (ofFn w h chunk f).data[b + 2],
      a := (ofFn w h chunk f).data[b + 3] }) =
    f ↑x ↑y
Tactic:
simp only [ByteArray.getElemNat_eq_get!]
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Tactic:
have xw := x.prop
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < (ofFn w h chunk f).width
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < (ofFn w h chunk f).width
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Tactic:
have yh := y.prop
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < (ofFn w h chunk f).width
yh : ↑y < (ofFn w h chunk f).height
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < (ofFn w h chunk f).width
yh : ↑y < (ofFn w h chunk f).height
⊢ { r := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y),
      g := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 1),
      b := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 2),
      a := (ofFn w h chunk f).data.get! (base (ofFn w h chunk f).width (ofFn w h chunk f).height ↑x ↑y + 3) } =
    f ↑x ↑y
Tactic:
simp only [width_ofFn, height_ofFn, Color.ext_iff] at xw yh ⊢
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
have w0 : 0 < w := by omega
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
have yh' : y ≤ h - 1 := by omega
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
have m0 : ∀ x : Fin 4, (x * 4 : Fin 4) = 0 := by
  intro x
  have e : (4 : Fin 4) = 0 := rfl
  simp only [e, mul_zero]
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
have f0 : 0 < 4 := by norm_num
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r ∧
    (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g ∧
      (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b ∧
        (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
Proof state after:
case refine_1
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y) = (f ↑x ↑y).r

case refine_2
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 1) = (f ↑x ↑y).g

case refine_3
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 2) = (f ↑x ↑y).b

case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
⊢ 0 < w
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
⊢ ↑y ≤ h - 1
Tactic:
omega
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
⊢ ∀ (x : Fin 4), x * 4 = 0
Tactic:
intro x
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x✝ : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x✝ < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
x : Fin 4
⊢ x * 4 = 0
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x✝ : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x✝ < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
x : Fin 4
⊢ x * 4 = 0
Tactic:
have e : (4 : Fin 4) = 0 := rfl
Proof state after:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x✝ : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x✝ < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
x : Fin 4
e : 4 = 0
⊢ x * 4 = 0
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x✝ : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x✝ < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
x : Fin 4
e : 4 = 0
⊢ x * 4 = 0
Tactic:
simp only [e, mul_zero]
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (ofFn w h chunk f).data.get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
nth_rw 1 [ofFn]
Proof state after:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ { data := parallel_colors (fun i => f (i % w) (h - 1 - i / w)) (h * w) chunk, width := w, height := h,
            size_eq := ⋯ }.data.get!
      (base w h ↑x ↑y + 3) =
    (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ { data := parallel_colors (fun i => f (i % w) (h - 1 - i / w)) (h * w) chunk, width := w, height := h,
            size_eq := ⋯ }.data.get!
      (base w h ↑x ↑y + 3) =
    (f ↑x ↑y).a
Tactic:
simp only
Proof state after:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (parallel_colors (fun i => f (i % w) (h - 1 - i / w)) (h * w) chunk).get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Theorem: Image.get_ofFn
Proof state before:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (parallel_colors (fun i => f (i % w) (h - 1 - i / w)) (h * w) chunk).get! (base w h ↑x ↑y + 3) = (f ↑x ↑y).a
Tactic:
rw [get!_parallel_colors]
Proof state after:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (f ((base w h ↑x ↑y + 3) / 4 % w) (h - 1 - (base w h ↑x ↑y + 3) / 4 / w))[↑(base w h ↑x ↑y + 3)] = (f ↑x ↑y).a

case refine_4.lt
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ base w h ↑x ↑y + 3 < h * w * 4
Theorem: Image.get_ofFn
Proof state before:
case refine_4
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ (f ((base w h ↑x ↑y + 3) / 4 % w) (h - 1 - (base w h ↑x ↑y + 3) / 4 / w))[↑(base w h ↑x ↑y + 3)] = (f ↑x ↑y).a
Tactic:
simp [base, add_comm _ (x : ℕ), Nat.add_mul_div_right _ _ w0, Nat.div_eq_of_lt xw,
  Nat.sub_sub_self yh', Nat.mod_eq_of_lt xw, m0, add_comm (_ * 4),
  Nat.add_mul_div_right _ _ f0]
Proof state after:
no goals
Theorem: Image.get_ofFn
Proof state before:
case refine_4.lt
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
⊢ base w h ↑x ↑y + 3 < h * w * 4
Tactic:
have le := base_le xw yh
Proof state after:
case refine_4.lt
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
le : base w h ↑x ↑y + 4 ≤ h * w * 4
⊢ base w h ↑x ↑y + 3 < h * w * 4
Theorem: Image.get_ofFn
Proof state before:
case refine_4.lt
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
xw : ↑x < w
yh : ↑y < h
w0 : 0 < w
yh' : ↑y ≤ h - 1
m0 : ∀ (x : Fin 4), x * 4 = 0
f0 : 0 < 4
le : base w h ↑x ↑y + 4 ≤ h * w * 4
⊢ base w h ↑x ↑y + 3 < h * w * 4
Tactic:
omega
Proof state after:
no goals
Theorem: test_pos_lt_sq
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
h : 0 < x
⊢ x ^ 2 > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_gt_sq
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
h : x > 0
⊢ x ^ 2 > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_mul
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
p : x > 0
q : y > 0
⊢ x * y > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_div
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
p : x > 0
q : y > 0
⊢ x / y > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_4
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 4
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_7
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 7
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_4_real
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 4
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_7_real
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 7
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_zero_one
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 1
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_nnreal
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
h : u > 0
⊢ 0 < ↑u
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_pow
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 2 ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: test_pos_inv
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 < 1⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: test_abs
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: test_abs_ge
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ Complex.abs z ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_nn_sq
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ x ^ 2 ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_mul
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
p : x ≥ 0
q : y ≥ 0
⊢ x * y ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_div
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
p : x ≥ 0
q : y ≥ 0
⊢ x / y ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_add
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
p : x ≥ 0
q : y ≥ 0
⊢ x + y ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_nat
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ ↑n ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_num
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 7
Tactic:
bound
Proof state after:
no goals
Theorem: test_num_real
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 7
Tactic:
bound
Proof state after:
no goals
Theorem: test_zero_one
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 1
Tactic:
bound
Proof state after:
no goals
Theorem: test_nnreal
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ ↑u
Tactic:
bound
Proof state after:
no goals
Theorem: test_zero
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_pow
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 2 ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: test_inv
Proof state before:
n : ℕ
x y : ℝ
u : ℝ≥0
z : ℂ
⊢ 0 ≤ 0⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: test_sq
Proof state before:
a b c x y : ℝ
z : ℂ
n✝ : ℕ
n : x ≥ 0
h : x ≤ y
⊢ x ^ 2 ≤ y ^ 2
Tactic:
bound
Proof state after:
no goals
Theorem: test_sq_ge
Proof state before:
a b c x y : ℝ
z : ℂ
n✝ : ℕ
n : x ≥ 0
h : x ≤ y
⊢ y ^ 2 ≥ x ^ 2
Tactic:
bound
Proof state after:
no goals
Theorem: test_mul_left
Proof state before:
a b c x y : ℝ
z : ℂ
n✝ : ℕ
n : a ≥ 0
h : x ≤ y
⊢ a * x ≤ a * y
Tactic:
bound
Proof state after:
no goals
Theorem: test_mul_right
Proof state before:
a b c x y : ℝ
z : ℂ
n✝ : ℕ
n : a ≥ 0
h : x ≤ y
⊢ x * a ≤ y * a
Tactic:
bound
Proof state after:
no goals
Theorem: test_mul_both
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
bp : b ≥ 0
xp : x ≥ 0
ab : a ≤ b
xy : x ≤ y
⊢ a * x ≤ b * y
Tactic:
bound
Proof state after:
no goals
Theorem: test_abs_mul
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x ≤ y
⊢ Complex.abs z * x ≤ Complex.abs z * y
Tactic:
bound
Proof state after:
no goals
Theorem: test_add_left
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x ≤ y
⊢ a + x ≤ a + y
Tactic:
bound
Proof state after:
no goals
Theorem: test_add_right
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x ≤ y
⊢ x + a ≤ y + a
Tactic:
bound
Proof state after:
no goals
Theorem: test_add_both
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
ab : a ≤ b
xy : x ≤ y
⊢ a + x ≤ b + y
Tactic:
bound
Proof state after:
no goals
Theorem: test_sub_left
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x ≥ y
⊢ a - x ≤ a - y
Tactic:
bound
Proof state after:
no goals
Theorem: test_sub_right
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x ≤ y
⊢ x - a ≤ y - a
Tactic:
bound
Proof state after:
no goals
Theorem: test_sub_both
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
ab : a ≤ b
xy : x ≥ y
⊢ a - x ≤ b - y
Tactic:
bound
Proof state after:
no goals
Theorem: test_sub_pos
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x < y
⊢ y - x > 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_le_of_lt
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
h : x > 0
⊢ x ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: test_extra
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
f : ℕ → ℝ
h : ∀ (n : ℕ), f n ≥ 0
⊢ f n ≥ 0
Tactic:
bound [h n]
Proof state after:
no goals
Theorem: test_1_4
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
⊢ 1 < 4
Tactic:
bound
Proof state after:
no goals
Theorem: test_2_4
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
⊢ 2 < 4
Tactic:
bound
Proof state after:
no goals
Theorem: test_div_left
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
hc : c ≥ 0
h : a ≤ b
⊢ a / c ≤ b / c
Tactic:
bound
Proof state after:
no goals
Theorem: test_div_right
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
ha : a ≥ 0
hc : c > 0
h : b ≥ c
⊢ a / b ≤ a / c
Tactic:
bound
Proof state after:
no goals
Theorem: test_coe
Proof state before:
a b c x✝ y✝ : ℝ
z : ℂ
n : ℕ
x y : ℝ≥0
h : x < y
⊢ ↑x < ↑y
Tactic:
bound
Proof state after:
no goals
Theorem: test_dist
Proof state before:
a b c x y : ℝ
z : ℂ
n : ℕ
⊢ dist a c ≤ dist a b + dist b c
Tactic:
bound
Proof state after:
no goals
Theorem: test_log
Proof state before:
a b c x✝ y✝ : ℝ
z : ℂ
n : ℕ
x y : ℝ
x0 : 0 < x
h : x ≤ y
⊢ x.log ≤ y.log
Tactic:
bound
Proof state after:
no goals
Theorem: test_le_max_of_le_left
Proof state before:
a b c : ℝ
n m : ℕ
h : a ≤ b
⊢ a ≤ max b c
Tactic:
bound
Proof state after:
no goals
Theorem: test_le_max_of_le_right
Proof state before:
a b c : ℝ
n m : ℕ
h : a ≤ c
⊢ a ≤ max b c
Tactic:
bound
Proof state after:
no goals
Theorem: test_lt_max_of_lt_left
Proof state before:
a b c : ℝ
n m : ℕ
h : a < b
⊢ a < max b c
Tactic:
bound
Proof state after:
no goals
Theorem: test_lt_max_of_lt_right
Proof state before:
a b c : ℝ
n m : ℕ
h : a < c
⊢ a < max b c
Tactic:
bound
Proof state after:
no goals
Theorem: test_min_le_of_left_le
Proof state before:
a b c : ℝ
n m : ℕ
h : a ≤ c
⊢ min a b ≤ c
Tactic:
bound
Proof state after:
no goals
Theorem: test_min_le_of_right_le
Proof state before:
a b c : ℝ
n m : ℕ
h : b ≤ c
⊢ min a b ≤ c
Tactic:
bound
Proof state after:
no goals
Theorem: test_min_lt_of_left_lt
Proof state before:
a b c : ℝ
n m : ℕ
h : a < c
⊢ min a b < c
Tactic:
bound
Proof state after:
no goals
Theorem: test_min_lt_of_right_lt
Proof state before:
a b c : ℝ
n m : ℕ
h : b < c
⊢ min a b < c
Tactic:
bound
Proof state after:
no goals
Theorem: test_pow_le_pow_right
Proof state before:
a b c : ℝ
n m : ℕ
a1 : 1 ≤ a
h : m ≤ n
⊢ a ^ m ≤ a ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: test_pow_le_pow_of_le_one
Proof state before:
a b c : ℝ
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
h : n ≤ m
⊢ a ^ m ≤ a ^ n
Tactic:
bound
Proof state after:
no goals