internlm/Lean-Github huggingface dataset:
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Tactic:
have ht : 0 ≤ t := le_trans (abs_nonneg _) habsx0t
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Tactic:
replace ⟨hx0t, hnx0t⟩ := abs_le.mp habsx0t
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Tactic:
split_ands
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2

case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t + x 0) / √2

case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2

case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t + x 0) / √2

case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Tactic:
{ field_simp
  have hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2 := by norm_cast; ring
  rw [hrw, le_sub_iff_add_le, add_comm]
  unfold soCone at h; norm_cast at h ⊢
  rw [← Fin.sum_univ_succ (f := fun i => (x i) ^ 2)]
  rw [← sqrt_le_left ht]
  exact h }
Proof state after:
case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t + x 0) / √2

case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t + x 0) / √2

case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Tactic:
{ simp [le_div_iff]; linarith }
Proof state after:
case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Tactic:
{ simp [le_div_iff]; linarith }
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
⊢ |x 0| ≤ t
Tactic:
rw [soCone, Fin.sum_univ_succ] at h
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (x 0 ^ 2 + ∑ i : Fin n, x i.succ ^ 2).sqrt ≤ t
⊢ |x 0| ≤ t
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (x 0 ^ 2 + ∑ i : Fin n, x i.succ ^ 2).sqrt ≤ t
⊢ |x 0| ≤ t
Tactic:
have hS : 0 ≤ ∑ i : Fin n, x (Fin.succ i) ^ 2 :=
  Finset.sum_nonneg (fun i _ => (rpow_two (x i.succ)).symm ▸ sq_nonneg (x i.succ))
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (x 0 ^ 2 + ∑ i : Fin n, x i.succ ^ 2).sqrt ≤ t
hS : 0 ≤ ∑ i : Fin n, x i.succ ^ 2
⊢ |x 0| ≤ t
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (x 0 ^ 2 + ∑ i : Fin n, x i.succ ^ 2).sqrt ≤ t
hS : 0 ≤ ∑ i : Fin n, x i.succ ^ 2
⊢ |x 0| ≤ t
Tactic:
exact abs_le_of_sqrt_sq_add_nonneg_le hS h
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2
Tactic:
field_simp
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) * (t - x 0)
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) * (t - x 0)
Tactic:
have hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2 := by norm_cast; ring
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) * (t - x 0)
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) * (t - x 0)
Tactic:
rw [hrw, le_sub_iff_add_le, add_comm]
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Tactic:
unfold soCone at h
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (∑ i : Fin n.succ, x i ^ 2).sqrt ≤ t
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : (∑ i : Fin n.succ, x i ^ 2).sqrt ≤ t
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Tactic:
norm_cast at h ⊢
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ x 0 ^ 2 + ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ t ^ 2
Tactic:
rw [← Fin.sum_univ_succ (f := fun i => (x i) ^ 2)]
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ ∑ i : Fin (n + 1), x i ^ 2 ≤ t ^ 2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ ∑ i : Fin (n + 1), x i ^ 2 ≤ t ^ 2
Tactic:
rw [← sqrt_le_left ht]
Proof state after:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ (∑ i : Fin (n + 1), x i ^ 2).sqrt ≤ t
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
hrw : (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
h : (∑ x_1 : Fin n.succ, x x_1 ^ 2).sqrt ≤ t
⊢ (∑ i : Fin (n + 1), x i ^ 2).sqrt ≤ t
Tactic:
exact h
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ (t + x 0) * (t - x 0) = t ^ 2 - x 0 ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t + x 0) / √2
Tactic:
simp [le_div_iff]
Proof state after:
case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ t + x 0
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_1
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ t + x 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ 0 ≤ (t - x 0) / √2
Tactic:
simp [le_div_iff]
Proof state after:
case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ x 0 ≤ t
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
case refine_2.refine_2
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
ht : 0 ≤ t
hx0t : -t ≤ x 0
hnx0t : x 0 ≤ t
⊢ x 0 ≤ t
Tactic:
linarith
Proof state after:
no goals
Theorem: Real.unrotateSoCone_soCone
Proof state before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ match v.unrotateSoCone w x with
  | (t, x) => t.soCone x
Tactic:
simp [soCone, unrotateSoCone]
Proof state after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Tactic:
replace ⟨h, hv, hw⟩ := h
Proof state after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Tactic:
rw [sqrt_le_iff]
Proof state after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2 ∧ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2 ∧ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
split_ands
Proof state after:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2

case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2

case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
{ simp [le_div_iff]; linarith }
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
{ rw [Fin.sum_univ_succ]
  simp [Matrix.vecCons]
  rw [add_comm, ← le_sub_iff_add_le]
  field_simp
  have hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2 := by norm_cast; ring
  norm_cast at hrw h
  rwa [hrw] }
Proof state after:
no goals
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2
Tactic:
simp [le_div_iff]
Proof state after:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ v + w
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ v + w
Tactic:
linarith
Proof state after:
no goals
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
rw [Fin.sum_univ_succ]
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ Matrix.vecCons ((v - w) / √2) x 0 ^ 2 + ∑ i : Fin n, Matrix.vecCons ((v - w) / √2) x i.succ ^ 2 ≤ ((v + w) / √2) ^ 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ Matrix.vecCons ((v - w) / √2) x 0 ^ 2 + ∑ i : Fin n, Matrix.vecCons ((v - w) / √2) x i.succ ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
simp [Matrix.vecCons]
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (v - w) ^ 2 / 2 + ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (v - w) ^ 2 / 2 + ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2
Tactic:
rw [add_comm, ← le_sub_iff_add_le]
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2 - (v - w) ^ 2 / 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2 - (v - w) ^ 2 / 2
Tactic:
field_simp
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
have hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2 := by norm_cast; ring
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
norm_cast at hrw h
Proof state after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
h : ∑ x_1 : Fin n, x x_1 ^ 2 ≤ v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Theorem: Real.unrotateSoCone_soCone
Proof state before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
h : ∑ x_1 : Fin n, x x_1 ^ 2 ≤ v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
rwa [hrw]
Proof state after:
no goals
Theorem: Real.unrotateSoCone_soCone
Proof state before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
Tactic:
ring
Proof state after:
no goals
Theorem: Real.soCone_add_sub_two_mul_of_nonneg
Proof state before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y
Tactic:
have hxy := add_nonneg hx hy
Proof state after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y
Theorem: Real.soCone_add_sub_two_mul_of_nonneg
Proof state before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y
Tactic:
conv => lhs; unfold soCone; simp [sqrt_le_left hxy, ← le_sub_iff_add_le']
Proof state after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (2 * z) ^ 2 ≤ (x + y) ^ 2 - (x - y) ^ 2 ↔ z ^ 2 ≤ x * y