case intro
σ : Type u_1
τ : Type ?u.155795
R : Type u_2
S : Type ?u.155801
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hm : IsHomogeneous φ m
hn : IsHomogeneous φ n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
σ : Type u_1
τ : Type ?u.155795
R : Type u_2
S : Type ?u.155801
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hm : IsHomogeneous φ m
hn : IsHomogeneous φ n
hφ : φ ≠ 0
⊢ m = n
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
no goals
case intro
σ : Type u_1
τ : Type ?u.155795
R : Type u_2
S : Type ?u.155801
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hm : IsHomogeneous φ m
hn : IsHomogeneous φ n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
rw [← hm hd, ← hn hd]