Physlib.Mathematics.RatComplexNum

Physlib
Mathematics
RatComplexNum

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Complex.Basic

Rational complex numbers

@[expose] public section

Rational complex numbers. This type is mainly used when decidability is needed.

The real part of a RatComplexNum.

The imaginary part of a RatComplexNum.

              structure RatComplexNum where  fst : ℚ  snd : ℚ

@[ext]
lemma ext {x y : RatComplexNum} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y := byx:RatComplexNumy:RatComplexNumh1:x.fst = y.fsth2:x.snd = y.snd⊢ x = y
  cases xmky:RatComplexNumfst✝:ℚsnd✝:ℚh1:{ fst := fst✝, snd := snd✝ }.fst = y.fsth2:{ fst := fst✝, snd := snd✝ }.snd = y.snd⊢ { fst := fst✝, snd := snd✝ } = y
  cases ymk.mkfst✝¹:ℚsnd✝¹:ℚfst✝:ℚsnd✝:ℚh1:{ fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fsth2:{ fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
  simp only at h1 h2mk.mkfst✝¹:ℚsnd✝¹:ℚfst✝:ℚsnd✝:ℚh1:fst✝¹ = fst✝h2:snd✝¹ = snd✝⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
  subst h1 h2mk.mkfst✝:ℚsnd✝:ℚ⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
  rflAll goals completed! 🐙

The equivalence as a type of RatComplexNum with ℚ × ℚ.

def equivToProd : RatComplexNum ≃ ℚ × ℚ where
  toFun := fun x => (x.1, x.2)
  invFun := fun x => ⟨x.1, x.2⟩
  left_inv := by⊢ Function.LeftInverse (fun x => { fst := x.1, snd := x.2 }) fun x => (x.fst, x.snd)
    intro xx:RatComplexNum⊢ (fun x => { fst := x.1, snd := x.2 }) ((fun x => (x.fst, x.snd)) x) = x
    cases xmkfst✝:ℚsnd✝:ℚ⊢ (fun x => { fst := x.1, snd := x.2 }) ((fun x => (x.fst, x.snd)) { fst := fst✝, snd := snd✝ }) =
  { fst := fst✝, snd := snd✝ }
    rflAll goals completed! 🐙
  right_inv := by⊢ Function.RightInverse (fun x => { fst := x.1, snd := x.2 }) fun x => (x.fst, x.snd)
    intro xx:ℚ × ℚ⊢ (fun x => (x.fst, x.snd)) ((fun x => { fst := x.1, snd := x.2 }) x) = x
    cases xmkfst✝:ℚsnd✝:ℚ⊢ (fun x => (x.fst, x.snd)) ((fun x => { fst := x.1, snd := x.2 }) (fst✝, snd✝)) = (fst✝, snd✝)
    rflAll goals completed! 🐙

              instance : DecidableEq RatComplexNum := Equiv.decidableEq equivToProdinstance : Add RatComplexNum where
  add := fun x y => ⟨x.fst + y.fst, x.snd + y.snd⟩@[simp]
lemma add_fst (x y : RatComplexNum) : (x + y).fst = x.fst + y.fst := rfl@[simp]
lemma add_snd (x y : RatComplexNum) : (x + y).snd = x.snd + y.snd := rflinstance : AddCommGroup RatComplexNum where
  add_assoc := by⊢ ∀ (a b c : RatComplexNum), a + b + c = a + (b + c)
    intro a b ca:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ a + b + c = a + (b + c)
    exth1a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ (a + b + c).fst = (a + (b + c)).fsth2a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ (a + b + c).snd = (a + (b + c)).snd
    ·h1a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ (a + b + c).fst = (a + (b + c)).fst simp only [add_fst]h1a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ a.fst + b.fst + c.fst = a.fst + (b.fst + c.fst)
      ringAll goals completed! 🐙
    ·h2a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ (a + b + c).snd = (a + (b + c)).snd simp only [add_snd]h2a:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ a.snd + b.snd + c.snd = a.snd + (b.snd + c.snd)
      ringAll goals completed! 🐙
  zero := ⟨0, 0⟩
  zero_add := by⊢ ∀ (a : RatComplexNum), 0 + a = a
    intro aa:RatComplexNum⊢ 0 + a = a
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ 0 + { fst := a1, snd := a2 } = { fst := a1, snd := a2 }
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ (0 + { fst := a1, snd := a2 }).fst = { fst := a1, snd := a2 }.fsth2a:RatComplexNuma1:ℚa2:ℚ⊢ (0 + { fst := a1, snd := a2 }).snd = { fst := a1, snd := a2 }.snd
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ (0 + { fst := a1, snd := a2 }).fst = { fst := a1, snd := a2 }.fst change 0 + a1 = a1h1a:RatComplexNuma1:ℚa2:ℚ⊢ 0 + a1 = a1
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ (0 + { fst := a1, snd := a2 }).snd = { fst := a1, snd := a2 }.snd change 0 + a2 = a2h2a:RatComplexNuma1:ℚa2:ℚ⊢ 0 + a2 = a2
        simpAll goals completed! 🐙
  add_zero := by⊢ ∀ (a : RatComplexNum), a + 0 = a
    intro aa:RatComplexNum⊢ a + 0 = a
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ { fst := a1, snd := a2 } + 0 = { fst := a1, snd := a2 }
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } + 0).fst = { fst := a1, snd := a2 }.fsth2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } + 0).snd = { fst := a1, snd := a2 }.snd
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } + 0).fst = { fst := a1, snd := a2 }.fst change a1 + 0 = a1h1a:RatComplexNuma1:ℚa2:ℚ⊢ a1 + 0 = a1
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } + 0).snd = { fst := a1, snd := a2 }.snd change a2 + 0 = a2h2a:RatComplexNuma1:ℚa2:ℚ⊢ a2 + 0 = a2
        simpAll goals completed! 🐙
  neg := fun x => ⟨-x.fst, -x.snd⟩
  nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩
  zsmul := fun n x => ⟨n • x.1, n • x.2⟩
  neg_add_cancel := by⊢ ∀ (a : RatComplexNum), { fst := -a.fst, snd := -a.snd } + a = 0
    intro aa:RatComplexNum⊢ { fst := -a.fst, snd := -a.snd } + a = 0
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ { fst := -{ fst := a1, snd := a2 }.fst, snd := -{ fst := a1, snd := a2 }.snd } + { fst := a1, snd := a2 } = 0
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := -{ fst := a1, snd := a2 }.fst, snd := -{ fst := a1, snd := a2 }.snd } + { fst := a1, snd := a2 }).fst = fst 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := -{ fst := a1, snd := a2 }.fst, snd := -{ fst := a1, snd := a2 }.snd } + { fst := a1, snd := a2 }).snd = snd 0
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := -{ fst := a1, snd := a2 }.fst, snd := -{ fst := a1, snd := a2 }.snd } + { fst := a1, snd := a2 }).fst = fst 0 change -a1 + a1 = 0h1a:RatComplexNuma1:ℚa2:ℚ⊢ -a1 + a1 = 0
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := -{ fst := a1, snd := a2 }.fst, snd := -{ fst := a1, snd := a2 }.snd } + { fst := a1, snd := a2 }).snd = snd 0 change -a2 + a2 = 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ -a2 + a2 = 0
        simpAll goals completed! 🐙
  add_comm := by⊢ ∀ (a b : RatComplexNum), a + b = b + a
    intro x yx:RatComplexNumy:RatComplexNum⊢ x + y = y + x
    exth1x:RatComplexNumy:RatComplexNum⊢ (x + y).fst = (y + x).fsth2x:RatComplexNumy:RatComplexNum⊢ (x + y).snd = (y + x).snd
    ·h1x:RatComplexNumy:RatComplexNum⊢ (x + y).fst = (y + x).fst simp only [add_fst]h1x:RatComplexNumy:RatComplexNum⊢ x.fst + y.fst = y.fst + x.fst
      ringAll goals completed! 🐙
    ·h2x:RatComplexNumy:RatComplexNum⊢ (x + y).snd = (y + x).snd simp only [add_snd]h2x:RatComplexNumy:RatComplexNum⊢ x.snd + y.snd = y.snd + x.snd
      ringAll goals completed! 🐙
  nsmul_zero := by⊢ ∀ (x : RatComplexNum), 0 • x = 0 intro xx:RatComplexNum⊢ 0 • x = 0; exth1x:RatComplexNum⊢ (0 • x).fst = fst 0h2x:RatComplexNum⊢ (0 • x).snd = snd 0 <;>h1x:RatComplexNum⊢ (0 • x).fst = fst 0h2x:RatComplexNum⊢ (0 • x).snd = snd 0 exact zero_nsmul _All goals completed! 🐙
  nsmul_succ := by⊢ ∀ (n : ℕ) (x : RatComplexNum), (n + 1) • x = n • x + x intro n xn:ℕx:RatComplexNum⊢ (n + 1) • x = n • x + x; exth1n:ℕx:RatComplexNum⊢ ((n + 1) • x).fst = (n • x + x).fsth2n:ℕx:RatComplexNum⊢ ((n + 1) • x).snd = (n • x + x).snd <;>h1n:ℕx:RatComplexNum⊢ ((n + 1) • x).fst = (n • x + x).fsth2n:ℕx:RatComplexNum⊢ ((n + 1) • x).snd = (n • x + x).snd exact succ_nsmul _ _All goals completed! 🐙
  zsmul_zero' := by⊢ ∀ (a : RatComplexNum), 0 • a = 0 intro aa:RatComplexNum⊢ 0 • a = 0; exth1a:RatComplexNum⊢ (0 • a).fst = fst 0h2a:RatComplexNum⊢ (0 • a).snd = snd 0 <;>h1a:RatComplexNum⊢ (0 • a).fst = fst 0h2a:RatComplexNum⊢ (0 • a).snd = snd 0 exact zero_zsmul _All goals completed! 🐙
  zsmul_succ' := by⊢ ∀ (n : ℕ) (a : RatComplexNum), ↑n.succ • a = ↑n • a + a
    intro n an:ℕa:RatComplexNum⊢ ↑n.succ • a = ↑n • a + a
    exth1n:ℕa:RatComplexNum⊢ (↑n.succ • a).fst = (↑n • a + a).fsth2n:ℕa:RatComplexNum⊢ (↑n.succ • a).snd = (↑n • a + a).snd
    ·h1n:ℕa:RatComplexNum⊢ (↑n.succ • a).fst = (↑n • a + a).fst show ((n : ℤ) + 1) • a.fst = (n : ℤ) • a.fst + a.fsth1n:ℕa:RatComplexNum⊢ (↑n + 1) • a.fst = ↑n • a.fst + a.fst
      exact add_one_zsmul _ _All goals completed! 🐙
    ·h2n:ℕa:RatComplexNum⊢ (↑n.succ • a).snd = (↑n • a + a).snd show ((n : ℤ) + 1) • a.snd = (n : ℤ) • a.snd + a.sndh2n:ℕa:RatComplexNum⊢ (↑n + 1) • a.snd = ↑n • a.snd + a.snd
      exact add_one_zsmul _ _All goals completed! 🐙
  zsmul_neg' := by⊢ ∀ (n : ℕ) (a : RatComplexNum), Int.negSucc n • a = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd } intro n an:ℕa:RatComplexNum⊢ Int.negSucc n • a = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd }; exth1n:ℕa:RatComplexNum⊢ (Int.negSucc n • a).fst = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd }.fsth2n:ℕa:RatComplexNum⊢ (Int.negSucc n • a).snd = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd }.snd <;>h1n:ℕa:RatComplexNum⊢ (Int.negSucc n • a).fst = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd }.fsth2n:ℕa:RatComplexNum⊢ (Int.negSucc n • a).snd = { fst := -(↑n.succ • a).fst, snd := -(↑n.succ • a).snd }.snd exact negSucc_zsmul _ _All goals completed! 🐙instance : Mul RatComplexNum where
  mul := fun x y => ⟨x.fst * y.fst - x.snd * y.snd, x.fst * y.snd + x.snd * y.fst⟩@[simp]
