[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : Kˣ
⊢ spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1
[PROOFSTEP]
simp only [spanSingleton_one, Units.mul_inv', spanSingleton_mul_spanSingleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : Kˣ
⊢ spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1
[PROOFSTEP]
simp only [spanSingleton_one, Units.inv_mul', spanSingleton_mul_spanSingleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
⊢ ↑((fun x =>
          { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
            val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
            inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
        1) =
    ↑1
[PROOFSTEP]
simp only [spanSingleton_one, Units.val_mk, Units.val_one]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x y : Kˣ
⊢ ↑(OneHom.toFun
        {
          toFun := fun x =>
            { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
              val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
              inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
          map_one' :=
            (_ :
              (fun x =>
                    { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                      val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                      inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                  1 =
                1) }
        (x * y)) =
    ↑(OneHom.toFun
          {
            toFun := fun x =>
              { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
            map_one' :=
              (_ :
                (fun x =>
                      { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                        val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                        inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                    1 =
                  1) }
          x *
        OneHom.toFun
          {
            toFun := fun x =>
              { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
            map_one' :=
              (_ :
                (fun x =>
                      { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                        val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                        inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                    1 =
                  1) }
          y)
[PROOFSTEP]
simp only [Units.val_mk, Units.val_mul, spanSingleton_mul_spanSingleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : Kˣ
⊢ ↑(↑(toPrincipalIdeal R K) x) = spanSingleton R⁰ ↑x
[PROOFSTEP]
simp only [toPrincipalIdeal]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : Kˣ
⊢ ↑(↑{
            toOneHom :=
              {
                toFun := fun x =>
                  { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                    val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                    inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                map_one' :=
                  (_ :
                    (fun x =>
                          { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                            val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                            inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : Kˣ),
                  OneHom.toFun
                      {
                        toFun := fun x =>
                          { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                            val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                            inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                        map_one' :=
                          (_ :
                            (fun x =>
                                  { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                    val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                    inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                              val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                              inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                          map_one' :=
                            (_ :
                              (fun x =>
                                    { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                      val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                      inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun x =>
                            { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                              val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                              inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                          map_one' :=
                            (_ :
                              (fun x =>
                                    { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                      val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                      inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                  1 =
                                1) }
                        y) }
        x) =
    spanSingleton R⁰ ↑x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ ↑(toPrincipalIdeal R K) x = I ↔ spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
simp only [toPrincipalIdeal]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
⊢ ↑{
            toOneHom :=
              {
                toFun := fun x =>
                  { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                    val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                    inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                map_one' :=
                  (_ :
                    (fun x =>
                          { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                            val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                            inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                        1 =
                      1) },
            map_mul' :=
              (_ :
                ∀ (x y : Kˣ),
                  OneHom.toFun
                      {
                        toFun := fun x =>
                          { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                            val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                            inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                        map_one' :=
                          (_ :
                            (fun x =>
                                  { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                    val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                    inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                1 =
                              1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun x =>
                            { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                              val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                              inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                          map_one' :=
                            (_ :
                              (fun x =>
                                    { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                      val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                      inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                  1 =
                                1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun x =>
                            { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                              val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                              inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) },
                          map_one' :=
                            (_ :
                              (fun x =>
                                    { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹,
                                      val_inv := (_ : spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1),
                                      inv_val := (_ : spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1) })
                                  1 =
                                1) }
                        y) }
        x =
      I ↔
    spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
exact Units.ext_iff
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈ MonoidHom.range (toPrincipalIdeal R K) ↔ ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) → ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) → ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
exact ⟨x, hx⟩
[GOAL]
case mpr.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
refine ⟨Units.mk0 x ?_, hx⟩
[GOAL]
case mpr.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : DecidableEq L
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
I : (FractionalIdeal R⁰ K)ˣ
hx : spanSingleton R⁰ 0 = ↑I
⊢ False
[PROOFSTEP]
simp [I.ne_zero.symm] at hx 
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk Setoid.r I = ↑mk I
[PROOFSTEP]
rw [ClassGroup.mk, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id, MonoidHom.comp_apply,
  MonoidHom.id_apply, QuotientGroup.mk'_apply]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk Setoid.r I = ↑I
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑mk I = ↑mk J ↔ ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
[PROOFSTEP]
erw [QuotientGroup.mk'_eq_mk', canonicalEquiv_self, Units.map_id, Set.exists_range_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (∃ i,
      ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * ↑(toPrincipalIdeal R (FractionRing R)) i =
        ↑(MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔
    ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ ↑mk I = ↑mk J ↔ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
[PROOFSTEP]
rw [ClassGroup.mk_eq_mk]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J) ↔
    ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J) →
    ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
x : (FractionRing R)ˣ
hJ : ↑(I * ↑(toPrincipalIdeal R (FractionRing R)) x) = ↑J'
⊢ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
[PROOFSTEP]
rw [Units.val_mul, hI, coe_toPrincipalIdeal, mul_comm, spanSingleton_mul_coeIdeal_eq_coeIdeal] at hJ 
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
x : (FractionRing R)ˣ
hJ : Ideal.span {(sec R⁰ ↑x).fst} * I' = Ideal.span {↑(sec R⁰ ↑x).snd} * J'
⊢ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
[PROOFSTEP]
exact ⟨_, _, sec_fst_ne_zero (R := R) le_rfl x.ne_zero, sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J') →
    ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
[PROOFSTEP]
rintro ⟨x, y, hx, hy, h⟩
[GOAL]
case mpr.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ ∃ x, I * ↑(toPrincipalIdeal R (FractionRing R)) x = J
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.intro.intro.intro.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ I * ↑(toPrincipalIdeal R (FractionRing R)) ?mpr.intro.intro.intro.intro.w = J
case mpr.intro.intro.intro.intro.w
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ (FractionRing R)ˣ
[PROOFSTEP]
rw [mul_comm, ← Units.eq_iff, Units.val_mul, coe_toPrincipalIdeal]
[GOAL]
case mpr.intro.intro.intro.intro.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ spanSingleton R⁰ ↑?mpr.intro.intro.intro.intro.h * ↑I = ↑J
case mpr.intro.intro.intro.intro.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ (FractionRing R)ˣ
[PROOFSTEP]
convert (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h
[GOAL]
case h.e'_2.h.e'_5.h.e'_8
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ ↑?mpr.intro.intro.intro.intro.h = mk' (FractionRing R) x { val := y, property := (_ : y ∈ R⁰) }
case mpr.intro.intro.intro.intro.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ (FractionRing R)ˣ
[PROOFSTEP]
apply (Ne.isUnit _).unit_spec
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ mk' (FractionRing R) x { val := y, property := (_ : y ∈ R⁰) } ≠ 0
[PROOFSTEP]
rwa [Ne, mk'_eq_zero_iff_eq_zero]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑mk I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
  ClassGroup.mk_eq_mk_of_coe_ideal hI (?_ : _ = ↑(⊤ : Ideal R))]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑⊤
[PROOFSTEP]
any_goals rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑⊤
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rintro ⟨x, y, hx, hy, h⟩
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rw [Ideal.mul_top] at h 
[GOAL]
case mp.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with ⟨i, _hi, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x * i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h 
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
[PROOFSTEP]
exact ⟨i, right_ne_zero_of_mul hy, h⟩
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ ∃ x_1 y, x_1 ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x_1} * Ideal.span {x} = Ideal.span {y} * ⊤
[PROOFSTEP]
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ Ideal.span {1} * Ideal.span {x} = Ideal.span {x} * ⊤
[PROOFSTEP]
rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (↑mk I)
x : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ P ↑I
[PROOFSTEP]
have :
  I =
    (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
      (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) :=
  by simp [← Units.eq_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (↑mk I)
x : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ I =
    ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) I)
[PROOFSTEP]
simp [← Units.eq_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (↑mk I)
x : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
this :
  I =
    ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) I)
⊢ P ↑I
[PROOFSTEP]
rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (↑mk I)
x : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
this :
  I =
    ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) I)
⊢ P
    ↑(↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))))
        (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) I))
[PROOFSTEP]
exact h _
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
⊢ ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ MonoidHom.range (toPrincipalIdeal R K)
[PROOFSTEP]
haveI :
  Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
      (toPrincipalIdeal R (FractionRing R)).range =
    (toPrincipalIdeal R K).range :=
  by
  ext I
  simp only [Subgroup.mem_map, mem_principal_ideals_iff]
  constructor
  · rintro ⟨I, ⟨x, hx⟩, rfl⟩
    refine ⟨FractionRing.algEquiv R K x, ?_⟩
    simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
      canonicalEquiv_spanSingleton]
    rfl
  · rintro ⟨x, hx⟩
    refine
      ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I, ⟨(FractionRing.algEquiv R K).symm x, ?_⟩,
        Units.ext ?_⟩
    · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
        canonicalEquiv_spanSingleton]
      rfl
    ·
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, RingEquiv.coe_toMulEquiv,
        canonicalEquiv_canonicalEquiv, canonicalEquiv_self, RingEquiv.refl_apply]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
⊢ Subgroup.map (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))))
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) =
    MonoidHom.range (toPrincipalIdeal R K)
[PROOFSTEP]
ext I
[GOAL]
case h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈
      Subgroup.map (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))))
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) ↔
    I ∈ MonoidHom.range (toPrincipalIdeal R K)
[PROOFSTEP]
simp only [Subgroup.mem_map, mem_principal_ideals_iff]
[GOAL]
case h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        ↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) x = I) ↔
    ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        ↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) x = I) →
    ∃ x, spanSingleton R⁰ x = ↑I
[PROOFSTEP]
rintro ⟨I, ⟨x, hx⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x,
    spanSingleton R⁰ x =
      ↑(↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) I)
[PROOFSTEP]
refine ⟨FractionRing.algEquiv R K x, ?_⟩
[GOAL]
case h.mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ (↑(FractionRing.algEquiv R K) x) =
    ↑(↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) I)
[PROOFSTEP]
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
  canonicalEquiv_spanSingleton]
[GOAL]
case h.mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ (↑(FractionRing.algEquiv R K) x) =
    spanSingleton R⁰ (↑(IsLocalization.map K (RingHom.id R) (_ : ∀ (y : R), y ∈ R⁰ → ↑(RingHom.id R) y ∈ R⁰)) x)
[PROOFSTEP]
rfl
[GOAL]
case h.mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) →
    ∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        ↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) x = I
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case h.mpr.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ∃ x,
    (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
      ↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)))) x = I
[PROOFSTEP]
refine
  ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I, ⟨(FractionRing.algEquiv R K).symm x, ?_⟩,
    Units.ext ?_⟩
[GOAL]
case h.mpr.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ (↑(AlgEquiv.symm (FractionRing.algEquiv R K)) x) =
    ↑(↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R)))) I)
[PROOFSTEP]
simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
[GOAL]
case h.mpr.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ spanSingleton R⁰ (↑(AlgEquiv.symm (FractionRing.algEquiv R K)) x) =
    spanSingleton R⁰
      (↑(IsLocalization.map (FractionRing R) (RingHom.id R) (_ : ∀ (y : R), y ∈ R⁰ → ↑(RingHom.id R) y ∈ R⁰)) x)
[PROOFSTEP]
rfl
[GOAL]
case h.mpr.intro.refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = ↑I
⊢ ↑(↑(MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))))
        (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R)))) I)) =
    ↑I
