-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem le_one_iff_exists_coeIdeal {J : FractionalIdeal S P} :
    J ≤ (1 : FractionalIdeal S P) ↔ ∃ I : Ideal R, ↑I = J

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∃ I, ↑I = J

Tactic:
refine ⟨⟨⟨⟨{ x : R | algebraMap R P x ∈ J }, ?_⟩, ?_⟩, ?_⟩, ?_⟩

Result:
case mp.refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ {a b : R},
    a ∈ {x | (algebraMap R P) x ∈ J} → b ∈ {x | (algebraMap R P) x ∈ J} → a + b ∈ {x | (algebraMap R P) x ∈ J}

case mp.refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1 }.carrier

case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ (c : R) {x : R},
    x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2 }.carrier →
      c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2 }.carrier

case mp.refine_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ?mp.refine_1, zero_mem' := ?mp.refine_2,
        smul_mem' := ?mp.refine_3 } =
    J

Proof state:
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ J ≤ 1

Tactic:
rw [← hI]

Result:
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ ↑I ≤ 1

Proof state:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
rw [smul_eq_mul, mem_setOf, RingHom.map_mul, ← Algebra.smul_def]

Result:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • (algebraMap R P) x ∈ J

Proof state:
case mp.refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ J

Tactic:
exact J.zero_mem

Result:
no goals

Proof state:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ (c : R) {x : R},
    x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier →
      c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
intro c x hx

Result:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Proof state:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • (algebraMap R P) x ∈ J

Tactic:
exact J.val.smul_mem c hx

Result:
no goals