awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ Eq (α := B →+* L) (algebraMap B L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap B Bₘ))
have rw : Eq (α := B →+* L) (algebraMap B L) (g.comp (algebraMap B Bₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this : Algebra Bₘ L := g.toAlgebra
rw : Eq (α := B →+* L) (algebraMap B L) (g.comp (algebraMap B Bₘ))
⊢ Eq (α := B →+* L) (algebraMap B L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap B Bₘ))
have rw₁ : Eq (α := B →+* L) (algebraMap B L) (RingHom.comp (algebraMap B L) (RingHom.id B))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this : Algebra Bₘ L := g.toAlgebra
rw : Eq (α := B →+* L) (algebraMap B L) (g.comp (algebraMap B Bₘ))
rw₁ : Eq (α := B →+* L) (algebraMap B L) (RingHom.comp (algebraMap B L) (RingHom.id B))
⊢ Eq (α := B →+* L) (algebraMap B L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap B Bₘ))
have rw₂ : Eq (α := B →+* L) (algebraMap B L) (algebraMap B L)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intNorm A B : (a : B) → A) x : A) : Aₘ)
    ((intNorm Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have this₁ : IsScalarTower B Bₘ L
Tactic: have : IsScalarTower B Bₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intNorm A B : (a : B) → A) x : A) : Aₘ)
    ((intNorm Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have this₁ : IsScalarTower Aₘ K L
Tactic: have : IsScalarTower Aₘ K L := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
⊢ IsScalarTower Aₘ Bₘ L
have h : Eq (α := Aₘ →+* L) (algebraMap Aₘ L)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ))
Tactic: apply IsScalarTower.of_algebraMap_eq'
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
⊢ Eq (α := Aₘ →+* L) (algebraMap Aₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ))
have h : Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
Tactic: apply IsLocalization.ringHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
have h : Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Bₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B Bₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
h :
  Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
have h₁ : Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Bₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B Bₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
h :
  Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
h₁ :
  Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
have h₂ : Eq (α := A →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap A Aₘ)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Bₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B Bₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
h :
  Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
h₁ :
  Eq (α := A →+* L) (RingHom.comp (RingHom.comp (algebraMap K L) f) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
h₂ :
  Eq (α := A →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap A Aₘ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (g.comp (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
have h₃ : Eq (α := A →+* L) (RingHom.comp (algebraMap K L) (f.comp (algebraMap A Aₘ)))
  (g.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ Bₘ) (algebraMap A Aₘ)))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Bₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B Bₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]