[GOAL]
k : ℕ
⊢ 0 < W k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
⊢ 0 < W Nat.zero
[PROOFSTEP]
unfold W
[GOAL]
case zero
⊢ 0 < ∏ i in range Nat.zero, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (Nat.succ k)
[PROOFSTEP]
rw [W_succ]
[GOAL]
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
[PROOFSTEP]
refine' mul_pos hk (mul_pos (div_pos _ _) (div_pos _ _))
[GOAL]
case succ.refine'_1
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_2
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 1
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_4
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 3
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
⊢ W n = ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ W Nat.zero = ↑(2 ^ (4 * Nat.zero)) * ↑(Nat.zero ! ^ 4) / (↑((2 * Nat.zero)! ^ 2) * (2 * ↑Nat.zero + 1))
[PROOFSTEP]
simp only [W, prod_range_zero, Nat.factorial_zero, mul_zero, pow_zero, algebraMap.coe_one, one_pow, mul_one,
  algebraMap.coe_zero, zero_add, div_self, Ne.def, one_ne_zero, not_false_iff]
[GOAL]
case zero
⊢ 1 = ↑(2 ^ (4 * Nat.zero)) * ↑1 / (↑((2 * Nat.zero)! ^ 2) * (2 * ↑Nat.zero + 1))
[PROOFSTEP]
norm_num
[GOAL]
case succ
n : ℕ
IH : W n = ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ W (Nat.succ n) = ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
unfold W at IH ⊢
[GOAL]
case succ
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ∏ i in range (Nat.succ n), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]
[GOAL]
case succ
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
refine' (div_eq_div_iff _ _).mpr _
[GOAL]
case succ.refine'_1
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0
case succ.refine'_2
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1) ≠ 0
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
any_goals exact ne_of_gt (by positivity)
[GOAL]
case succ.refine'_1
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 0 < ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_2
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1) ≠ 0
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 0 < ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ?m.19110 < ?m.19109
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
simp_rw [Nat.mul_succ, Nat.factorial_succ, pow_succ]
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! * (n ! * (n ! * (n ! * n ! ^ 0)))) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) *
            ((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) * ((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) ^ 0)) *
        (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 * (2 * (2 * (2 * 2 ^ (4 * n))))) *
        ↑((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n !) ^ 0)))) *
      (↑((2 * n)! * ((2 * n)! * (2 * n)! ^ 0)) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
push_cast
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! * (↑n ! * (↑n ! * (↑n ! * ↑n ! ^ 0)))) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!) * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0) *
        (2 * (↑n + 1) + 1)) =
    2 * (2 * (2 * (2 * 2 ^ (4 * n)))) *
        ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n !) ^ 0)))) *
      (↑(2 * n)! * (↑(2 * n)! * ↑(2 * n)! ^ 0) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
ring_nf
[GOAL]
k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
[GOAL]
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
[PROOFSTEP]
simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
[GOAL]
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
⊢ W k ≤ π / 2
[PROOFSTEP]
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
[GOAL]
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
[PROOFSTEP]
rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
[GOAL]
k : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
apply integral_sin_pow_succ_le
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k
[PROOFSTEP]
rw [← le_div_iff pi_div_two_pos, div_eq_inv_mul (W k) _]
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
[PROOFSTEP]
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff (integral_sin_pow_pos _)]
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
[PROOFSTEP]
convert integral_sin_pow_succ_le (2 * k + 1)
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)
[PROOFSTEP]
rw [integral_sin_pow (2 * k)]
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
simp only [sin_zero, zero_pow', Ne.def, Nat.succ_ne_zero, zero_mul, sin_pi, tsub_zero, zero_div, zero_add]
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
norm_cast
[GOAL]
⊢ Tendsto W atTop (𝓝 (π / 2))
[PROOFSTEP]
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le _ tendsto_const_nhds le_W W_le
[GOAL]
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
[PROOFSTEP]
have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]
[GOAL]
⊢ 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
[PROOFSTEP]
rw [sub_zero, one_mul]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
[PROOFSTEP]
rw [this]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))
[PROOFSTEP]
refine' Tendsto.mul _ tendsto_const_nhds
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
have h : ∀ n : ℕ, ((2 : ℝ) * n + 1) / (2 * n + 2) = 1 - 1 / (2 * n + 2) :=
  by
  intro n
  rw [sub_div' _ _ _
      (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),
    one_mul]
  congr 1; ring
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
[PROOFSTEP]
intro n
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
[PROOFSTEP]
rw [sub_div' _ _ _
    (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),
  one_mul]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1
[PROOFSTEP]
ring
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
simp_rw [h]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
refine' (tendsto_const_nhds.div_atTop _).const_sub _
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i + 2) atTop atTop
[PROOFSTEP]
refine' Tendsto.atTop_add _ tendsto_const_nhds
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i) atTop atTop
[PROOFSTEP]
exact tendsto_nat_cast_atTop_atTop.const_mul_atTop two_pos


[GOAL]
a b : ℕ+
⊢ card (Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← Nat.card_Icc]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Icc a b) = card (Icc ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Icc _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Icc a b) = card (map (Embedding.subtype fun n => 0 < n) (Icc a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ico]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = card (Ico ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ico _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = card (map (Embedding.subtype fun n => 0 < n) (Ico a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ioc]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = card (Ioc ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ioc _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = card (map (Embedding.subtype fun n => 0 < n) (Ioc a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← Nat.card_Ioo]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = card (Ioo ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ioo _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = card (map (Embedding.subtype fun n => 0 < n) (Ioo a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]


[GOAL]
m : ℕ
⊢ ↑(toPNat' (m + 1)) = if 0 < m + 1 then m + 1 else 1
[PROOFSTEP]
rw [if_pos (succ_pos m)]
[GOAL]
m : ℕ
⊢ ↑(toPNat' (m + 1)) = m + 1
[PROOFSTEP]
rfl
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
[PROOFSTEP]
dsimp [mod, modDiv]
[GOAL]
m k : ℕ+
⊢ ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
m k : ℕ+
x✝ : ℕ
⊢ ↑(modDivAux k x✝ (↑m / ↑k)).fst = if x✝ = 0 then ↑k else x✝
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = if zero = 0 then ↑k else zero
[PROOFSTEP]

| zero =>
  rw [if_pos rfl]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = if zero = 0 then ↑k else zero
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = ↑k
[PROOFSTEP]
rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = if succ n = 0 then ↑k else succ n
[PROOFSTEP]

| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = if succ n = 0 then ↑k else succ n
[PROOFSTEP]
rw [if_neg n.succ_ne_zero]
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = succ n
[PROOFSTEP]
rfl
[GOAL]
m k : ℕ+
⊢ div m k = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
dsimp [div, modDiv]
[GOAL]
m k : ℕ+
⊢ (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
m k : ℕ+
x✝ : ℕ
⊢ (modDivAux k x✝ (↑m / ↑k)).snd = if x✝ = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = if zero = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]

| zero =>
  rw [if_pos rfl]
  rfl
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = if zero = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
rw [if_pos rfl]
[GOAL]
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = pred (↑m / ↑k)
[PROOFSTEP]
rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = if succ n = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]

| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = if succ n = 0 then pred (↑m / ↑k) else ↑m / ↑k
[PROOFSTEP]
rw [if_neg n.succ_ne_zero]
[GOAL]
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = ↑m / ↑k
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
hn : 0 < n
⊢ ↑↑(Nat.toPNat' (natAbs n)) = n
[PROOFSTEP]
rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'), Int.natAbs_of_nonneg hn.le]


[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ get v i ∈ toList v
[PROOFSTEP]
rw [get_eq_get]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) i) ∈ toList v
[PROOFSTEP]
exact List.get_mem _ _ _
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ a ∈ toList v ↔ ∃ i, get v i = a
[PROOFSTEP]
simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ (∃ i h, List.get (toList v) { val := i, isLt := h } = a) ↔
    ∃ i h, List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
[PROOFSTEP]
exact ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi , h⟩, fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length], h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
x✝ : ∃ i h, List.get (toList v) { val := i, isLt := h } = a
i : ℕ
hi : i < List.length (toList v)
h : List.get (toList v) { val := i, isLt := hi } = a
⊢ i < n
[PROOFSTEP]
rwa [toList_length] at hi
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
x✝ : ∃ i h, List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := h }) = a
i : ℕ
hi : i < n
h : List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) { val := i, isLt := hi }) = a
⊢ i < List.length (toList v)
[PROOFSTEP]
rwa [toList_length]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ toList nil
[PROOFSTEP]
unfold Vector.nil
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ toList { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
⊢ ¬a ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
⊢ a' ∈ toList (a ::ᵥ v) ↔ a' = a ∨ a' ∈ toList v
[PROOFSTEP]
rw [Vector.toList_cons, List.mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α (n + 1)
⊢ a ∈ toList v ↔ a = head v ∨ a ∈ toList (tail v)
[PROOFSTEP]
obtain ⟨a', v', h⟩ := exists_eq_cons v
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
a a'✝ : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ toList v ↔ a = head v ∨ a ∈ toList (tail v)
[PROOFSTEP]
simp_rw [h, Vector.mem_cons_iff, Vector.head_cons, Vector.tail_cons]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v : Vector α n
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
induction' n with n _
[GOAL]
case zero
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
v✝ : Vector α n
ha✝ : a ∈ toList (tail v✝)
v : Vector α Nat.zero
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
exact False.elim (Vector.not_mem_zero a v.tail ha)
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ : ℕ
a a' : α
v✝ : Vector α n✝
ha✝ : a ∈ toList (tail v✝)
n : ℕ
n_ih✝ : ∀ (v : Vector α n), a ∈ toList (tail v) → a ∈ toList v
v : Vector α (Nat.succ n)
ha : a ∈ toList (tail v)
⊢ a ∈ toList v
[PROOFSTEP]
exact (mem_succ_iff a v).2 (Or.inr ha)
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α n
f : α → β
⊢ b ∈ toList (map f v) ↔ ∃ a, a ∈ toList v ∧ f a = b
[PROOFSTEP]
rw [Vector.toList_map, List.mem_map]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α 0
f : α → β
⊢ ¬b ∈ toList (map f v)
[PROOFSTEP]
simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil b
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ toList (map f v) ↔ f (head v) = b ∨ ∃ a, a ∈ toList (tail v) ∧ f a = b
[PROOFSTEP]
rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]


[GOAL]
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊥ ↑y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (hy | rfl | hy)
[GOAL]
case inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊥ ↑y
case inr.inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
⊢ P ⊥ ↑0
case inr.inr
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : 0 < y
⊢ P ⊥ ↑y
[PROOFSTEP]
exacts [bot_neg y hy, bot_zero, bot_pos y hy]
[GOAL]
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊥
[PROOFSTEP]
rcases lt_trichotomy x 0 with (hx | rfl | hx)
[GOAL]
case inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P ↑x ⊥
case inr.inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
⊢ P ↑0 ⊥
case inr.inr
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
hx : 0 < x
⊢ P ↑x ⊥
[PROOFSTEP]
exacts [neg_bot x hx, zero_bot, pos_bot x hx]
[GOAL]
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊤
[PROOFSTEP]
rcases lt_trichotomy x 0 with (hx | rfl | hx)
[GOAL]
case inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P ↑x ⊤
case inr.inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
⊢ P ↑0 ⊤
case inr.inr
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
hx : 0 < x
⊢ P ↑x ⊤
[PROOFSTEP]
exacts [neg_top x hx, zero_top, pos_top x hx]
[GOAL]
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊤ ↑y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (hy | rfl | hy)
[GOAL]
case inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊤ ↑y
case inr.inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
⊢ P ⊤ ↑0
case inr.inr
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ (x : ℝ), x < 0 → P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ (x : ℝ), x < 0 → P ↑x ⊤
neg_bot : ∀ (x : ℝ), x < 0 → P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ (x : ℝ), x < 0 → P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : 0 < y
⊢ P ⊤ ↑y
[PROOFSTEP]
exacts [top_neg y hy, top_zero, top_pos y hy]
[GOAL]
x y : EReal
⊢ x * y = y * x
[PROOFSTEP]
induction' x using EReal.rec with x
[GOAL]
case h_bot
y : EReal
⊢ ⊥ * y = y * ⊥
[PROOFSTEP]
induction' y using EReal.rec with y
[GOAL]
case h_real
y : EReal
x : ℝ
⊢ ↑x * y = y * ↑x
[PROOFSTEP]
induction' y using EReal.rec with y
[GOAL]
case h_top
y : EReal
⊢ ⊤ * y = y * ⊤
[PROOFSTEP]
induction' y using EReal.rec with y
[GOAL]
case h_bot.h_bot
⊢ ⊥ * ⊥ = ⊥ * ⊥
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_bot.h_bot
⊢ ⊥ * ⊥ = ⊥ * ⊥
[PROOFSTEP]
{rfl
}
[GOAL]
case h_bot.h_bot
⊢ ⊥ * ⊥ = ⊥ * ⊥
[PROOFSTEP]
rfl
[GOAL]
case h_bot.h_real
y : ℝ
⊢ ⊥ * ↑y = ↑y * ⊥
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_bot.h_real
y : ℝ
⊢ ⊥ * ↑y = ↑y * ⊥
[PROOFSTEP]
{rfl
}
[GOAL]
case h_bot.h_real
y : ℝ
⊢ ⊥ * ↑y = ↑y * ⊥
[PROOFSTEP]
rfl
[GOAL]
case h_bot.h_top
⊢ ⊥ * ⊤ = ⊤ * ⊥
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_bot.h_top
⊢ ⊥ * ⊤ = ⊤ * ⊥
[PROOFSTEP]
{rfl
}
[GOAL]
case h_bot.h_top
⊢ ⊥ * ⊤ = ⊤ * ⊥
[PROOFSTEP]
rfl
[GOAL]
case h_real.h_bot
x : ℝ
⊢ ↑x * ⊥ = ⊥ * ↑x
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_real.h_bot
x : ℝ
⊢ ↑x * ⊥ = ⊥ * ↑x
[PROOFSTEP]
{rfl
}
[GOAL]
case h_real.h_bot
x : ℝ
⊢ ↑x * ⊥ = ⊥ * ↑x
[PROOFSTEP]
rfl
[GOAL]
case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
{rfl
}
[GOAL]
case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
rfl
[GOAL]
case h_real.h_top
x : ℝ
⊢ ↑x * ⊤ = ⊤ * ↑x
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_real.h_top
x : ℝ
⊢ ↑x * ⊤ = ⊤ * ↑x
[PROOFSTEP]
{rfl
}
[GOAL]
case h_real.h_top
x : ℝ
⊢ ↑x * ⊤ = ⊤ * ↑x
[PROOFSTEP]
rfl
[GOAL]
case h_top.h_bot
⊢ ⊤ * ⊥ = ⊥ * ⊤
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_top.h_bot
⊢ ⊤ * ⊥ = ⊥ * ⊤
[PROOFSTEP]
{rfl
}
[GOAL]
case h_top.h_bot
⊢ ⊤ * ⊥ = ⊥ * ⊤
[PROOFSTEP]
rfl
[GOAL]
case h_top.h_real
y : ℝ
⊢ ⊤ * ↑y = ↑y * ⊤
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_top.h_real
y : ℝ
⊢ ⊤ * ↑y = ↑y * ⊤
[PROOFSTEP]
{rfl
}
[GOAL]
case h_top.h_real
y : ℝ
⊢ ⊤ * ↑y = ↑y * ⊤
[PROOFSTEP]
rfl
[GOAL]
case h_top.h_top
⊢ ⊤ * ⊤ = ⊤ * ⊤
[PROOFSTEP]
try {rfl
}
[GOAL]
case h_top.h_top
⊢ ⊤ * ⊤ = ⊤ * ⊤
[PROOFSTEP]
{rfl
}
[GOAL]
case h_top.h_top
⊢ ⊤ * ⊤ = ⊤ * ⊤
[PROOFSTEP]
rfl
[GOAL]
case h_real.h_real
x y : ℝ
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
rw [← coe_mul, ← coe_mul, mul_comm]
[GOAL]
x : EReal
⊢ x * 1 = x
[PROOFSTEP]
rw [EReal.mul_comm, EReal.one_mul]
[GOAL]
x : EReal
⊢ x * 0 = 0
[PROOFSTEP]
rw [EReal.mul_comm, EReal.zero_mul]
[GOAL]
x : EReal
hx : x ≠ ⊤ ∧ x ≠ ⊥
⊢ ∃ y, ↑y = x
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case h_bot
hx : ⊥ ≠ ⊤ ∧ ⊥ ≠ ⊥
⊢ ∃ y, ↑y = ⊥
[PROOFSTEP]
simp at hx
[GOAL]
case h_real
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝
[PROOFSTEP]
simp
[GOAL]
case h_top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤
[PROOFSTEP]
simp at hx
[GOAL]
⊢ range Real.toEReal = {⊥, ⊤}ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case h.h_bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ {⊥, ⊤}ᶜ
[PROOFSTEP]
simp
[GOAL]
case h.h_real
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ {⊥, ⊤}ᶜ
[PROOFSTEP]
simp
[GOAL]
case h.h_top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ {⊥, ⊤}ᶜ
[PROOFSTEP]
simp
[GOAL]
⊢ range Real.toEReal = Ioo ⊥ ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case h.h_bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ Ioo ⊥ ⊤
[PROOFSTEP]
simp
[GOAL]
case h.h_real
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ Ioo ⊥ ⊤
[PROOFSTEP]
simp
[GOAL]
case h.h_top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ Ioo ⊥ ⊤
[PROOFSTEP]
simp
[GOAL]
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ toReal x ≤ toReal y
[PROOFSTEP]
lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
[GOAL]
case intro
y : EReal
hy : y ≠ ⊤
x : ℝ
h : ↑x ≤ y
hx : ↑x ≠ ⊥
⊢ toReal ↑x ≤ toReal y
[PROOFSTEP]
lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
[GOAL]
case intro.intro
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ toReal ↑x ≤ toReal ↑y
[PROOFSTEP]
simpa using h
[GOAL]
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ ↑(toReal x) = x
[PROOFSTEP]
lift x to ℝ using ⟨hx, h'x⟩
[GOAL]
case intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(toReal ↑x) = ↑x
[PROOFSTEP]
rfl
[GOAL]
x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑(toReal x)
[PROOFSTEP]
by_cases h' : x = ⊥
[GOAL]
case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑(toReal x)
[PROOFSTEP]
simp only [h', bot_le]
[GOAL]
case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑(toReal x)
[PROOFSTEP]
simp only [le_refl, coe_toReal h h']
[GOAL]
x : EReal
h : x ≠ ⊥
⊢ ↑(toReal x) ≤ x
[PROOFSTEP]
by_cases h' : x = ⊤
[GOAL]
case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑(toReal x) ≤ x
[PROOFSTEP]
simp only [h', le_top]
[GOAL]
case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑(toReal x) ≤ x
[PROOFSTEP]
simp only [le_refl, coe_toReal h' h]
[GOAL]
x : EReal
⊢ x = ⊤ ↔ ∀ (y : ℝ), ↑y < x
[PROOFSTEP]
constructor
[GOAL]
case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
⊢ ∀ (y : ℝ), ↑y < ⊤
[PROOFSTEP]
exact EReal.coe_lt_top
[GOAL]
case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
x : EReal
⊢ x ≠ ⊤ → ∃ y, x ≤ ↑y
[PROOFSTEP]
intro h
[GOAL]
case mpr
x : EReal
h : x ≠ ⊤
⊢ ∃ y, x ≤ ↑y
[PROOFSTEP]
exact ⟨x.toReal, le_coe_toReal h⟩
[GOAL]
x : EReal
⊢ x = ⊥ ↔ ∀ (y : ℝ), x < ↑y
[PROOFSTEP]
constructor
[GOAL]
case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
⊢ ∀ (y : ℝ), ⊥ < ↑y
[PROOFSTEP]
exact bot_lt_coe
[GOAL]
case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
x : EReal
⊢ x ≠ ⊥ → ∃ y, ↑y ≤ x
[PROOFSTEP]
intro h
[GOAL]
case mpr
x : EReal
h : x ≠ ⊥
⊢ ∃ y, ↑y ≤ x
[PROOFSTEP]
exact ⟨x.toReal, coe_toReal_le h⟩
[GOAL]
x : ℝ≥0∞
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]
[GOAL]
x : ℝ≥0∞
⊢ ↑x = 1 ↔ x = 1
[PROOFSTEP]
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]
[GOAL]
x : ℝ≥0∞
⊢ 0 < ↑x ↔ 0 < x
[PROOFSTEP]
rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]
[GOAL]
x y : ℝ≥0∞
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
cases x
[GOAL]
case none
y : ℝ≥0∞
⊢ ↑(none + y) = ↑none + ↑y
[PROOFSTEP]
cases y
[GOAL]
case some
y : ℝ≥0∞
val✝ : ℝ≥0
⊢ ↑(Option.some val✝ + y) = ↑(Option.some val✝) + ↑y
[PROOFSTEP]
cases y
[GOAL]
case none.none
⊢ ↑(none + none) = ↑none + ↑none
[PROOFSTEP]
rfl
[GOAL]
case none.some
val✝ : ℝ≥0
⊢ ↑(none + Option.some val✝) = ↑none + ↑(Option.some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some.none
val✝ : ℝ≥0
⊢ ↑(Option.some val✝ + none) = ↑(Option.some val✝) + ↑none
[PROOFSTEP]
rfl
[GOAL]
case some.some
val✝¹ val✝ : ℝ≥0
⊢ ↑(Option.some val✝¹ + Option.some val✝) = ↑(Option.some val✝¹) + ↑(Option.some val✝)
[PROOFSTEP]
rfl
[GOAL]
x : ℝ≥0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | h0)
[GOAL]
case inl
⊢ ↑(⊤ * ↑0) = ⊤ * ↑↑0
[PROOFSTEP]
simp
[GOAL]
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(⊤ * ↑x) = ⊤ * ↑↑x
[PROOFSTEP]
rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]
[GOAL]
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑⊤ = ⊤ * ↑↑x
[PROOFSTEP]
exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt
[GOAL]
x : ℝ≥0
⊢ ↑(↑x * ⊤) = ↑↑x * ↑⊤
[PROOFSTEP]
rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
[GOAL]
x y : ℝ≥0
⊢ ↑(↑x * ↑y) = ↑↑x * ↑↑y
[PROOFSTEP]
simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]
[GOAL]
a b : ℝ
h : ↑a < ↑b
⊢ ∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b
[PROOFSTEP]
simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]
[GOAL]
a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ ↑a < ↑↑b
[PROOFSTEP]
simpa using hab
[GOAL]
a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑↑b < ↑a
[PROOFSTEP]
simpa using hab
[GOAL]
x : ℝ
⊢ ↑x ∈ {⊥, ⊤}ᶜ
[PROOFSTEP]
simp
[GOAL]
x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ (fun x => { val := ↑x, property := (_ : ↑x ∈ {⊥, ⊤}ᶜ) }) ((fun x => toReal ↑x) { val := x, property := hx }) =
    { val := x, property := hx }
[PROOFSTEP]
lift x to ℝ
[GOAL]
x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ x ≠ ⊤ ∧ x ≠ ⊥
[PROOFSTEP]
simpa [not_or, and_comm] using hx
[GOAL]
case intro
x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x => { val := ↑x, property := (_ : ↑x ∈ {⊥, ⊤}ᶜ) }) ((fun x => toReal ↑x) { val := ↑x, property := hx }) =
    { val := ↑x, property := hx }
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ (fun x => toReal ↑x) ((fun x => { val := ↑x, property := (_ : ↑x ∈ {⊥, ⊤}ᶜ) }) x) = x
[PROOFSTEP]
simp
[GOAL]
x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
[PROOFSTEP]
simp [bot_lt_iff_ne_bot, not_or]
[GOAL]
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ toReal (x + y) = toReal x + toReal y
[PROOFSTEP]
lift x to ℝ using ⟨hx, h'x⟩
[GOAL]
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ toReal (↑x + y) = toReal ↑x + toReal y
[PROOFSTEP]
lift y to ℝ using ⟨hy, h'y⟩
[GOAL]
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ toReal (↑x + ↑y) = toReal ↑x + toReal ↑y
[PROOFSTEP]
rfl
[GOAL]
x z : ℝ
h : ↑x + ⊤ ≤ ↑x + ↑z
⊢ ⊤ ≤ ↑z
[PROOFSTEP]
simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h
[GOAL]
x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ ≤ ⊥
[PROOFSTEP]
simpa using h
[GOAL]
x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z
[PROOFSTEP]
simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h
[GOAL]
x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y
[PROOFSTEP]
simpa [add_comm] using add_lt_add_right_coe h z
[GOAL]
x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t
[PROOFSTEP]
rcases eq_or_ne x ⊥ with (rfl | hx)
[GOAL]
case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t
[PROOFSTEP]
simp [h1, bot_le.trans_lt h2]
[GOAL]
case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t
[PROOFSTEP]
lift x to ℝ using ⟨h1.ne_top, hx⟩
[GOAL]
case inr.intro
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t
[PROOFSTEP]
calc
  (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
  _ ≤ y + t := add_le_add_right h1.le _
[GOAL]
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t
[PROOFSTEP]
rcases h'.eq_or_lt with (rfl | hlt)
[GOAL]
case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z
[PROOFSTEP]
rcases eq_or_ne z ⊤ with (rfl | hz)
[GOAL]
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤
[PROOFSTEP]
obtain rfl := htop rfl rfl
[GOAL]
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤
[PROOFSTEP]
simpa
[GOAL]
case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
[PROOFSTEP]
lift z to ℝ using ⟨hz, hbot⟩
[GOAL]
case inl.inr.intro
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z
[PROOFSTEP]
exact add_lt_add_right_coe h z
[GOAL]
case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
[PROOFSTEP]
exact add_lt_add h hlt
[GOAL]
x y : EReal
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x + y < ⊤
[PROOFSTEP]
rw [← EReal.top_add_top]
[GOAL]
x y : EReal
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x + y < ⊤ + ⊤
[PROOFSTEP]
exact EReal.add_lt_add hx.lt_top hy.lt_top
[GOAL]
⊢ toReal (-⊤) = -toReal ⊤
[PROOFSTEP]
simp
[GOAL]
⊢ toReal (-⊥) = -toReal ⊥
[PROOFSTEP]
simp
[GOAL]
a b : EReal
⊢ -a ≤ b ↔ -b ≤ a
[PROOFSTEP]
rw [← neg_le_neg_iff, neg_neg]
[GOAL]
a b : EReal
h : a ≤ -b
⊢ b ≤ -a
[PROOFSTEP]
rwa [← neg_neg b, EReal.neg_le, neg_neg]
[GOAL]
a b : EReal
⊢ -a < b ↔ -b < a
[PROOFSTEP]
rw [← neg_lt_neg_iff, neg_neg]
[GOAL]
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥
[PROOFSTEP]
simp [ht]
[GOAL]
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -z ≠ ⊤
[PROOFSTEP]
simp [hz]
[GOAL]
x : ℝ
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
[PROOFSTEP]
rcases le_total 0 x with (h | h)
[GOAL]
case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
[PROOFSTEP]
lift x to ℝ≥0 using h
[GOAL]
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑(Real.toNNReal ↑x) - ↑↑(Real.toNNReal (-↑x))
[PROOFSTEP]
rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero, coe_ennreal_zero,
  sub_zero]
[GOAL]
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑x
[PROOFSTEP]
rfl
[GOAL]
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑(Real.toNNReal x) - ↑↑(Real.toNNReal (-x))
[PROOFSTEP]
rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real, Real.coe_toNNReal, zero_sub,
  coe_neg, neg_neg]
