Theorem: new.to_and_from (LoVe/Lectures/Complex.lean)

State before:
p : Polar
hpmag : p.magnitude > 0
hpangle1 : -(Real.pi / 2) < p.angle
hpangle2 : p.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex p) = p
Tactic:
cases' p with pangle pmag
State after:
case mk
pangle pmag : ℝ
hpmag : { angle := pangle, magnitude := pmag }.magnitude > 0
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }

State before:
case mk
pangle pmag : ℝ
hpmag : { angle := pangle, magnitude := pmag }.magnitude > 0
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Tactic:
simp at hpmag
State after:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }

State before:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Tactic:
simp [Complex.toPolar, Polar.toComplex]
State after:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle ∧
    Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

State before:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle ∧
    Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
constructor
State after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle

case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

State before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle

case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
{ rw [mul_div_mul_left]
  rw [← Real.tan_eq_sin_div_cos]
  rw [Real.arctan_tan]
  all_goals aesop }
State after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

State before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
{ suffices : (pmag * Real.cos pangle)^2 + (pmag * Real.sin pangle)^2 = pmag^2
  rw [this]
  rw [Real.sqrt_sq] 
  linarith
  have h : (Real.sin pangle)^2 + (Real.cos pangle)^2 = 1 :=
    Real.sin_sq_add_cos_sq pangle
  linear_combination pmag ^ 2 * h }
State after:
no goals

State before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle
Tactic:
rw [mul_div_mul_left]
State after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.sin pangle / Real.cos pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0

State before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.sin pangle / Real.cos pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
rw [← Real.tan_eq_sin_div_cos]
State after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.tan pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0

State before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.tan pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
rw [Real.arctan_tan]
State after:
case mk.left.hx₁
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ -(Real.pi / 2) < pangle

case mk.left.hx₂
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pangle < Real.pi / 2

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0

State before:
case mk.left.hx₁
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ -(Real.pi / 2) < pangle

case mk.left.hx₂
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pangle < Real.pi / 2

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
all_goals aesop
State after:
no goals

State before:
case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
aesop
State after:
no goals

State before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
suffices : (pmag * Real.cos pangle)^2 + (pmag * Real.sin pangle)^2 = pmag^2
State after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2

State before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
rw [this]
State after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt (pmag ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2

State before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt (pmag ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
rw [Real.sqrt_sq]
State after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ 0 ≤ pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2

State before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ 0 ≤ pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
linarith
State after:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2

State before:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
have h : (Real.sin pangle)^2 + (Real.cos pangle)^2 = 1 :=
  Real.sin_sq_add_cos_sq pangle
State after:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
h : Real.sin pangle ^ 2 + Real.cos pangle ^ 2 = 1
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2

State before:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
h : Real.sin pangle ^ 2 + Real.cos pangle ^ 2 = 1
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
linear_combination pmag ^ 2 * h
State after:
no goals