awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
C : Type u_9
inst_9 : CommRing C
inst_10 : IsDomain C
inst_11 : IsIntegrallyClosed C
inst_12 : Algebra A C
inst_13 : Algebra B C
inst_14 : IsScalarTower A B C
inst_15 : Algebra.IsIntegral A C
inst_16 : Algebra.IsIntegral B C
inst_17 : IsTorsionFree A C
inst_18 : IsTorsionFree B C
x : C
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) ((intNorm B C : (a : C) → B) x)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A C : (a : C) → A) x) : FractionRing A)
a₁ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((norm (FractionRing B) : (a : FractionRing C) → FractionRing B)
          ((algebraMap C (FractionRing C) : (a : C) → FractionRing C) x)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A C : (a : C) → A) x) : FractionRing A)
a₂ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((norm (FractionRing B) : (a : FractionRing C) → FractionRing B)
          ((algebraMap C (FractionRing C) : (a : C) → FractionRing C) x)) :
      FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing C) → FractionRing A)
        ((algebraMap C (FractionRing C) : (a : C) → FractionRing C) x) :
      FractionRing A)
a₃ a₄ :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing C) → FractionRing A)
        ((algebraMap C (FractionRing C) : (a : C) → FractionRing C) x) :
      FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing C) → FractionRing A)
        ((algebraMap C (FractionRing C) : (a : C) → FractionRing C) x) :
      FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B : (a : B) → A) ((intNorm B C : (a : C) → B) x : B)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A C : (a : C) → A) x) : FractionRing A)

Tactic:
rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    algebraMap_intNorm_fractionRing, Algebra.norm_norm]

Premises used: Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_norm
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
h : ∀ (x : B), Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) x : A) ((norm A : (a : B) → A) x : A)
⊢ Eq (α := B →* A) (intNorm A B) (norm A)

Tactic:
ext x
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
⊢ IsIntegralClosure B A (FractionRing B)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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 (α := 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)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) x : A) ((norm A : (a : B) → A) x : A)

Tactic:
apply IsFractionRing.injective A (FractionRing A)

Premises used: IsFractionRing.injective, FractionRing
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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)
h₁ 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)
⊢ 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)

Tactic:
rw [Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization A A⁰]

Premises used: Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization, nonZeroDivisors
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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)
⊢ IsIntegralClosure B A (FractionRing B)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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)
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)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) 0 : A) (0 : A)

Tactic:
apply IsFractionRing.injective A (FractionRing A)

Premises used: IsFractionRing.injective, FractionRing
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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 (α := 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:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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 (α := 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)
⊢ 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)

Tactic:
apply FaithfulSMul.algebraMap_injective A (FractionRing A)

Premises used: FractionRing, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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)
a₃ 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)
⊢ 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:
rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
    ← galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]

Premises used: Algebra.algebraMap_intNorm_fractionRing, FractionRing, Algebra.norm_eq_of_algEquiv, galLiftEquiv_algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
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)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) x : A) (0 : A) ↔ x = 0

Tactic:
rw [← (IsFractionRing.injective A (FractionRing A)).eq_iff,
    ← (IsFractionRing.injective B (FractionRing B)).eq_iff]

Premises used: IsFractionRing.injective, Function.Injective.eq_iff, FractionRing
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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 (α := 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:
simp only [algebraMap_intNorm_fractionRing, map_zero, norm_eq_zero_iff]

Premises used: Algebra.algebraMap_intNorm_fractionRing, map_zero, Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
⊢ Ne.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) x : A) (0 : A) ↔ x ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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ₘ)
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ₘ)
⊢ 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
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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ₘ)

Tactic:
subsingleton [IsLocalization.uniqueOfZeroMem (S := Aₘ) hM]

Premises used: IsLocalization.uniqueOfZeroMem
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
⊢ M ≤ A⁰

Tactic:
replace hM : M ≤ A⁰ := fun x hx ↦ mem_nonZeroDivisors_iff_ne_zero.mpr (fun e ↦ hM (e ▸ hx))
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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))
rw₂ rw₃ : Eq (α := A →+* K) (algebraMap A K) (algebraMap A K)
⊢ Eq (α := A →+* K) (algebraMap A K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ K) (algebraMap A Aₘ))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
⊢ 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])
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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))
rw₂ rw₃ : Eq (α := B →+* L) (algebraMap B L) (algebraMap B L)
⊢ Eq (α := B →+* L) (algebraMap B L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap B Bₘ))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra