awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
by_contra! : ∀ (h' : ∀ (a : M) (_ : a ∈ N), a = 0), False
⊢ ∃ a ∈ N, a ≠ 0

Tactic:
by_contra! h'
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
h' : ∀ (a : M) (_ : a ∈ N), a = 0
apply : N = ⊥
⊢ False

Tactic:
apply hN
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
h' : ∀ (a : M) (_ : a ∈ N), a = 0
rwa rwa₁ rwa₂ rwa₃ : N ≤ ⊥
⊢ N = ⊥

Tactic:
rwa [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
obtain : ∀ (a : M) (ha₁ : a ∈ N) (ha₂ : a ≠ 0), IsIntegral R x
⊢ IsIntegral R x

Tactic:
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
change :
  Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f.toLinearMap : (a : ↥A') → Module.End R ↥N)
⊢ Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)

Tactic:
change Function.Injective f.toLinearMap

Premises used: AlgHom.toLinearMap, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
rw : f.toLinearMap.ker ≤ ⊥
⊢ Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f.toLinearMap : (a : ↥A') → Module.End R ↥N)

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Premises used: LinearMap.ker_eq_bot, eq_bot_iff
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
s : ↥A'
hs : s ∈ f.toLinearMap.ker
⊢ (↑s : A) • a = 0

Tactic:
have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
s : ↥A'
hs : s ∈ f.toLinearMap.ker
this : (↑s : A) • a = 0
⊢ Membership.mem (γ := Submodule R ↥A') ⊥ s

Tactic:
Subtype.ext ((smul_eq_zero_iff_left ha₂).1 this)

Premises used: Set.Mem, setOf, smul_eq_zero_iff_left, Set.singleton, Iff.mp, Subtype.ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
s : ↥A'
hs : s ∈ f.toLinearMap.ker
this : (↑s : A) • a = 0
⊢ Membership.mem (γ := Submodule R ↥A') ⊥ s

Tactic:
exact Subtype.ext ((smul_eq_zero_iff_left ha₂).1 this)

Premises used: Subtype.ext
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
⊢ Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)

Tactic:
have : Function.Injective f := by
    change Function.Injective f.toLinearMap
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro s hs
    have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
    exact Subtype.ext ((smul_eq_zero_iff_left ha₂).1 this)
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)
change : IsIntegral R (A := A) ((A'.val : (a : ↥A') → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : A)
⊢ IsIntegral R x

Tactic:
change IsIntegral R (A'.val ⟨x, hx⟩)

Premises used: Subalgebra.val, Subtype.mk, IsIntegral, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)
rw :
  IsIntegral.{u_1, u_5} R (A := Module.End R ↥N)
    ((f : (a : ↥A') → Module.End R ↥N) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : Module.End R ↥N)
⊢ IsIntegral R (A := A) ((A'.val : (a : ↥A') → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : A)

Tactic:
rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this]

Premises used: Subtype.val_injective, Subalgebra.val, isIntegral_algHom_iff
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)
rwa rwa₁ rwa₂ rwa₃ : N.FG
⊢ Module.Finite.{u_1, u_5} R ↥N

Tactic:
rwa [Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)
⊢ Module.Finite.{u_1, u_5} R ↥N

Tactic:
haveI : Module.Finite R N := by rwa [Module.Finite.iff_fg]
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsDomain A
M : Type u_5
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
inst_8 : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : AlgHom.{u_1, u_2, u_5} R (↥A') (Module.End R ↥N) :=
  AlgHom.ofLinearMap
    { toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this_1 : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f : (a : ↥A') → Module.End R ↥N)
this : Module.Finite.{u_1, u_5} R ↥N
⊢ IsIntegral.{u_1, u_5} R (A := Module.End R ↥N)
    ((f : (a : ↥A') → Module.End R ↥N) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : Module.End R ↥N)

Tactic:
apply Algebra.IsIntegral.isIntegral

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h : f.Finite
⊢ f.IsIntegral

Tactic:
letI := f.toAlgebra
  fun _ ↦ IsIntegral.of_mem_of_fg ⊤ h.1 _ trivial

Premises used: Module.Finite.fg_top, trivial, IsIntegral, RingHom.IsIntegral, IsIntegral.of_mem_of_fg, Top.top
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : Membership.mem (γ := Subring S) (Subring.closure {x, y}) z
this : Algebra R S := f.toAlgebra
⊢ (HMul.hMul (α := Submodule R S) (β := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[y] : Submodule R S)).FG

Tactic:
have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : Membership.mem (γ := Subring S) (Subring.closure {x, y}) z
this_1 : Algebra R S := f.toAlgebra
this :
  (HMul.hMul (α := Submodule R S) (β := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[y] : Submodule R S)).FG
⊢ FG.{u_1, u_4} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x, y])

Tactic:
rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this

Premises used: Set.singleton_union, Algebra.adjoin_union_coe_submodule
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : Membership.mem (γ := Subring S) (Subring.closure {x, y}) z
this_1 : Algebra R S := f.toAlgebra
this : FG.{u_1, u_4} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x, y])
⊢ f.IsIntegralElem z

Tactic:
IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z
      (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

Premises used: Iff.mpr, Algebra.mem_adjoin_iff, Subring.closure_mono, Set.subset_union_right, Algebra.adjoin, Insert.insert, IsIntegral, IsIntegral.of_mem_of_fg, Singleton.singleton
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : Membership.mem (γ := Subring S) (Subring.closure {x, y}) z
this_1 : Algebra R S := f.toAlgebra
this : FG.{u_1, u_4} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x, y])
⊢ f.IsIntegralElem z

Tactic:
exact
    IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z
      (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

Premises used: Iff.mpr, Algebra.mem_adjoin_iff, Subring.closure_mono, Set.subset_union_right, Algebra.adjoin, Insert.insert, IsIntegral.of_mem_of_fg, Singleton.singleton
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x y z : A
hx : IsIntegral R x
hy : IsIntegral R y
hz : Membership.mem (γ := Subring A) (Subring.closure {x, y}) z
⊢ IsIntegral R z

Tactic:
hx.of_mem_closure (algebraMap R A) hy hz

Premises used: Algebra.algebraMap, IsIntegral, RingHom.IsIntegralElem.of_mem_closure
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x + y)

Tactic:
hx.of_mem_closure f hy <|
    Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))

Premises used: Subring.add_mem, Subring.subset_closure, RingHom.IsIntegralElem.of_mem_closure, Or.inl, Or.inr, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x y : A
hx : IsIntegral R x
hy : IsIntegral R y
⊢ IsIntegral R (x + y)

Tactic:
hx.add (algebraMap R A) hy

Premises used: Algebra.algebraMap, RingHom.IsIntegralElem.add, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : S
hx : f.IsIntegralElem x
⊢ f.IsIntegralElem (-x)

Tactic:
hx.of_mem_closure f hx (Subring.neg_mem _ (Subring.subset_closure (Or.inl rfl)))

Premises used: Subring.neg_mem, Subring.subset_closure, RingHom.IsIntegralElem.of_mem_closure, Or.inl, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : S
h : f.IsIntegralElem (-x)
⊢ f.IsIntegralElem x

Tactic:
neg_neg x ▸ h.neg

Premises used: RingHom.IsIntegralElem.neg, Eq.rec, neg_neg
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x : S
⊢ f.IsIntegralElem (-x) ↔ f.IsIntegralElem x

Tactic:
⟨fun h => h.of_neg, fun h => h.neg⟩

Premises used: RingHom.IsIntegralElem.neg, Iff.intro, RingHom.IsIntegralElem.of_neg
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
⊢ IsIntegral R (-x)

Tactic:
.of_mem_of_fg _ hx.fg_adjoin_singleton _ (Subalgebra.neg_mem _ <| Algebra.subset_adjoin rfl)

Premises used: Algebra.subset_adjoin, Subalgebra.neg_mem, IsIntegral.of_mem_of_fg, IsIntegral.fg_adjoin_singleton, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R (-x)
⊢ IsIntegral R x

Tactic:
neg_neg x ▸ hx.neg

Premises used: Eq.rec, neg_neg, IsIntegral.neg
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
⊢ IsIntegral R (-x) ↔ IsIntegral R x

Tactic:
⟨IsIntegral.of_neg, IsIntegral.neg⟩

Premises used: IsIntegral.of_neg, IsIntegral.neg, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x - y)

Tactic:
simpa only [sub_eq_add_neg] using hx.add f (hy.neg f)

Premises used: RingHom.IsIntegralElem.add, sub_eq_add_neg, RingHom.IsIntegralElem.neg
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x y : A
hx : IsIntegral R x
hy : IsIntegral R y
⊢ IsIntegral R (x - y)

Tactic:
hx.sub (algebraMap R A) hy

Premises used: RingHom.IsIntegralElem.sub, Algebra.algebraMap, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x * y)

Tactic:
hx.of_mem_closure f hy
    (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)))

