Theorem: Grid.square_dz (Ray/Render/Grid.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
⊢ (square lo hi n).dz.1 = (square lo hi n).dz.2
Tactic:
rw [square]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
⊢ (let c := ((lo.1 + hi.1) / 2, (lo.2 + hi.2) / 2);
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := ((lo.1 + hi.1) / 2, (lo.2 + hi.2) / 2);
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
⊢ (let c := ((lo.1 + hi.1) / 2, (lo.2 + hi.2) / 2);
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := ((lo.1 + hi.1) / 2, (lo.2 + hi.2) / 2);
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
generalize ((lo.1 + hi.1) / 2, (lo.2 + hi.2) / 2) = c
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c : ℚ × ℚ
⊢ (let c := c;
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c : ℚ × ℚ
⊢ (let c := c;
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := hi - lo;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
generalize hi - lo = d
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
generalize hdx : max d.1 d.2 / (n : ℚ) = dx
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
generalize hn1 : max 1 (d.1 / dx).ceil.toNat = n1
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
generalize hn2 : max 1 (d.2 / dx).ceil.toNat = n2
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
have n1z : (n1 : ℚ) ≠ 0 := by
  rw [←hn1]; exact Nat.cast_ne_zero.mpr (ne_of_gt (lt_max_of_lt_left zero_lt_one))
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
have n2z : (n2 : ℚ) ≠ 0 := by
  rw [←hn2]; exact Nat.cast_ne_zero.mpr (ne_of_gt (lt_max_of_lt_left zero_lt_one))
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
n2z : ↑n2 ≠ 0
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
n2z : ↑n2 ≠ 0
⊢ (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.1 =
    (let c := c;
        let d := d;
        let dx := max d.1 d.2 / ↑n;
        let n := (max 1 (d.1 / dx).ceil.toNat, max 1 (d.2 / dx).ceil.toNat);
        let h := (dx / 2) • (↑n.1, ↑n.2);
        { lo := c - h, hi := c + h, n := n }).dz.2
Tactic:
simp only [dz, hdx, hn1, hn2, Prod.smul_mk, smul_eq_mul, Prod.fst_add, Prod.fst_sub, add_sub_sub_cancel,
  add_div, mul_div_assoc, div_self n1z, mul_one, add_halves', Prod.snd_add, Prod.snd_sub, div_self n2z]
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
⊢ ↑n1 ≠ 0
Tactic:
rw [←hn1]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
⊢ ↑(max 1 (d.1 / dx).ceil.toNat) ≠ 0

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
⊢ ↑(max 1 (d.1 / dx).ceil.toNat) ≠ 0
Tactic:
exact Nat.cast_ne_zero.mpr (ne_of_gt (lt_max_of_lt_left zero_lt_one))
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
⊢ ↑n2 ≠ 0
Tactic:
rw [←hn2]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
⊢ ↑(max 1 (d.2 / dx).ceil.toNat) ≠ 0

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
lo hi : ℚ × ℚ
n : ℕ
c d : ℚ × ℚ
dx : ℚ
hdx : max d.1 d.2 / ↑n = dx
n1 : ℕ
hn1 : max 1 (d.1 / dx).ceil.toNat = n1
n2 : ℕ
hn2 : max 1 (d.2 / dx).ceil.toNat = n2
n1z : ↑n1 ≠ 0
⊢ ↑(max 1 (d.2 / dx).ceil.toNat) ≠ 0
Tactic:
exact Nat.cast_ne_zero.mpr (ne_of_gt (lt_max_of_lt_left zero_lt_one))
State after:
no goals