internlm/Lean-Github huggingface dataset:
Theorem: neg_log_one_sub_le_linear
Proof state before:
case neg
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ (1 + x * (1 - x)⁻¹ / 2) * x ≤ c * x
Tactic:
apply mul_le_mul_of_nonneg_right _ x0
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + x * (1 - x)⁻¹ / 2 ≤ c
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + x * (1 - x)⁻¹ / 2 ≤ c
Tactic:
nth_rw 1 [←inv_inv x]
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + x⁻¹⁻¹ * (1 - x)⁻¹ / 2 ≤ c
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + x⁻¹⁻¹ * (1 - x)⁻¹ / 2 ≤ c
Tactic:
rw [←mul_inv, mul_sub, mul_one, inv_mul_cancel xz]
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + (x⁻¹ - 1)⁻¹ / 2 ≤ c
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 1 + (x⁻¹ - 1)⁻¹ / 2 ≤ c
Tactic:
rw [add_comm, ←le_sub_iff_add_le, div_le_iff (by norm_num)]
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ (x⁻¹ - 1)⁻¹ ≤ (c - 1) * 2
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ (x⁻¹ - 1)⁻¹ ≤ (c - 1) * 2
Tactic:
apply inv_le_of_inv_le c1p
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ ((c - 1) * 2)⁻¹ ≤ x⁻¹ - 1
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ ((c - 1) * 2)⁻¹ ≤ x⁻¹ - 1
Tactic:
rw [le_sub_iff_add_le, le_inv (add_pos (inv_pos.mpr c1p) (by norm_num)) x0']
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact xc
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : x = 0
⊢ -(1 - x).log ≤ c * x
Tactic:
simp only [xz, sub_zero, Real.log_one, neg_zero, mul_zero, le_refl]
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : x = 1
⊢ -(1 - x).log ≤ c * x
Tactic:
simp only [xe, sub_self, Real.log_zero, neg_zero, mul_one]
Proof state after:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : x = 1
⊢ 0 ≤ c
Theorem: neg_log_one_sub_le_linear
Proof state before:
case pos
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
x1 : x ≤ 1
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : x = 1
⊢ 0 ≤ c
Tactic:
linarith
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
⊢ 0 < 1 - x
Tactic:
linarith
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
⊢ ‖-↑x‖ < 1
Tactic:
simp only [norm_neg, Complex.norm_eq_abs, Complex.abs_ofReal, abs_of_nonneg x0]
Proof state after:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
⊢ x < 1
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
⊢ x < 1
Tactic:
exact x1
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(x ^ 2 * (1 - x)⁻¹ / 2) ≤ (1 - x).log - -x ∧ (1 - x).log - -x ≤ x ^ 2 * (1 - x)⁻¹ / 2
⊢ -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_le_linear
Proof state before:
x c : ℝ
x0 : 0 ≤ x
c1 : 1 < c
xc✝ : x ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
xc : x ≤ (((c - 1) * 2)⁻¹ + 1)⁻¹
xz : ¬x = 0
xe : ¬x = 1
x1 : x < 1
x0' : 0 < x
c1p : 0 < (c - 1) * 2
x1p : 0 < 1 - x
h : -(1 - x).log ≤ x + x ^ 2 * (1 - x)⁻¹ / 2
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Grid.square_dz
Proof 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]
Proof 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
Theorem: Grid.square_dz
Proof 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
Proof 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
Theorem: Grid.square_dz
Proof 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
Proof 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
Theorem: Grid.square_dz
Proof 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
Proof 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
Theorem: Grid.square_dz
Proof 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
Proof 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
Theorem: Grid.square_dz
Proof 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
Proof 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
Theorem: Grid.square_dz
Proof 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))
Proof 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
Theorem: Grid.square_dz
Proof 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))
Proof 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
Theorem: Grid.square_dz
Proof 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]
Proof state after:
no goals
Theorem: Grid.square_dz
Proof 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]
Proof 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
Theorem: Grid.square_dz
Proof 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))
Proof state after:
no goals
Theorem: Grid.square_dz
Proof 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]
Proof 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
Theorem: Grid.square_dz
Proof 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))
Proof state after:
no goals
Theorem: Image.size_push_colors
Proof state before:
f : ℕ → Color UInt8
n o : ℕ
d : ByteArray
⊢ (push_colors f n o d).size = d.size + n * 4
Tactic:
induction' n with n h generalizing d o
Proof state after:
case zero
f : ℕ → Color UInt8
o : ℕ
d : ByteArray
⊢ (push_colors f 0 o d).size = d.size + 0 * 4

case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (push_colors f (n + 1) o d).size = d.size + (n + 1) * 4
Theorem: Image.size_push_colors
Proof state before:
case zero
f : ℕ → Color UInt8
o : ℕ
d : ByteArray
⊢ (push_colors f 0 o d).size = d.size + 0 * 4
Tactic:
simp only [Nat.zero_eq, push_colors, ↓reduceIte, zero_mul, add_zero]
Proof state after:
no goals
Theorem: Image.size_push_colors
Proof state before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (push_colors f (n + 1) o d).size = d.size + (n + 1) * 4
Tactic:
rw [push_colors]
Proof state after:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (if n + 1 = 0 then d
      else
        let c := f o;
        push_colors f (n + 1 - 1) (o + 1) ((((d.push c.r).push c.g).push c.b).push c.a)).size =
    d.size + (n + 1) * 4
Theorem: Image.size_push_colors
Proof state before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ (if n + 1 = 0 then d
      else
        let c := f o;
        push_colors f (n + 1 - 1) (o + 1) ((((d.push c.r).push c.g).push c.b).push c.a)).size =
    d.size + (n + 1) * 4
Tactic:
simp only [Nat.succ_eq_add_one, add_eq_zero, one_ne_zero, and_false, ↓reduceIte,
  add_tsub_cancel_right, h, ByteArray.size_push]
Proof state after:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ d.size + 1 + 1 + 1 + 1 + n * 4 = d.size + (n + 1) * 4
Theorem: Image.size_push_colors
Proof state before:
case succ
f : ℕ → Color UInt8
n : ℕ
h : ∀ (o : ℕ) (d : ByteArray), (push_colors f n o d).size = d.size + n * 4
o : ℕ
d : ByteArray
⊢ d.size + 1 + 1 + 1 + 1 + n * 4 = d.size + (n + 1) * 4
Tactic:
omega
Proof state after:
no goals