lemma mul_fst (x y : RatComplexNum) : (x * y).fst = x.fst * y.fst - x.snd * y.snd := rfl@[simp]
lemma mul_snd (x y : RatComplexNum) : (x * y).snd = x.fst * y.snd + x.snd * y.fst := rflinstance : Ring RatComplexNum where
  one := ⟨1, 0⟩
  mul_assoc := by⊢ ∀ (a b c : RatComplexNum), a * b * c = a * (b * c)
    intro x y zx:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ x * y * z = x * (y * z)
    exth1x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x * y * z).fst = (x * (y * z)).fsth2x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x * y * z).snd = (x * (y * z)).snd
    ·h1x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x * y * z).fst = (x * (y * z)).fst simp only [mul_fst, mul_snd]h1x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x.fst * y.fst - x.snd * y.snd) * z.fst - (x.fst * y.snd + x.snd * y.fst) * z.snd =
  x.fst * (y.fst * z.fst - y.snd * z.snd) - x.snd * (y.fst * z.snd + y.snd * z.fst)
      ringAll goals completed! 🐙
    ·h2x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x * y * z).snd = (x * (y * z)).snd simp only [mul_fst, mul_snd]h2x:RatComplexNumy:RatComplexNumz:RatComplexNum⊢ (x.fst * y.fst - x.snd * y.snd) * z.snd + (x.fst * y.snd + x.snd * y.fst) * z.fst =
  x.fst * (y.fst * z.snd + y.snd * z.fst) + x.snd * (y.fst * z.fst - y.snd * z.snd)
      ringAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : RatComplexNum), 1 * a = a
    intro xx:RatComplexNum⊢ 1 * x = x
    match x with
    | ⟨x1, x2⟩ =>x:RatComplexNumx1:ℚx2:ℚ⊢ 1 * { fst := x1, snd := x2 } = { fst := x1, snd := x2 }
      exth1x:RatComplexNumx1:ℚx2:ℚ⊢ (1 * { fst := x1, snd := x2 }).fst = { fst := x1, snd := x2 }.fsth2x:RatComplexNumx1:ℚx2:ℚ⊢ (1 * { fst := x1, snd := x2 }).snd = { fst := x1, snd := x2 }.snd
      ·h1x:RatComplexNumx1:ℚx2:ℚ⊢ (1 * { fst := x1, snd := x2 }).fst = { fst := x1, snd := x2 }.fst change 1 * x1 - 0 * x2 = x1h1x:RatComplexNumx1:ℚx2:ℚ⊢ 1 * x1 - 0 * x2 = x1
        simpAll goals completed! 🐙
      ·h2x:RatComplexNumx1:ℚx2:ℚ⊢ (1 * { fst := x1, snd := x2 }).snd = { fst := x1, snd := x2 }.snd change 1 * x2 + 0 * x1 = x2h2x:RatComplexNumx1:ℚx2:ℚ⊢ 1 * x2 + 0 * x1 = x2
        simpAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : RatComplexNum), a * 1 = a
    intro xx:RatComplexNum⊢ x * 1 = x
    match x with
    | ⟨x1, x2⟩ =>x:RatComplexNumx1:ℚx2:ℚ⊢ { fst := x1, snd := x2 } * 1 = { fst := x1, snd := x2 }
      exth1x:RatComplexNumx1:ℚx2:ℚ⊢ ({ fst := x1, snd := x2 } * 1).fst = { fst := x1, snd := x2 }.fsth2x:RatComplexNumx1:ℚx2:ℚ⊢ ({ fst := x1, snd := x2 } * 1).snd = { fst := x1, snd := x2 }.snd
      ·h1x:RatComplexNumx1:ℚx2:ℚ⊢ ({ fst := x1, snd := x2 } * 1).fst = { fst := x1, snd := x2 }.fst change x1 * 1 - x2 * 0 = x1h1x:RatComplexNumx1:ℚx2:ℚ⊢ x1 * 1 - x2 * 0 = x1
        simpAll goals completed! 🐙
      ·h2x:RatComplexNumx1:ℚx2:ℚ⊢ ({ fst := x1, snd := x2 } * 1).snd = { fst := x1, snd := x2 }.snd change x1 * 0 + x2 * 1 = x2h2x:RatComplexNumx1:ℚx2:ℚ⊢ x1 * 0 + x2 * 1 = x2
        simpAll goals completed! 🐙
  left_distrib := by⊢ ∀ (a b c : RatComplexNum), a * (b + c) = a * b + a * c
    intro a b ca:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ a * (b + c) = a * b + a * c
    match a, b, c with
    | ⟨a1, a2⟩, ⟨b1, b2⟩, ⟨c1, c2⟩ =>a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ { fst := a1, snd := a2 } * ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) =
  { fst := a1, snd := a2 } * { fst := b1, snd := b2 } + { fst := a1, snd := a2 } * { fst := c1, snd := c2 }
      exth1a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ ({ fst := a1, snd := a2 } * ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 })).fst =
  ({ fst := a1, snd := a2 } * { fst := b1, snd := b2 } + { fst := a1, snd := a2 } * { fst := c1, snd := c2 }).fsth2a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ ({ fst := a1, snd := a2 } * ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 })).snd =
  ({ fst := a1, snd := a2 } * { fst := b1, snd := b2 } + { fst := a1, snd := a2 } * { fst := c1, snd := c2 }).snd
      ·h1a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ ({ fst := a1, snd := a2 } * ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 })).fst =
  ({ fst := a1, snd := a2 } * { fst := b1, snd := b2 } + { fst := a1, snd := a2 } * { fst := c1, snd := c2 }).fst change a1 * (b1 + c1) - a2 * (b2 + c2) =
          (a1 * b1 - a2 * b2) + (a1 * c1 - a2 * c2)h1a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ a1 * (b1 + c1) - a2 * (b2 + c2) = a1 * b1 - a2 * b2 + (a1 * c1 - a2 * c2)
        ringAll goals completed! 🐙
      ·h2a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ ({ fst := a1, snd := a2 } * ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 })).snd =
  ({ fst := a1, snd := a2 } * { fst := b1, snd := b2 } + { fst := a1, snd := a2 } * { fst := c1, snd := c2 }).snd change a1 * (b2 + c2) + a2 * (b1 + c1) =
          (a1 * b2 + a2 * b1) + (a1 * c2 + a2 * c1)h2a:RatComplexNumb:RatComplexNumc:RatComplexNuma1:ℚa2:ℚb1:ℚb2:ℚc1:ℚc2:ℚ⊢ a1 * (b2 + c2) + a2 * (b1 + c1) = a1 * b2 + a2 * b1 + (a1 * c2 + a2 * c1)
        ringAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : RatComplexNum), (a + b) * c = a * c + b * c
    intro a b ca:RatComplexNumb:RatComplexNumc:RatComplexNum⊢ (a + b) * c = a * c + b * c
    match a, b, c with
    | ⟨b1, b2⟩, ⟨c1, c2⟩, ⟨a1, a2⟩ =>a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ ({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) * { fst := a1, snd := a2 } =
  { fst := b1, snd := b2 } * { fst := a1, snd := a2 } + { fst := c1, snd := c2 } * { fst := a1, snd := a2 }
      exth1a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) * { fst := a1, snd := a2 }).fst =
  ({ fst := b1, snd := b2 } * { fst := a1, snd := a2 } + { fst := c1, snd := c2 } * { fst := a1, snd := a2 }).fsth2a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) * { fst := a1, snd := a2 }).snd =
  ({ fst := b1, snd := b2 } * { fst := a1, snd := a2 } + { fst := c1, snd := c2 } * { fst := a1, snd := a2 }).snd
      ·h1a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) * { fst := a1, snd := a2 }).fst =
  ({ fst := b1, snd := b2 } * { fst := a1, snd := a2 } + { fst := c1, snd := c2 } * { fst := a1, snd := a2 }).fst change (b1 + c1) * a1 - (b2 + c2) * a2 =
          (b1 * a1 - b2 * a2) + (c1 * a1 - c2 * a2)h1a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (b1 + c1) * a1 - (b2 + c2) * a2 = b1 * a1 - b2 * a2 + (c1 * a1 - c2 * a2)
        ringAll goals completed! 🐙
      ·h2a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (({ fst := b1, snd := b2 } + { fst := c1, snd := c2 }) * { fst := a1, snd := a2 }).snd =
  ({ fst := b1, snd := b2 } * { fst := a1, snd := a2 } + { fst := c1, snd := c2 } * { fst := a1, snd := a2 }).snd change (b1 + c1) * a2 + (b2 + c2) * a1 =
          (b1 * a2 + b2 * a1) + (c1 * a2 + c2 * a1)h2a:RatComplexNumb:RatComplexNumc:RatComplexNumb1:ℚb2:ℚc1:ℚc2:ℚa1:ℚa2:ℚ⊢ (b1 + c1) * a2 + (b2 + c2) * a1 = b1 * a2 + b2 * a1 + (c1 * a2 + c2 * a1)
        ringAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : RatComplexNum), 0 * a = 0
    intro aa:RatComplexNum⊢ 0 * a = 0
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ 0 * { fst := a1, snd := a2 } = 0
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ (0 * { fst := a1, snd := a2 }).fst = fst 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ (0 * { fst := a1, snd := a2 }).snd = snd 0
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ (0 * { fst := a1, snd := a2 }).fst = fst 0 change 0 * a1 - 0 * a2 = 0h1a:RatComplexNuma1:ℚa2:ℚ⊢ 0 * a1 - 0 * a2 = 0
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ (0 * { fst := a1, snd := a2 }).snd = snd 0 change 0 * a2 + 0 * a1 = 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ 0 * a2 + 0 * a1 = 0
        simpAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : RatComplexNum), a * 0 = 0
    intro aa:RatComplexNum⊢ a * 0 = 0
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ { fst := a1, snd := a2 } * 0 = 0
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } * 0).fst = fst 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } * 0).snd = snd 0
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } * 0).fst = fst 0 change a1 * 0 - a2 * 0 = 0h1a:RatComplexNuma1:ℚa2:ℚ⊢ a1 * 0 - a2 * 0 = 0
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ ({ fst := a1, snd := a2 } * 0).snd = snd 0 change a1 * 0 + a2 * 0 = 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ a1 * 0 + a2 * 0 = 0
        simpAll goals completed! 🐙
  neg_add_cancel := by⊢ ∀ (a : RatComplexNum), -a + a = 0
    intro aa:RatComplexNum⊢ -a + a = 0
    match a with
    | ⟨a1, a2⟩ =>a:RatComplexNuma1:ℚa2:ℚ⊢ -{ fst := a1, snd := a2 } + { fst := a1, snd := a2 } = 0
      exth1a:RatComplexNuma1:ℚa2:ℚ⊢ (-{ fst := a1, snd := a2 } + { fst := a1, snd := a2 }).fst = fst 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ (-{ fst := a1, snd := a2 } + { fst := a1, snd := a2 }).snd = snd 0
      ·h1a:RatComplexNuma1:ℚa2:ℚ⊢ (-{ fst := a1, snd := a2 } + { fst := a1, snd := a2 }).fst = fst 0 change -a1 + a1 = 0h1a:RatComplexNuma1:ℚa2:ℚ⊢ -a1 + a1 = 0
        simpAll goals completed! 🐙
      ·h2a:RatComplexNuma1:ℚa2:ℚ⊢ (-{ fst := a1, snd := a2 } + { fst := a1, snd := a2 }).snd = snd 0 change -a2 + a2 = 0h2a:RatComplexNuma1:ℚa2:ℚ⊢ -a2 + a2 = 0
        simpAll goals completed! 🐙@[simp]
