∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Ring : Type w)
  [commRing : CommRing Ring] [algebra₁ : Algebra R Ring] [algebra₂ : Algebra Ring S]
  [isScalarTower : IsScalarTower R Ring S] (σ : S → Ring) (algebraMap_σ : ∀ (x : S), (algebraMap Ring S) (σ x) = x)
  (Ring_1 : Type w) (commRing_1 : CommRing Ring_1) (algebra₁_1 : Algebra R Ring_1) (algebra₂_1 : Algebra Ring_1 S)
  (isScalarTower_1 : IsScalarTower R Ring_1 S) (σ_1 : S → Ring_1)
  (algebraMap_σ_1 : ∀ (x : S), (algebraMap Ring_1 S) (σ_1 x) = x),
  ({ Ring := Ring, commRing := commRing, algebra₁ := algebra₁, algebra₂ := algebra₂, isScalarTower := isScalarTower,
        σ := σ, algebraMap_σ := algebraMap_σ } =
      { Ring := Ring_1, commRing := commRing_1, algebra₁ := algebra₁_1, algebra₂ := algebra₂_1,
        isScalarTower := isScalarTower_1, σ := σ_1, algebraMap_σ := algebraMap_σ_1 }) =
    (Ring = Ring_1 ∧ commRing ≍ commRing_1 ∧ algebra₁ ≍ algebra₁_1 ∧ algebra₂ ≍ algebra₂_1 ∧ σ ≍ σ_1)