awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
rw : p ∣ n.natAbs
⊢ (↑p : ℤ) ∣ n

Tactic:
rw [Int.natCast_dvd]

Premises used: Int.natCast_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
⊢ p ∣ n.natAbs

Tactic:
Int.Prime.dvd_pow hp h

Premises used: Int.Prime.dvd_pow
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
⊢ p ∣ n.natAbs

Tactic:
exact Int.Prime.dvd_pow hp h

Premises used: Int.Prime.dvd_pow
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
inl : ∀ (hp2 : p ∣ Int.natAbs 2), p = 2 ∨ p ∣ m.natAbs
inr : ∀ (hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs), p = 2 ∨ p ∣ m.natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
rcases Int.Prime.dvd_mul hp h with hp2 | hpp

Premises used: Int.Prime.dvd_mul
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hp2 : p ∣ Int.natAbs 2
inl : p = 2
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
apply Or.intro_left

Premises used: Or.intro_left
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Tactic:
le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)

Premises used: le_antisymm, Nat.Prime.two_le, zero_lt_two, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Tactic:
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)

Premises used: le_antisymm, Nat.Prime.two_le, zero_lt_two, Nat.le_of_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs
inr : p ∣ m.natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
apply Or.intro_right

Premises used: Or.intro_right
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs
⊢ p ∣ m.natAbs * m.natAbs

Tactic:
rw [sq, Int.natAbs_mul] at hpp

Premises used: Int.natAbs_mul, sq
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs

Tactic:
or_self_iff.mp ((Nat.Prime.dvd_mul hp).mp hpp)

Premises used: or_self_iff, Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs

Tactic:
exact or_self_iff.mp ((Nat.Prime.dvd_mul hp).mp hpp)

Premises used: or_self_iff, Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
hn : n.natAbs ≠ 1
obtain : ∀ (p : ℕ) (pp : Nat.Prime p) (pd : p ∣ n.natAbs), ∃ (p : ℤ), Prime p ∧ p ∣ n
⊢ ∃ (p : ℤ), Prime p ∧ p ∣ n

Tactic:
obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn

Premises used: Nat.exists_prime_and_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
hn : n.natAbs ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ n.natAbs
⊢ ∃ (p : ℤ), Prime p ∧ p ∣ n

Tactic:
⟨p, Nat.prime_iff_prime_int.mp pp, Int.natCast_dvd.mpr pd⟩

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Nat.cast, And.intro, Exists.intro, Iff.mp, Int.natCast_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
hn : n.natAbs ≠ 1
p : ℕ
pp : Nat.Prime p
pd : p ∣ n.natAbs
⊢ ∃ (p : ℤ), Prime p ∧ p ∣ n

Tactic:
exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.natCast_dvd.mpr pd⟩
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
k : ℤ
⊢ Prime k ↔ Nat.Prime k.natAbs

Tactic:
(Int.associated_natAbs k).prime_iff.trans Nat.prime_iff_prime_int.symm

Premises used: Nat.prime_iff_prime_int, Iff.trans, Associated.prime_iff, Iff.symm, Int.associated_natAbs
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a : ℤ
rw : Associated (↑a.natAbs : ℤ) a
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑a.natAbs : ℤ)}) (Ideal.span {a})

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]

Premises used: Ideal.span_singleton_eq_span_singleton
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a : ℤ
⊢ Associated (↑a.natAbs : ℤ) a

Tactic:
(associated_natAbs _).symm

Premises used: Associated.symm, Int.associated_natAbs
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a : ℤ
⊢ Associated (↑a.natAbs : ℤ) a

Tactic:
exact (associated_natAbs _).symm

Premises used: Associated.symm, Int.associated_natAbs
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
⊢ IsCoprime 2 m ↔ Odd m

Tactic:
simp [isCoprime_iff_nat_coprime]

Premises used: Int.isCoprime_iff_nat_coprime
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m : ℤ
⊢ IsCoprime m 2 ↔ Odd m

Tactic:
simp [isCoprime_iff_nat_coprime]

Premises used: Int.isCoprime_iff_nat_coprime
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
obtain : ∀ (d : ℤ) (hd : Associated (d ^ k) a), ∃ (d : ℤ), a = d ^ k
⊢ ∃ (d : ℤ), a = d ^ k

Tactic:
obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h

Premises used: exists_associated_pow_of_mul_eq_pow'
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated (d ^ k) a
⊢ Associated a (d ^ k)

Tactic:
replace hd := hd.symm
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated a (d ^ k)
⊢ a = d ^ k ∨ a = (-d) ^ k

Tactic:
rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← hk.neg_pow] at hd

