Theorem: QSqrt2.ext (FormalisingMathematics2024/Solutions/Section19algebraicNumberTheory/Sheet1.lean)

State before:
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
a b : QSqrt2
h1 : a.R = b.R
h2 : a.i = b.i
⊢ a = b
Tactic:
cases a
State after:
case mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
b : QSqrt2
R✝ i✝ : ℚ
h1 : { R := R✝, i := i✝ }.R = b.R
h2 : { R := R✝, i := i✝ }.i = b.i
⊢ { R := R✝, i := i✝ } = b

State before:
case mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
b : QSqrt2
R✝ i✝ : ℚ
h1 : { R := R✝, i := i✝ }.R = b.R
h2 : { R := R✝, i := i✝ }.i = b.i
⊢ { R := R✝, i := i✝ } = b
Tactic:
cases b
State after:
case mk.mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
R✝¹ i✝¹ R✝ i✝ : ℚ
h1 : { R := R✝¹, i := i✝¹ }.R = { R := R✝, i := i✝ }.R
h2 : { R := R✝¹, i := i✝¹ }.i = { R := R✝, i := i✝ }.i
⊢ { R := R✝¹, i := i✝¹ } = { R := R✝, i := i✝ }

State before:
case mk.mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
R✝¹ i✝¹ R✝ i✝ : ℚ
h1 : { R := R✝¹, i := i✝¹ }.R = { R := R✝, i := i✝ }.R
h2 : { R := R✝¹, i := i✝¹ }.i = { R := R✝, i := i✝ }.i
⊢ { R := R✝¹, i := i✝¹ } = { R := R✝, i := i✝ }
Tactic:
simp_all
State after:
no goals