awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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_1 : A
hx : ∀ n ∈ N, x_1 • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ LinearMap.restrict (DistribSMul.toLinearMap R M (x + y)) ⋯ =
    HAdd.hAdd (α := Module.End R ↥N) (LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯)
      (LinearMap.restrict (DistribSMul.toLinearMap R M y) ⋯)
have h : ∀ (x_2 : ↥N),
  Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (x + y)) sorry : (a : ↥N) → ↥N) x_2) : M)
    (↑((HAdd.hAdd (α := Module.End R ↥N) (LinearMap.restrict (DistribSMul.toLinearMap R M x) sorry)
              (LinearMap.restrict (DistribSMul.toLinearMap R M y) sorry) :
            (a : ↥N) → ↥N)
          x_2) :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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' := ⋯ }
r : R
s : ↥A'
⊢ LinearMap.restrict (DistribSMul.toLinearMap R M (r • s)) ⋯ =
    HSMul.hSMul (α := R) (β := Module.End R ↥N) ((RingHom.id R : (a : R) → R) r : R)
      (LinearMap.restrict (DistribSMul.toLinearMap R M s) ⋯)
have h : ∀ (x : ↥N),
  Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (r • s)) sorry : (a : ↥N) → ↥N) x) : M)
    (↑((HSMul.hSMul (α := R) (β := Module.End R ↥N) ((RingHom.id R : (a : R) → R) r : R)
              (LinearMap.restrict (DistribSMul.toLinearMap R M s) sorry) :
            (a : ↥N) → ↥N)
          x) :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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' := ⋯ }
⊢ Eq.{u_5 + 1} (α := Module.End R ↥N)
    (({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } :
        (a : ↥A') → Module.End R ↥N)
      1)
    1
have h : ∀ (x : ↥N),
  Eq.{u_5 + 1} (α := M)
    (↑((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) sorry, map_add' := sorry,
                  map_smul' := sorry } :
                (a : ↥A') → Module.End R ↥N)
              1 :
            (a : ↥N) → ↥N)
          x) :
      M)
    (↑((1 : (a : ↥N) → ↥N) x) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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_1 : A
hx : ∀ n ∈ N, x_1 • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x : A | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ ({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ } :
        (a : ↥A') → Module.End R ↥N)
      (x * y) =
    HMul.hMul (α := Module.End R ↥N) (β := Module.End R ↥N)
      (({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (↥A') (Module.End R ↥N) } :
            (a : ↥A') → Module.End R ↥N)
          x :
        Module.End R ↥N)
      (({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (↥A') (Module.End R ↥N) } :
            (a : ↥A') → Module.End R ↥N)
          y :
        Module.End R ↥N)
have h : ∀ (x_2 : ↥N),
  Eq.{u_5 + 1} (α := M)
    (↑(((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) sorry, map_add' := sorry,
                    map_smul' := sorry } :
                  (a : ↥A') → Module.End R ↥N)
                (x * y) :
              Module.End R ↥N) :
            (a : ↥N) → ↥N)
          x_2) :
      M)
    (↑((HMul.hMul (α := Module.End R ↥N) (β := Module.End R ↥N)
              (({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) sorry, map_add' := sorry,
                      map_smul' := sorry : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (↥A') (Module.End R ↥N) } :
                    (a : ↥A') → Module.End R ↥N)
                  x :
                Module.End R ↥N)
              (({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) sorry, map_add' := sorry,
                      map_smul' := sorry : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (↥A') (Module.End R ↥N) } :
                    (a : ↥A') → Module.End R ↥N)
                  y :
                Module.End R ↥N) :
            (a : ↥N) → ↥N)
          x_2) :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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 ∈ N, a ≠ 0
have by_contra! : ∀ (h' : ∀ (a : M) (_ : a ∈ N), a = 0), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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
⊢ False
have apply : N = ⊥
Tactic: apply hN
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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
⊢ N = ⊥
have rwa : N ≤ ⊥
Tactic: rwa [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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' := ⋯ } ⋯ ⋯
⊢ IsIntegral R x
have obtain : ∀ (a : M) (ha₁ : a ∈ N) (ha₂ : a ≠ 0), IsIntegral R x
Tactic: obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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)
have change : Function.Injective.{u_2 + 1, u_5 + 1} (α := ↥A') (β := Module.End R ↥N) (⇑f.toLinearMap : (a : ↥A') → Module.End R ↥N)
Tactic: change Function.Injective f.toLinearMap
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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.toLinearMap : (a : ↥A') → Module.End R ↥N)
have rw : f.toLinearMap.ker ≤ ⊥
Tactic: rw [← LinearMap.ker_eq_bot, eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (hypothesis)
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
⊢ Membership.mem (γ := Submodule R ↥A') ⊥ s
have this : (↑s : A) • a = 0
Tactic: have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (hypothesis)
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
⊢ IsIntegral R x
have this : 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)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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)
⊢ IsIntegral R x
have change : IsIntegral R (A := A) ((A'.val : (a : ↥A') → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : A)
Tactic: change IsIntegral R (A'.val ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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)
⊢ IsIntegral R (A := A) ((A'.val : (a : ↥A') → A) (Subtype.mk (p := fun (x : A) ↦ x ∈ A') x hx) : A)
have 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)
Tactic: rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (hypothesis)
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)
⊢ 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)
have this₁ : Module.Finite.{u_1, u_5} R ↥N
Tactic: haveI : Module.Finite R N := by rwa [Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (hypothesis)
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
⊢ f.IsIntegralElem z
have 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
Tactic: have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (hypothesis)
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
⊢ f.IsIntegralElem z
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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
⊢ Membership.mem (γ := Subalgebra S B) S[x] (r • x)
have 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)
Tactic: rw [← algebraMap_smul S]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
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
⊢ 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)
have hx₁ : Membership.mem (γ := Subalgebra S B) S[x] x
Tactic: apply Subalgebra.smul_mem
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (A := A ⊗[R] B) (x ⊗ₜ[R] y)
have rw : IsIntegral A (HSMul.hSMul (β := A ⊗[R] B) x (1 ⊗ₜ[R] y))
Tactic: rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ (g * h) • x = g • h • x
have a : (↑((g * h) • x) : K) = (↑(g • h • x) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x = x
have a : (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := G) 1 x) : K) = (↑x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ HSMul.hSMul (β := ↥(integralClosure R K)) g 0 = 0
have a : (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 0) : K) = (↑0 : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x + y) = g • x + g • y
have a : (↑(g • (x + y)) : K) = (↑(g • x + g • y) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
⊢ HSMul.hSMul (β := ↥(integralClosure R K)) g 1 = 1
have a : (↑(HSMul.hSMul (β := ↥(integralClosure R K)) g 1) : K) = (↑1 : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Basic (goal)
Goal:
G : Type u_1
R : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : Group G
inst_4 : MulSemiringAction G K
inst_5 : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x * y) = g • x * g • y
have a : (↑(g • (x * y)) : K) = (↑(g • x * g • y) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x : R[X]
hx :
  Membership.mem (γ := Set R[X])
    {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x} x
i : ℕ
⊢ x.coeff i ∈ I ^ i
have mem : ∀ (r : R) (hrI : r ∈ I), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X).coeff i ∈ I ^ i
Tactic: obtain ⟨r, hrI, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.Algebra.Ideal (goal)
Goal:
R : Type u_3
inst : CommRing R
I : Ideal R
P x y : R[X]
hx_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) x
hy_1 :
  Membership.mem (γ := Subalgebra R R[X])
    (Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}) y
hx : ∀ (i : ℕ), x.coeff i ∈ I ^ i
hy : ∀ (i : ℕ), y.coeff i ∈ I ^ i
i : ℕ
⊢ (x * y).coeff i ∈ I ^ i
have mul : ∑ x_1 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, x.coeff x_1.1 * y.coeff x_1.2 ∈ I ^ i
Tactic: rw [coeff_mul]