Theorem: HTPI.prod_inv_iff_inv (HTPILib/Chap7.lean)

State before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) ↔ invertible Y
Tactic:
apply Iff.intro
State after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) → invertible Y

case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible Y → invertible (X * Y)

State before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible (X * Y) → invertible Y
Tactic:
assume h2 : invertible (X * Y)
State after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
⊢ invertible Y

State before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
⊢ invertible Y
Tactic:
obtain (Z : ZMod m) (h3 : X * Y * Z = [1]_m) from h2
State after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ invertible Y

State before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ invertible Y
Tactic:
apply Exists.intro (X * Z)
State after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = [1]_m

State before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = [1]_m
Tactic:
rewrite [←h3]
State after:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = X * Y * Z

State before:
case mp
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible (X * Y)
Z : ZMod m
h3 : X * Y * Z = [1]_m
⊢ Y * (X * Z) = X * Y * Z
Tactic:
ring
State after:
no goals

State before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
⊢ invertible Y → invertible (X * Y)
Tactic:
assume h2 : invertible Y
State after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
⊢ invertible (X * Y)

State before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
⊢ invertible (X * Y)
Tactic:
obtain (Xi : ZMod m) (h3 : X * Xi = [1]_m) from h1
State after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
⊢ invertible (X * Y)

State before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
⊢ invertible (X * Y)
Tactic:
obtain (Yi : ZMod m) (h4 : Y * Yi = [1]_m) from h2
State after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ invertible (X * Y)

State before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ invertible (X * Y)
Tactic:
apply Exists.intro (Xi * Yi)
State after:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = [1]_m

State before:
case mpr
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = [1]_m
Tactic:
show (X * Y) * (Xi * Yi) = [1]_m from
  calc X * Y * (Xi * Yi)
    _ = (X * Xi) * (Y * Yi) := by ring
    _ = [1]_m * [1]_m := by rw [h3, h4]
    _ = [1]_m := Theorem_7_3_6_7 [1]_m
State after:
no goals

State before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Y * (Xi * Yi) = X * Xi * (Y * Yi)
Tactic:
ring
State after:
no goals

State before:
m : ℕ
X : ZMod m
h1 : invertible X
Y : ZMod m
h2 : invertible Y
Xi : ZMod m
h3 : X * Xi = [1]_m
Yi : ZMod m
h4 : Y * Yi = [1]_m
⊢ X * Xi * (Y * Yi) = [1]_m * [1]_m
Tactic:
rw [h3, h4]
State after:
no goals