Theorem: ℤθ.unit_sq (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ ↑(unit ^ 2) = { f := -5, g := -14, h := -4 }
Tactic:
rw [pow_two]
State after:
a b c : ℤθ
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Tactic:
have h1 : ((unit * unit : ℤθˣ) : ℤθ) = ((unit : ℤθˣ) : ℤθ) * ((unit : ℤθˣ) : ℤθ) := by rfl
State after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Tactic:
rw [h1]
State after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑unit * ↑unit = { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑unit * ↑unit = { f := -5, g := -14, h := -4 }
Tactic:
rw [unit_l]
State after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 } = { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 } = { f := -5, g := -14, h := -4 }
Tactic:
rw [hMul_mule_3]
State after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g } =
    { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g } =
    { f := -5, g := -14, h := -4 }
Tactic:
dsimp
State after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1 * -1 + 6 * -1 * -1 - 2 * -3 * -1 - 2 * -1 * -3,
      g := -1 * -3 + -3 * -1 + 16 * -1 * -1 - 6 * -3 * -1 - 6 * -1 * -3,
      h := -1 * -1 + -1 * -1 + -3 * -3 + 3 * -1 * -1 - 3 * -3 * -1 - 3 * -1 * -3 } =
    { f := -5, g := -14, h := -4 }

State before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1 * -1 + 6 * -1 * -1 - 2 * -3 * -1 - 2 * -1 * -3,
      g := -1 * -3 + -3 * -1 + 16 * -1 * -1 - 6 * -3 * -1 - 6 * -1 * -3,
      h := -1 * -1 + -1 * -1 + -3 * -3 + 3 * -1 * -1 - 3 * -3 * -1 - 3 * -1 * -3 } =
    { f := -5, g := -14, h := -4 }
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
⊢ ↑(unit * unit) = ↑unit * ↑unit
Tactic:
rfl
State after:
no goals