Theorem: ENatValRing.sub_val_sub_val (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
Tactic:
have general : ∀ y : R, sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y := by
  induction m with
  | zero => simp [sub_val_x_zero]
  | succ m ih =>
    intro y
    cases @eq_zero_or_pos _ _ (evr.valtn y) with
    | inl h' => simp [sub_val_val_zero evr y _ h']
    | inr h' =>
      rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
      exact ih (evr.decr_val y)
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
general : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ sub_val evr n (sub_val evr m x) = sub_val evr (m + n) x
Tactic:
exact general x
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
m n : ℕ
⊢ ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
Tactic:
induction m with
| zero => simp [sub_val_x_zero]
| succ m ih =>
  intro y
  cases @eq_zero_or_pos _ _ (evr.valtn y) with
  | inl h' => simp [sub_val_val_zero evr y _ h']
  | inr h' =>
    rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
    exact ih (evr.decr_val y)
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n : ℕ
⊢ ∀ (y : R), sub_val evr n (sub_val evr Nat.zero y) = sub_val evr (Nat.zero + n) y
Tactic:
simp [sub_val_x_zero]
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ ∀ (y : R), sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
intro y
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn y) with
| inl h' => simp [sub_val_val_zero evr y _ h']
| inr h' =>
  rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
  exact ih (evr.decr_val y)
State after:
no goals

State before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : v evr.valtn y = 0
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
simp [sub_val_val_zero evr y _ h']
State after:
no goals

State before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
State after:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr m (decr_val evr y)) = sub_val evr (m + n) (decr_val evr y)

State before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr m (decr_val evr y)) = sub_val evr (m + n) (decr_val evr y)
Tactic:
exact ih (evr.decr_val y)
State after:
no goals