Theorem: ℤω.x_from_coe (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ ↑a.x = (OneHom.toFun (↑↑inclusion) a).re + rt3⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x =
    (OneHom.toFun ↑↑inclusion { x := x, y := y }).re + rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x =
    (OneHom.toFun ↑↑inclusion { x := x, y := y }).re + rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Tactic:
simp only [coe_of_mk]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x - ↑y / 2 + rt3⁻¹ * (↑y * rt3 / 2)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x - ↑y / 2 + rt3⁻¹ * (↑y * rt3 / 2)
Tactic:
ring_nf
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * rt3 * rt3⁻¹ * (↑(ofNat 1) / ↑2) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * rt3 * rt3⁻¹ * (↑(ofNat 1) / ↑2) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Tactic:
rw [mul_assoc,mul_assoc,mul_comm rt3]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Tactic:
simp only [ofNat_eq_coe, Nat.cast_one, cast_one, Nat.cast_ofNat, one_div, cast_negOfNat, mul_neg,
  mul_one, neg_mul]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * 2⁻¹ * rt3) + -(↑y * 2⁻¹)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * 2⁻¹ * rt3) + -(↑y * 2⁻¹)
Tactic:
rw [mul_comm ((rt3)⁻¹),mul_assoc]
State after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (2⁻¹ * (rt3⁻¹ * rt3)) + -(↑y * 2⁻¹)

State before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (2⁻¹ * (rt3⁻¹ * rt3)) + -(↑y * 2⁻¹)
Tactic:
simp only [ne_eq, sqrt3_inv_hMul_self, mul_one, add_neg_cancel_right]
State after:
no goals