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
inst_3 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
inst_10 : Module.Finite A B
x : B
this : IsIntegralClosure B A (FractionRing B)
h :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((norm A : (a : B) → A) x) : FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((norm A : (a : B) → A) x) : FractionRing A)
have h₁ : Eq (α := FractionRing A)
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((norm A : (a : B) → A) x) : FractionRing A)
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((norm A : (a : B) → A) x) : FractionRing A)
Tactic: rw [Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization A A⁰]
-- 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
inst_3 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
inst_9 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) 0 : A) (0 : A)
have this : IsIntegralClosure B A (FractionRing B)
Tactic: haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- 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
inst_3 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
inst_9 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsIntegralClosure B A (FractionRing B)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) 0 : A) (0 : A)
have a : Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) 0))
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) 0)
Tactic: apply IsFractionRing.injective A (FractionRing A)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : IsIntegrallyClosed A
inst_6 : IsDomain A
inst_7 : IsDomain B
inst_8 : IsIntegrallyClosed B
inst_9 : Algebra.IsIntegral A B
inst_10 : IsTorsionFree A B
inst_11 : IsDomain B₂
inst_12 : IsIntegrallyClosed B₂
inst_13 : Algebra.IsIntegral A B₂
inst_14 : IsTorsionFree A B₂
inst_15 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
inst_16 : Algebra.IsAlgebraic.{u_1, u_7} (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂) : A)
    ((intNorm A B : (a : B) → A) x : A)
have a : Eq (α := FractionRing A)
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
      ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂)) :
    FractionRing A)
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
Tactic: apply FaithfulSMul.algebraMap_injective A (FractionRing A)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : IsIntegrallyClosed A
inst_6 : IsDomain A
inst_7 : IsDomain B
inst_8 : IsIntegrallyClosed B
inst_9 : Algebra.IsIntegral A B
inst_10 : IsTorsionFree A B
inst_11 : IsDomain B₂
inst_12 : IsIntegrallyClosed B₂
inst_13 : Algebra.IsIntegral A B₂
inst_14 : IsTorsionFree A B₂
inst_15 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
inst_16 : Algebra.IsAlgebraic.{u_1, u_7} (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
have a : Eq.{u_1 + 1} (α := FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
      ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
    FractionRing A)
  ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
Tactic: rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : IsIntegrallyClosed A
inst_6 : IsDomain A
inst_7 : IsDomain B
inst_8 : IsIntegrallyClosed B
inst_9 : Algebra.IsIntegral A B
inst_10 : IsTorsionFree A B
inst_11 : IsDomain B₂
inst_12 : IsIntegrallyClosed B₂
inst_13 : Algebra.IsIntegral A B₂
inst_14 : IsTorsionFree A B₂
inst_15 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
inst_16 : Algebra.IsAlgebraic.{u_1, u_7} (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
have a₁ : Eq.{u_1 + 1} (α := FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
      ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
    FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
    FractionRing A)
Tactic: rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : IsIntegrallyClosed A
inst_6 : IsDomain A
inst_7 : IsDomain B
inst_8 : IsIntegrallyClosed B
inst_9 : Algebra.IsIntegral A B
inst_10 : IsTorsionFree A B
inst_11 : IsDomain B₂
inst_12 : IsIntegrallyClosed B₂
inst_13 : Algebra.IsIntegral A B₂
inst_14 : IsTorsionFree A B₂
inst_15 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
inst_16 : Algebra.IsAlgebraic.{u_1, u_7} (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
a₁ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
      FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
have a₂ : Eq.{u_1 + 1} (α := FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
      (((galLiftEquiv (FractionRing A) (FractionRing B) (FractionRing B₂) σ :
            AlgEquiv.{u_1, u_6, u_7} (FractionRing A) (FractionRing B) (FractionRing B₂)) :
          (a : FractionRing B) → FractionRing B₂)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x)) :
    FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
    FractionRing A)
Tactic: rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : IsIntegrallyClosed A
inst_6 : IsDomain A
inst_7 : IsDomain B
inst_8 : IsIntegrallyClosed B
inst_9 : Algebra.IsIntegral A B
inst_10 : IsTorsionFree A B
inst_11 : IsDomain B₂
inst_12 : IsIntegrallyClosed B₂
inst_13 : Algebra.IsIntegral A B₂
inst_14 : IsTorsionFree A B₂
inst_15 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
inst_16 : Algebra.IsAlgebraic.{u_1, u_7} (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
a₁ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        ((algebraMap B₂ (FractionRing B₂) : (a : B₂) → FractionRing B₂) ((σ : (a : B) → B₂) x)) :
      FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
a₂ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B₂) → FractionRing A)
        (((galLiftEquiv (FractionRing A) (FractionRing B) (FractionRing B₂) σ :
              AlgEquiv.{u_1, u_6, u_7} (FractionRing A) (FractionRing B) (FractionRing B₂)) :
            (a : FractionRing B) → FractionRing B₂)
          ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x)) :
      FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B₂ : (a : B₂) → A) ((σ : (a : B) → B₂) x : B₂)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
have a₃ : Eq.{u_1 + 1} (α := FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
    FractionRing A)
  ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
    FractionRing A)
Tactic: rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]
-- 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
inst_3 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
inst_9 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) x : A) (0 : A) ↔ x = 0
have rw : Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) 0 : FractionRing A) ↔
  Eq (α := FractionRing B) ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x : FractionRing B)
    ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) 0 : FractionRing B)
Tactic: rw [← (IsFractionRing.injective A (FractionRing A)).eq_iff,
    ← (IsFractionRing.injective B (FractionRing B)).eq_iff]
-- 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
⊢ 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 pos : ∀ (hM : 0 ∈ M),
  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ₘ)
Tactic: by_cases hM : 0 ∈ 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
pos :
  ∀ (hM : 0 ∈ M),
    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ₘ)
⊢ 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 neg : ∀ (hM : 0 ∉ M),
  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ₘ)
Tactic: by_cases hM : 0 ∈ M
-- 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 : 0 ∉ M
⊢ 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 hM₁ : M ≤ A⁰
Tactic: replace hM : M ≤ A⁰ := fun x hx ↦ mem_nonZeroDivisors_iff_ne_zero.mpr (fun e ↦ hM (e ▸ hx))
Cleared hypotheses: hM
-- 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 : Algebra Aₘ K := f.toAlgebra
⊢ Eq (α := A →+* K) (algebraMap A K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ K) (algebraMap A Aₘ))
have rw : Eq (α := A →+* K) (algebraMap A K) (f.comp (algebraMap A Aₘ))
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 : Algebra Aₘ K := f.toAlgebra
rw : Eq (α := A →+* K) (algebraMap A K) (f.comp (algebraMap A Aₘ))
⊢ Eq (α := A →+* K) (algebraMap A K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ K) (algebraMap A Aₘ))
have rw₁ : Eq (α := A →+* K) (algebraMap A K) (RingHom.comp (algebraMap A K) (RingHom.id A))
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 : Algebra Aₘ K := f.toAlgebra
rw : Eq (α := A →+* K) (algebraMap A K) (f.comp (algebraMap A Aₘ))
rw₁ : Eq (α := A →+* K) (algebraMap A K) (RingHom.comp (algebraMap A K) (RingHom.id A))
⊢ Eq (α := A →+* K) (algebraMap A K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ K) (algebraMap A Aₘ))
have rw₂ : Eq (α := A →+* K) (algebraMap A K) (algebraMap A K)
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 : Algebra Aₘ K := f.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 A Aₘ K
Tactic: have : IsScalarTower A Aₘ K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])