awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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 : Algebra.IsSeparable K L
ι : Type u_5
inst_15 : Finite ι
inst_16 : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral.{u_1, u_3} A (A := L) ((b : (a : ι) → L) i : L)
inst_17 : IsIntegrallyClosed A
⊢ LE.le (α := Submodule A L)
    (LinearMap.range
      ((↑A :
          {S M : Type u_4} →
            {M₂ : Type u_3} →
              [inst : Semiring A] →
                [inst_18 : Semiring S] →
                  [inst_19 : AddCommMonoid M] →
                    [inst_20 : AddCommMonoid M₂] →
                      [inst_21 : Module A M] →
                        [inst_22 : Module A M₂] →
                          [inst_23 : Module S M] →
                            [inst_24 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.linearMap C L)))
    (Submodule.span A
      (Set.range.{u_3, u_5 + 1} (ι := ι)
        (⇑(LinearMap.BilinForm.dualBasis.{u_3, u_2, u_5} (V := L) (K := K) (ι := ι) (traceForm K L) ⋯ b : Basis ι K L) :
          (a : ι) → L)))
have rw : Set.range.{u_3, u_5 + 1} (ι := ι) (⇑b : (a : ι) → L) ⊆
  (↑(LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} (R := A) (S := K) (M := L)
          (LinearMap.BilinForm.flip (traceForm K L))
          (LinearMap.range
            ((↑A :
                {S M : Type u_4} →
                  {M₂ : Type u_3} →
                    [inst : Semiring A] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module A M] →
                              [inst_22 : Module A M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (Algebra.linearMap C L))) :
        Submodule A L) :
    Set L)
Tactic: rw [← LinearMap.BilinForm.dualSubmodule_span_of_basis,
    ← LinearMap.BilinForm.le_flip_dualSubmodule, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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 : Algebra.IsSeparable K L
ι : Type u_5
inst_15 : Finite ι
inst_16 : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral.{u_1, u_3} A (A := L) ((b : (a : ι) → L) i : L)
inst_17 : IsIntegrallyClosed A
i : ι
y : C
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    ((((LinearMap.BilinForm.flip (traceForm K L) : (a : L) → L →ₗ[K] K) ((b : (a : ι) → L) i) : L →ₗ[K] K) :
          (a : L) → K)
        (((↑A :
                  {S M : Type u_4} →
                    {M₂ : Type u_3} →
                      [inst : Semiring A] →
                        [inst_18 : Semiring S] →
                          [inst_19 : AddCommMonoid M] →
                            [inst_20 : AddCommMonoid M₂] →
                              [inst_21 : Module A M] →
                                [inst_22 : Module A M₂] →
                                  [inst_23 : Module S M] →
                                    [inst_24 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (Algebra.linearMap C L) :
              (a : C) → L)
            y :
          L) :
      K)
have simp : Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
  ((trace K L : (a : L) → K)
      (HMul.hMul (α := L) (β := L) ((algebraMap C L : (a : C) → L) y : L) ((b : (a : ι) → L) i : L)) :
    K)
Tactic: simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply,
    traceForm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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 : Algebra.IsSeparable K L
ι : Type u_5
inst_15 : Finite ι
inst_16 : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral.{u_1, u_3} A (A := L) ((b : (a : ι) → L) i : L)
inst_17 : IsIntegrallyClosed A
i : ι
y : C
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    ((trace K L : (a : L) → K)
        (HMul.hMul (α := L) (β := L) ((algebraMap C L : (a : C) → L) y : L) ((b : (a : ι) → L) i : L)) :
      K)
have refine : IsIntegral.{u_1, u_2} A (A := K)
  ((trace K L : (a : L) → K)
      (HMul.hMul (α := L) (β := L) ((algebraMap C L : (a : C) → L) y : L) ((b : (a : ι) → L) i : L)) :
    K)
Tactic: refine Submodule.mem_one.mpr <| IsIntegrallyClosed.isIntegral_iff.mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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 : Algebra.IsSeparable K L
ι : Type u_5
inst_10 : Finite ι
inst_11 : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral.{u_1, u_3} A (A := L) ((b : (a : ι) → L) i : L)
inst_12 : IsIntegrallyClosed A
⊢ LE.le (α := Submodule A L)
    ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) (integralClosure A L) : Submodule A L)
    (Submodule.span A
        (Set.range.{u_3, u_5 + 1} (ι := ι)
          (⇑(LinearMap.BilinForm.dualBasis.{u_3, u_2, u_5} (V := L) (K := K) (ι := ι) (traceForm K L) ⋯ b :
                Basis ι K L) :
            (a : ι) → L)) :
      Submodule A L)
have refine : LE.le (α := Submodule A L)
  ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) (integralClosure A L) : Submodule A L)
  (LinearMap.range (M := ↥(integralClosure A L))
      ((↑A :
          {S M M₂ : Type u_3} →
            [inst : Semiring A] →
              [inst_13 : Semiring S] →
                [inst_14 : AddCommMonoid M] →
                  [inst_15 : AddCommMonoid M₂] →
                    [inst_16 : Module A M] →
                      [inst_17 : Module A M₂] →
                        [inst_18 : Module S M] →
                          [inst_19 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.linearMap (↥(integralClosure A L)) L)) :
    Submodule A L)
Tactic: refine le_trans ?_ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
have obtain : ∀ (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)),
  ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
