mathlib-initiative/mathlib-tactics huggingface dataset:
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
N : LieSubmodule R L M
x : L
h : ∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N
⊢ LinearMap.restrict ((toEnd R L M) x) h = (toEnd R L ↥N) x

Tactic:
by

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
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo ⇑(((toEnd R L M) x - (algebraMap R (Module.End R M)) φ) ^ k) ↑N ↑N

Tactic:
by

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₂
⊢ Subsingleton (LieSubalgebra R ↥⊥)

Tactic:
by

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 K' : LieSubalgebra R L
⊢ Disjoint K.toSubmodule K'.toSubmodule ↔ Disjoint K K'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ ⇑(ad R A) = LinearMap.mulLeft R - LinearMap.mulRight R

Tactic:
by

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 K' : LieSubalgebra R L
h : K ≤ K'
x y : ↥K
⊢ (inclusion h) x = (inclusion h) y → x = y

Tactic:
by

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
⊢ (ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (ad R ↥K) x

Tactic:
by

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 K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ x ∈ ofLe h ↔ ↑x ∈ K

Tactic:
simp only [ofLe, inclusion_apply, LieHom.mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    exact y.property
  · intro h
    use ⟨(x : L), h⟩

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 K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ x ∈ ofLe h ↔ ↑x ∈ K

Tactic:
by

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 K' : LieSubalgebra R L
h : K ≤ K'
⊢ ofLe h = comap K'.incl K

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ (Subalgebra.toSubmodule A').carrier
hy : y ∈ (Subalgebra.toSubmodule A').carrier
⊢ ⁅x, y⁆ ∈ (Subalgebra.toSubmodule A').carrier

Tactic:
by

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 L
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
by

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 L
⊢ s ⊆ ↑(lieSpan R L s)

Tactic:
by

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 L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule

Tactic:
by

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

Goal state before:
pp: R : Type u
A₁ : Type v
A₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : Ring A₁
inst✝² : Ring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆

Tactic:
by

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 L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ ↑K

Tactic:
by

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 t : Set L
h : s ⊆ t
⊢ lieSpan R L s ≤ lieSpan R L t

Tactic:
by

Goal state after:
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
⊢ e.toLinearEquiv.conj ((ad R L) x) = (ad R L') (e x)

Tactic:
by

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
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p

Tactic:
by

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
x y : L
h : x ∈ I
⊢ ⁅x, y⁆ ∈ I

Tactic:
by

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

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ {x y : L}, x ∈ (↑I).carrier → y ∈ (↑I).carrier → ⁅x, y⁆ ∈ (↑I).carrier

Tactic:
by

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
K : LieSubalgebra R L
⊢ (∃ I, LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
by

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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
by

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 L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
this : ∀ {x y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
⊢ (lieSpan R L s).toSubmodule = span R s

Tactic:
by

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

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'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier
this : ⁅f x, f y⁆ ∈ J
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
by

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

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'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
by

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
h : ↑(map f I) = ⇑f '' ↑I
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
by

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
x : L
hx : x ∈ I
⊢ f x ∈ map f I

Tactic:
by

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
J : LieIdeal R L'
⊢ map f I ≤ J ↔ I ≤ comap f J

Tactic:
by

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 L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
⊢ (lieSpan R L s).toSubmodule = span R s

Tactic:
by

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'
J : LieIdeal R L'
⊢ map f (comap f J) ≤ J

Tactic:
by

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
⊢ I ≤ comap f (map f I)

Tactic:
by

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₂
s : Set L
⊢ map f (lieSpan R L s) = lieSpan R L₂ (⇑f '' s)

Tactic:
by

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₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ map f I₁ ≤ map f I₂

Tactic:
by

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'
J₁ J₂ : LieIdeal R L'
h : J₁ ≤ J₂
⊢ comap f J₁ ≤ comap f J₂

Tactic:
by

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 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:
by

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 L
this : ∀ (s : Set L), lieSpan R L (-s) ≤ lieSpan R L s
⊢ lieSpan R L s ≤ lieSpan R L (-s)

Tactic:
by

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' N O : LieSubmodule R L M
h : (fun s ↦ (↑s).carrier) N = (fun s ↦ (↑s).carrier) O
⊢ N = O

Tactic:
by

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

Goal state before:
pp: case lie
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s✝ s : Set L
x x✝ y✝ : L
hx✝ : x✝ ∈ lieSpan R L (-s)
hy✝ : y✝ ∈ lieSpan R L (-s)
hu : x✝ ∈ lieSpan R L s
hv : y✝ ∈ lieSpan R L s
⊢ ⁅x✝, y✝⁆ ∈ lieSpan R L s

Tactic:
| lie _ _ _ _ hu hv =>

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 L
⊢ lieSpan R L (-s) = lieSpan R L s

Tactic:
by

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 : L
m : M
h : m ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, m⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
by

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 L
x u : L
hu : u ∈ s
⊢ ⟨u, ⋯⟩ ∈ Subtype.val ⁻¹' s

Tactic:
by

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
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
⊢ ↑{ toSubmodule := p, lie_mem := h } = p

Tactic:
by

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
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I = J

Tactic:
by

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

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'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ Subsingleton (LieIdeal R ↥⊥)

Tactic:
by

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
x y : LieSubmodule R L M
h : ↑x = ↑y
⊢ x = y

Tactic:
by

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'
⊢ f.idealRange = LieIdeal.map f ⊤

Tactic:
by

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 M
hs : s = ↑N
a✝ b✝ : M
x : a✝ ∈ s
y : b✝ ∈ s
⊢ a✝ + b✝ ∈ s

Tactic:
by

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 M
hs : s = ↑N
⊢ 0 ∈ s

Tactic:
by

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 M
hs : s = ↑N
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
by

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 M
hs : s = ↑N
⊢ ∀ {x : L} {m : M}, m ∈ s → ⁅x, m⁆ ∈ s

Tactic:
by

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 L
⊢ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤

Tactic:
by

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 y : L) (m : ↥N), ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩

Tactic:
by

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
x : L
hx : x ∈ K
hx' : x ∈ lieSpan R L (range (Subtype.val ∘ f))
this : x ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ ⟨x, hx⟩ ∈ lieSpan R (↥K) (range f)

Tactic:
by

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 : L) (m n : ↥N), ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩

Tactic:
by

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 y : L) (m : ↥N), ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩

Tactic:
by

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'
⊢ f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z

Tactic:
by

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:
by

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
⊢ comap K.incl (lieSpan R L (range (Subtype.val ∘ f))) = lieSpan R (↥K) (range f)

Tactic:
by

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
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
by

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

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.Injective ⇑f
⊢ Function.Injective ⇑↑f

Tactic:
by

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

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : ↑L₁' = ↑L₁''
⊢ L₁'.toSubmodule = L₁''.toSubmodule

Tactic:
by

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'
x : L
⊢ f x ∈ f.idealRange

Tactic:
by

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

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
⊢ (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun ⁅x, y⁆ =
    ⁅(↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun x,
      (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun y⁆

Tactic:
by

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

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑e.toLinearEquiv) L₁'.toSubmodule = L₂'.toSubmodule

Tactic:
by

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

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
⊢ (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun ⁅x, y⁆ =
    ⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun x,
      (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun y⁆

Tactic:
by

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 : f.IsIdealMorphism
y : L'
⊢ y ∈ f.idealRange ↔ ∃ x, f x = y

Tactic:
by

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ ∀ (t : R) (x : L) (m : ↥N), ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by

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₂
hf : N₂ ≤ f.range
⊢ map f (comap f N₂) = N₂

Tactic:
by

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₂
hf : f.ker = ⊥
⊢ comap f (map f N) = N

Tactic:
by

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

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
⊢ map N.incl (comap N.incl N') = N ⊓ N'

Tactic:
by

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
⊢ I ≤ f.ker ↔ ∀ x ∈ I, f x = 0

Tactic:
by

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ ∀ (t : R) (x : L) (m : ↥N), ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
by

Goal state after: