awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (hypothesis)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ (PD l R)ᵀ * JD l R * PD l R = HSMul.hSMul (α := R) 2 (S l R)
have h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
Tactic: have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
    simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = HSMul.hSMul (α := R) 2 (S l R)
have rw : fromBlocks (HMul.hMul (α := Matrix l l R) 1 1 + HMul.hMul (α := Matrix l l R) 1 1)
    (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 1 1)
    (HMul.hMul (α := Matrix l l R) 1 1 + HMul.hMul (α := Matrix l l R) (-1) 1)
    (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) (-1) 1) =
  fromBlocks (HSMul.hSMul (α := R) (β := Matrix l l R) 2 1) (HSMul.hSMul (α := R) (β := Matrix l l R) 2 0)
    (HSMul.hSMul (α := R) (β := Matrix l l R) 2 0) (HSMul.hSMul (α := R) (β := Matrix l l R) 2 (-1))
Tactic: rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
⊢ PD l R * HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (PD l R)ᵀ = 1
have rw : fromBlocks
    (1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ +
      -1 *
        HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-1)ᵀ)
    (1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ +
      -1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ)
    (1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ +
      1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-1)ᵀ)
    (1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ +
      1 * HSMul.hSMul (α := R) (β := Matrix l l R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 1ᵀ) =
  1
Tactic: rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
    Matrix.fromBlocks_multiply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)
have apply : ↥(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) ≃ₗ⁅R⁆ ↥(so' l l R)
Tactic: apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ ↥(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) ≃ₗ⁅R⁆ ↥(so' l l R)
have h : (↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) : Set (Matrix (l ⊕ l) (l ⊕ l) R)) =
  (↑(so' l l R) : Set (Matrix (l ⊕ l) (l ⊕ l) R))
Tactic: apply LieEquiv.ofEq
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
⊢ (↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) : Set (Matrix (l ⊕ l) (l ⊕ l) R)) =
    (↑(so' l l R) : Set (Matrix (l ⊕ l) (l ⊕ l) R))
have h : ∀ (A : Matrix.{u_4, u_4, u₂} (l ⊕ l) (l ⊕ l) R),
  A ∈ (↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) : Set (Matrix (l ⊕ l) (l ⊕ l) R)) ↔
    A ∈ (↑(so' l l R) : Set (Matrix (l ⊕ l) (l ⊕ l) R))
Tactic: ext A
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype p
inst_6 : Fintype q
inst_7 : Fintype l
inst_8 : Invertible (α := R) 2
A : Matrix.{u_4, u_4, u₂} (l ⊕ l) (l ⊕ l) R
⊢ A ∈ (↑(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) : Set (Matrix (l ⊕ l) (l ⊕ l) R)) ↔
    A ∈ (↑(so' l l R) : Set (Matrix (l ⊕ l) (l ⊕ l) R))
have h : Membership.mem (γ := LieSubalgebra R (Matrix.{u_4, u_4, u₂} (l ⊕ l) (l ⊕ l) R))
    (skewAdjointMatricesLieSubalgebra (S l R)) A ↔
  A ∈ (↑(so' l l R) : Set (Matrix (l ⊕ l) (l ⊕ l) R))
Tactic: rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    mem_skewAdjointMatricesLieSubalgebra_unit_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
⊢ PB l R * fromBlocks 1 0 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (PD l R) _) = 1
have rw : fromBlocks (HMul.hMul (α := Matrix Unit Unit R) 1 1 + HMul.hMul (α := Matrix.{0, u_4, u₂} Unit (l ⊕ l) R) 0 0)
    (HMul.hMul (α := Matrix Unit Unit R) 1 0 + 0 * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (PD l R) _)
    (HMul.hMul (α := Matrix.{u_4, 0, u₂} (l ⊕ l) Unit R) 0 1 + PD l R * 0)
    (HMul.hMul (α := Matrix.{u_4, 0, u₂} (l ⊕ l) Unit R) 0 0 + 1) =
  1
Tactic: rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a : indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
  (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
      (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
    (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₁ : ∀ (j₃ : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₂ : ∀ (val : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
a₂ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₃ : ∀ (i₃ : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
a₂ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
a₃ :
  ∀ (i₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₄ : ∀ (i₃ j₃ : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
a₂ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
a₃ :
  ∀ (i₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
a₄ :
  ∀ (i₃ j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₅ : ∀ (i₃ val : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inr val)
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
a₂ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
a₃ :
  ∀ (i₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
a₄ :
  ∀ (i₃ j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))
a₅ :
  ∀ (i₃ val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inr val)
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₆ : ∀ (val : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
have a : Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inl j₃))
Tactic: simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
      Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
      Sum.elim_inl, if_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
      Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr, Sum.inl_injective.eq_iff,
      Sum.inr_injective.eq_iff, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
have a : Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inr val))
Tactic: simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
      Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
      Sum.elim_inl, if_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
      Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr, Sum.inl_injective.eq_iff,
      Sum.inr_injective.eq_iff, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
i₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
have a : Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inl i₃) PUnit.unit)
Tactic: simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
      Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
      Sum.elim_inl, if_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
      Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr, Sum.inl_injective.eq_iff,
      Sum.inr_injective.eq_iff, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit))
have a : Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inr val) PUnit.unit)
Tactic: simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
      Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
      Sum.elim_inl, if_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
      Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.elim_inr, Sum.inl_injective.eq_iff,
      Sum.inr_injective.eq_iff, reduceCtorEq]