awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' :
  ∀ (x : L),
    Membership.mem (γ := Finset L)
        (Finset.image (α := ↥(IsNoetherian.finsetBasisIndex K L))
          (⇑bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) Finset.univ)
        x →
      IsIntegral A (y • x)
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)

Tactic:
⟨s', bs'.map {Algebra.lmul _ _ (algebraMap A L y) with
    toFun := fun x => algebraMap A L y * x
    invFun := fun x => (algebraMap A L y)⁻¹ * x
    left_inv := ?_
    right_inv := ?_}, ?_⟩

Premises used: Algebra.lmul, HMul.hMul, LinearEquiv.mk, Algebra.algebraMap, Module.Basis.map, LinearMap.toAddHom, AddHom.map_add', Inv.inv, LinearMap.mk, Exists.intro, LinearMap.map_smul', AddHom.mk, DFunLike.coe
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' :
  ∀ (x : L),
    Membership.mem (γ := Finset L)
        (Finset.image (α := ↥(IsNoetherian.finsetBasisIndex K L))
          (⇑bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) Finset.univ)
        x →
      IsIntegral A (y • x)
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
refine_1 :
  Function.LeftInverse (fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x) fun (x : L) ↦
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x
refine_2 :
  Function.RightInverse (fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x) fun (x : L) ↦
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x
refine_3 :
  ∀ (x : ↥s'),
    IsIntegral A (A := L)
      ((bs'.map
              (let __src : End K L := (lmul K L : (a : L) → End K L) ((algebraMap A L : (a : A) → L) y : L);
              { toFun := fun (x : L) ↦ HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x, map_add' := ⋯,
                map_smul' := ⋯, invFun := fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x,
                left_inv := ⋯, right_inv := ⋯ }) :
            (a : ↥s') → L)
          x :
        L)
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)

Tactic:
refine ⟨s', bs'.map {Algebra.lmul _ _ (algebraMap A L y) with
    toFun := fun x => algebraMap A L y * x
    invFun := fun x => (algebraMap A L y)⁻¹ * x
    left_inv := ?_
    right_inv := ?_}, ?_⟩
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' :
  ∀ (x : L),
    Membership.mem (γ := Finset L)
        (Finset.image (α := ↥(IsNoetherian.finsetBasisIndex K L))
          (⇑bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) Finset.univ)
        x →
      IsIntegral A (y • x)
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
x : L
⊢ (fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x)
      ((fun (x : L) ↦ HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x) x) =
    x

Tactic:
simp only [inv_mul_cancel_left₀ hy']

Premises used: inv_mul_cancel_left₀
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' :
  ∀ (x : L),
    Membership.mem (γ := Finset L)
        (Finset.image (α := ↥(IsNoetherian.finsetBasisIndex K L))
          (⇑bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) Finset.univ)
        x →
      IsIntegral A (y • x)
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
x : L
⊢ (fun (x : L) ↦ HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x)
      ((fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x) x) =
    x

Tactic:
simp only [mul_inv_cancel_left₀ hy']

Premises used: mul_inv_cancel_left₀
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' :
  ∀ (x : L),
    Membership.mem (γ := Finset L)
        (Finset.image (α := ↥(IsNoetherian.finsetBasisIndex K L))
          (⇑bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) Finset.univ)
        x →
      IsIntegral A (y • x)
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
x' : L
hx' : x' ∈ s'
⊢ ∀ (x : L),
    (∃ (a : ↥(IsNoetherian.finsetBasisIndex K L)), (bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) a = x) →
      IsIntegral A (HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x)

Tactic:
simp only [Algebra.smul_def, Finset.mem_image, Finset.mem_univ,
      true_and] at his'

Premises used: Finset.mem_univ, Finset.mem_image, Algebra.smul_def, true_and
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
x' : L
hx' : x' ∈ s'
his' :
  ∀ (x : L),
    (∃ (a : ↥(IsNoetherian.finsetBasisIndex K L)), (bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) a = x) →
      IsIntegral A (HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x)
⊢ IsIntegral A (A := L)
    ((bs'.map
            (let __src : End K L := (lmul K L : (a : L) → End K L) ((algebraMap A L : (a : A) → L) y : L);
            { toFun := fun (x : L) ↦ HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x, map_add' := ⋯,
              map_smul' := ⋯, invFun := fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x,
              left_inv := ⋯, right_inv := ⋯ }) :
          (a : ↥s') → L)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ s') x' hx') :
      L)

Tactic:
his' _ ⟨_, rfl⟩

Premises used: Exists.intro, 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
x' : L
hx' : x' ∈ s'
his' :
  ∀ (x : L),
    (∃ (a : ↥(IsNoetherian.finsetBasisIndex K L)), (bs' : (a : ↥(IsNoetherian.finsetBasisIndex K L)) → L) a = x) →
      IsIntegral A (HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x)
⊢ IsIntegral A (A := L)
    ((bs'.map
            (let __src : End K L := (lmul K L : (a : L) → End K L) ((algebraMap A L : (a : A) → L) y : L);
            { toFun := fun (x : L) ↦ HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) y : L) x, map_add' := ⋯,
              map_smul' := ⋯, invFun := fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x,
              left_inv := ⋯, right_inv := ⋯ }) :
          (a : ↥s') → L)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ s') x' hx') :
      L)

Tactic:
exact his' _ ⟨_, rfl⟩

Premises used: Exists.intro, 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
haveI : ∀ (this : DecidableEq L), IsNoetherian A C
⊢ IsNoetherian A C

Tactic:
haveI := Classical.decEq 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
this : DecidableEq L
obtain :
  ∀ (s : Finset L) (b : Basis (↥s) K L) (hb_int : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)),
    IsNoetherian A C
⊢ IsNoetherian A C

Tactic:
obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L

Premises used: FiniteDimensional.exists_is_basis_integral
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
⊢ IsNoetherianRing C

Tactic:
isNoetherianRing_iff.mpr <| isNoetherian_of_tower A (IsIntegralClosure.isNoetherian A K L C)

Premises used: Iff.mpr, isNoetherianRing_iff, isNoetherian_of_tower, IsIntegralClosure.isNoetherian
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
⊢ IsNoetherian A C

Tactic:
haveI := IsIntegralClosure.isNoetherian A K L C
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
this : IsNoetherian A C
⊢ Module.Finite A C

Tactic:
Module.IsNoetherian.finite A C

Premises used: Module.IsNoetherian.finite
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
this : IsNoetherian A C
⊢ Module.Finite A C

Tactic:
exact Module.IsNoetherian.finite A C

Premises used: Module.IsNoetherian.finite
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsTorsionFree A L
inst_17 : IsPrincipalIdealRing A
⊢ Free A C

Tactic:
haveI : IsTorsionFree A C := IsIntegralClosure.isTorsionFree A L
  haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L _
  inferInstance

Premises used: inferInstance
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsPrincipalIdealRing A
inst_17 : IsTorsionFree A L
⊢ Free A C

Tactic:
haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsPrincipalIdealRing A
inst_17 : IsTorsionFree A L
this : Free A C
⊢ IsNoetherian A C

Tactic:
haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsPrincipalIdealRing A
inst_17 : IsTorsionFree A L
this_1 : Free A C
this : IsNoetherian A C
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L

Tactic:
haveI : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
    IsIntegralClosure.isLocalization A K L C
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsPrincipalIdealRing A
inst_17 : IsTorsionFree A L
this_1 : Free A C
this_2 : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid.{u_1, u_4} (R := A) C A⁰) L
b : Basis.{u_4, u_2, u_3} (Free.ChooseBasisIndex A C) K L :=
  Basis.localizationLocalization.{u_1, u_2, u_4, u_3, u_4} (R := A) K A⁰ (A := C) L (Free.chooseBasis A C)
rw : Fintype.card.{u_4} (Free.ChooseBasisIndex A C) = finrank K L
rw₁ rw₂ : Fintype.card.{u_4} (Free.ChooseBasisIndex A C) = Fintype.card.{u_4} (Free.ChooseBasisIndex A C)
⊢ finrank A C = finrank K L

Tactic:
rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis, Module.finrank_eq_card_chooseBasisIndex
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
inst_12 : IsNoetherianRing A
⊢ IsNoetherianRing.{u_3} ↥(integralClosure A L)

Tactic:
IsIntegralClosure.isNoetherianRing A K L (integralClosure A L)

Premises used: Set.Mem, Membership.mem, Subtype, integralClosure, IsIntegralClosure.isNoetherianRing
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsDomain C
inst_17 : IsDedekindDomain A
⊢ IsDedekindDomain C

Tactic:
have : IsFractionRing C L := IsIntegralClosure.isFractionRing_of_finite_extension A K L C
  have : Algebra.IsIntegral A C := IsIntegralClosure.isIntegral_algebra A L
  { IsIntegralClosure.isNoetherianRing A K L C,
    Ring.DimensionLEOne.of_isIntegral A C,
    (isIntegrallyClosed_iff L).mpr fun {x} hx =>
      ⟨IsIntegralClosure.mk' C x (isIntegral_trans (R := A) _ hx),
        IsIntegralClosure.algebraMap_mk' _ _ _⟩ with : IsDedekindDomain C }

Premises used: Iff.mpr, IsIntegralClosure.isIntegral_algebra, IsIntegralClosure.isFractionRing_of_finite_extension, isIntegral_trans, IsIntegralClosure.mk', IsIntegralClosure.algebraMap_mk', IsDedekindDomain.mk, Exists.intro, isIntegrallyClosed_iff, Ring.DimensionLEOne.of_isIntegral, IsIntegralClosure.isNoetherianRing
-- 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
inst_5 : Algebra K L
inst_6 : Algebra A L
inst_7 : IsScalarTower A K L
inst_8 : FiniteDimensional K L
inst_9 : IsDomain A
inst_10 : Algebra.IsSeparable K L
inst_11 : IsDedekindDomain A
⊢ IsDedekindDomain.{u_3} ↥(integralClosure A L)

Tactic:
IsIntegralClosure.isDedekindDomain A K L (integralClosure A L)

Premises used: Membership.mem, Subtype, integralClosure, IsIntegralClosure.isDedekindDomain
-- 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 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsDomain C
inst_17 : Algebra.{u_1, u_3} (FractionRing A) L
inst_18 : IsScalarTower A (FractionRing A) L
inst_19 : FiniteDimensional.{u_1, u_3} (FractionRing A) L
inst_20 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) L
inst_21 : IsDedekindDomain A
⊢ IsDedekindDomain.{u_3} ↥(integralClosure A L)

Tactic:
integralClosure.isDedekindDomain A (FractionRing A) L

Premises used: integralClosure.isDedekindDomain, FractionRing
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

Tactic:
simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg IntermediateField.toSubalgebra h₂

Premises used: congr_arg, IntermediateField.sup_toSubalgebra_of_isAlgebraic_right, IntermediateField.toSubalgebra