Theorem: Subsemigroup.submonoid.powers_absorbing (Kaplanski4/Absorbing.lean)

State before:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
⊢ ProdProperty (Submonoid.powers p).toSubsemigroup
Tactic:
rintro x y hxy
State after:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z

State before:
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
cases' ((Submonoid.mem_powers_iff _ _).1 hxy) with m hm
State after:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z

State before:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rw [← one_mul (p^m)] at hm
State after:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z

State before:
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rcases (mul_eq_mul_prime_pow hp hm.symm) with ⟨i, j, _, _, ⟨_, hbc, hx, hy⟩⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
Tactic:
rw [hx, hy]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝¹ * p ^ i) z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝ * p ^ j) z

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝¹ * p ^ i) z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated (w✝ * p ^ j) z
Tactic:
refine' ⟨⟨p^i, (Submonoid.mem_powers_iff _ _).2 ⟨i, rfl⟩,
  (associated_isUnit_mul_left_iff (isUnit_of_mul_eq_one _ _ hbc.symm)).2 (Associated.refl (p^i))⟩,
    p^j, (Submonoid.mem_powers_iff _ _).2 ⟨j, rfl⟩, _⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝¹ * w✝
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Tactic:
rw [mul_comm] at hbc
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝ * w✝¹
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
i j : ℕ
w✝¹ w✝ : R
left✝ : i + j = m
hbc : 1 = w✝ * w✝¹
hx : x = w✝¹ * p ^ i
hy : y = w✝ * p ^ j
⊢ Associated (w✝ * p ^ j) (p ^ j)
Tactic:
exact (associated_isUnit_mul_left_iff (isUnit_of_mul_eq_one _ _ hbc.symm)).2
  (Associated.refl (p^j))
State after:
no goals