-- Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean
theorem FiniteDimensional.exists_is_basis_integral :
    ∃ (s : Finset L) (b : Basis s K L), ∀ x, IsIntegral A (b x)

Proof state:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)

Tactic:
letI : IsNoetherian K L := IsNoetherian.iff_fg.2 inferInstance

Result:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)

Proof state:
case intro.intro.refine_3.mk
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : (algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
his' : ∀ (x : L), (∃ a, bs' a = x) → IsIntegral A ((algebraMap A L) y * x)
⊢ IsIntegral A
    ((bs'.map
        (let __src := (lmul K L) ((algebraMap A L) y);
        { toFun := fun x => (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯,
          invFun := fun x => ((algebraMap A L) y)⁻¹ * x, left_inv := ⋯, right_inv := ⋯ }))
      ⟨x', hx'⟩)

Tactic:
simp only [Basis.map_apply, LinearEquiv.coe_mk]

Result:
case intro.intro.refine_3.mk
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : (algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
his' : ∀ (x : L), (∃ a, bs' a = x) → IsIntegral A ((algebraMap A L) y * x)
⊢ IsIntegral A ((algebraMap A L) y * bs' ⟨x', hx'⟩)

Proof state:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)

Tactic:
letI := Classical.decEq L

Result:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)

Proof state:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
⊢ (algebraMap A L) y ≠ 0

Tactic:
refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy

Result:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
⊢ Function.Injective ⇑(algebraMap A L)

Proof state:
case intro.intro.refine_1
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
hy' : (algebraMap A L) y ≠ 0
x : L
⊢ (fun x => ((algebraMap A L) y)⁻¹ * x)
      ({ toFun := fun x => (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯ }.toFun x) =
    x

Tactic:
simp only [inv_mul_cancel_left₀ hy']

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)

Tactic:
let s' := IsNoetherian.finsetBasisIndex K L

Result:
A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this✝ : DecidableEq L := Classical.decEq L
this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance
s' : Finset L := IsNoetherian.finsetBasisIndex K L
⊢ ∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)