awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
rw :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)))
rw₁ :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap S Sₚ)) (algebraMap R S))
rw₂ :
  Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Tₚ) (algebraMap R S))
rw₃ rw₄ : Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ) (algebraMap R Tₚ)
⊢ Eq (α := RingHom.{u_1, u_3} R Tₚ) (algebraMap R Tₚ)
    (@RingHom.comp.{u_1, u_2, u_3} _ Sₚ _ _ Semiring.toNonAssocSemiring _ (algebraMap Sₚ Tₚ) (algebraMap R Sₚ))

Tactic:
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq S, ← IsScalarTower.algebraMap_eq]

Premises used: RingHom.comp_assoc, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : Module.Finite S T
⊢ Module.Finite.{u_2, u_3} Sₚ Tₚ

Tactic:
Module.Finite.of_isLocalization S T P'

Premises used: Module.Finite.of_isLocalization, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree S T
⊢ IsTorsionFree.{u_2, u_3} Sₚ Tₚ

Tactic:
.of_isLocalization S T <| algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ <|
    Ideal.primeCompl_le_nonZeroDivisors P

Premises used: Module.IsTorsionFree.of_isLocalization, Ideal.primeCompl_le_nonZeroDivisors, algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : Algebra.IsIntegral R S
⊢ Algebra.IsIntegral.{u_1, u_2} Rₚ Sₚ

Tactic:
Algebra.isIntegral_def.mpr <| (algebraMap_eq_map_map_submonoid P.primeCompl S Rₚ Sₚ ▸
    isIntegral_localization : (algebraMap Rₚ Sₚ).IsIntegral)

Premises used: Iff.mpr, isIntegral_localization, Algebra.isIntegral_def, Localization.AtPrime, Eq.rec, Localization, Ideal.primeCompl, Algebra.algebraMapSubmonoid, Eq.symm, IsLocalization.algebraMap_eq_map_map_submonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
⊢ IsScalarTower.{u_1, u_2, u_3} Rₚ Sₚ Tₚ

Tactic:
⟨fun a b c ↦ a.ind fun ⟨a₁, a₂⟩ ↦ ?_⟩

Premises used: Localization.ind, IsScalarTower.mk
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
refine :
  ∀ (a : Rₚ) (b : Sₚ) (c : Tₚ) (x : R × ↥P.primeCompl) (a₁ : R) (a₂ : ↥P.primeCompl),
    HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
      HSMul.hSMul (α := Rₚ) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
⊢ IsScalarTower.{u_1, u_2, u_3} Rₚ Sₚ Tₚ

Tactic:
refine ⟨fun a b c ↦ a.ind fun ⟨a₁, a₂⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
a : Rₚ
b : Sₚ
c : Tₚ
x : R × ↥P.primeCompl
a₁ : R
a₂ : ↥P.primeCompl
⊢ (↑a₂ : R) ≠ 0

Tactic:
have : a₂.val ≠ 0 := nonZeroDivisors.ne_zero <| Ideal.primeCompl_le_nonZeroDivisors P <| a₂.prop
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
⊢ Algebra.IsSeparable.{u_2, u_3} (FractionRing Sₚ) (FractionRing Tₚ)