[GOAL]
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
[PROOFSTEP]
exact neg_nonneg.2 h
[GOAL]
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ toReal (x - y) = toReal x - toReal y
[PROOFSTEP]
lift x to ℝ using ⟨hx, h'x⟩
[GOAL]
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ toReal (↑x - y) = toReal ↑x - toReal y
[PROOFSTEP]
lift y to ℝ using ⟨hy, h'y⟩
[GOAL]
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ toReal (↑x - ↑y) = toReal ↑x - toReal ↑y
[PROOFSTEP]
rfl
[GOAL]
x : EReal
h : 0 < x
⊢ ⊤ * x = ⊤
[PROOFSTEP]
rw [EReal.mul_comm]
[GOAL]
x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤
[PROOFSTEP]
exact mul_top_of_pos h
[GOAL]
x : EReal
h : x < 0
⊢ ⊤ * x = ⊥
[PROOFSTEP]
rw [EReal.mul_comm]
[GOAL]
x : EReal
h : x < 0
⊢ x * ⊤ = ⊥
[PROOFSTEP]
exact mul_top_of_neg h
[GOAL]
x : EReal
h : 0 < x
⊢ ⊥ * x = ⊥
[PROOFSTEP]
rw [EReal.mul_comm]
[GOAL]
x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥
[PROOFSTEP]
exact mul_bot_of_pos h
[GOAL]
x : EReal
h : x < 0
⊢ ⊥ * x = ⊤
[PROOFSTEP]
rw [EReal.mul_comm]
[GOAL]
x : EReal
h : x < 0
⊢ x * ⊥ = ⊤
[PROOFSTEP]
exact mul_bot_of_neg h
[GOAL]
x y : EReal
⊢ toReal (x * y) = toReal x * toReal y
[PROOFSTEP]
induction x, y using induction₂_symm with
| top_zero| zero_bot| top_top| top_bot| bot_bot => simp
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => norm_cast
| top_pos _ h => simp [top_mul_coe_of_pos h]
| top_neg _ h => simp [top_mul_coe_of_neg h]
| pos_bot _ h => simp [coe_mul_bot_of_pos h]
| neg_bot _ h => simp [coe_mul_bot_of_neg h]
[GOAL]
x y : EReal
⊢ toReal (x * y) = toReal x * toReal y
[PROOFSTEP]
induction x, y using induction₂_symm with
| top_zero => simp
| zero_bot => simp
| top_top => simp
| top_bot => simp
| bot_bot => simp
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => norm_cast
| top_pos _ h => simp [top_mul_coe_of_pos h]
| top_neg _ h => simp [top_mul_coe_of_neg h]
| pos_bot _ h => simp [coe_mul_bot_of_pos h]
| neg_bot _ h => simp [coe_mul_bot_of_neg h]
[GOAL]
x y : EReal
⊢ toReal (x * y) = toReal x * toReal y
[PROOFSTEP]
induction x, y using induction₂_symm with
| top_zero => simp
| zero_bot => simp
| top_top => simp
| top_bot => simp
| bot_bot => simp
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => norm_cast
| top_pos _ h => simp [top_mul_coe_of_pos h]
| top_neg _ h => simp [top_mul_coe_of_neg h]
| pos_bot _ h => simp [coe_mul_bot_of_pos h]
| neg_bot _ h => simp [coe_mul_bot_of_neg h]
[GOAL]
case top_zero
⊢ toReal (⊤ * 0) = toReal ⊤ * toReal 0
[PROOFSTEP]