Premises used: Odd.neg_pow, Int.natAbs_eq_natAbs_iff, Int.associated_iff_natAbs
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
inl : ∀ (hab : IsCoprime (d ^ k) b) (h : d ^ k * b = c ^ k), ∃ (d_1 : ℤ), d ^ k = d_1 ^ k
inr : ∀ (hab : IsCoprime ((-d) ^ k) b) (h : (-d) ^ k * b = c ^ k), ∃ (d_1 : ℤ), (-d) ^ k = d_1 ^ k
⊢ ∃ (d : ℤ), a = d ^ k

Tactic:
obtain rfl | rfl := hd

Premises used: rfl
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime (d ^ k) b
h : d ^ k * b = c ^ k
⊢ ∃ (d_1 : ℤ), d ^ k = d_1 ^ k

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime (d ^ k) b
h : d ^ k * b = c ^ k
⊢ ∃ (d_1 : ℤ), d ^ k = d_1 ^ k

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime ((-d) ^ k) b
h : (-d) ^ k * b = c ^ k
⊢ ∃ (d_1 : ℤ), (-d) ^ k = d_1 ^ k

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime ((-d) ^ k) b
h : (-d) ^ k * b = c ^ k
⊢ ∃ (d_1 : ℤ), (-d) ^ k = d_1 ^ k

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : b * a = c ^ k), b * a = c ^ k
⊢ b * a = c ^ k

Tactic:
rwa [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ (∃ (d : ℤ), a = d ^ k) ∧ ∃ (e : ℤ), b = e ^ k

Tactic:
⟨eq_pow_of_mul_eq_pow_odd_left hab hk h, eq_pow_of_mul_eq_pow_odd_right hab hk h⟩

Premises used: Int.eq_pow_of_mul_eq_pow_odd_right, Int.eq_pow_of_mul_eq_pow_odd_left, And.intro
-- 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
S : Subalgebra R B
⊢ Algebra.IsIntegral.{u_1, u_3} R ↥S ↔ ∀ x ∈ S, IsIntegral R x

Tactic:
Algebra.isIntegral_def.trans <| .trans
    (forall_congr' fun _ ↦ (isIntegral_algHom_iff S.val Subtype.val_injective).symm) Subtype.forall

Premises used: Algebra.isIntegral_def, Subtype.val_injective, Subalgebra.val, isIntegral_algHom_iff, Subtype.forall, forall_congr', Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : Algebra.IsIntegral R B
⊢ Algebra.IsIntegral R A

Tactic:
⟨fun _ ↦ (isIntegral_algHom_iff f hf).mp (isIntegral _)⟩

Premises used: Algebra.IsIntegral.isIntegral, isIntegral_algHom_iff, Iff.mp, Algebra.IsIntegral.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra.IsIntegral R A
f : A →ₐ[R] B
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Algebra.IsIntegral R B

Tactic:
isIntegral_def.mpr fun b ↦ let ⟨a, ha⟩ := hf b; ha ▸ (isIntegral_def.mp ‹_› a).map f

Premises used: Iff.mpr, Algebra.isIntegral_def, Eq.rec, IsIntegral, IsIntegral.map, Iff.mp, _private.0.Algebra.IsIntegral.of_surjective.match_1
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ Algebra.IsIntegral R A ↔ Algebra.IsIntegral R B

Tactic:
⟨fun h ↦ h.of_injective e.symm e.symm.injective, fun h ↦ h.of_injective e e.injective⟩

Premises used: Algebra.IsIntegral.of_injective, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : Algebra R A
inst_5 : Algebra R B
f : R →+* S
M : Type u_5
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module.Finite R M
⊢ Algebra.IsIntegral.{u_1, u_5} R (End R M)

Tactic:
⟨LinearMap.exists_monic_and_aeval_eq_zero R⟩

Premises used: LinearMap.exists_monic_and_aeval_eq_zero, Algebra.IsIntegral.mk
-- 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
inst_3 : Module.Finite R B
x : B
⊢ IsIntegral R x

Tactic:
(isIntegral_algHom_iff (Algebra.lmul R B) Algebra.lmul_injective).mp
    (Algebra.IsIntegral.isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, Algebra.lmul, Algebra.lmul_injective, isIntegral_algHom_iff, Iff.mp
-- 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
h : IsNoetherian R B
x : B
⊢ IsIntegral R x

Tactic:
.of_finite R x

Premises used: IsIntegral.of_finite
-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Ring B
inst_3 : CommRing S
inst_4 : Algebra R A
inst_5 : Algebra R B
f : R →+* S
inst_6 : Module.Finite R B
⊢ Algebra.IsIntegral R B

Tactic:
⟨.of_finite R⟩

Premises used: IsIntegral.of_finite, Algebra.IsIntegral.mk
-- 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
H : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
⊢ Algebra.IsIntegral R B

Tactic:
.of_surjective (Algebra.ofId R B) H

Premises used: Algebra.IsIntegral.of_surjective, Algebra.ofId
-- 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
S : Subalgebra R B
HS : FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) S)
x : B
hx : x ∈ S
⊢ IsIntegral R x

Tactic:
have : Module.Finite R S := .of_fg HS
  (isIntegral_algHom_iff S.val Subtype.val_injective).mpr (.of_finite R (⟨x, hx⟩ : S))

Premises used: Iff.mpr, Subtype.val_injective, Subalgebra.val, isIntegral_algHom_iff, Subtype.mk, Module.Finite.of_fg, IsIntegral.of_finite
-- 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
S : Subalgebra R B
H : IsNoetherian.{u_1, u_3} R ↥((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) S : Submodule R B)
x : B
hx : x ∈ S
⊢ IsIntegral R x

Tactic:
.of_mem_of_fg _ ((Submodule.fg_top _).mp <| H.noetherian _) _ hx

Premises used: IsNoetherian.noetherian, Iff.mp, Submodule.fg_top, IsIntegral.of_mem_of_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_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'
h :
  ∀ (x_2 : ↥N),
    Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (x + y)) ⋯ : (a : ↥N) → ↥N) x_2) : M)
      (↑((HAdd.hAdd (α := Module.End R ↥N) (LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯)
                (LinearMap.restrict (DistribSMul.toLinearMap R M y) ⋯) :
              (a : ↥N) → ↥N)
            x_2) :
        M)
