mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ (DistribSMul.toLinearMap R M (x + y)).restrict ⋯ =
    (DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ (DistribSMul.toLinearMap R M (x + y)).restrict ⋯ =
    (DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x y : ↥A'
x✝ : ↥N
⊢ ↑(((DistribSMul.toLinearMap R M (x + y)).restrict ⋯) x✝) =
    ↑(((DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯) x✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x y : ↥A'
x✝ : ↥N
⊢ ↑(((DistribSMul.toLinearMap R M (x + y)).restrict ⋯) x✝) =
    ↑(((DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯) x✝)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
⊢ ∀ (m : R) (x : ↥A'),
    (DistribSMul.toLinearMap R M (m • x)).restrict ⋯ = (RingHom.id R) m • (DistribSMul.toLinearMap R M x).restrict ⋯

Tactic:
intro r

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
r : R
⊢ ∀ (x : ↥A'),
    (DistribSMul.toLinearMap R M (r • x)).restrict ⋯ = (RingHom.id R) r • (DistribSMul.toLinearMap R M x).restrict ⋯
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
r : R
s : ↥A'
⊢ (DistribSMul.toLinearMap R M (r • s)).restrict ⋯ = (RingHom.id R) r • (DistribSMul.toLinearMap R M s).restrict ⋯

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
r : R
s : ↥A'
⊢ (DistribSMul.toLinearMap R M (r • s)).restrict ⋯ = (RingHom.id R) r • (DistribSMul.toLinearMap R M s).restrict ⋯
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
r : R
s : ↥A'
x✝ : ↥N
⊢ ↑(((DistribSMul.toLinearMap R M (r • s)).restrict ⋯) x✝) =
    ↑(((RingHom.id R) r • (DistribSMul.toLinearMap R M s).restrict ⋯) x✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
r : R
s : ↥A'
x✝ : ↥N
⊢ ↑(((DistribSMul.toLinearMap R M (r • s)).restrict ⋯) x✝) =
    ↑(((RingHom.id R) r • (DistribSMul.toLinearMap R M s).restrict ⋯) x✝)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x✝ : ↥N
⊢ ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } 1) x✝) = ↑(1 x✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x✝ : ↥N
⊢ ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } 1) x✝) = ↑(1 x✝)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
x y : ↥A'
⊢ { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x y : ↥A'
x✝ : ↥N
⊢ ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y)) x✝) =
    ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
          { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y)
        x✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : 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 := ⋯
x y : ↥A'
x✝ : ↥N
⊢ ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y)) x✝) =
    ↑(({ toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
          { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y)
        x✝)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C (A⁻¹.det * A.det) * ((scalar n) X - C.mapMatrix A⁻¹).det =
    C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C (A⁻¹.det * A.det) * ((scalar n) X - C.mapMatrix A⁻¹).det =
    C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix (A * A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix (A * A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ S[x]

Tactic:
;

Goal state after:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ S[x]
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ S[x]

Tactic:
;

Goal state after:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ S[x]
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ S[x]

Tactic:
exact Algebra.subset_adjoin rfl

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ ↑((g * h) • x) = ↑(g • h • x)

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ ↑((g * h) • x) = ↑(g • h • x)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ ↑(1 • x) = ↑x

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ ↑(1 • x) = ↑x
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ ↑(g • 0) = ↑0

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ ↑(g • 0) = ↑0
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ ↑(g • (x + y)) = ↑(g • x + g • y)

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ ↑(g • (x + y)) = ↑(g • x + g • y)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A.det⁻¹ʳ * ((-1) ^ Fintype.card n * (1 - (diagonal fun x ↦ X) * A.map ⇑C).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * (1 - (diagonal fun x ↦ X) * A.map ⇑C).det

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A.det⁻¹ʳ * ((-1) ^ Fintype.card n * (1 - (diagonal fun x ↦ X) * A.map ⇑C).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * (1 - (diagonal fun x ↦ X) * A.map ⇑C).det
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ ↑(g • 1) = ↑1

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ ↑(g • 1) = ↑1
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ ↑(g • (x * y)) = ↑(g • x * g • y)

Tactic:
;

Goal state after:
G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ ↑(g • (x * y)) = ↑(g • x * g • y)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
⊢ (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
⊢ (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
s : Finset n
⊢ D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
s : Finset n
⊢ D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
s : Finset n
⊢ (map (s.piecewise M 1) ⇑C).det = C (det (s.piecewise M 1))

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
s : Finset n
⊢ (map (s.piecewise M 1) ⇑C).det = C (det (s.piecewise M 1))
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
;

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case e_a.e_f.e_a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
h_smul :
  (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i) = fun i ↦
    (if i ∈ s then X else 1) • s.piecewise (fun i ↦ M.map (⇑C) i) (fun i ↦ 1 i) i
⊢ (∏ i, if i ∈ s then X else 1) • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) =
    X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)

Tactic:
simp only [Finset.prod_ite_mem, Finset.univ_inter, Finset.prod_const]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
⊢ s ∈ {s | #s = k} ↔ s ∈ powersetCard k univ

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
⊢ s ∈ {s | #s = k} ↔ s ∈ powersetCard k univ
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
hy : y ^ 2 = 0
c : R
h : c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p
⊢ c * 0 + eval x (derivative p) * y + eval x p = eval x p + eval x (derivative p) * y

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
hy : y ^ 2 = 0
c : R
h : c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p
⊢ c * 0 + eval x (derivative p) * y + eval x p = eval x p + eval x (derivative p) * y