case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝ } n = coeff y n
⊢ { coeff := coeff✝ } = y
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = coeff y n
⊢ x = y
cases x
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝¹ } n = coeff { coeff := coeff✝ } n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝ } n = coeff y n
⊢ { coeff := coeff✝ } = y
cases y
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝¹ } n = coeff { coeff := coeff✝ } n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
simp only at h
no goals
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
simp [Function.funext_iff, h]