-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem coeff_add_of_disjoint (x y : 𝕎 R) (h : ∀ n, x.coeff n = 0 ∨ y.coeff n = 0) :
    (x + y).coeff n = x.coeff n + y.coeff n

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
let P : ℕ → Prop := fun n => y.coeff n = 0

Result:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ (if P n then x.coeff n else y.coeff n) = x.coeff n + y.coeff n

Tactic:
split_ifs with y0

Result:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n + y.coeff n

case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : ¬P n
⊢ y.coeff n = x.coeff n + y.coeff n

Proof state:
case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n

Tactic:
rw [(h n).resolve_right hn]

Result:
no goals

Proof state:
case h
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n

Tactic:
split_ifs with hn

Result:
case pos
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : P n
⊢ 0 = y.coeff n

case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : ¬P n
⊢ y.coeff n = y.coeff n

Proof state:
case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : ¬P n
⊢ y.coeff n = x.coeff n + y.coeff n

Tactic:
rw [h n |>.resolve_right y0, zero_add]

Result:
no goals

Proof state:
case pos
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : P n
⊢ 0 = y.coeff n

Tactic:
exact hn.symm

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
set z := mk p fun n => if P n then x.coeff n else y.coeff n

Result:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
⊢ select P z = x

Tactic:
ext1 n

Result:
case h
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (select P z).coeff n = x.coeff n

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ (x + y).coeff n = z.coeff n

Tactic:
rw [← hx, ← hy, select_add_select_not P z]

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
haveI : DecidablePred P := Classical.decPred P

Result:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Proof state:
case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : ¬P n
⊢ y.coeff n = y.coeff n

Tactic:
rfl

Result:
no goals

Proof state:
case pos
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
hn : P n
⊢ x.coeff n = x.coeff n

Tactic:
rfl

Result:
no goals

Proof state:
case h
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n

Tactic:
split_ifs with hn

Result:
case pos
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
hn : P n
⊢ x.coeff n = x.coeff n

case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n => y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then x.coeff n else y.coeff n
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n