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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ : R
x✝ : L₁
⊢ x✝² (x✝¹ • x✝) = (RingHom.id R) x✝¹ • x✝² x✝

Tactic:
← coe_toLinearEquiv,

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ : R
x✝ : L₁
⊢ x✝².toLinearEquiv (x✝¹ • x✝) = (RingHom.id R) x✝¹ • x✝².toLinearEquiv x✝
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ x✝ : M
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
← coe_toLinearEquiv,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ x✝ : M
⊢ x✝².toLinearEquiv (x✝¹ + x✝) = x✝².toLinearEquiv x✝¹ + x✝².toLinearEquiv x✝
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ : R
x✝ : M
⊢ x✝² (x✝¹ • x✝) = (RingHom.id R) x✝¹ • x✝² x✝

Tactic:
← coe_toLinearEquiv,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ : R
x✝ : M
⊢ x✝².toLinearEquiv (x✝¹ • x✝) = (RingHom.id R) x✝¹ • x✝².toLinearEquiv x✝
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq pq'
⊢ (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact

Tactic:
refine (ShortComplex.exact_iff_mono _ ((page X data r hr).shape _ _ h)).mpr ?_
    have := isIso_mapFourδ₄Toδ₃' X data r r' hrr' hr pq pq' hpq
      i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' h
    dsimp
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x✝ : L
h : x✝ ∈ ⊥
⊢ x✝ ∈ N

Tactic:
rw [mem_bot] at h

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x✝ : L
h : x✝ = 0
⊢ x✝ ∈ N
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ ⁅e x, e (e.toLinearEquiv.symm y')⁆ = ⁅e x, y'⁆

Tactic:
← coe_toLinearEquiv,

Goal state after:
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ ⁅e.toLinearEquiv x, e.toLinearEquiv (e.toLinearEquiv.symm y')⁆ = ⁅e.toLinearEquiv x, y'⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
p : (x : L) → x ∈ lieSpan R L s → Prop
mem : ∀ (x : L) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : x ∈ lieSpan R L s), p x hx → p (a • x) ⋯
x : L
lie : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p x hx → p y hy → p ⁅x, y⁆ ⋯
hx : x ∈ lieSpan R L s
⊢ p x hx

Tactic:
let p : LieSubalgebra R L :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩
      lie_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ _ hpx hpy⟩ }

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
p✝ : (x : L) → x ∈ lieSpan R L s → Prop
mem : ∀ (x : L) (h : x ∈ s), p✝ x ⋯
zero : p✝ 0 ⋯
add : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p✝ x hx → p✝ y hy → p✝ (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : x ∈ lieSpan R L s), p✝ x hx → p✝ (a • x) ⋯
x : L
lie : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p✝ x hx → p✝ y hy → p✝ ⁅x, y⁆ ⋯
hx : x ∈ lieSpan R L s
p : LieSubalgebra R L :=
  { carrier := {x | ∃ (hx : x ∈ lieSpan R L s), p✝ x hx}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }
⊢ p✝ x hx
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
by exact hs.symm ▸ N.smul_mem'

Goal state after:
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
⊢ y ∈ ↑f.idealRange ↔ ∃ x, f x = y

Tactic:
← LieIdeal.coe_toLieSubalgebra,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
⊢ y ∈ ↑(LieIdeal.toLieSubalgebra R L' f.idealRange) ↔ ∃ x, f x = y
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ x ∈ f.ker

Tactic:
rw [mem_ker]

Goal state after:
case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ f x = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⨅ i, ↑(p i)

Tactic:
rw [iInf, sInf_toSubmodule]; ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
⊢ f.IsIdealMorphism

Tactic:
isIdealMorphism_def,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
⊢ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ ⁅↑z, ↑(-y)⁆ ∈ ↑⁅J, I⁆

Tactic:
apply lie_coe_mem_lie

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ⨆ i, ↑(N i) = ⊤ ↔ ⨆ i, N i = ⊤

Tactic:
← iSup_toSubmodule,

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ↑(⨆ i, N i) = ⊤ ↔ ⨆ i, N i = ⊤
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
⊢ x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0

Tactic:
by
  simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    toEnd_apply_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₁, hn₁⟩⁆ ∈ ⁅I, N⁆

Tactic:
apply lie_coe_mem_lie

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑(⨆ x, ↑↑x) = ⋃ i, ↑↑↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N

Tactic:
← iSup_toSubmodule,

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
hne : Nonempty ↑s
this : ↑↑(⨆ i, ↑i) = ⋃ i, ↑↑↑i
⊢ ↑(sSup s) = ⋃ N ∈ s, ↑N
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅↑x, ↑⟨n₂, hn₂⟩⁆ ∈ ⁅I, N'⁆

Tactic:
apply lie_coe_mem_lie

Goal state after:
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
⊢ ⁅x, ↑f⁆ m = 0

Tactic:
rw [f.property x, LinearMap.zero_apply]

Goal state after:
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆

Tactic:
apply lie_coe_mem_lie

Goal state after:
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆

Tactic:
apply lie_coe_mem_lie

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) ((mapRingHom ((algebraMap E A).comp (algebraMap F E))) g) = 0

Tactic:
← mapRingHom_comp,

Goal state after:
F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
g : F[X]
hg : map (algebraMap F E) g = minpoly E a
hgdeg : g.natDegree = (minpoly E a).natDegree
hgmon : g.Monic
⊢ (Polynomial.aeval a) (((mapRingHom (algebraMap E A)).comp (mapRingHom (algebraMap F E))) g) = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)

