From 4b00aa2dd38154206ddf6906dd505b0d42535c70 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 17 Oct 2021 11:01:31 +0000 Subject: [PATCH] refactor(ring_theory/jacobson): avoid shadowing hypothesis (#9736) This PR postpones a `rw` in a proof, which was creating a shadowed hypothesis. At present, this shadowing was not a big deal, but in another branch it caused a hard-to-diagnose error. Co-authored-by: Scott Morrison --- src/ring_theory/jacobson.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ring_theory/jacobson.lean b/src/ring_theory/jacobson.lean index be162b39533d0..4d48450c328d7 100644 --- a/src/ring_theory/jacobson.lean +++ b/src/ring_theory/jacobson.lean @@ -448,7 +448,7 @@ begin let φ : (P.comap C : ideal R).quotient →+* P.quotient := quotient_map P C le_rfl, let M : submonoid (P.comap C : ideal R).quotient := submonoid.powers ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff, - rw ← bot_quotient_is_maximal_iff at hP ⊢, + rw ← bot_quotient_is_maximal_iff, have hp0 : ((m : polynomial R).map (quotient.mk (P.comap C : ideal R))).leading_coeff ≠ 0 := λ hp0', this $ map_injective (quotient.mk (P.comap C : ideal R)) ((quotient.mk (P.comap C : ideal R)).injective_iff.2 (λ x hx, @@ -473,7 +473,8 @@ begin apply is_integral_is_localization_polynomial_quotient P _ (submodule.coe_mem m) }, rw (map_bot.symm : (⊥ : ideal (localization M')) = map (algebra_map P.quotient (localization M')) ⊥), - refine map.is_maximal (algebra_map _ _) (localization_map_bijective_of_field hM' _) hP, + let bot_maximal := ((bot_quotient_is_maximal_iff _).mpr hP), + refine map.is_maximal (algebra_map _ _) (localization_map_bijective_of_field hM' _) bot_maximal, rwa [← quotient.maximal_ideal_iff_is_field_quotient, ← bot_quotient_is_maximal_iff], end