∀ {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