Tactic:
FractionRing.isSeparable_of_isLocalization T Sₚ Tₚ (M := P') ?_

Premises used: FractionRing.isSeparable_of_isLocalization, Localization, Ideal.primeCompl, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
refine : LE.le (α := Submonoid S) P' S⁰
⊢ Algebra.IsSeparable.{u_2, u_3} (FractionRing Sₚ) (FractionRing Tₚ)

Tactic:
refine FractionRing.isSeparable_of_isLocalization T Sₚ Tₚ (M := P') ?_
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
hS : P.primeCompl ≤ R⁰
⊢ LE.le (α := Submonoid S) P' S⁰

Tactic:
apply algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul

Premises used: algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
x : R
h : x ∈ P.primeCompl
⊢ 0 ∉ P.primeCompl

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Instances
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsDomain T
inst_6 : Algebra R S
P : Ideal R
inst_7 : P.IsPrime
inst_8 : FaithfulSMul R S
inst_9 : Algebra S T
inst_10 : Algebra R T
inst_11 : IsScalarTower R S T
inst_12 : IsTorsionFree R T
inst_13 : IsTorsionFree S T
inst_14 : Algebra.IsSeparable.{u_2, u_3} L F
⊢ P.primeCompl ≤ R⁰

Tactic:
exact fun _ h ↦ mem_nonZeroDivisors_of_ne_zero <| ne_of_mem_of_not_mem h <| by simp

Premises used: ne_of_mem_of_not_mem, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
⊢ IsDomain C

Tactic:
haveI : IsDomain C :=
    (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this : IsDomain C
⊢ IsTorsionFree A L

Tactic:
haveI : IsTorsionFree A L := .trans_faithfulSMul A K L
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this : IsTorsionFree A L
⊢ IsTorsionFree A C

Tactic:
haveI : IsTorsionFree A C := IsIntegralClosure.isTorsionFree A L
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L

Tactic:
⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩

Premises used: IsLocalization'.mk, Submonoid.IsLocalizationMap.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
refine_1 :
  ∀ (y : ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    IsUnit.{u_3} (M := L) ((algebraMap C L : (a : C) → L) (↑y : C) : L)
refine_2 :
  ∀ (z : L),
    ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
      HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
refine_3 :
  ∀ {x y : C} (h : Eq.{u_3 + 1} (α := L) ((algebraMap C L : (a : C) → L) x : L) ((algebraMap C L : (a : C) → L) y : L)),
    (↑1 : C) * x = (↑1 : C) * y
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L

Tactic:
refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ (↑(A⁰ : Submonoid A) : Set A)
refine_1 : x ≠ 0
⊢ IsUnit.{u_3} (M := L)
    ((algebraMap C L : (a : C) → L)
        ((↑(Subtype.mk (p := fun (x : C) ↦
                Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                ((algebraMap A C : (a : A) → C) x) ⋯) :
            C) :
          C) :
      L)

Tactic:
rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
      Subtype.coe_mk, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)]

Premises used: Subtype.coe_mk, IsIntegralClosure.algebraMap_injective, isUnit_iff_ne_zero, FaithfulSMul.algebraMap_injective, map_ne_zero_iff
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ (↑(A⁰ : Submonoid A) : Set A)
⊢ x ≠ 0

Tactic:
mem_nonZeroDivisors_iff_ne_zero.mp hx

Premises used: Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
x : A
hx : x ∈ (↑(A⁰ : Submonoid A) : Set A)
⊢ x ≠ 0

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero.mp hx

Premises used: Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
refine_2 :
  ∀ (m : ↥(A⁰ : Submonoid A)) (hm : IsIntegral A (m • z)),
    ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
      HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1

Tactic:
obtain ⟨m, hm⟩ :=
      IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z
        (Algebra.IsIntegral.isIntegral (R := K) z)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.exists_multiple_integral_of_isLocalization, nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
⊢ ∃ (x : C), (algebraMap C L : (a : C) → L) x = m • z

Tactic:
IsIntegralClosure.isIntegral_iff.mp hm

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
refine_2 :
  ∀ (x : C) (hx : (algebraMap C L : (a : C) → L) x = m • z),
    ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
      HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1

Tactic:
obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1

Tactic:
⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩

Premises used: Algebra.algebraMap, SetLike.coe_mem, Prod.mk, Subtype.mk, And.intro, Exists.intro, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
⊢ ∃ (x : C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)),
    HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) (↑x.2 : C) : L) = (algebraMap C L : (a : C) → L) x.1

Tactic:
refine ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥(A⁰ : Submonoid A)
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L : (a : C) → L) x = m • z
refine_2 :
  HMul.hMul (β := L) z ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) (↑m : A) : C) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₁ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1
refine_2₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) (↑m : A) : L) = m • z
refine_2₃ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = m • z
refine_2₄ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z = (↑m : A) • z
refine_2₅ refine_2₆ :
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z =
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) (↑m : A) : L) z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(x,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
                      ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((x,
            Subtype.mk (p := fun (x : C) ↦
              Membership.mem (γ := Submonoid C) (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) x)
              ((algebraMap A C : (a : A) → C) (↑m : A)) ⋯) :
          C × ↥(algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰)).1

Tactic:
rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
      smul_def]

Premises used: Subtype.coe_mk, Submonoid.smul_def, mul_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : IsDomain A
inst_14 : Algebra.IsAlgebraic K L
this_1 : IsDomain C
this_2 : IsTorsionFree A L
this : IsTorsionFree A C
x y : C
h : Eq.{u_3 + 1} (α := L) ((algebraMap C L : (a : C) → L) x : L) ((algebraMap C L : (a : C) → L) y : L)
⊢ (↑1 : C) * x = (↑1 : C) * y

Tactic:
simp only [IsIntegralClosure.algebraMap_injective C A L h]

Premises used: IsIntegralClosure.algebraMap_injective