⊢ 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) ⋯)

Tactic:
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_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'
x_2 : ↥N
⊢ Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (x + y)) ⋯ : (a : ↥N) → ↥N) x_2) : M)
    (↑((HAdd.hAdd (α := Module.End R ↥N) (LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯)
              (LinearMap.restrict (DistribSMul.toLinearMap R M y) ⋯) :
            (a : ↥N) → ↥N)
          x_2) :
      M)

Tactic:
add_smul _ _ _

Premises used: add_smul
-- 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_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'
x_2 : ↥N
⊢ Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (x + y)) ⋯ : (a : ↥N) → ↥N) x_2) : M)
    (↑((HAdd.hAdd (α := Module.End R ↥N) (LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯)
              (LinearMap.restrict (DistribSMul.toLinearMap R M y) ⋯) :
            (a : ↥N) → ↥N)
          x_2) :
      M)

Tactic:
exact add_smul _ _ _

Premises used: add_smul
-- 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' := ⋯ }
r : R
s : ↥A'
h :
  ∀ (x : ↥N),
    Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (r • s)) ⋯ : (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) ⋯) :
              (a : ↥N) → ↥N)
            x) :
        M)
⊢ 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) ⋯)

Tactic:
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' := ⋯ }
r : R
s : ↥A'
x_1 : ↥N
⊢ Eq.{u_5 + 1} (α := M) (↑((LinearMap.restrict (DistribSMul.toLinearMap R M (r • s)) ⋯ : (a : ↥N) → ↥N) x_1) : M)
    (↑((HSMul.hSMul (α := R) (β := Module.End R ↥N) ((RingHom.id R : (a : R) → R) r : R)
              (LinearMap.restrict (DistribSMul.toLinearMap R M s) ⋯) :
            (a : ↥N) → ↥N)
          x_1) :
      M)

Tactic:
apply smul_assoc

Premises used: smul_assoc
-- 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' := ⋯ }
h :
  ∀ (x : ↥N),
    Eq.{u_5 + 1} (α := M)
      (↑((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (a : ↥A') → Module.End R ↥N)
                1 :
              (a : ↥N) → ↥N)
            x) :
        M)
      (↑((1 : (a : ↥N) → ↥N) x) : M)
⊢ 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

Tactic:
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' := ⋯ }
x_1 : ↥N
⊢ Eq.{u_5 + 1} (α := M)
    (↑((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : ↥A') → Module.End R ↥N)
              1 :
            (a : ↥N) → ↥N)
          x_1) :
      M)
    (↑((1 : (a : ↥N) → ↥N) x_1) : M)

Tactic:
apply one_smul

Premises used: one_smul
-- 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_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'
h :
  ∀ (x_2 : ↥N),
    Eq.{u_5 + 1} (α := M)
      (↑(((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯,
                      map_smul' := ⋯ } :
                    (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) ⋯, 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) :
              (a : ↥N) → ↥N)
            x_2) :
        M)
⊢ ({ 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)

Tactic:
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_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'
x_2 : ↥N
⊢ Eq.{u_5 + 1} (α := M)
    (↑(((({ toFun := fun (x : ↥A') ↦ LinearMap.restrict (DistribSMul.toLinearMap R M x) ⋯, map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (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) ⋯, 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) :
            (a : ↥N) → ↥N)
          x_2) :
      M)

Tactic:
apply mul_smul

Premises used: SemigroupAction.mul_smul