lemma one_fst : (1 : RatComplexNum).fst = 1 := rfl@[simp]
lemma one_snd : (1 : RatComplexNum).snd = 0 := rfl@[simp]
lemma zero_fst : (0 : RatComplexNum).fst = 0 := rfl@[simp]
lemma zero_snd : (0 : RatComplexNum).snd = 0 := rfl@[simp]
lemma I_mul_toComplexNum (a : RatComplexNum) : I * toComplexNum a = toComplexNum (⟨0, 1⟩ * a) := bya:RatComplexNum⊢ I * toComplexNum a = toComplexNum ({ fst := 0, snd := 1 } * a)
  simp only [toComplexNum, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mul_fst, zero_mul,
    one_mul, zero_sub, Rat.cast_neg, mul_snd, zero_add]a:RatComplexNum⊢ I * (↑a.fst + ↑a.snd * I) = -↑a.snd + ↑a.fst * I
  ring_nfa:RatComplexNum⊢ I * ↑a.fst + I ^ 2 * ↑a.snd = I * ↑a.fst - ↑a.snd
  simp only [I_sq, neg_mul, one_mul]a:RatComplexNum⊢ I * ↑a.fst + -↑a.snd = I * ↑a.fst - ↑a.snd
  ringAll goals completed! 🐙lemma ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) :
    n * toComplexNum a = toComplexNum (n * a) := byn:ℕa:RatComplexNum⊢ ↑n * toComplexNum a = toComplexNum (↑n * a)
  simp only [map_mul, map_natCast]All goals completed! 🐙