| top_zero => simp
[GOAL]
case top_zero
⊢ toReal (⊤ * 0) = toReal ⊤ * toReal 0
[PROOFSTEP]
simp
[GOAL]
case zero_bot
⊢ toReal (0 * ⊥) = toReal 0 * toReal ⊥
[PROOFSTEP]

| zero_bot => simp
[GOAL]
case zero_bot
⊢ toReal (0 * ⊥) = toReal 0 * toReal ⊥
[PROOFSTEP]
simp
[GOAL]
case top_top
⊢ toReal (⊤ * ⊤) = toReal ⊤ * toReal ⊤
[PROOFSTEP]

| top_top => simp
[GOAL]
case top_top
⊢ toReal (⊤ * ⊤) = toReal ⊤ * toReal ⊤
[PROOFSTEP]
simp
[GOAL]
case top_bot
⊢ toReal (⊤ * ⊥) = toReal ⊤ * toReal ⊥
[PROOFSTEP]

| top_bot => simp
[GOAL]
case top_bot
⊢ toReal (⊤ * ⊥) = toReal ⊤ * toReal ⊥
[PROOFSTEP]
simp
[GOAL]
case bot_bot
⊢ toReal (⊥ * ⊥) = toReal ⊥ * toReal ⊥
[PROOFSTEP]

