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

State before:
a b c : ℤθ
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }
Tactic:
have elem : 9 = 3 + 3 + 3 := by norm_num;
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ 9 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [elem]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3 + 3) = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3 + 3) = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [pow_add]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
have elem1 : 3 + 3 = 6 := by norm_num;
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ (3 + 3) * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [elem1]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * ↑unit ^ 3 = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [unit_cubed]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ ↑unit ^ 6 * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [unit_pow_six]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901, g := -4842, h := -336 } * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901, g := -4842, h := -336 } * { f := -23, g := -63, h := -15 } = { f := -113633, g := -251019, h := 75015 }
Tactic:
rw [hMul_mule_3]
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ {
      f :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ {
      f :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -113633, g := -251019, h := 75015 }
Tactic:
dsimp
State after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901 * -23 + 6 * -336 * -15 - 2 * -4842 * -15 - 2 * -336 * -63,
      g := -1901 * -63 + -4842 * -23 + 16 * -336 * -15 - 6 * -4842 * -15 - 6 * -336 * -63,
      h := -1901 * -15 + -336 * -23 + -4842 * -63 + 3 * -336 * -15 - 3 * -4842 * -15 - 3 * -336 * -63 } =
    { f := -113633, g := -251019, h := 75015 }

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901 * -23 + 6 * -336 * -15 - 2 * -4842 * -15 - 2 * -336 * -63,
      g := -1901 * -63 + -4842 * -23 + 16 * -336 * -15 - 6 * -4842 * -15 - 6 * -336 * -63,
      h := -1901 * -15 + -336 * -23 + -4842 * -63 + 3 * -336 * -15 - 3 * -4842 * -15 - 3 * -336 * -63 } =
    { f := -113633, g := -251019, h := 75015 }
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℤθ
⊢ 9 = 3 + 3 + 3
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ 3 + 3 = 6
Tactic:
norm_num
State after:
no goals