Theorem: Image.get_ofFn (Ray/Render/Image.lean)

State before:
f : ℕ → ℕ → Color UInt8
w h chunk : ℕ
x : Fin (ofFn w h chunk f).width
y : Fin (ofFn w h chunk f).height
⊢ (ofFn w h chunk f).get x y = f ↑x ↑y
Tactic:
rw [get]
State after:
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

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!]
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

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
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

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
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

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 ⊢
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

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
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

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
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

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]
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

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
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

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 ⟨?_, ?_, ?_, ?_⟩
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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]
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

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
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

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]
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

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]
State after:
no goals

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
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

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
State after:
no goals