d x y x' y' : ℤ
re_eq✝ : x = x'
im_eq✝ : y = y'
⊢ { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
d x y x' y' : ℤ
h : { re := x, im := y } = { re := x', im := y' }
⊢ { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
injection h
no goals
d x y x' y' : ℤ
re_eq✝ : x = x'
im_eq✝ : y = y'
⊢ { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
constructor <;> assumption
no goals
d x y x' y' : ℤ
x✝ : { re := x, im := y }.re = { re := x', im := y' }.re ∧ { re := x, im := y }.im = { re := x', im := y' }.im
h₁ : { re := x, im := y }.re = { re := x', im := y' }.re
h₂ : { re := x, im := y }.im = { re := x', im := y' }.im
⊢ { re := x, im := y } = { re := x', im := y' }
congr