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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ int_val p ↑p = 1
Tactic:
simp only [natAbs_cast, int_val]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1
Tactic:
match p with
| 0 =>
  apply False.elim
  apply Nat.not_lt_zero 1
  assumption
| Nat.succ 0 =>
  apply False.elim
  apply Nat.lt_irrefl 1
  assumption
| q+2 =>
  rw [nat_val_succ, Nat.mod_self, if_neg _]
  rw [Nat.div_self, nat_val_succ, if_pos, zero_add]
  rw [Nat.mod_eq_of_lt]
  exact Nat.succ_ne_zero 0
  assumption
  exact lt_trans (Nat.lt_succ_self 0) gt1
  exact Ne.irrefl
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ nat_valuation 0 0 = 1
Tactic:
apply False.elim
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ False

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ False
Tactic:
apply Nat.not_lt_zero 1
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ 1 < 0

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ 1 < 0
Tactic:
assumption
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ nat_valuation (Nat.succ 0) (Nat.succ 0) = 1
Tactic:
apply False.elim
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ False

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ False
Tactic:
apply Nat.lt_irrefl 1
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ 1 < 1

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ 1 < 1
Tactic:
assumption
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) (q + 2) = 1
Tactic:
rw [nat_val_succ, Nat.mod_self, if_neg _]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) ((q + 1 + 1) / (q + 2)) + 1 = 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) ((q + 1 + 1) / (q + 2)) + 1 = 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
rw [Nat.div_self, nat_val_succ, if_pos, zero_add]
State after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ (0 + 1) % (q + 2) ≠ 0

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ (0 + 1) % (q + 2) ≠ 0

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
rw [Nat.mod_eq_of_lt]
State after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 ≠ 0

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 ≠ 0

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact Nat.succ_ne_zero 0
State after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
assumption
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact lt_trans (Nat.lt_succ_self 0) gt1
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact Ne.irrefl
State after:
no goals