R : Type u_1
K : Type u_2
L : Type ?u.669485
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
R : Type u_1
K : Type u_2
L : Type ?u.669485
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
have : I = (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
  (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) := by
  simp [← Units.eq_iff]
R : Type u_1
K : Type u_2
L : Type ?u.669485
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))
R : Type u_1
K : Type u_2
L : Type ?u.669485
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
rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
no goals
R : Type u_1
K : Type u_2
L : Type ?u.669485
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))
exact h _
no goals
R : Type u_1
K : Type u_2
L : Type ?u.669485
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)
simp [← Units.eq_iff]