case refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ⁅0, a • y⁆ = a • ⁅0, y⁆

case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L), ⁅x ⊗ₜ[R] y_1, a • y⁆ = a • ⁅x ⊗ₜ[R] y_1, y⁆

case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L), ⁅x, a • y⁆ = a • ⁅x, y⁆ → ⁅y_1, a • y⁆ = a • ⁅y_1, y⁆ → ⁅x + y_1, a • y⁆ = a • ⁅x + y_1, y⁆
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ⁅x, a • y⁆ = a • ⁅x, y⁆
refine' x.induction_on _ _ _
no goals
case refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ⁅0, a • y⁆ = a • ⁅0, y⁆
simp only [zero_lie, smul_zero]
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, y⁆
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L), ⁅x ⊗ₜ[R] y_1, a • y⁆ = a • ⁅x ⊗ₜ[R] y_1, y⁆
intro a₁ l₁
case refine'_2.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • 0⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, 0⁆

case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L), ⁅a₁ ⊗ₜ[R] l₁, a • x ⊗ₜ[R] y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x ⊗ₜ[R] y⁆

case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ⁅a₁ ⊗ₜ[R] l₁, a • x⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x⁆ →
      ⁅a₁ ⊗ₜ[R] l₁, a • y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, y⁆ → ⁅a₁ ⊗ₜ[R] l₁, a • (x + y)⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x + y⁆
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, y⁆
refine' y.induction_on _ _ _
no goals
case refine'_2.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • 0⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, 0⁆
simp only [lie_zero, smul_zero]
case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • a₂ ⊗ₜ[R] l₂⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, a₂ ⊗ₜ[R] l₂⁆
case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L), ⁅a₁ ⊗ₜ[R] l₁, a • x ⊗ₜ[R] y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x ⊗ₜ[R] y⁆
intro a₂ l₂
no goals
case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • a₂ ⊗ₜ[R] l₂⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, a₂ ⊗ₜ[R] l₂⁆
simp only [bracket_def, bracket', TensorProduct.smul_tmul', mul_left_comm a₁ a a₂,
  TensorProduct.curry_apply, LinearMap.mul'_apply, Algebra.id.smul_eq_mul,
  Function.comp_apply, LinearEquiv.coe_coe, LinearMap.coe_comp, TensorProduct.map_tmul,
  TensorProduct.tensorTensorTensorComm_tmul]
case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
z₁ z₂ : A ⊗[R] L
h₁ : ⁅a₁ ⊗ₜ[R] l₁, a • z₁⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₁⁆
h₂ : ⁅a₁ ⊗ₜ[R] l₁, a • z₂⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₂⁆
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • (z₁ + z₂)⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₁ + z₂⁆
case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ⁅a₁ ⊗ₜ[R] l₁, a • x⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x⁆ →
      ⁅a₁ ⊗ₜ[R] l₁, a • y⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, y⁆ → ⁅a₁ ⊗ₜ[R] l₁, a • (x + y)⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, x + y⁆
intro z₁ z₂ h₁ h₂
no goals
case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
a₁ : A
l₁ : L
z₁ z₂ : A ⊗[R] L
h₁ : ⁅a₁ ⊗ₜ[R] l₁, a • z₁⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₁⁆
h₂ : ⁅a₁ ⊗ₜ[R] l₁, a • z₂⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₂⁆
⊢ ⁅a₁ ⊗ₜ[R] l₁, a • (z₁ + z₂)⁆ = a • ⁅a₁ ⊗ₜ[R] l₁, z₁ + z₂⁆
simp only [h₁, h₂, smul_add, lie_add]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y z₁ z₂ : A ⊗[R] L
h₁ : ⁅z₁, a • y⁆ = a • ⁅z₁, y⁆
h₂ : ⁅z₂, a • y⁆ = a • ⁅z₂, y⁆
⊢ ⁅z₁ + z₂, a • y⁆ = a • ⁅z₁ + z₂, y⁆
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L), ⁅x, a • y⁆ = a • ⁅x, y⁆ → ⁅y_1, a • y⁆ = a • ⁅y_1, y⁆ → ⁅x + y_1, a • y⁆ = a • ⁅x + y_1, y⁆
intro z₁ z₂ h₁ h₂
no goals
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
a : A
x y z₁ z₂ : A ⊗[R] L
h₁ : ⁅z₁, a • y⁆ = a • ⁅z₁, y⁆
h₂ : ⁅z₂, a • y⁆ = a • ⁅z₂, y⁆
⊢ ⁅z₁ + z₂, a • y⁆ = a • ⁅z₁ + z₂, y⁆
simp only [h₁, h₂, smul_add, add_lie]