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

case mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
⊢ (∃ I, ↑I = J) → J ≤ 1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
⊢ J ≤ 1 ↔ ∃ I, ↑I = J
constructor
case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∃ I, ↑I = J
case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
⊢ J ≤ 1 → ∃ I, ↑I = J
intro hJ
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
loc : IsLocalization S 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
loc : IsLocalization S 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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ (c : R) {x : R},
    x ∈
        { toAddSubsemigroup := { carrier := {x | ↑(algebraMap R P) x ∈ J}, add_mem' := ?mp.refine'_1 },
              zero_mem' := ?mp.refine'_2 }.toAddSubsemigroup.carrier →
      c • x ∈
        { toAddSubsemigroup := { carrier := {x | ↑(algebraMap R P) x ∈ J}, add_mem' := ?mp.refine'_1 },
              zero_mem' := ?mp.refine'_2 }.toAddSubsemigroup.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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ↑{
        toAddSubmonoid :=
          { toAddSubsemigroup := { carrier := {x | ↑(algebraMap R P) x ∈ J}, add_mem' := ?mp.refine'_1 },
            zero_mem' := ?mp.refine'_2 },
        smul_mem' := ?mp.refine'_3 } =
    J
case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∃ I, ↑I = J
refine' ⟨⟨⟨⟨{ x : R | algebraMap R P x ∈ J }, _⟩, _⟩, _⟩, _⟩
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : a ∈ {x | ↑(algebraMap R P) x ∈ J}
hb : b ∈ {x | ↑(algebraMap R P) x ∈ J}
⊢ a + b ∈ {x | ↑(algebraMap R P) x ∈ J}
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
loc : IsLocalization S 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}
intro a b ha hb
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : a ∈ {x | ↑(algebraMap R P) x ∈ J}
hb : b ∈ {x | ↑(algebraMap R P) x ∈ J}
⊢ ↑(algebraMap R P) a + ↑(algebraMap R P) b ∈ J
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : a ∈ {x | ↑(algebraMap R P) x ∈ J}
hb : b ∈ {x | ↑(algebraMap R P) x ∈ J}
⊢ a + b ∈ {x | ↑(algebraMap R P) x ∈ J}
rw [mem_setOf, RingHom.map_add]
no goals
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
a b : R
ha : a ∈ {x | ↑(algebraMap R P) x ∈ J}
hb : b ∈ {x | ↑(algebraMap R P) x ∈ J}
⊢ ↑(algebraMap R P) a + ↑(algebraMap R P) b ∈ J
exact J.val.add_mem ha hb
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ 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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈
    { carrier := {x | ↑(algebraMap R P) x ∈ J},
        add_mem' :=
          (_ :
            ∀ {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}) }.carrier
rw [mem_setOf, RingHom.map_zero]
no goals
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ 0 ∈ J
exact J.val.zero_mem
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ∀ (c : R) {x : R},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
intro c x hx
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • ↑(algebraMap R P) x ∈ J
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
rw [smul_eq_mul, mem_setOf, RingHom.map_mul, ← Algebra.smul_def]
no goals
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ↑(algebraMap R P) x ∈ J},
              add_mem' :=
                (_ :
                  ∀ {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}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                    add_mem' :=
                      (_ :
                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • ↑(algebraMap R P) x ∈ J
exact J.val.smul_mem c hx
case mp.refine'_4.a
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) } ↔
    x ∈ J
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
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
⊢ ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) } =
    J
ext x
case mp.refine'_4.a.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) } →
    x ∈ J

case mp.refine'_4.a.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ J →
    x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
case mp.refine'_4.a
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) } ↔
    x ∈ J
constructor
case mp.refine'_4.a.mp.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy :
  y ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
eq_y : ↑(Algebra.linearMap R P) y = x
⊢ x ∈ J
case mp.refine'_4.a.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) } →
    x ∈ J
rintro ⟨y, hy, eq_y⟩
no goals
case mp.refine'_4.a.mp.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy :
  y ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
eq_y : ↑(Algebra.linearMap R P) y = x
⊢ x ∈ J
rwa [← eq_y]
case mp.refine'_4.a.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
hx : x ∈ J
⊢ x ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
case mp.refine'_4.a.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ J →
    x ∈
      ↑{
          toAddSubmonoid :=
            {
              toAddSubsemigroup :=
                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {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}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | ↑(algebraMap R P) x ∈ J},
                        add_mem' :=
                          (_ :
                            ∀ {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}) }.carrier) },
          smul_mem' :=
            (_ :
              ∀ (c : R) {x : R},
                x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                  c • x ∈
                    {
                          toAddSubsemigroup :=
                            { carrier := {x | ↑(algebraMap R P) x ∈ J},
                              add_mem' :=
                                (_ :
                                  ∀ {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}) },
                          zero_mem' :=
                            (_ :
                              0 ∈
                                { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                    add_mem' :=
                                      (_ :
                                        ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
intro hx
case mp.refine'_4.a.mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
y : R
hx : ↑(algebraMap R P) y ∈ J
⊢ ↑(algebraMap R P) y ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
case mp.refine'_4.a.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
hx : x ∈ J
⊢ x ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)
no goals
case mp.refine'_4.a.mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
hJ : J ≤ 1
y : R
hx : ↑(algebraMap R P) y ∈ J
⊢ ↑(algebraMap R P) y ∈
    ↑{
        toAddSubmonoid :=
          {
            toAddSubsemigroup :=
              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                add_mem' :=
                  (_ :
                    ∀ {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}) },
            zero_mem' :=
              (_ :
                0 ∈
                  { carrier := {x | ↑(algebraMap R P) x ∈ J},
                      add_mem' :=
                        (_ :
                          ∀ {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}) }.carrier) },
        smul_mem' :=
          (_ :
            ∀ (c : R) {x : R},
              x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier →
                c • x ∈
                  {
                        toAddSubsemigroup :=
                          { carrier := {x | ↑(algebraMap R P) x ∈ J},
                            add_mem' :=
                              (_ :
                                ∀ {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}) },
                        zero_mem' :=
                          (_ :
                            0 ∈
                              { carrier := {x | ↑(algebraMap R P) x ∈ J},
                                  add_mem' :=
                                    (_ :
                                      ∀ {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}) }.carrier) }.toAddSubsemigroup.carrier) }
exact mem_setOf.mpr ⟨y, hx, rfl⟩
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ J ≤ 1
case mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
⊢ (∃ I, ↑I = J) → J ≤ 1
rintro ⟨I, hI⟩
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ ↑I ≤ 1
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ J ≤ 1
rw [← hI]
no goals
case mpr.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
J : FractionalIdeal S P
I : Ideal R
hI : ↑I = J
⊢ ↑I ≤ 1
apply coeIdeal_le_one