case intro.mk
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
case intro.mk
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
have ha₀ : a₀ ≠ 0 := by
  haveI :=
    @isDomain_of_le_nonZeroDivisors B _ R _ _ _ (Submonoid.powers x) _
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
  simp only [map_zero, ← hy, map_pow] at H
  apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
  rw [← H]
  apply mul_ne_zero hb (pow_ne_zero _ _)
  exact
    IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
      (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
  exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
simp only [← hy] at H
no goals
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
classical
obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx
refine' ⟨a, m - d, _⟩
rw [← mk'_one (M := Submonoid.powers x) B, selfZpow_pow_sub, selfZpow_coe_nat, selfZpow_coe_nat,
  ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
⊢ a₀ ≠ 0
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
⊢ a₀ ≠ 0
haveI :=
  @isDomain_of_le_nonZeroDivisors B _ R _ _ _ (Submonoid.powers x) _
    (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ a₀ ≠ 0
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
H : b * ↑(algebraMap R B) ↑(a₀, y).snd = ↑(algebraMap R B) (a₀, y).fst
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
⊢ a₀ ≠ 0
simp only [map_zero, ← hy, map_pow] at H
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬↑(algebraMap R B) a₀ = 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ a₀ ≠ 0
apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬b * ↑(algebraMap R B) x ^ d = 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬↑(algebraMap R B) a₀ = 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
rw [← H]
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ↑(algebraMap R B) x ≠ 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ¬b * ↑(algebraMap R B) x ^ d = 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
apply mul_ne_zero hb (pow_ne_zero _ _)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ ↑(algebraMap R B) x ≠ 0

R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
exact
  IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
    (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
    (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
no goals
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * ↑(algebraMap R B) x ^ d = ↑(algebraMap R B) a₀
⊢ Function.Injective ↑(algebraMap R B)
exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
case intro.mk.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZpow x B (↑m - ↑d) * ↑(algebraMap R B) a = b
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ∃ a n, ¬x ∣ a ∧ selfZpow x B n * ↑(algebraMap R B) a = b
refine' ⟨a, m - d, _⟩
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ ↑(algebraMap R B) x ^ m * mk' B a 1 = ↑(algebraMap R B) x ^ m * ↑(algebraMap R B) a
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZpow x B (↑m - ↑d) * ↑(algebraMap R B) a = b
rw [← mk'_one (M := Submonoid.powers x) B, selfZpow_pow_sub, selfZpow_coe_nat, selfZpow_coe_nat,
  ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
no goals
case intro.mk.intro.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
x : R
B : Type u_1
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : IsLocalization.Away x B
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : { x_1 // x_1 ∈ Submonoid.powers x }
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * ↑(algebraMap R B) (x ^ d) = ↑(algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ ↑(algebraMap R B) x ^ m * mk' B a 1 = ↑(algebraMap R B) x ^ m * ↑(algebraMap R B) a
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