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 : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq' + 1 = data.deg pq''
⊢ n₃ = data.deg pq''

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₀
r : ℤ
hr : r₀ ≤ r
pq pq' pq'' : κ
hpq : (c r).Rel pq pq'
hpq' : (c r).Rel pq' pq''
n₀ n₁ n₂ n₃ n₄ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
hn₄ : n₃ + 1 = n₄
hn₂' : n₂ = data.deg pq'
this : data.deg pq' + 1 = data.deg pq''
⊢ n₃ = data.deg pq''
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'' : κ
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : ¬(c r).Rel pq' pq''
⊢ (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
        (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
      (page X data r hr).d pq' pq'' =
    0

Tactic:
rw [HomologicalComplex.shape _ _ _ h, comp_zero]

Goal state after:
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).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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''
this : data.deg pq' + 1 = data.deg pq''
⊢ n₂ = data.deg pq''

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₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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''
this : data.deg pq' + 1 = data.deg pq''
⊢ n₂ = data.deg pq''
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : IsArtinian R M
⊢ Surjective ⇑f

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : IsArtinian R M
⊢ Surjective ⇑f
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 0

Tactic:
;

Goal state after:
L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 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₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
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'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₀ = data.deg pq

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₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
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'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
this : data.deg pq + 1 = data.deg pq'
⊢ n₀ = data.deg pq
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x y z : L
m n✝ n : M
⊢ { toFun := fun m ↦ ⁅0, m⁆, map_zero' := ⋯, map_add' := ⋯ } n = 0 n

Tactic:
;

Goal state after:
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
t : R
x y z : L
m n✝ n : M
⊢ { toFun := fun m ↦ ⁅0, m⁆, map_zero' := ⋯, map_add' := ⋯ } n = 0 n
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x y✝ z✝ : L
m n✝ : M
y z : L
n : M
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
        { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ })
      n

Tactic:
;

Goal state after:
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
t : R
x y✝ z✝ : L
m n✝ : M
y z : L
n : M
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
        { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x✝ y✝ z : L
m✝ n✝ : M
x y : L
m : M →ₗ[R] R
n : M
⊢ { toFun := fun m_1 ↦ -m ⁅x + y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m_1 ↦ -m ⁅y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ })
      n

Tactic:
;

Goal state after:
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
t : R
x✝ y✝ z : L
m✝ n✝ : M
x y : L
m : M →ₗ[R] R
n : M
⊢ { toFun := fun m_1 ↦ -m ⁅x + y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m_1 ↦ -m ⁅y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x✝ y z : L
m✝ n✝ : M
x : L
m n : M →ₗ[R] R
p : M
⊢ { toFun := fun m_1 ↦ -(m + n) ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } p =
    ({ toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ -n ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      p

Tactic:
;

Goal state after:
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
t : R
x✝ y z : L
m✝ n✝ : M
x : L
m n : M →ₗ[R] R
p : M
⊢ { toFun := fun m_1 ↦ -(m + n) ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } p =
    ({ toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ -n ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      p
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x✝ y z : L
m✝ n✝ : M
x m : L
n : M →ₗ[R] R
p : M
⊢ { toFun := fun m_1 ↦ -{ toFun := fun m_2 ↦ -n ⁅m, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m_1⁆, map_add' := ⋯,
        map_smul' := ⋯ }
      p =
    ({ toFun := fun m_1 ↦ -n ⁅⁅x, m⁆, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m_1 ↦ -{ toFun := fun m ↦ -n ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅m, m_1⁆, map_add' := ⋯,
          map_smul' := ⋯ })
      p

Tactic:
;

Goal state after:
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
t : R
x✝ y z : L
m✝ n✝ : M
x m : L
n : M →ₗ[R] R
p : M
⊢ { toFun := fun m_1 ↦ -{ toFun := fun m_2 ↦ -n ⁅m, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m_1⁆, map_add' := ⋯,
        map_smul' := ⋯ }
      p =
    ({ toFun := fun m_1 ↦ -n ⁅⁅x, m⁆, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m_1 ↦ -{ toFun := fun m ↦ -n ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅m, m_1⁆, map_add' := ⋯,
          map_smul' := ⋯ })
      p
Module: Mathlib.Algebra.Lie.Basic

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
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅t • x, m⁆ n = (t • ⁅x, m⁆) n

Tactic:
;

Goal state after:
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
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅t • x, m⁆ n = (t • ⁅x, m⁆) n
Module: Mathlib.Algebra.Lie.Basic

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
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅x, t • m⁆ n = (t • ⁅x, m⁆) n

Tactic:
;

Goal state after:
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
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅x, t • m⁆ n = (t • ⁅x, m⁆) n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
y : L₁ →ₗ⁅R⁆ L₂
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h : (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = (fun f ↦ (↑f).toFun) y
⊢ { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = y

Tactic:
;

Goal state after:
case mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
y : L₁ →ₗ⁅R⁆ L₂
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h : (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = (fun f ↦ (↑f).toFun) y
⊢ { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ } = y
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h :
  (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } =
    (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h :
  (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } =
    (fun f ↦ (↑f).toFun) { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h : toLinearMap✝¹ = toLinearMap✝
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
toLinearMap✝¹ : L₁ →ₗ[R] L₂
map_lie'✝¹ : ∀ {x y : L₁}, toLinearMap✝¹.toFun ⁅x, y⁆ = ⁅toLinearMap✝¹.toFun x, toLinearMap✝¹.toFun y⁆
toLinearMap✝ : L₁ →ₗ[R] L₂
map_lie'✝ : ∀ {x y : L₁}, toLinearMap✝.toFun ⁅x, y⁆ = ⁅toLinearMap✝.toFun x, toLinearMap✝.toFun y⁆
h : toLinearMap✝¹ = toLinearMap✝
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
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✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
x✝² : L₁ →ₗ⁅R⁆ L₂
x✝¹ : R
x✝ : L₁
⊢ x✝² (x✝¹ • x✝) = (RingHom.id R) x✝¹ • x✝² x✝

Tactic:
rw [← coe_toLinearMap, map_smulₛₗ]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk
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₃
g : L₁ ≃ₗ⁅R⁆ L₂
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₁ :
  (↑{ toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toLieHom).toFun =
    (↑g.toLieHom).toFun
h₂ : { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = g.invFun
⊢ { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = g

Tactic:
;

Goal state after:
case mk
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₃
g : L₁ ≃ₗ⁅R⁆ L₂
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₁ :
  (↑{ toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toLieHom).toFun =
    (↑g.toLieHom).toFun
h₂ : { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = g.invFun
⊢ { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = g
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
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₃
toLieHom✝¹ : L₁ →ₗ⁅R⁆ L₂
invFun✝¹ : L₂ → L₁
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieHom✝¹).toFun
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₁ :
  (↑{ toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toLieHom).toFun =
    (↑{ toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toLieHom).toFun
h₂ :
  { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk.mk
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₃
toLieHom✝¹ : L₁ →ₗ⁅R⁆ L₂
invFun✝¹ : L₂ → L₁
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieHom✝¹).toFun
toLieHom✝ : L₁ →ₗ⁅R⁆ L₂
invFun✝ : L₂ → L₁
left_inv✝ : LeftInverse invFun✝ (↑toLieHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieHom✝).toFun
h₁ :
  (↑{ toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toLieHom).toFun =
    (↑{ toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toLieHom).toFun
h₂ :
  { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieHom := toLieHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieHom := toLieHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ x, M✝ (e x))

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ x, M✝ (e x))