-- 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
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
⊢ select (fun i => ¬P i) z = y

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
hx : select P z = x
n : ℕ
⊢ (select (fun i => ¬P i) z).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
⊢ z.coeff n = x.coeff n + y.coeff n

Tactic:
simp only [z, mk.eq_1]

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
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

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
hy : select (fun i => ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n + y.coeff n

Tactic:
rw [y0, add_zero]

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 : ℕ
⊢ (select (fun i => ¬P i) z).coeff n = y.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

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
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

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 : ℕ
⊢ (select P z).coeff n = x.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

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 : ℕ
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n