Theorem: HTPI.fqn_one_one (HTPILib/Chap8Part2.lean)

State before:
⊢ one_to_one fqn
Tactic:
define
State after:
⊢ ∀ (x1 x2 : ℚ), fqn x1 = fqn x2 → x1 = x2

State before:
⊢ ∀ (x1 x2 : ℚ), fqn x1 = fqn x2 → x1 = x2
Tactic:
fix q1 : Rat
State after:
q1 : ℚ
⊢ ∀ (x2 : ℚ), fqn q1 = fqn x2 → q1 = x2

State before:
q1 : ℚ
⊢ ∀ (x2 : ℚ), fqn q1 = fqn x2 → q1 = x2
Tactic:
fix q2 : Rat
State after:
q1 q2 : ℚ
⊢ fqn q1 = fqn q2 → q1 = q2

State before:
q1 q2 : ℚ
⊢ fqn q1 = fqn q2 → q1 = q2
Tactic:
assume h1 : fqn q1 = fqn q2
State after:
q1 q2 : ℚ
h1 : fqn q1 = fqn q2
⊢ q1 = q2

State before:
q1 q2 : ℚ
h1 : fqn q1 = fqn q2
⊢ q1 = q2
Tactic:
rewrite [fqn_def, fqn_def] at h1
State after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
⊢ q1 = q2

State before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
⊢ q1 = q2
Tactic:
have h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den) :=
  fnnn_one_one _ _ h1
State after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
⊢ q1 = q2

State before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
⊢ q1 = q2
Tactic:
have h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den :=
  Prod.mk.inj h2
State after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
⊢ q1 = q2

State before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
⊢ q1 = q2
Tactic:
have h4 : q1.num = q2.num := fzn_one_one _ _ h3.left
State after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
h4 : q1.num = q2.num
⊢ q1 = q2

State before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
h4 : q1.num = q2.num
⊢ q1 = q2
Tactic:
show q1 = q2 from Rat.ext q1 q2 h4 h3.right
State after:
no goals