lemma toComplexNum_injective : Function.Injective toComplexNum := by⊢ Function.Injective ⇑toComplexNum
  intro a b haa:RatComplexNumb:RatComplexNumha:toComplexNum a = toComplexNum b⊢ a = b
  simp only [toComplexNum, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] at haa:RatComplexNumb:RatComplexNumha:↑a.fst + ↑a.snd * I = ↑b.fst + ↑b.snd * I⊢ a = b
  rw [Complex.ext_iffa:RatComplexNumb:RatComplexNumha:(↑a.fst + ↑a.snd * I).re = (↑b.fst + ↑b.snd * I).re ∧ (↑a.fst + ↑a.snd * I).im = (↑b.fst + ↑b.snd * I).im⊢ a = ba:RatComplexNumb:RatComplexNumha:(↑a.fst + ↑a.snd * I).re = (↑b.fst + ↑b.snd * I).re ∧ (↑a.fst + ↑a.snd * I).im = (↑b.fst + ↑b.snd * I).im⊢ a = b] at haa:RatComplexNumb:RatComplexNumha:(↑a.fst + ↑a.snd * I).re = (↑b.fst + ↑b.snd * I).re ∧ (↑a.fst + ↑a.snd * I).im = (↑b.fst + ↑b.snd * I).im⊢ a = b
  simp only [add_re, ratCast_re, mul_re, I_re, mul_zero, ratCast_im, I_im, mul_one, sub_self,
    add_zero, Rat.cast_inj, add_im, mul_im, zero_add] at haa:RatComplexNumb:RatComplexNumha:a.fst = b.fst ∧ a.snd = b.snd⊢ a = b
  exth1a:RatComplexNumb:RatComplexNumha:a.fst = b.fst ∧ a.snd = b.snd⊢ a.fst = b.fsth2a:RatComplexNumb:RatComplexNumha:a.fst = b.fst ∧ a.snd = b.snd⊢ a.snd = b.snd
  ·h1a:RatComplexNumb:RatComplexNumha:a.fst = b.fst ∧ a.snd = b.snd⊢ a.fst = b.fst exact ha.1All goals completed! 🐙
  ·h2a:RatComplexNumb:RatComplexNumha:a.fst = b.fst ∧ a.snd = b.snd⊢ a.snd = b.snd exact ha.2All goals completed! 🐙