R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h : ↑(rescale a) p = ↑(rescale a) q
⊢ p = q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
⊢ Function.Injective ↑(rescale a)
intro p q h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
h : ∀ (n : ℕ), ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
⊢ ∀ (n : ℕ), ↑(coeff R n) p = ↑(coeff R n) q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h : ↑(rescale a) p = ↑(rescale a) q
⊢ p = q
rw [PowerSeries.ext_iff] at *
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
h : ∀ (n : ℕ), ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
n : ℕ
⊢ ↑(coeff R n) p = ↑(coeff R n) q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
h : ∀ (n : ℕ), ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
⊢ ∀ (n : ℕ), ↑(coeff R n) p = ↑(coeff R n) q
intro n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
⊢ ↑(coeff R n) p = ↑(coeff R n) q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
h : ∀ (n : ℕ), ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
n : ℕ
⊢ ↑(coeff R n) p = ↑(coeff R n) q
specialize h n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
⊢ ↑(coeff R n) p = ↑(coeff R n) q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) (↑(rescale a) p) = ↑(coeff R n) (↑(rescale a) q)
⊢ ↑(coeff R n) p = ↑(coeff R n) q
rw [coeff_rescale, coeff_rescale, mul_eq_mul_left_iff] at h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
⊢ ¬a ^ n = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
⊢ ↑(coeff R n) p = ↑(coeff R n) q
apply h.resolve_right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
h' : a ^ n = 0
⊢ False
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
⊢ ¬a ^ n = 0
intro h'
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : PowerSeries R
h✝ : ↑(rescale a) p = ↑(rescale a) q
n : ℕ
h : ↑(coeff R n) p = ↑(coeff R n) q ∨ a ^ n = 0
h' : a ^ n = 0
⊢ False
exact ha (pow_eq_zero h')