Theorem: ℤθ.norm_one_if_unit (Mordell4/CubicRing.lean)

State before:
a b c k : ℤθ
⊢ IsUnit k → norm k = 1
Tactic:
intro h
State after:
a b c k : ℤθ
h : IsUnit k
⊢ norm k = 1

State before:
a b c k : ℤθ
h : IsUnit k
⊢ norm k = 1
Tactic:
rw [isUnit_iff_exists_inv] at h
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ norm k = 1
Tactic:
have p : ∃ b : ℤθ, 1 = k * b := by tauto
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : ∃ b, 1 = k * b
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : ∃ b, 1 = k * b
⊢ norm k = 1
Tactic:
change k ∣ 1 at p
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
⊢ norm k = 1
Tactic:
have l := norm_divides p
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm k = 1
Tactic:
have d : norm 1 = 1 := by ring
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
d : norm 1 = 1
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
d : norm 1 = 1
⊢ norm k = 1
Tactic:
rw [d] at l
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ norm k = 1

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ norm k = 1
Tactic:
refine' Int.eq_one_of_dvd_one _ l
State after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ 0 ≤ norm k

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ 0 ≤ norm k
Tactic:
exact abs_nonneg _
State after:
no goals

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ ∃ b, 1 = k * b
Tactic:
tauto
State after:
no goals

State before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm 1 = 1
Tactic:
ring
State after:
no goals