| bot_bot => simp
[GOAL]
case bot_bot
⊢ toReal (⊥ * ⊥) = toReal ⊥ * toReal ⊥
[PROOFSTEP]
simp
[GOAL]
case symm
x✝ y✝ : EReal
h : toReal (x✝ * y✝) = toReal x✝ * toReal y✝
⊢ toReal (y✝ * x✝) = toReal y✝ * toReal x✝
[PROOFSTEP]

| symm h => rwa [mul_comm, EReal.mul_comm]
[GOAL]
case symm
x✝ y✝ : EReal
h : toReal (x✝ * y✝) = toReal x✝ * toReal y✝
⊢ toReal (y✝ * x✝) = toReal y✝ * toReal x✝
[PROOFSTEP]
rwa [mul_comm, EReal.mul_comm]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ toReal (↑x✝ * ↑y✝) = toReal ↑x✝ * toReal ↑y✝
[PROOFSTEP]

| coe_coe => norm_cast
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ toReal (↑x✝ * ↑y✝) = toReal ↑x✝ * toReal ↑y✝
[PROOFSTEP]
norm_cast
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
[PROOFSTEP]

| top_pos _ h => simp [top_mul_coe_of_pos h]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
[PROOFSTEP]
simp [top_mul_coe_of_pos h]
[GOAL]
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
[PROOFSTEP]

