mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ : invFun✝¹ = invFun✝
h₁ : toLieHom✝¹ = toLieHom✝
⊢ { 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₂ : invFun✝¹ = invFun✝
h₁ : toLieHom✝¹ = toLieHom✝
⊢ { 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.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h : Bijective ⇑f
x y : L₁
⊢ f ⁅x, y⁆ = ⁅f x, f y⁆

Tactic:
;

Goal state after:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h : Bijective ⇑f
x y : L₁
⊢ f ⁅x, y⁆ = ⁅f x, f y⁆
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
y : M →ₗ⁅R,L⁆ N
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
y : M →ₗ⁅R,L⁆ N
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLinearMap✝¹ : M →ₗ[R] N
map_lie'✝¹ : ∀ {x : L} {m : M}, toLinearMap✝¹.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝¹.toFun m⁆
toLinearMap✝ : M →ₗ[R] N
map_lie'✝ : ∀ {x : L} {m : M}, toLinearMap✝.toFun ⁅x, m⁆ = ⁅x, toLinearMap✝.toFun m⁆
h : toLinearMap✝¹ = toLinearMap✝
⊢ { toLinearMap := toLinearMap✝¹, map_lie' := map_lie'✝¹ } = { toLinearMap := toLinearMap✝, map_lie' := map_lie'✝ }
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 ι
M✝ : PEmpty.{u_5 + 1} → Submodule R P
inst✝ : ∀ (i : PEmpty.{u_5 + 1}), 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 ι
M✝ : PEmpty.{u_5 + 1} → Submodule R P
inst✝ : ∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)
Module: Mathlib.Algebra.Lie.Basic

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

Tactic:
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 ι
M✝ : PEmpty.{u_5 + 1} → Submodule R P
inst✝ : ∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥⊥

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 ι
M✝ : PEmpty.{u_5 + 1} → Submodule R P
inst✝ : ∀ (i : PEmpty.{u_5 + 1}), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥⊥
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
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R P
inst✝ : ∀ (i : Option α✝), 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
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R P
inst✝ : ∀ (i : Option α✝), 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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
g : M ≃ₗ⁅R,L⁆ N
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝,
            right_inv := right_inv✝ }.toLieModuleHom).toFun =
    (↑g.toLieModuleHom).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun =
    g.invFun
⊢ { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
g : M ≃ₗ⁅R,L⁆ N
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝,
            right_inv := right_inv✝ }.toLieModuleHom).toFun =
    (↑g.toLieModuleHom).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun =
    g.invFun
⊢ { toLieModuleHom := toLieModuleHom✝, 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
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
            right_inv := right_inv✝¹ }.toLieModuleHom).toFun =
    (↑{ toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝,
            right_inv := right_inv✝ }.toLieModuleHom).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
            right_inv := right_inv✝¹ }.toLieModuleHom).toFun =
    (↑{ toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝,
            right_inv := right_inv✝ }.toLieModuleHom).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, 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
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R P
inst✝ : ∀ (i : Option α✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(M✝ none ⊔ ⨆ b, M✝ (some b))

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
inst✝¹ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R P
inst✝ : ∀ (i : Option α✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(M✝ none ⊔ ⨆ b, M✝ (some b))
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: case mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₂ : invFun✝¹ = invFun✝
h₁ : toLieModuleHom✝¹ = toLieModuleHom✝
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
toLieModuleHom✝¹ : M →ₗ⁅R,L⁆ N
invFun✝¹ : N → M
left_inv✝¹ : LeftInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
right_inv✝¹ : RightInverse invFun✝¹ (↑toLieModuleHom✝¹).toFun
toLieModuleHom✝ : M →ₗ⁅R,L⁆ N
invFun✝ : N → M
left_inv✝ : LeftInverse invFun✝ (↑toLieModuleHom✝).toFun
right_inv✝ : RightInverse invFun✝ (↑toLieModuleHom✝).toFun
h₂ : invFun✝¹ = invFun✝
h₁ : toLieModuleHom✝¹ = toLieModuleHom✝
⊢ { toLieModuleHom := toLieModuleHom✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toLieModuleHom := toLieModuleHom✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
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'
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).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'
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✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : Module.Finite R ↥N
⊢ IsArtinian R ↥N

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : Module.Finite R ↥N
⊢ IsArtinian R ↥N
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ R⁰
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsRight R

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsRight R
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsRightRegular x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsRightRegular x✝
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsLeft R

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ x✝ ∈ nonZeroDivisorsLeft R
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsLeftRegular x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsLeftRegular x✝
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ Jac ^ (n + 1) = Jac ^ n

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ Jac ^ (n + 1) = Jac ^ n
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := ⋯
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
⊢ Ring.jacobson R ^ n = 0

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := ⋯
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
⊢ Ring.jacobson R ^ n = 0
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ (LinearMap.toSpanSingleton R R x).range

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ (LinearMap.toSpanSingleton R R x).range