Premises used: Subring.subset_closure, RingHom.IsIntegralElem.of_mem_closure, Or.inl, Subring.mul_mem, Or.inr, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x y : A
hx : IsIntegral R x
hy : IsIntegral R y
⊢ IsIntegral R (x * y)

Tactic:
hx.mul (algebraMap R A) hy

Premises used: Algebra.algebraMap, IsIntegral, RingHom.IsIntegralElem.mul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
B : Type u_3
S : Type u_4
inst : Ring B
inst_1 : CommRing S
R : Type u_5
inst_2 : CommSemiring R
inst_3 : Algebra R B
inst_4 : Algebra S B
inst_5 : Algebra R S
inst_6 : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
rw :
  Membership.mem (γ := Subalgebra S B) S[x]
    (HSMul.hSMul.{u_4, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x)
⊢ Membership.mem (γ := Subalgebra S B) S[x] (r • x)

Tactic:
rw [← algebraMap_smul S]

Premises used: algebraMap_smul
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
B : Type u_3
S : Type u_4
inst : Ring B
inst_1 : CommRing S
R : Type u_5
inst_2 : CommSemiring R
inst_3 : Algebra R B
inst_4 : Algebra S B
inst_5 : Algebra R S
inst_6 : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
hx₁ : Membership.mem (γ := Subalgebra S B) S[x] x
⊢ Membership.mem (γ := Subalgebra S B) S[x]
    (HSMul.hSMul.{u_4, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x)

Tactic:
apply Subalgebra.smul_mem

Premises used: Subalgebra.smul_mem