[PROOFSTEP]
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, RingEquiv.coe_toMulEquiv,
  canonicalEquiv_canonicalEquiv, canonicalEquiv_self, RingEquiv.refl_apply]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
this :
  Subgroup.map (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))))
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) =
    MonoidHom.range (toPrincipalIdeal R K)
⊢ ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ MonoidHom.range (toPrincipalIdeal R K)
[PROOFSTEP]
exact
  @QuotientGroup.congr (FractionalIdeal R⁰ (FractionRing R))ˣ _ (FractionalIdeal R⁰ K)ˣ _
    (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K).range _ _
    (Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(equiv K') (↑mk I) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
[PROOFSTEP]
rw [ClassGroup.equiv, ClassGroup.mk, MonoidHom.comp_apply, QuotientGroup.congr_mk']
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K')))
      (↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
        (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K'))) (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I
[PROOFSTEP]
rw [← Units.eq_iff, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
[GOAL]
case h.e_6.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) (↑↑(canonicalEquiv R⁰ K (FractionRing R)) ↑I) =
    ↑↑(canonicalEquiv R⁰ K K') ↑I
[PROOFSTEP]
exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑mk (↑(Units.map ↑(canonicalEquiv R⁰ K K')) I) = ↑mk I
[PROOFSTEP]
rw [ClassGroup.mk, MonoidHom.comp_apply, ← MonoidHom.comp_apply (Units.map _), ← Units.map_comp, ←
  RingEquiv.coe_monoidHom_trans, FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra K L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
      (↑(Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    ↑mk I
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ (fun I => Units.mk0 ↑↑I (_ : ↑↑I ≠ 0)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
x y : { x // x ∈ (Ideal R)⁰ }
⊢ OneHom.toFun { toFun := fun I => Units.mk0 ↑↑I (_ : ↑↑I ≠ 0), map_one' := (_ : Units.mk0 ↑↑1 (_ : ↑↑1 ≠ 0) = 1) }
      (x * y) =
    OneHom.toFun { toFun := fun I => Units.mk0 ↑↑I (_ : ↑↑I ≠ 0), map_one' := (_ : Units.mk0 ↑↑1 (_ : ↑↑1 ≠ 0) = 1) }
        x *
      OneHom.toFun { toFun := fun I => Units.mk0 ↑↑I (_ : ↑↑I ≠ 0), map_one' := (_ : Units.mk0 ↑↑1 (_ : ↑↑1 ≠ 0) = 1) }
        y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : DecidableEq L
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra K L
inst✝⁷ : FiniteDimensional K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R K L
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K' : Type u_4
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(canonicalEquiv R⁰ K K') ↑(↑(mk0 K) I) = ↑(↑(mk0 K') I)
[PROOFSTEP]
simp only [FractionalIdeal.coe_mk0, FractionalIdeal.canonicalEquiv_coeIdeal]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑mk (↑(FractionalIdeal.mk0 K) I) = ↑mk0 I
[PROOFSTEP]
rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
  FractionalIdeal.map_canonicalEquiv_mk0]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(equiv K) (↑mk0 I) = ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) (↑(FractionalIdeal.mk0 K) I)
[PROOFSTEP]
rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)))
      (↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I)) =
    ↑(QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K))) (↑(FractionalIdeal.mk0 K) I)
[PROOFSTEP]
congr 1
[GOAL]
case h.e_6.h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) (↑(FractionalIdeal.mk0 (FractionRing R)) I) =
    ↑(FractionalIdeal.mk0 K) I
[PROOFSTEP]
simp [← Units.eq_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ ↑mk0 I = ↑mk0 J ↔ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ ↑(equiv K) (↑mk0 I) = ↑(equiv K) (↑mk0 J) ↔ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
simp only [ClassGroup.equiv_mk0, QuotientGroup.mk'_eq_mk', mem_principal_ideals_iff, Units.ext_iff, Units.val_mul,
  FractionalIdeal.coe_mk0, exists_prop]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) ↔ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) → ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
rintro ⟨X, ⟨x, hX⟩, hx⟩
[GOAL]
case mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
refine ⟨x, ?_, ?_⟩
[GOAL]
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
hX : spanSingleton R⁰ 0 = ↑X
⊢ False
[PROOFSTEP]
simp [X.ne_zero.symm] at hX 
[GOAL]
case mp.intro.intro.intro.refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
X : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
simpa only [hX, mul_comm] using hx
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
[PROOFSTEP]
rintro ⟨x, hx, eq_J⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
[PROOFSTEP]
refine ⟨Units.mk0 _ (spanSingleton_ne_zero_iff.mpr hx), ⟨x, rfl⟩, ?_⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ↑↑I * ↑(Units.mk0 (spanSingleton R⁰ x) (_ : spanSingleton R⁰ x ≠ 0)) = ↑↑J
[PROOFSTEP]
simpa only [mul_comm] using eq_J
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ ↑mk0 I = ↑mk0 J ↔ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
[PROOFSTEP]
refine (ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring (FractionRing R)).trans ⟨?_, ?_⟩
[GOAL]
case refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
[PROOFSTEP]
rintro ⟨z, hz, h⟩
[GOAL]
case refine_1.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
z : FractionRing R
hz : z ≠ 0
h : spanSingleton R⁰ z * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
[PROOFSTEP]
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective R⁰ z
[GOAL]
case refine_1.intro.intro.intro.intro.mk
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
[PROOFSTEP]
refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩
[GOAL]
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ x ≠ 0
[PROOFSTEP]
rintro hx
[GOAL]
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ False
[PROOFSTEP]
apply hz
[GOAL]
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ mk' (FractionRing R) x { val := y, property := hy } = 0
[PROOFSTEP]
rw [hx, IsFractionRing.mk'_eq_div, _root_.map_zero, zero_div]
[GOAL]
case refine_1.intro.intro.intro.intro.mk.refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
[PROOFSTEP]
exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy).mp h
[GOAL]
case refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) → ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
rintro ⟨x, y, hx, hy, h⟩
[GOAL]
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
have hy' : y ∈ R⁰ := mem_nonZeroDivisors_iff_ne_zero.mpr hy
[GOAL]
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
[PROOFSTEP]
refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩
[GOAL]
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ mk' (FractionRing R) x { val := y, property := hy' } ≠ 0
[PROOFSTEP]
contrapose! hx
[GOAL]
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : mk' (FractionRing R) x { val := y, property := hy' } = 0
⊢ x = 0
[PROOFSTEP]
rwa [mk'_eq_iff_eq_mul, zero_mul, ← (algebraMap R (FractionRing R)).map_zero,
  (IsFractionRing.injective R (FractionRing R)).eq_iff] at hx 
[GOAL]
case refine_2.intro.intro.intro.intro.refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy' }) * ↑↑I = ↑↑J
[PROOFSTEP]
exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy').mpr h
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ ∀ {a_1 b : R},
    a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
      b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
        a_1 + b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, RingHom.map_add, mul_add]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ ∀ {a b : R},
    (↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ * ↑(algebraMap R (FractionRing R)) a ∈
        ↑I →
      (↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ *
            ↑(algebraMap R (FractionRing R)) b ∈
          ↑I →
        (↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ *
              ↑(algebraMap R (FractionRing R)) a +
            (↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ *
              ↑(algebraMap R (FractionRing R)) b ∈
          ↑I
[PROOFSTEP]
exact fun ha hb => Submodule.add_mem _ ha hb
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ 0 ∈
    { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
        add_mem' :=
          (_ :
            ∀ {a_1 b : R},
              a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                  a_1 + b ∈
                    {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) }.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq, RingHom.map_zero, mul_zero]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ 0 ∈ ↑I
[PROOFSTEP]
exact Submodule.zero_mem _
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ ∀ (c : R) {x : R},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                  add_mem' :=
                    (_ :
                      ∀ {a_1 b : R},
                        a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                          b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            a_1 + b ∈
                              {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                        add_mem' :=
                          (_ :
                            ∀ {a_1 b : R},
                              a_1 ∈
                                  {x |
                                    (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                                b ∈
                                    {x |
                                      (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                        ↑I} →
                                  a_1 + b ∈
                                    {x |
                                      (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                        ↑I}) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                  add_mem' :=
                    (_ :
                      ∀ {a_2 b : R},
                        a_2 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                          b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            a_2 + b ∈
                              {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                        add_mem' :=
                          (_ :
                            ∀ {a_2 b : R},
                              a_2 ∈
                                  {x |
                                    (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                                b ∈
                                    {x |
                                      (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                        ↑I} →
                                  a_2 + b ∈
                                    {x |
                                      (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                        ↑I}) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
intro c _ hb
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
c x✝ : R
hb :
  x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
              add_mem' :=
                (_ :
                  ∀ {a_1 b : R},
                    a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                      b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                        a_1 + b ∈
                          {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                    add_mem' :=
                      (_ :
                        ∀ {a_1 b : R},
                          a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                              a_1 + b ∈
                                {x |
                                  (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                    ↑I}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c • x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
              add_mem' :=
                (_ :
                  ∀ {a_1 b : R},
                    a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                      b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                        a_1 + b ∈
                          {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                    add_mem' :=
                      (_ :
                        ∀ {a_1 b : R},
                          a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                              a_1 + b ∈
                                {x |
                                  (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                    ↑I}) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp only [smul_eq_mul, Set.mem_setOf_eq, RingHom.map_mul, mul_left_comm ((algebraMap R (FractionRing R)) a)⁻¹]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
c x✝ : R
hb :
  x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
              add_mem' :=
                (_ :
                  ∀ {a_1 b : R},
                    a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                      b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                        a_1 + b ∈
                          {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                    add_mem' :=
                      (_ :
                        ∀ {a_1 b : R},
                          a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                              a_1 + b ∈
                                {x |
                                  (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                    ↑I}) }.carrier) }.toAddSubsemigroup.carrier
⊢ ↑(algebraMap R (FractionRing R)) c *
      ((↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ *
        ↑(algebraMap R (FractionRing R)) x✝) ∈
    ↑I
[PROOFSTEP]
rw [← Algebra.smul_def c]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
c x✝ : R
hb :
  x✝ ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
              add_mem' :=
                (_ :
                  ∀ {a_1 b : R},
                    a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                      b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                        a_1 + b ∈
                          {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I},
                    add_mem' :=
                      (_ :
                        ∀ {a_1 b : R},
                          a_1 ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                            b ∈ {x | (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈ ↑I} →
                              a_1 + b ∈
                                {x |
                                  (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) x ∈
                                    ↑I}) }.carrier) }.toAddSubsemigroup.carrier
⊢ c •
      ((↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑I)))⁻¹ *
        ↑(algebraMap R (FractionRing R)) x✝) ∈
    ↑I
[PROOFSTEP]
exact Submodule.smul_mem _ c hb
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
⊢ integralRep I ∈ (Ideal R)⁰
[PROOFSTEP]
let a := I.2.choose
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
⊢ integralRep I ∈ (Ideal R)⁰
[PROOFSTEP]
have a_ne_zero' := I.2.choose_spec.1
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
⊢ integralRep I ∈ (Ideal R)⁰
[PROOFSTEP]
have a_ne_zero := mem_nonZeroDivisors_iff_ne_zero.mp a_ne_zero'
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
⊢ integralRep I ∈ (Ideal R)⁰
[PROOFSTEP]
have fa_ne_zero : (algebraMap R (FractionRing R)) a ≠ 0 :=
  IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors a_ne_zero'
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ integralRep I ∈ (Ideal R)⁰
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot, Submodule.ne_bot_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ∃ x, x ∈ integralRep I ∧ x ≠ 0
[PROOFSTEP]
obtain ⟨x, x_ne, x_mem⟩ := exists_ne_zero_mem_isInteger hI
[GOAL]
case intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
x : R
x_ne : x ≠ 0
x_mem : ↑(algebraMap R (FractionRing R)) x ∈ I
⊢ ∃ x, x ∈ integralRep I ∧ x ≠ 0
[PROOFSTEP]
refine ⟨a * x, ?_, mul_ne_zero a_ne_zero x_ne⟩
[GOAL]
case intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
x : R
x_ne : x ≠ 0
x_mem : ↑(algebraMap R (FractionRing R)) x ∈ I
⊢ a * x ∈ integralRep I
[PROOFSTEP]
change ((algebraMap R _) a)⁻¹ * (algebraMap R _) (a * x) ∈ I
[GOAL]
case intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
a : R := Exists.choose (_ : IsFractional R⁰ ↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑I) ∈ R⁰
a_ne_zero : Exists.choose (_ : IsFractional R⁰ ↑I) ≠ 0
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
x : R
x_ne : x ≠ 0
x_mem : ↑(algebraMap R (FractionRing R)) x ∈ I
⊢ (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) (a * x) ∈ I
[PROOFSTEP]
rwa [RingHom.map_mul, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = ↑mk I
[PROOFSTEP]
let a := I.1.2.choose
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = ↑mk I
[PROOFSTEP]
have a_ne_zero' := I.1.2.choose_spec.1
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = ↑mk I
[PROOFSTEP]
have ha := I.1.2.choose_spec.2
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = ↑mk I
[PROOFSTEP]
have fa_ne_zero : (algebraMap R (FractionRing R)) a ≠ 0 :=
  IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors a_ne_zero'
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = ↑mk I
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑mk I = ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) }
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑(Units.map ↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R))) I ≈
    ↑(Units.map ↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)))
      (↑(FractionalIdeal.mk0 (FractionRing R)) { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) })
[PROOFSTEP]
change @Setoid.r _ (QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) _ _
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ Setoid.r (↑(Units.map ↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R))) I)
    (↑(Units.map ↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)))
      (↑(FractionalIdeal.mk0 (FractionRing R))
        { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) }))
[PROOFSTEP]
rw [canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id, MonoidHom.id_apply, MonoidHom.id_apply,
  QuotientGroup.leftRel_apply]
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ I⁻¹ *
      ↑(FractionalIdeal.mk0 (FractionRing R)) { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } ∈
    MonoidHom.range (toPrincipalIdeal R (FractionRing R))
[PROOFSTEP]
refine ⟨Units.mk0 (algebraMap R _ a) fa_ne_zero, ?_⟩
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑(toPrincipalIdeal R (FractionRing R)) (Units.mk0 (↑(algebraMap R (FractionRing R)) a) fa_ne_zero) =
    I⁻¹ *
      ↑(FractionalIdeal.mk0 (FractionRing R)) { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) }
[PROOFSTEP]
rw [_root_.eq_inv_mul_iff_mul_eq, eq_comm, mul_comm I]
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑(FractionalIdeal.mk0 (FractionRing R)) { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } =
    ↑(toPrincipalIdeal R (FractionRing R)) (Units.mk0 (↑(algebraMap R (FractionRing R)) a) fa_ne_zero) * I
[PROOFSTEP]
apply Units.ext
[GOAL]
case a.a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ↑(↑(FractionalIdeal.mk0 (FractionRing R)) { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) }) =
    ↑(↑(toPrincipalIdeal R (FractionRing R)) (Units.mk0 (↑(algebraMap R (FractionRing R)) a) fa_ne_zero) * I)
[PROOFSTEP]
simp only [FractionalIdeal.coe_mk0, FractionalIdeal.map_canonicalEquiv_mk0, Units.val_mk0, coe_toPrincipalIdeal,
  Units.val_mul, FractionalIdeal.eq_spanSingleton_mul]
[GOAL]
case a.a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ (∀ (zI : FractionRing R),
      zI ∈ ↑(integralRep ↑I) →
        ∃ zJ, zJ ∈ ↑I ∧ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zJ = zI) ∧
    ∀ (z : FractionRing R),
      z ∈ ↑I → ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * z ∈ ↑(integralRep ↑I)
[PROOFSTEP]
constructor
[GOAL]
case a.a.left
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ∀ (zI : FractionRing R),
    zI ∈ ↑(integralRep ↑I) →
      ∃ zJ, zJ ∈ ↑I ∧ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zJ = zI
[PROOFSTEP]
intro zJ' hzJ'
[GOAL]
case a.a.left
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zJ' : FractionRing R
hzJ' : zJ' ∈ ↑(integralRep ↑I)
⊢ ∃ zJ, zJ ∈ ↑I ∧ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zJ = zJ'
[PROOFSTEP]
obtain ⟨zJ, hzJ, rfl⟩ := (mem_coeIdeal R⁰).mp hzJ'
[GOAL]
case a.a.left.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zJ : R
hzJ : zJ ∈ integralRep ↑I
hzJ' : ↑(algebraMap R (FractionRing R)) zJ ∈ ↑(integralRep ↑I)
⊢ ∃ zJ_1,
    zJ_1 ∈ ↑I ∧
      ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zJ_1 =
        ↑(algebraMap R (FractionRing R)) zJ
[PROOFSTEP]
refine ⟨_, hzJ, ?_⟩
[GOAL]
case a.a.left.intro.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zJ : R
hzJ : zJ ∈ integralRep ↑I
hzJ' : ↑(algebraMap R (FractionRing R)) zJ ∈ ↑(integralRep ↑I)
⊢ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) *
      ((↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)))⁻¹ *
        ↑(algebraMap R (FractionRing R)) zJ) =
    ↑(algebraMap R (FractionRing R)) zJ
[PROOFSTEP]
rw [← mul_assoc, mul_inv_cancel fa_ne_zero, one_mul]
[GOAL]
case a.a.right
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
⊢ ∀ (z : FractionRing R),
    z ∈ ↑I → ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * z ∈ ↑(integralRep ↑I)
[PROOFSTEP]
intro zI' hzI'
[GOAL]
case a.a.right
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zI' : FractionRing R
hzI' : zI' ∈ ↑I
⊢ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zI' ∈ ↑(integralRep ↑I)
[PROOFSTEP]
obtain ⟨y, hy⟩ := ha zI' hzI'
[GOAL]
case a.a.right.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zI' : FractionRing R
hzI' : zI' ∈ ↑I
y : R
hy : ↑(algebraMap R (FractionRing R)) y = Exists.choose (_ : IsFractional R⁰ ↑↑I) • zI'
⊢ ↑(algebraMap R (FractionRing R)) (Exists.choose (_ : IsFractional R⁰ ↑↑I)) * zI' ∈ ↑(integralRep ↑I)
[PROOFSTEP]
rw [← Algebra.smul_def, mem_coeIdeal]
[GOAL]
case a.a.right.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zI' : FractionRing R
hzI' : zI' ∈ ↑I
y : R
hy : ↑(algebraMap R (FractionRing R)) y = Exists.choose (_ : IsFractional R⁰ ↑↑I) • zI'
⊢ ∃ x', x' ∈ integralRep ↑I ∧ ↑(algebraMap R (FractionRing R)) x' = Exists.choose (_ : IsFractional R⁰ ↑↑I) • zI'
[PROOFSTEP]
refine' ⟨y, _, hy⟩
[GOAL]
case a.a.right.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zI' : FractionRing R
hzI' : zI' ∈ ↑I
y : R
hy : ↑(algebraMap R (FractionRing R)) y = Exists.choose (_ : IsFractional R⁰ ↑↑I) • zI'
⊢ y ∈ integralRep ↑I
[PROOFSTEP]
show (algebraMap R _ a)⁻¹ * algebraMap R _ y ∈ (I : FractionalIdeal R⁰ (FractionRing R))
[GOAL]
case a.a.right.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
a : R := Exists.choose (_ : IsFractional R⁰ ↑↑I)
a_ne_zero' : Exists.choose (_ : IsFractional R⁰ ↑↑I) ∈ R⁰
ha : ∀ (b : FractionRing R), b ∈ ↑↑I → IsInteger R (Exists.choose (_ : IsFractional R⁰ ↑↑I) • b)
fa_ne_zero : ↑(algebraMap R (FractionRing R)) a ≠ 0
zI' : FractionRing R
hzI' : zI' ∈ ↑I
y : R
hy : ↑(algebraMap R (FractionRing R)) y = Exists.choose (_ : IsFractional R⁰ ↑↑I) • zI'
⊢ (↑(algebraMap R (FractionRing R)) a)⁻¹ * ↑(algebraMap R (FractionRing R)) y ∈ ↑I
[PROOFSTEP]
rwa [hy, Algebra.smul_def, ← mul_assoc, inv_mul_cancel fa_ne_zero, one_mul]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ Function.Surjective ↑mk0
[PROOFSTEP]
rintro ⟨I⟩
[GOAL]
case mk
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ∃ a, ↑mk0 a = Quot.mk Setoid.r I
[PROOFSTEP]
refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩
[GOAL]
case mk
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑mk0 { val := integralRep ↑I, property := (_ : integralRep ↑I ∈ (Ideal R)⁰) } = Quot.mk Setoid.r I
[PROOFSTEP]
rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑mk I = 1 ↔ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
rw [← (ClassGroup.equiv K).injective.eq_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ ↑(equiv K) (↑mk I) = ↑(equiv K) 1 ↔ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
simp only [equiv_mk, canonicalEquiv_self, RingEquiv.coe_mulEquiv_refl, QuotientGroup.mk'_apply, _root_.map_one,
  QuotientGroup.eq_one_iff, MonoidHom.mem_range, ext_iff, coe_toPrincipalIdeal, coe_mapEquiv, MulEquiv.refl_apply]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ Submodule.IsPrincipal ↑↑I
[PROOFSTEP]
refine ⟨fun ⟨x, hx⟩ => ⟨⟨x, by rw [← hx, coe_spanSingleton]⟩⟩, ?_⟩
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x✝ : ∃ x, spanSingleton R⁰ ↑x = ↑I
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ↑↑I = Submodule.span R {↑x}
[PROOFSTEP]
rw [← hx, coe_spanSingleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ Submodule.IsPrincipal ↑↑I → ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
intro hI
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
obtain ⟨x, hx⟩ := @Submodule.IsPrincipal.principal _ _ _ _ _ _ hI
[GOAL]
case intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
have hx' : (I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x :=
  by
  apply Subtype.coe_injective
  simp only [val_eq_coe, hx, coe_spanSingleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ↑I = spanSingleton R⁰ x
[PROOFSTEP]
apply Subtype.coe_injective
[GOAL]
case a
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ (fun a => ↑a) ↑I = (fun a => ↑a) (spanSingleton R⁰ x)
[PROOFSTEP]
simp only [val_eq_coe, hx, coe_spanSingleton]
[GOAL]
case intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
[PROOFSTEP]
refine ⟨Units.mk0 x ?_, ?_⟩
[GOAL]
case intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0
[PROOFSTEP]
intro x_eq
[GOAL]
case intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ False
[PROOFSTEP]
apply Units.ne_zero I
[GOAL]
case intro.refine_1
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0
[PROOFSTEP]
simp [hx', x_eq]
[GOAL]
case intro.refine_2
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x (_ : x = 0 → False)) = ↑I
[PROOFSTEP]
simp [hx']
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), x ∈ {1}
[PROOFSTEP]
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑ClassGroup.mk I ∈ {1}
[PROOFSTEP]
rw [Finset.mem_singleton]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑ClassGroup.mk I = 1
[PROOFSTEP]
exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1
[PROOFSTEP]
rw [Fintype.card_eq_one_iff]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∃ x, ∀ (y : ClassGroup R), y = x
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (y : ClassGroup R), y = 1
[PROOFSTEP]
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
[GOAL]
case h
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ↑ClassGroup.mk I = 1
[PROOFSTEP]
exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1
[PROOFSTEP]
swap
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1
[PROOFSTEP]
intros
[GOAL]
case mpr
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
a✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1
[PROOFSTEP]
convert card_classGroup_eq_one (R := R)
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
[PROOFSTEP]
rw [Fintype.card_eq_one_iff]
[GOAL]
case mp
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ (∃ x, ∀ (y : ClassGroup R), y = x) → IsPrincipalIdealRing R
[PROOFSTEP]
rintro ⟨I, hI⟩
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I
⊢ IsPrincipalIdealRing R
[PROOFSTEP]
have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I
eq_one : ∀ (J : ClassGroup R), J = 1
⊢ IsPrincipalIdealRing R
[PROOFSTEP]
refine ⟨fun I => ?_⟩
[GOAL]
case mp.intro
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
by_cases hI : I = ⊥
[GOAL]
case pos
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
rw [hI]
[GOAL]
case pos
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal ⊥
[PROOFSTEP]
exact bot_isPrincipal
[GOAL]
case neg
R : Type u_1
K : Type u_2
L : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : DecidableEq L
inst✝⁸ : Algebra R K
inst✝⁷ : IsFractionRing R K
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : ¬I = ⊥
⊢ Submodule.IsPrincipal I
[PROOFSTEP]
exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)