| top_neg _ h => simp [top_mul_coe_of_neg h]
[GOAL]
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ toReal (⊤ * ↑x✝) = toReal ⊤ * toReal ↑x✝
[PROOFSTEP]
simp [top_mul_coe_of_neg h]
[GOAL]
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
[PROOFSTEP]

| pos_bot _ h => simp [coe_mul_bot_of_pos h]
[GOAL]
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
[PROOFSTEP]
simp [coe_mul_bot_of_pos h]
[GOAL]
case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
[PROOFSTEP]

| neg_bot _ h => simp [coe_mul_bot_of_neg h]
[GOAL]
case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ toReal (↑x✝ * ⊥) = toReal ↑x✝ * toReal ⊥
[PROOFSTEP]
simp [coe_mul_bot_of_neg h]
[GOAL]
x y : EReal
⊢ -x * y = -(x * y)
[PROOFSTEP]
induction x, y using induction₂_neg_left with
| top_zero| zero_top| zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top| top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
[GOAL]
x y : EReal
⊢ -x * y = -(x * y)
[PROOFSTEP]
induction x, y using induction₂_neg_left with
| top_zero => simp only [zero_mul, mul_zero, neg_zero]
| zero_top => simp only [zero_mul, mul_zero, neg_zero]
| zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top => rfl
| top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
[GOAL]
x y : EReal
⊢ -x * y = -(x * y)
[PROOFSTEP]
induction x, y using induction₂_neg_left with
| top_zero => simp only [zero_mul, mul_zero, neg_zero]
| zero_top => simp only [zero_mul, mul_zero, neg_zero]
| zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top => rfl
| top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
[GOAL]
case top_zero
⊢ -⊤ * 0 = -(⊤ * 0)
[PROOFSTEP]

| top_zero => simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case top_zero
⊢ -⊤ * 0 = -(⊤ * 0)
[PROOFSTEP]
simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case zero_top
⊢ -0 * ⊤ = -(0 * ⊤)
[PROOFSTEP]

| zero_top => simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case zero_top
⊢ -0 * ⊤ = -(0 * ⊤)
[PROOFSTEP]
simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case zero_bot
⊢ -0 * ⊥ = -(0 * ⊥)
[PROOFSTEP]

| zero_bot => simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case zero_bot
⊢ -0 * ⊥ = -(0 * ⊥)
[PROOFSTEP]
simp only [zero_mul, mul_zero, neg_zero]
[GOAL]
case top_top
⊢ -⊤ * ⊤ = -(⊤ * ⊤)
[PROOFSTEP]

| top_top => rfl
[GOAL]
case top_top
⊢ -⊤ * ⊤ = -(⊤ * ⊤)
[PROOFSTEP]
rfl
[GOAL]
case top_bot
⊢ -⊤ * ⊥ = -(⊤ * ⊥)
[PROOFSTEP]

| top_bot => rfl
[GOAL]
case top_bot
⊢ -⊤ * ⊥ = -(⊤ * ⊥)
[PROOFSTEP]
rfl
[GOAL]
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = -(-x✝ * y✝)
[PROOFSTEP]

| neg_left h => rw [h, neg_neg, neg_neg]
[GOAL]
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = -(-x✝ * y✝)
[PROOFSTEP]
rw [h, neg_neg, neg_neg]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ -↑x✝ * ↑y✝ = -(↑x✝ * ↑y✝)
[PROOFSTEP]

| coe_coe => norm_cast; exact neg_mul _ _
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ -↑x✝ * ↑y✝ = -(↑x✝ * ↑y✝)
[PROOFSTEP]
norm_cast
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)
[PROOFSTEP]
exact neg_mul _ _
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
[PROOFSTEP]

| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
[PROOFSTEP]
rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
[GOAL]
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -(↑x✝ * ⊤)
[PROOFSTEP]

| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
[GOAL]
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -(↑x✝ * ⊤)
[PROOFSTEP]
rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
[GOAL]
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
[PROOFSTEP]

| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
[GOAL]
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)
[PROOFSTEP]
rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
[GOAL]
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)
[PROOFSTEP]

| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
[GOAL]
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)
[PROOFSTEP]
rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
[GOAL]
x y : EReal
⊢ x * -y = -(x * y)
[PROOFSTEP]
rw [x.mul_comm, x.mul_comm]
[GOAL]
x y : EReal
⊢ -y * x = -(y * x)
[PROOFSTEP]
exact y.neg_mul x
[GOAL]
x : EReal
⊢ EReal.abs x = 0 ↔ x = 0
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case h_bot
⊢ EReal.abs ⊥ = 0 ↔ ⊥ = 0
[PROOFSTEP]
simp only [abs_bot, ENNReal.top_ne_zero, bot_ne_zero]
[GOAL]
case h_real
a✝ : ℝ
⊢ EReal.abs ↑a✝ = 0 ↔ ↑a✝ = 0
[PROOFSTEP]
simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
[GOAL]
case h_top
⊢ EReal.abs ⊤ = 0 ↔ ⊤ = 0
[PROOFSTEP]
simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]
[GOAL]
⊢ EReal.abs 0 = 0
[PROOFSTEP]
rw [abs_eq_zero_iff]
[GOAL]
x : ℝ
⊢ ↑(EReal.abs ↑x) = ↑|x|
[PROOFSTEP]
rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]
[GOAL]
x : ℝ
⊢ ↑↑(↑Real.nnabs x) = ↑↑(↑Real.nnabs x)
[PROOFSTEP]
rfl
[GOAL]
x : ℝ
⊢ EReal.abs (-↑x) = EReal.abs ↑x
[PROOFSTEP]
rw [abs_def, ← coe_neg, abs_def, abs_neg]
[GOAL]
x y : EReal
⊢ EReal.abs (x * y) = EReal.abs x * EReal.abs y
[PROOFSTEP]
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, abs_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
  rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
  exact h.ne'
| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
[GOAL]
x y : EReal
⊢ EReal.abs (x * y) = EReal.abs x * EReal.abs y
[PROOFSTEP]
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, abs_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
  rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
  exact h.ne'
| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
[GOAL]
case top_zero
⊢ EReal.abs (⊤ * 0) = EReal.abs ⊤ * EReal.abs 0
[PROOFSTEP]

