awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1),
      HSMul.hSMul (β := M₁ ⊗[R] M₂) ((k₁ + k₂ - 1).choose x.1)
        ((f₁ ^ x.1 * f₂ ^ x.2 : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂))
    0
have h : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1),
  HSMul.hSMul (β := M₁ ⊗[R] M₂) ((k₁ + k₂ - 1).choose x.1)
      ((f₁ ^ x.1 * f₂ ^ x.2 : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) =
    0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
this :
  Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
⊢ HSMul.hSMul (β := M₁ ⊗[R] M₂) ((k₁ + k₂ - 1).choose (i, j).1)
      ((f₁ ^ (i, j).1 * f₂ ^ (i, j).2 : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) =
    0
have rw : HSMul.hSMul (β := M₁ ⊗[R] M₂) ((k₁ + k₂ - 1).choose (i, j).1) 0 = 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
⊢ HSMul.hSMul (β := M₁ ⊗[R] M₂) ((k₁ + k₂ - 1).choose (i, j).1)
      ((f₁ ^ (i, j).1 * f₂ ^ (i, j).2 : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) =
    0
have h : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
Tactic: suffices (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ m₂) = 0 by rw [this]; apply smul_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h : ∀ (hi : k₁ ≤ (i, j).1),
  Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
Tactic: rcases Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi | hj
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
h :
  ∀ (hi : k₁ ≤ (i, j).1),
    Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₁ : ∀ (hj : k₂ ≤ (i, j).2),
  Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
Tactic: rcases Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi | hj
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j * f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
Tactic: rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁,
      map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
h : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j * f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₁ : Eq (α := M₁ ⊗[R] M₂)
  ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
  (0 : M₁ ⊗[R] M₂)
Tactic: rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁,
      map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
h : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j * f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
h₁ :
  Eq (α := M₁ ⊗[R] M₂)
    ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
    (0 : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) 0) 0
Tactic: rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁,
      map_zero]