Theorem: Int.int_val_eq_top_iff_zero (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ ↔ a = 0
Tactic:
apply Iff.intro
State after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤

State before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
. intro hval
  simp [int_val, nat_valuation] at hval
  cases abs_a : (natAbs a) with
  | zero => exact natAbs_eq_zero.1 abs_a
  | succ n =>
    cases hp : p with
    | zero =>
      rw [hp] at gt1
      apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
    | succ p' =>
      cases hp' : p' with
      | zero =>
        rw [hp, hp'] at gt1
        apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
      | succ n =>
        simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
State after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤

State before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
. intro ha
  simp [ha, int_val, nat_valuation]
State after:
no goals

State before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0
Tactic:
intro hval
State after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval : int_val p a = ⊤
⊢ a = 0

State before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval : int_val p a = ⊤
⊢ a = 0
Tactic:
simp [int_val, nat_valuation] at hval
State after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
⊢ a = 0

State before:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
⊢ a = 0
Tactic:
cases abs_a : (natAbs a) with
| zero => exact natAbs_eq_zero.1 abs_a
| succ n =>
  cases hp : p with
  | zero =>
    rw [hp] at gt1
    apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
  | succ p' =>
    cases hp' : p' with
    | zero =>
      rw [hp, hp'] at gt1
      apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
    | succ n =>
      simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
State after:
no goals

State before:
case mp.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
abs_a : natAbs a = Nat.zero
⊢ a = 0
Tactic:
exact natAbs_eq_zero.1 abs_a
State after:
no goals

State before:
case mp.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
⊢ a = 0
Tactic:
cases hp : p with
| zero =>
  rw [hp] at gt1
  apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
| succ p' =>
  cases hp' : p' with
  | zero =>
    rw [hp, hp'] at gt1
    apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
  | succ n =>
    simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
State after:
no goals

State before:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0
Tactic:
rw [hp] at gt1
State after:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.zero
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0

State before:
case mp.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.zero
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
hp : p = Nat.zero
⊢ a = 0
Tactic:
apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
State after:
no goals

State before:
case mp.succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
hp : p = Nat.succ p'
⊢ a = 0
Tactic:
cases hp' : p' with
| zero =>
  rw [hp, hp'] at gt1
  apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
| succ n =>
  simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
State after:
no goals

State before:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0
Tactic:
rw [hp, hp'] at gt1
State after:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
gt1 : 1 < Nat.succ Nat.zero
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0

State before:
case mp.succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n : ℕ
abs_a : natAbs a = Nat.succ n
p' : ℕ
gt1 : 1 < Nat.succ Nat.zero
hp : p = Nat.succ p'
hp' : p' = Nat.zero
⊢ a = 0
Tactic:
apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
State after:
no goals

State before:
case mp.succ.succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
n✝ : ℕ
abs_a : natAbs a = Nat.succ n✝
p' : ℕ
hp : p = Nat.succ p'
n : ℕ
hp' : p' = Nat.succ n
⊢ a = 0
Tactic:
simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
State after:
no goals

State before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
Tactic:
intro ha
State after:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
ha : a = 0
⊢ int_val p a = ⊤

State before:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
ha : a = 0
⊢ int_val p a = ⊤
Tactic:
simp [ha, int_val, nat_valuation]
State after:
no goals