| top_zero => simp only [zero_mul, mul_zero, abs_zero]
[GOAL]
case top_zero
⊢ EReal.abs (⊤ * 0) = EReal.abs ⊤ * EReal.abs 0
[PROOFSTEP]
simp only [zero_mul, mul_zero, abs_zero]
[GOAL]
case top_top
⊢ EReal.abs (⊤ * ⊤) = EReal.abs ⊤ * EReal.abs ⊤
[PROOFSTEP]

| top_top => rfl
[GOAL]
case top_top
⊢ EReal.abs (⊤ * ⊤) = EReal.abs ⊤ * EReal.abs ⊤
[PROOFSTEP]
rfl
[GOAL]
case symm
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (y✝ * x✝) = EReal.abs y✝ * EReal.abs x✝
[PROOFSTEP]

| symm h => rwa [mul_comm, EReal.mul_comm]
[GOAL]
case symm
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (y✝ * x✝) = EReal.abs y✝ * EReal.abs x✝
[PROOFSTEP]
rwa [mul_comm, EReal.mul_comm]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ EReal.abs (↑x✝ * ↑y✝) = EReal.abs ↑x✝ * EReal.abs ↑y✝
[PROOFSTEP]

| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ EReal.abs (↑x✝ * ↑y✝) = EReal.abs ↑x✝ * EReal.abs ↑y✝
[PROOFSTEP]
simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs (⊤ * ↑x✝) = EReal.abs ⊤ * EReal.abs ↑x✝
[PROOFSTEP]

| top_pos _ h =>
  rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
  rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
  exact h.ne'
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs (⊤ * ↑x✝) = EReal.abs ⊤ * EReal.abs ↑x✝
[PROOFSTEP]
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ EReal.abs ↑x✝ ≠ 0
[PROOFSTEP]
rw [Ne.def, abs_eq_zero_iff, coe_eq_zero]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0
[PROOFSTEP]
exact h.ne'
[GOAL]
case neg_left
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (-x✝ * y✝) = EReal.abs (-x✝) * EReal.abs y✝
[PROOFSTEP]

| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
[GOAL]
case neg_left
x✝ y✝ : EReal
h : EReal.abs (x✝ * y✝) = EReal.abs x✝ * EReal.abs y✝
⊢ EReal.abs (-x✝ * y✝) = EReal.abs (-x✝) * EReal.abs y✝
[PROOFSTEP]
rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
[GOAL]
x : ℝ
⊢ ↑sign ↑x = ↑sign x
[PROOFSTEP]
simp only [sign, OrderHom.coe_mk, EReal.coe_pos, EReal.coe_neg']
[GOAL]
x : SignType
⊢ ↑↑x = ↑x
[PROOFSTEP]
cases x
[GOAL]
case zero
⊢ ↑↑SignType.zero = ↑SignType.zero
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ ↑↑SignType.neg = ↑SignType.neg
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ ↑↑SignType.pos = ↑SignType.pos
[PROOFSTEP]
rfl
[GOAL]
x : ℝ
⊢ ↑sign (-↑x) = -↑sign ↑x
[PROOFSTEP]
rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]
[GOAL]
x y : EReal
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, sign_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h => rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
[GOAL]
x y : EReal
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, sign_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h => rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
[GOAL]
case top_zero
⊢ ↑sign (⊤ * 0) = ↑sign ⊤ * ↑sign 0
[PROOFSTEP]

| top_zero => simp only [zero_mul, mul_zero, sign_zero]
[GOAL]
case top_zero
⊢ ↑sign (⊤ * 0) = ↑sign ⊤ * ↑sign 0
[PROOFSTEP]
simp only [zero_mul, mul_zero, sign_zero]
[GOAL]
case top_top
⊢ ↑sign (⊤ * ⊤) = ↑sign ⊤ * ↑sign ⊤
[PROOFSTEP]

| top_top => rfl
[GOAL]
case top_top
⊢ ↑sign (⊤ * ⊤) = ↑sign ⊤ * ↑sign ⊤
[PROOFSTEP]
rfl
[GOAL]
case symm
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (y✝ * x✝) = ↑sign y✝ * ↑sign x✝
[PROOFSTEP]

| symm h => rwa [mul_comm, EReal.mul_comm]
[GOAL]
case symm
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (y✝ * x✝) = ↑sign y✝ * ↑sign x✝
[PROOFSTEP]
rwa [mul_comm, EReal.mul_comm]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ ↑sign (↑x✝ * ↑y✝) = ↑sign ↑x✝ * ↑sign ↑y✝
[PROOFSTEP]

| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
[GOAL]
case coe_coe
x✝ y✝ : ℝ
⊢ ↑sign (↑x✝ * ↑y✝) = ↑sign ↑x✝ * ↑sign ↑y✝
[PROOFSTEP]
simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ↑sign (⊤ * ↑x✝) = ↑sign ⊤ * ↑sign ↑x✝
[PROOFSTEP]

| top_pos _ h => rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
[GOAL]
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ↑sign (⊤ * ↑x✝) = ↑sign ⊤ * ↑sign ↑x✝
[PROOFSTEP]
rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
[GOAL]
case neg_left
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (-x✝ * y✝) = ↑sign (-x✝) * ↑sign y✝
[PROOFSTEP]

| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
[GOAL]
case neg_left
x✝ y✝ : EReal
h : ↑sign (x✝ * y✝) = ↑sign x✝ * ↑sign y✝
⊢ ↑sign (-x✝ * y✝) = ↑sign (-x✝) * ↑sign y✝
[PROOFSTEP]
rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
[GOAL]
⊢ ↑(↑sign ⊥) * ↑(EReal.abs ⊥) = ⊥
[PROOFSTEP]
simp
[GOAL]
⊢ ↑(↑sign ⊤) * ↑(EReal.abs ⊤) = ⊤
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ ↑(↑sign ↑x) * ↑(EReal.abs ↑x) = ↑x
[PROOFSTEP]
rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]
[GOAL]
x : EReal
⊢ ↑(EReal.abs x) * ↑(↑sign x) = x
[PROOFSTEP]
rw [EReal.mul_comm, EReal.sign_mul_abs]
[GOAL]
x y : EReal
⊢ EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : EReal
⊢ EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y → x = y
[PROOFSTEP]
rintro ⟨habs, hsign⟩
[GOAL]
case mp.intro
x y : EReal
habs : EReal.abs x = EReal.abs y
hsign : ↑sign x = ↑sign y
⊢ x = y
[PROOFSTEP]
rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
[GOAL]
case mpr
x y : EReal
⊢ x = y → EReal.abs x = EReal.abs y ∧ ↑sign x = ↑sign y
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
x : EReal
⊢ EReal.abs x = EReal.abs x ∧ ↑sign x = ↑sign x
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
x y : EReal
⊢ x ≤ y ↔
    ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : EReal
⊢ x ≤ y →
    ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
intro h
[GOAL]
case mp
x y : EReal
h : x ≤ y
⊢ ↑sign x < ↑sign y ∨
    ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
      ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
        ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