Tactic: obtain ⟨y, hy, his'⟩ := exists_integral_multiples A K (Finset.univ.image bs')
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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)
⊢ Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
have refine : Function.Injective.{u_1 + 1, u_3 + 1} (α := A) (β := L) (⇑(algebraMap A L) : (a : A) → L)
Tactic: refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := A) (β := L) (⇑(algebraMap A L) : (a : A) → L)
have rw : Function.Injective.{u_1 + 1, u_3 + 1} (α := A) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K)) : (a : A) → L)
Tactic: rw [IsScalarTower.algebraMap_eq A K L]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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)
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
have hy' : Ne.{u_3 + 1} (α := L) ((algebraMap A L : (a : A) → L) y : L) (0 : L)
Tactic: have hy' : algebraMap A L y ≠ 0 := by
    refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy
    rw [IsScalarTower.algebraMap_eq A K L]
    exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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)
have 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
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 := ?_}, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
have 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
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 := ?_}, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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
⊢ ∃ (s : Finset L) (b : Basis (↥s) K L), ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
have 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' := sorry,
              map_smul' := sorry, invFun := fun (x : L) ↦ HMul.hMul (α := L) (((algebraMap A L : (a : A) → L) y)⁻¹ : L) x,
              left_inv := sorry, right_inv := sorry }) :
          (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 := ?_}, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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'
⊢ 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)
have 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)
Tactic: simp only [Algebra.smul_def, Finset.mem_image, Finset.mem_univ,
      true_and] at his'
Cleared hypotheses: his'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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
have haveI : ∀ (this : DecidableEq L), IsNoetherian A C
Tactic: haveI := Classical.decEq L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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
⊢ IsNoetherian A C
have 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
Tactic: obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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
⊢ Module.Finite A C
have this : IsNoetherian A C
Tactic: haveI := IsIntegralClosure.isNoetherian A K L C
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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
⊢ finrank A C = finrank K L
have this : Free A C
Tactic: haveI : Module.Free A C := IsIntegralClosure.module_free A K L C
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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
⊢ finrank A C = finrank K L
have this₁ : IsNoetherian A C
Tactic: haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (hypothesis)
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
⊢ finrank A C = finrank K L
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.IntegralClosure (goal)
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)
⊢ finrank A C = finrank K L
have rw : Fintype.card.{u_4} (Free.ChooseBasisIndex A C) = finrank K L
Tactic: rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b]