awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Classical
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 = 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]
-- Module: Mathlib.Algebra.Lie.Classical
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)
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))
⊢ (PD l R)ᵀ * JD l R * PD l R = HSMul.hSMul (α := R) 2 (S l R)

Tactic:
rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]

Premises used: LieAlgebra.Orthogonal.s_as_blocks, LieAlgebra.Orthogonal.PD, Matrix.fromBlocks_smul, Matrix.fromBlocks_multiply
-- Module: Mathlib.Algebra.Lie.Classical
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)
⊢ 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:
simp [two_smul]

Premises used: two_smul
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
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
⊢ PD l R * HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (PD l R)ᵀ = 1

Tactic:
rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
    Matrix.fromBlocks_multiply]

Premises used: Matrix.fromBlocks_transpose, LieAlgebra.Orthogonal.PD, Matrix.fromBlocks_smul, Matrix.fromBlocks_multiply
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
⊢ 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:
simp
-- Module: Mathlib.Algebra.Lie.Classical
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
⊢ Invertible (PD l R)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Classical
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
apply : ↥(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) ≃ₗ⁅R⁆ ↥(so' l l R)
⊢ ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)

Tactic:
apply (skewAdjointMatricesLieSubalgebraEquiv (JD l R) (PD l R) (by infer_instance)).trans

Premises used: skewAdjointMatricesLieSubalgebraEquiv, LieAlgebra.Orthogonal.JD, LieAlgebra.Orthogonal.PD, LieEquiv.trans
-- Module: Mathlib.Algebra.Lie.Classical
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
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))
⊢ ↥(skewAdjointMatricesLieSubalgebra ((PD l R)ᵀ * JD l R * PD l R)) ≃ₗ⁅R⁆ ↥(so' l l R)

Tactic:
apply LieEquiv.ofEq

Premises used: LieEquiv.ofEq
-- Module: Mathlib.Algebra.Lie.Classical
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
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))
⊢ (↑(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:
ext A
-- Module: Mathlib.Algebra.Lie.Classical
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
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))
⊢ 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:
rw [jd_transform, ← val_unitOfInvertible (2 : R), ← Units.smul_def, LieSubalgebra.mem_coe,
    mem_skewAdjointMatricesLieSubalgebra_unit_smul]

Premises used: mem_skewAdjointMatricesLieSubalgebra_unit_smul, Units.smul_def, LieAlgebra.Orthogonal.jd_transform, val_unitOfInvertible, LieSubalgebra.mem_coe, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Classical
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
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
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
⊢ PB l R * fromBlocks 1 0 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (PD l R) _) = 1

Tactic:
rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]

Premises used: mul_invOf_self, Matrix.fromBlocks_multiply, LieAlgebra.Orthogonal.PB
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
inst_3 : Invertible (α := R) 2
⊢ 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:
simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero,
    Matrix.fromBlocks_one]

Premises used: Matrix.mul_zero, zero_add, Matrix.fromBlocks_one, Matrix.zero_mul, Matrix.mul_one, add_zero
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ (PB l R)ᵀ * JB l R * PB l R =
    HSMul.hSMul (α := R) (β := Matrix.{u_4, u_4, u₂} (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) 2 (fromBlocks 1 0 0 (S l R))

Tactic:
simp [PB, JB, jd_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply,
    Matrix.fromBlocks_smul]

Premises used: Matrix.fromBlocks_transpose, LieAlgebra.Orthogonal.jd_transform, Matrix.fromBlocks_smul, Matrix.fromBlocks_multiply, LieAlgebra.Orthogonal.PB, LieAlgebra.Orthogonal.JB
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ 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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
j₃ : l
a : Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inl j₃))
⊢ 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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
a : Eq.{u₂ + 1} (α := R) 0 (0 PUnit.unit (Sum.inr val))
⊢ 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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
i₃ : l
a : Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inl i₃) PUnit.unit)
⊢ 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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val : l
a : Eq.{u₂ + 1} (α := R) 0 (0 (Sum.inr val) PUnit.unit)
⊢ 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:
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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
val j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (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.inr val) (Sum.inl (Sum.inr 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]

Premises used: Matrix.fromBlocks_apply₁₁, reduceCtorEq, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr, Sum.inr_injective, if_true, Sum.inl_injective, if_false, Equiv.sumAssoc_apply_inl_inl, Function.Injective.eq_iff, Matrix.reindex_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, Equiv.symm_symm, Matrix.fromBlocks_apply₂₁, Matrix.reindexLieEquiv_apply, Equiv.sumAssoc_apply_inl_inr, Sum.elim_inr, Matrix.diagonal_apply, Sum.elim_inl, Matrix.submatrix_apply, Matrix.one_apply_eq