-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem den_mul_self_eq_num' (I : FractionalIdeal S P) :
    spanSingleton S (algebraMap R P I.den) * I = I.num

Proof state:
case h.e'_2
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (algebraMap R P) ↑I.den • ↑I = I.den • ↑I

Tactic:
ext

Result:
case h.e'_2.h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
x✝ : P
⊢ x✝ ∈ (algebraMap R P) ↑I.den • ↑I ↔ x✝ ∈ I.den • ↑I

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ↑(spanSingleton S ((algebraMap R P) ↑I.den) * I) = ↑↑I.num

Tactic:
rw [coe_mul, ← smul_eq_mul, coe_spanSingleton, smul_eq_mul, Submodule.span_singleton_mul]

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (algebraMap R P) ↑I.den • ↑I = ↑↑I.num

Proof state:
case h.e'_2.h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
x✝ : P
⊢ x✝ ∈ (algebraMap R P) ↑I.den • ↑I ↔ x✝ ∈ I.den • ↑I

Tactic:
erw [Set.mem_smul_set, Set.mem_smul_set]

Result:
case h.e'_2.h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
x✝ : P
⊢ (∃ y ∈ ↑↑I, (algebraMap R P) ↑I.den • y = x✝) ↔ ∃ y ∈ ↑↑I, ↑I.den • y = x✝

Proof state:
case h.e'_2.h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
x✝ : P
⊢ (∃ y ∈ ↑↑I, (algebraMap R P) ↑I.den • y = x✝) ↔ ∃ y ∈ ↑↑I, ↑I.den • y = x✝

Tactic:
simp [Algebra.smul_def]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (fun I => ↑I) (spanSingleton S ((algebraMap R P) ↑I.den) * I) = (fun I => ↑I) ↑I.num

Tactic:
dsimp only

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ↑(spanSingleton S ((algebraMap R P) ↑I.den) * I) = ↑↑I.num

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num

Tactic:
apply coeToSubmodule_injective

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (fun I => ↑I) (spanSingleton S ((algebraMap R P) ↑I.den) * I) = (fun I => ↑I) ↑I.num

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (algebraMap R P) ↑I.den • ↑I = ↑↑I.num

Tactic:
convert I.den_mul_self_eq_num using 1

Result:
case h.e'_2
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ (algebraMap R P) ↑I.den • ↑I = I.den • ↑I