Tactic:
rw [minpoly.eq_zero hx, minpoly.eq_zero, zero_comp]
    · simp only [natDegree_zero, pow_zero, mul_zero]
    · exact IsIntegral.neg_iff.not.mpr hx

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

Tactic:
simp only [SModEq.sub_mem, sub_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : ↑U ⊆ (y - x) +ᵥ ↑U
⊢ x - y ∈ U

Tactic:
simpa [Set.mem_vadd_set_iff_neg_vadd_mem] using h U.zero_mem

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + q * (X - C b) = P

Tactic:
mul_comm q,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + (X - C b) * q = P
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case hf
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ Injective ⇑↑(AlgEquiv.algHomUnitsEquiv K L)

Tactic:
exact (AlgEquiv.algHomUnitsEquiv K L).injective

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
refine Fintype.linearIndependent_iff.2 fun g hg i => ?_

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
hg : ∑ i, g i • x ^ ↑i = 0
i : Fin (minpoly K x).natDegree
⊢ g i = 0
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬↑p = 0

Tactic:
Nat.cast_eq_zero

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬p = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M' * (M * N)).det = N.det

Tactic:
← Matrix.mul_assoc,

Goal state after:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M' * M * N).det = N.det
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
⊢ ∀ (b : Basis (↥s) 𝕜 M), ((toMatrix b b) f).det = 1

Tactic:
b

Goal state after:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
⊢ ((toMatrix b b) f).det = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ ((toMatrix b (b.map e)) ↑e * ((toMatrix b b) f * (toMatrix (b.map e) b) ↑e.symm)).det = ((toMatrix b b) f).det

Tactic:
← Matrix.mul_assoc,

Goal state after:
case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ ((toMatrix b (b.map e)) ↑e * (toMatrix b b) f * (toMatrix (b.map e) b) ↑e.symm).det = ((toMatrix b b) f).det
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ f ((⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobeniusEquiv S p).symm)^[n] (f x)

Tactic:
apply_fun (frobeniusEquiv S p)^[n]

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ (⇑(frobeniusEquiv S p))^[n] (f ((⇑(frobeniusEquiv R p).symm)^[n] x)) =
    (⇑(frobeniusEquiv S p))^[n] ((⇑(frobeniusEquiv S p).symm)^[n] (f x))

case inj
R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Injective (⇑(frobeniusEquiv S p))^[n]
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Tactic:
subst hgf₂

Goal state after:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hgf₁ : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst✝⁵ : Field A₁
inst✝⁴ : Ring B₁
inst✝³ : Field A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x✝ : Algebra.IsSeparable A₂ B₂
x : A₂
⊢ ((algebraMap A₁ B₁).comp ↑e₁.symm) x = ((↑e₂.symm).comp (algebraMap A₂ B₂)) x

Tactic:
simpa [RingEquiv.eq_symm_apply] using (RingHom.ext_iff.mp he (e₁.symm x)).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit ((toMatrix v v') ↑f).det

Tactic:
apply isUnit_det_of_left_inverse

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ ?B * (toMatrix v v') ↑f = 1

case B
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι✝ : Type u_4
inst✝³ : DecidableEq ι✝
inst✝² : Fintype ι✝
e : Basis ι✝ R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this✝¹ : Finite ι
this✝ : Fintype ι
this : DecidableEq ι
⊢ M ≃ₗ[R] M

Tactic:
exact LinearEquiv.ofIsUnitDet (v := b) (v' := b) (f := f) (by rwa [det_toMatrix b])

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
M✝ : Type u_2
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
M' : Type u_3
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M✝
𝕜 : Type u_5
inst✝³ : Field 𝕜
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 0
⊢ IsUnit ((toMatrix (finBasis 𝕜 M) (finBasis 𝕜 M)) f).det

Tactic:
by
    rw [LinearMap.det_toMatrix]
    exact isUnit_iff_ne_zero.2 hf

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ (basisFun R ι).det v = (of v).det

Tactic:
Pi.basisFun_det

Goal state after:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ detRowAlternating v = (of v).det