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

State before:
m : ℕ
X : ZMod 0
⊢ ∃ a, X = [a]_0
Tactic:
apply Exists.intro X
State after:
m : ℕ
X : ZMod 0
⊢ X = [X]_0

State before:
m : ℕ
X : ZMod 0
⊢ X = [X]_0
Tactic:
rfl
State after:
no goals

State before:
m n : ℕ
X : ZMod (n + 1)
⊢ ∃ a, X = [a]_(n + 1)
Tactic:
apply Exists.intro ↑(X.val)
State after:
m n : ℕ
X : ZMod (n + 1)
⊢ X = [↑(ZMod.val X)]_(n + 1)

State before:
m n : ℕ
X : ZMod (n + 1)
⊢ X = [↑(ZMod.val X)]_(n + 1)
Tactic:
have h1 : X.val < n + 1 := Fin.prop X
State after:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ X = [↑(ZMod.val X)]_(n + 1)

State before:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ X = [↑(ZMod.val X)]_(n + 1)
Tactic:
rewrite [cc_eq_iff_val_eq, val_nat_eq_mod, Nat.mod_eq_of_lt h1]
State after:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ ZMod.val X = ZMod.val X

State before:
m n : ℕ
X : ZMod (n + 1)
h1 : ZMod.val X < n + 1
⊢ ZMod.val X = ZMod.val X
Tactic:
rfl
State after:
no goals