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₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ q + 1 ≤ 0

Tactic:
;

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
⊢ p < 0

Tactic:
;

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.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝ + x✝¹ * x✝ - (x✝ * x✝² + x✝ * x✝¹) = x✝² * x✝ - x✝ * x✝² + (x✝¹ * x✝ - x✝ * x✝¹)

Tactic:
;

Goal state after:
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝ + x✝¹ * x✝ - (x✝ * x✝² + x✝ * x✝¹) = x✝² * x✝ - x✝ * x✝² + (x✝¹ * x✝ - x✝ * x✝¹)
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝¹ + x✝² * x✝ - (x✝¹ * x✝² + x✝ * x✝²) = x✝² * x✝¹ - x✝¹ * x✝² + (x✝² * x✝ - x✝ * x✝²)

Tactic:
;

Goal state after:
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * x✝¹ + x✝² * x✝ - (x✝¹ * x✝² + x✝ * x✝²) = x✝² * x✝¹ - x✝¹ * x✝² + (x✝² * x✝ - x✝ * x✝²)
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * (x✝¹ * x✝) - x✝² * (x✝ * x✝¹) - (x✝¹ * (x✝ * x✝²) - x✝ * (x✝¹ * x✝²)) =
    x✝² * (x✝¹ * x✝) - x✝¹ * (x✝² * x✝) - (x✝ * (x✝² * x✝¹) - x✝ * (x✝¹ * x✝²)) +
      (x✝¹ * (x✝² * x✝) - x✝¹ * (x✝ * x✝²) - (x✝² * (x✝ * x✝¹) - x✝ * (x✝² * x✝¹)))

Tactic:
;

Goal state after:
A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ x✝² * (x✝¹ * x✝) - x✝² * (x✝ * x✝¹) - (x✝¹ * (x✝ * x✝²) - x✝ * (x✝¹ * x✝²)) =
    x✝² * (x✝¹ * x✝) - x✝¹ * (x✝² * x✝) - (x✝ * (x✝² * x✝¹) - x✝ * (x✝¹ * x✝²)) +
      (x✝¹ * (x✝² * x✝) - x✝¹ * (x✝ * x✝²) - (x✝² * (x✝ * x✝¹) - x✝ * (x✝² * x✝¹)))
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ f a = g a

Tactic:
;

