Theorem: Real.rotateSoCone_rotatedSoCone (CvxLean/Lib/Cones/SOCone.lean)

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
⊢ match t.rotateSoCone x with
  | (v, w, x) => v.rotatedSoCone w x
Tactic:
simp [rotatedSoCone, rotateSoCone]
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
⊢ ∑ 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

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_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 habsx0t : |x 0| ≤ t := by
  rw [soCone, Fin.sum_univ_succ] at h
  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))
  exact abs_le_of_sqrt_sq_add_nonneg_le hS h
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
⊢ ∑ 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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