Theorem: Ideal.mem_iff_associated (FormalisingMathematics2024/Solutions/Section14UFDsAndPIDsEtc/Sheet3.lean)

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a b : R
hab : Associated a b
⊢ a ∈ I ↔ b ∈ I
Tactic:
rcases hab with ⟨u, rfl⟩
State after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a ∈ I ↔ a * ↑u ∈ I

State before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a ∈ I ↔ a * ↑u ∈ I
Tactic:
refine' ⟨I.mul_mem_right _, _⟩
State after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a * ↑u ∈ I → a ∈ I

State before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a * ↑u ∈ I → a ∈ I
Tactic:
intro h
State after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a ∈ I

State before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a ∈ I
Tactic:
convert I.mul_mem_right ((u⁻¹ : Rˣ) : R) h
State after:
case h.e'_4
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a = a * ↑u * ↑u⁻¹

State before:
case h.e'_4
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a = a * ↑u * ↑u⁻¹
Tactic:
simp
State after:
no goals