Exists valuation algebra Map eq valuation pow

theorem exists_valuation_algebraMap_eq_valuation_pow    (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L] [ValuativeRel L]    [Algebra.IsAlgebraic K L] (y : L) :    ∃ x n, n ≠ 0 ∧ valuation L (algebraMap K L x) = valuation L y ^ n := by  by_cases hy : y = 0  · use 0, 1, one_ne_zero    simp [hy]  by_contra! H  have := congr(valuation L $(minpoly.aeval K y))  rw [Polynomial.aeval_eq_sum_range, Valuation.sum_eq_iSup] at this; swap  · simp only [Finset.mem_range, Nat.lt_succ_iff, ne_eq, map_eq_zero, smul_eq_zero,      pow_eq_zero_iff', hy, false_and, or_false]    intros i hi j hj hij hi' hj' e    wlog hij' : i ≤ j generalizing i j    · exact this j hj i hi (Ne.symm hij) hj' hi' e.symm (by omega)    obtain ⟨k, rfl⟩ := exists_add_of_le hij'    simp [Algebra.smul_def] at e    apply H ((minpoly K y).coeff i / (minpoly K y).coeff (i + k)) k (by simpa using hij)    apply mul_left_injective₀ (b := (valuation L) y ^ i) (by simp [hy])    simp [*, -mul_eq_mul_right_iff, div_mul_eq_mul_div, pow_add, mul_comm]  · simp only [map_zero, ← bot_eq_zero, Finset.sup_eq_bot_iff] at this    simp only [Finset.mem_range, Function.comp_apply, bot_eq_zero, map_eq_zero, smul_eq_zero,      pow_eq_zero_iff', hy, ne_eq, false_and, or_false, Nat.lt_succ_iff] at this    exact minpoly.coeff_zero_ne_zero (Algebra.IsIntegral.isIntegral _) hy (this 0 (by simp))