Goal state after:
A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ f a = g a
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
m : M
⊢ { toFun := fun m ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ({ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      m

Tactic:
;

Goal state after:
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
m : M
⊢ { toFun := fun m ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ({ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      m
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
t : R
x : L
m : M
⊢ { toFun := fun m ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ((RingHom.id R) t • { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }) m

Tactic:
;

Goal state after:
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
t : R
x : L
m : M
⊢ { toFun := fun m ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ((RingHom.id R) t • { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }) m
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
m : M
⊢ { toFun := fun m ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ⁅{ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ },
        { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }⁆
      m

Tactic:
;

Goal state after:
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
m : M
⊢ { toFun := fun m ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } m =
    ⁅{ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ },
        { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }⁆
      m
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m

Tactic:
;

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m
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
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
m : M
⊢ ((toEnd R L M) x) m = 0 m

Tactic:
;

Goal state after:
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
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
m : M
⊢ ((toEnd R L M) x) m = 0 m
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₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩

Tactic:
;

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₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩
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₂
x : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤

Tactic:
;

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₂
x : L
hx : x ∈ ⊥
⊢ ⟨x, hx⟩ ∈ ⊥ ↔ ⟨x, hx⟩ ∈ ⊤
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₂
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ ⟨x, hx✝⟩ ∈ ⊥ ↔ ⟨x, hx✝⟩ ∈ ⊤

Tactic:
;

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₂
x : L
hx✝ : x ∈ ⊥
hx : x = 0
⊢ ⟨x, hx✝⟩ ∈ ⊥ ↔ ⟨x, hx✝⟩ ∈ ⊤
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 b : A
⊢ ((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ ((ad R A) a) b = ((LinearMap.mulLeft R - LinearMap.mulRight R) a) b
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:
;

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

Tactic:
;

Goal state after:
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⁆ ∈ A'
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
hy : y ∈ (Subalgebra.toSubmodule A').carrier
hx : x ∈ A'
⊢ ⁅x, y⁆ ∈ A'

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : Ring A
inst✝ : Algebra R A
A' : Subalgebra R A
x y : A
hy : y ∈ (Subalgebra.toSubmodule A').carrier
hx : x ∈ A'
⊢ ⁅x, y⁆ ∈ A'
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
      change ⁅x, y⁆ ∈ A'; change x ∈ A' at hx; change y ∈ A' at hy
      rw [LieRing.of_associative_ring_bracket]
      have hxy := A'.mul_mem hx hy
      have hyx := A'.mul_mem hy hx
      exact Submodule.sub_mem (Subalgebra.toSubmodule A') hxy hyx

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 ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
;

Goal state after:
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 ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
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
⊢ ⁅-y, x⁆ ∈ I

Tactic:
;

Goal state after:
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
⊢ ⁅-y, x⁆ ∈ I
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 ∈ I

Tactic:
;

Goal state after:
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 ∈ I
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
a✝ : x ∈ (↑I).carrier
hy : y ∈ (↑I).carrier
⊢ ⁅x, y⁆ ∈ (↑I).carrier

Tactic:
;

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

Tactic:
;

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
x y : L
a✝ : x ∈ (↑I).carrier
hy : y ∈ (↑I).carrier
⊢ y ∈ I
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Tactic:
;

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑⟨y, hy⟩ ∈ K
⊢ ⁅↑⟨x, hx⟩, ↑⟨y, hy⟩⁆ ∈ K

Tactic:
;

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑⟨y, hy⟩ ∈ K
⊢ ⁅↑⟨x, hx⟩, ↑⟨y, hy⟩⁆ ∈ K
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
⊢ ⇑f '' ↑I = ⇑↑f '' ↑↑I

Tactic:
;

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'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ ⇑f '' ↑I = ⇑↑f '' ↑↑I
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case a
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₂
⊢ (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule

Tactic:
;

Goal state after:
case a
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₂
⊢ (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk
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' O : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = (fun s ↦ (↑s).carrier) O
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = O

Tactic:
;

Goal state after:
case mk
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' O : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = (fun s ↦ (↑s).carrier) O
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = O
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }

Tactic:
;

Goal state after:
case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } = { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ toSubmodule✝¹ = toSubmodule✝

Tactic:
;

Goal state after:
case mk.mk
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
toSubmodule✝¹ : Submodule R M
lie_mem✝¹ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝¹.carrier → ⁅x, m⁆ ∈ toSubmodule✝¹.carrier
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h :
  (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝¹, lie_mem := lie_mem✝¹ } =
    (fun s ↦ (↑s).carrier) { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ }
⊢ toSubmodule✝¹ = toSubmodule✝
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, 0⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
;

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
N N' : LieSubmodule R L M
x : L
m : M
h : m ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, 0⁆ ∈ (Submodule.toAddSubmonoid 0).carrier
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk
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
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x : L} {m : M},
    m ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ ↑{ toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem := h } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }

Tactic:
;

Goal state after:
case mk
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
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  ∀ {x : L} {m : M},
    m ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier →
      ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }.carrier
⊢ ↑{ toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝, lie_mem := h } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case a
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
⊢ ⇑f '' ↑I ⊆ ↑(map f I)

Tactic:
;

Goal state after:
case a
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
⊢ ⇑f '' ↑I ⊆ ↑(map f I)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
      ⟨u + v, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
;

Goal state after:
case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
      ⟨u + v, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mk
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
y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y

Tactic:
;

Goal state after:
case mk
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
y : LieSubmodule R L M
toSubmodule✝ : Submodule R M
lie_mem✝ : ∀ {x : L} {m : M}, m ∈ toSubmodule✝.carrier → ⁅x, m⁆ ∈ toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = ↑y
⊢ { toSubmodule := toSubmodule✝, lie_mem := lie_mem✝ } = y