[GOAL]
case mp
x y : EReal
h : x ≤ y
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
[GOAL]
case mp
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
⊢ ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
      ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
cases hy : sign y
[GOAL]
case mp.zero
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.zero
⊢ ↑sign x = SignType.neg ∧ SignType.zero = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ SignType.zero = SignType.zero ∨
      ↑sign x = SignType.pos ∧ SignType.zero = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
rw [hs, hy] at h ⊢
[GOAL]
case mp.neg
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ ↑sign x = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ SignType.neg = SignType.zero ∨
      ↑sign x = SignType.pos ∧ SignType.neg = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
rw [hs, hy] at h ⊢
[GOAL]
case mp.pos
x y : EReal
h : ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ ↑sign x = SignType.neg ∧ SignType.pos = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    ↑sign x = SignType.zero ∧ SignType.pos = SignType.zero ∨
      ↑sign x = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
rw [hs, hy] at h ⊢
[GOAL]
case mp.zero
x y : EReal
h : ↑SignType.zero * ↑(EReal.abs x) ≤ ↑SignType.zero * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.zero
⊢ SignType.zero = SignType.neg ∧ SignType.zero = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.zero = SignType.zero ∧ SignType.zero = SignType.zero ∨
      SignType.zero = SignType.pos ∧ SignType.zero = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
simp
[GOAL]
case mp.neg
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.neg = SignType.zero ∧ SignType.neg = SignType.zero ∨
      SignType.neg = SignType.pos ∧ SignType.neg = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
left
[GOAL]
case mp.neg.h
x y : EReal
h : ↑SignType.neg * ↑(EReal.abs x) ≤ ↑SignType.neg * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.neg
⊢ SignType.neg = SignType.neg ∧ SignType.neg = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
[PROOFSTEP]
simpa using h
[GOAL]
case mp.pos
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.neg ∧ SignType.pos = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
    SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
      SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
right
[GOAL]
case mp.pos.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.zero ∧ SignType.pos = SignType.zero ∨
    SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
right
[GOAL]
case mp.pos.h.h
x y : EReal
h : ↑SignType.pos * ↑(EReal.abs x) ≤ ↑SignType.pos * ↑(EReal.abs y)
hs : ↑sign x = ↑sign y
hy : ↑sign y = SignType.pos
⊢ SignType.pos = SignType.pos ∧ SignType.pos = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
x y : EReal
⊢ ↑sign x < ↑sign y ∨
      ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x ∨
        ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero ∨
          ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y →
    x ≤ y
[PROOFSTEP]
rintro (h | h | h | h)
[GOAL]
case mpr.inl
x y : EReal
h : ↑sign x < ↑sign y
⊢ x ≤ y
[PROOFSTEP]
exact (sign.monotone.reflect_lt h).le
[GOAL]
case mpr.inr.inl
x y : EReal
h : ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
⊢ x ≤ y
case mpr.inr.inr.inl
x y : EReal
h : ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero
⊢ x ≤ y
case mpr.inr.inr.inr x y : EReal h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y ⊢ x ≤ y
[PROOFSTEP]
all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]
[GOAL]
case mpr.inr.inl
x y : EReal
h : ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
⊢ x ≤ y
[PROOFSTEP]
rw [← x.sign_mul_abs, ← y.sign_mul_abs]
[GOAL]
case mpr.inr.inl
x y : EReal
h : ↑sign x = SignType.neg ∧ ↑sign y = SignType.neg ∧ EReal.abs y ≤ EReal.abs x
⊢ ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
[PROOFSTEP]
simp [h]
[GOAL]
case mpr.inr.inr.inl
x y : EReal
h : ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero
⊢ x ≤ y
[PROOFSTEP]
rw [← x.sign_mul_abs, ← y.sign_mul_abs]
[GOAL]
case mpr.inr.inr.inl
x y : EReal
h : ↑sign x = SignType.zero ∧ ↑sign y = SignType.zero
⊢ ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
[PROOFSTEP]
simp [h]
[GOAL]
case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ x ≤ y
[PROOFSTEP]
rw [← x.sign_mul_abs, ← y.sign_mul_abs]
[GOAL]
case mpr.inr.inr.inr
x y : EReal
h : ↑sign x = SignType.pos ∧ ↑sign y = SignType.pos ∧ EReal.abs x ≤ EReal.abs y
⊢ ↑(↑sign x) * ↑(EReal.abs x) ≤ ↑(↑sign y) * ↑(EReal.abs y)
[PROOFSTEP]
simp [h]
[GOAL]
src✝ : MulZeroOneClass EReal := inferInstanceAs (MulZeroOneClass EReal)
x y z : EReal
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
rw [← sign_eq_and_abs_eq_iff_eq]
[GOAL]
src✝ : MulZeroOneClass EReal := inferInstanceAs (MulZeroOneClass EReal)
x y z : EReal
⊢ EReal.abs (x * y * z) = EReal.abs (x * (y * z)) ∧ ↑sign (x * y * z) = ↑sign (x * (y * z))
[PROOFSTEP]
simp only [mul_assoc, abs_mul, eq_self_iff_true, sign_mul, and_self_iff]
[GOAL]
⊢ Covariant { x // 0 < x } EReal (fun x y => ↑x * y) fun x x_1 => x ≤ x_1
[PROOFSTEP]
rintro ⟨x, x0⟩ a b h
[GOAL]
case mk
x : EReal
x0 : 0 < x
a b : EReal
h : a ≤ b
⊢ (fun x y => ↑x * y) { val := x, property := x0 } a ≤ (fun x y => ↑x * y) { val := x, property := x0 } b
[PROOFSTEP]
simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢
[GOAL]
case mk
x : EReal
x0 : 0 < x
a b : EReal
h :
  ↑sign a < ↑sign b ∨
    ↑sign a = SignType.neg ∧ ↑sign b = SignType.neg ∧ EReal.abs b ≤ EReal.abs a ∨
      ↑sign a = SignType.zero ∧ ↑sign b = SignType.zero ∨
        ↑sign a = SignType.pos ∧ ↑sign b = SignType.pos ∧ EReal.abs a ≤ EReal.abs b
⊢ ↑sign a < ↑sign b ∨
    ↑sign a = SignType.neg ∧ ↑sign b = SignType.neg ∧ EReal.abs x * EReal.abs b ≤ EReal.abs x * EReal.abs a ∨
      ↑sign a = SignType.zero ∧ ↑sign b = SignType.zero ∨
        ↑sign a = SignType.pos ∧ ↑sign b = SignType.pos ∧ EReal.abs x * EReal.abs a ≤ EReal.abs x * EReal.abs b
[PROOFSTEP]
exact
  h.imp_right <|
    Or.imp (And.imp_right <| And.imp_right (mul_le_mul_left' · _)) <|
      Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_left' · _)