mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: 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'
⊢ (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      (X.dCokernelSequence (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)
          (have this := homOfLE ⋯;
          this)
          (homOfLE ⋯ ≫ homOfLE ⋯) ⋯ (n₀ - 1) n₀ n₁ n₂ ⋯ ⋯ ⋯).g =
    (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).g ≫
      (Iso.refl (ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).X₃).hom

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinianRing R
⊢ IsArtinianRing S

Tactic:
isArtinianRing_iff

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinian R R
⊢ IsArtinian S S
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: 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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe 0

Tactic:
simp

Goal state after:
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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ q + 1 ≤ 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: 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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ WithBotTop.coe (coreE₂Cohomological.deg (p, q)) < coreE₂Cohomological.i₁ (p, q)

Tactic:
simp

Goal state after:
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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ p < 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: 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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ WithBotTop.coe 0 < coreE₂Cohomological.i₁ (p, q)

Tactic:
simp

Goal state after:
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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ 0 < q
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: 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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe (coreE₂Cohomological.deg (p, q))

Tactic:
simp

Goal state after:
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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ q + 1 ≤ p + q
Module: Mathlib.Algebra.Lie.OfAssociative

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 y : L
z : M
⊢ (φ x) ⁅y, z⁆ = ⁅((ad R L) x) y, z⁆ + ⁅y, (φ x) z⁆

Tactic:
simp

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

Goal state before:
pp: case zero
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 y : L
z : M
⊢ (φ x ^ 0) ⁅y, z⁆ = ∑ ij ∈ antidiagonal 0, Nat.choose 0 ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆

Tactic:
simp

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₂
hf : Function.Injective ⇑f
x y : ↥K
⊢ f ⁅↑x, ↑y⁆ = ⁅f ↑x, f ↑y⁆

Tactic:
simp

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₂
x✝ : L₂
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
simp

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
S : Set (LieSubalgebra R L)
x : L
⊢ x ∈ ⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p ↔ x ∈ ⋂ s ∈ S, ↑s

Tactic:
simp

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

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
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
x✝ : M
⊢ ((toEnd R L M₂) x ∘ₗ ↑f) x✝ = (↑f ∘ₗ (toEnd R L M) x) x✝

Tactic:
simp

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
⊢ Subsingleton ↑↑⊥

Tactic:
simp

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

Goal state before:
pp: case zero_left
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y✝ y : L
hy : y ∈ span R s
⊢ ⁅0, y⁆ ∈ span R s

Tactic:
simp

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

Goal state before:
pp: case zero_right
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝ y x : L
hx : x ∈ span R s
⊢ ⁅x, 0⁆ ∈ span R s

Tactic:
simp

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
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
i : ι
⊢ ↑(f i) ∈ range (Subtype.val ∘ f)

Tactic:
simp

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
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sInf {x | ∃ s ∈ range fun i ↦ p i, ↑s = x} ↔ x✝ ∈ ⨅ i, ↑(p i)

Tactic:
simp

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

Goal state before:
pp: case refine_2
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 : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
⊢ ⁅y, 0⁆ ∈ Submodule.span R s

Tactic:
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'
I : LieIdeal R L
y : L'
h₁ : Function.Surjective ⇑f
h₂ : y ∈ map f I
⊢ ∃ x, f ↑x = y

Tactic:
rw [← LieSubmodule.mem_toSubmodule, coe_map_of_surjective h₁, Submodule.mem_map] at h₂
  obtain ⟨x, hx, rfl⟩ := h₂
  use ⟨x, hx⟩
  rw [LieHom.coe_toLinearMap]

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
N N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
hs : ↑(insert q t) ⊆ {x | ∃ p ∈ S, ↑p = x}
m' : M
hm' : m' ∈ q
u : M
hu : u ∈ ⨆ x ∈ t, x
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ ↑t ⊆ ↑(insert q t)

Tactic:
simp

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ comap I.incl I ↔ m✝ ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ I.incl.ker ↔ m✝ ∈ ⊥

Tactic:
simp

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
N N' : LieSubmodule R L M
x : M
hx : x ∈ N'
⊢ 0 ∈ N

Tactic:
simp

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
N N' : LieSubmodule R L M
x : M
hx : x ∈ N'
⊢ 0 + x = x

Tactic:
simp

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
N : LieSubmodule R L M
⊢ ∀ b ∈ (fun x ↦ lieSpan R L {x}) '' ↑N, b ≤ N

Tactic:
simp

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 : M →ₗ⁅R,L⁆ N
m n : ↥(maxTrivSubmodule R L M)
⊢ ↑⟨f ↑(m + n), ⋯⟩ = ↑(⟨f ↑m, ⋯⟩ + ⟨f ↑n, ⋯⟩)

Tactic:
simp

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 : M →ₗ⁅R,L⁆ N
t : R
m : ↥(maxTrivSubmodule R L M)
⊢ ↑⟨f ↑(t • m), ⋯⟩ = ↑((RingHom.id R) t • ⟨f ↑m, ⋯⟩)

Tactic:
simp

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
e : M ≃ₗ⁅R,L⁆ N
m : ↥(maxTrivSubmodule R L M)
⊢ ↑((maxTrivHom e.symm.toLieModuleHom) ((maxTrivHom e.toLieModuleHom) m)) = ↑m

Tactic:
simp

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
e : M ≃ₗ⁅R,L⁆ N
n : ↥(maxTrivSubmodule R L N)
⊢ ↑((maxTrivHom e.toLieModuleHom) ((maxTrivHom e.symm.toLieModuleHom) n)) = ↑n

Tactic:
simp

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 g : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
m✝ : M
⊢ (let __LinearMap := ↑(f + g);
      { toLinearMap := __LinearMap, map_lie' := ⋯ })
      m✝ =
    ((let __LinearMap := ↑f;
        { toLinearMap := __LinearMap, map_lie' := ⋯ }) +
        let __LinearMap := ↑g;
        { toLinearMap := __LinearMap, map_lie' := ⋯ })
      m✝

Tactic:
simp

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 : R
G : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
m✝ : M
⊢ (let __LinearMap := ↑(F • G);
      { toLinearMap := __LinearMap, map_lie' := ⋯ })
      m✝ =
    ((RingHom.id R) F •
        let __LinearMap := ↑G;
        { toLinearMap := __LinearMap, map_lie' := ⋯ })
      m✝

Tactic:
simp

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 : M →ₗ⁅R,L⁆ N
x : L
x✝ : M
⊢ ⁅x, ↑F⁆ x✝ = 0 x✝

Tactic:
simp

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))
⊢ (fun F ↦ ⟨↑F, ⋯⟩)
      ((fun f ↦
          let __LinearMap := ↑f;
          { toLinearMap := __LinearMap, map_lie' := ⋯ })
        f) =
    f

Tactic:
simp

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 : M →ₗ⁅R,L⁆ N
⊢ (fun f ↦
        let __LinearMap := ↑f;
        { toLinearMap := __LinearMap, map_lie' := ⋯ })
      ((fun F ↦ ⟨↑F, ⋯⟩) F) =
    F

Tactic:
simp

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
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ map LieModuleHom.id N ↔ m✝ ∈ N

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x y : L) (m : TrivialLieModule R L M), 0 = 0 + 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x : L) (m n : TrivialLieModule R L M), 0 = 0 + 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m✝ ∈ N

Tactic:
simp

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f✝ : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), f m ∈ P
x : L
m : M
⊢ ↑((LinearMap.codRestrict (↑P) (↑f) h) ⁅x, m⁆) = ↑⁅x, (LinearMap.codRestrict (↑P) (↑f) h) m⁆

Tactic:
simp

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
N : LieSubmodule R L M
⊢ map N.incl ⊤ = N

Tactic:
simp

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
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
m✝ : M
⊢ m✝ ∈ map (N.incl.restrictLie H) ⊤ ↔ m✝ ∈ N.restr H

Tactic:
simp

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

Goal state before:
pp: case e'_1.e'_4
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
N' : LieSubmodule R L ↥N
⊢ N = (mapOrderEmbedding ⋯) ⊤

Tactic:
simp

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)
⊢ (Polynomial.aeval a) (map (algebraMap F E) (minpoly F a)) = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
this : Nontrivial A
⊢ (Polynomial.aeval ((algebraMap A B) x)) (X - C x) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
⊢ m ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ↔ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
simp

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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
⊢ ∀ (q : A[X]), q.degree < (X - C a).degree → q = 0 ∨ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0

Tactic:
simp_rw [or_iff_not_imp_left]

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
⊢ ∀ (q : A[X]), q.degree < (X - C a).degree → ¬q = 0 → (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
· rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]

Goal state after:
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 I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker

Tactic:
simp

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

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
hx : IsIntegral A 0
⊢ (minpoly A 0).coeff 0 = 0

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
w✝¹ w✝ : R[X][X]
⊢ eval a (eval b (w✝¹ * C (X - C a) + w✝ * (X - C b))) = 0

Tactic:
simp

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

Goal state before:
pp: 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 σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
x✝ : L
⊢ σ.toLinearMap x✝ = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
⊢ ∀ (i : ℕ), coeff 0 i ∈ I

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0