awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
a :
  (↑(HAdd.hAdd (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle i k : (a : R) → ↥(sl n R)) r) : Matrix n n R)
⊢ HAdd.hAdd (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R))
      ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R)) =
    (singleSubSingle i k : (a : R) → ↥(sl n R)) r

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
⊢ (↑(HAdd.hAdd (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle i k : (a : R) → ↥(sl n R)) r) : Matrix n n R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
a :
  (↑(HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle j k : (a : R) → ↥(sl n R)) r) : Matrix n n R)
⊢ HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
      ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R)) =
    (singleSubSingle j k : (a : R) → ↥(sl n R)) r

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
⊢ (↑(HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle i j : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle j k : (a : R) → ↥(sl n R)) r) : Matrix n n R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
a :
  (↑(HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle i j : (a : R) → ↥(sl n R)) r) : Matrix n n R)
⊢ HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
      ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R)) =
    (singleSubSingle i j : (a : R) → ↥(sl n R)) r

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j k : n
r : R
⊢ (↑(HSub.hSub (α := ↥(sl n R)) (β := ↥(sl n R)) ((singleSubSingle i k : (a : R) → ↥(sl n R)) r : ↥(sl n R))
          ((singleSubSingle j k : (a : R) → ↥(sl n R)) r : ↥(sl n R))) :
      Matrix n n R) =
    (↑((singleSubSingle i j : (a : R) → ↥(sl n R)) r) : Matrix n n R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
inst_3 : Nontrivial R
h : 1 < Fintype.card n
rcases : ∀ (i j : n) (hij : i ≠ j), ¬IsLieAbelian ↥(sl n R)
⊢ ¬IsLieAbelian ↥(sl n R)

Tactic:
rcases Fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩

Premises used: Fintype.exists_pair_of_one_lt_card
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
inst_3 : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij : (a : R) → ↥(sl n R)) 1
B : ↥(sl n R) := (single j i ⋯ : (a : R) → ↥(sl n R)) 1
c : IsLieAbelian ↥(sl n R)
rw : (↑A : Matrix n n R) * (↑B : Matrix n n R) - (↑B : Matrix n n R) * (↑A : Matrix n n R) = 0
rw₁ : (↑⁅A, B⁆ : Matrix n n R) = 0
rw₂ : Eq (α := Matrix n n R) (↑0 : Matrix n n R) 0
rw₃ rw₄ : Eq (α := Matrix n n R) 0 0
⊢ (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)

Tactic:
rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]

Premises used: sub_eq_zero, LieAlgebra.SpecialLinear.sl_bracket, ZeroMemClass.coe_zero, LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
inst_3 : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij : (a : R) → ↥(sl n R)) 1
B : ↥(sl n R) := (single j i ⋯ : (a : R) → ↥(sl n R)) 1
c : IsLieAbelian ↥(sl n R)
⊢ (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)

Tactic:
have c' : A.val * B.val = B.val * A.val := by
    rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
inst_3 : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij : (a : R) → ↥(sl n R)) 1
B : ↥(sl n R) := (single j i ⋯ : (a : R) → ↥(sl n R)) 1
c : IsLieAbelian ↥(sl n R)
c' : (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)
⊢ False

Tactic:
simpa [A, B, Matrix.single, Matrix.mul_apply, hij.symm] using congr_fun (congr_fun c' i) i

Premises used: Matrix.mul_apply, Ne.symm, congr_fun, Matrix.single
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
A : Matrix n n R
rw : Matrix.IsSkewAdjoint 1 A ↔ Aᵀ = -A
⊢ Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (so n R) A ↔ Aᵀ = -A

Tactic:
rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]

Premises used: mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule, LieAlgebra.Orthogonal.so
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
A : Matrix n n R
⊢ Matrix.IsSkewAdjoint 1 A ↔ Aᵀ = -A

Tactic:
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]

Premises used: Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
a : ∀ (x y : p ⊕ q), (Pso p q R i * Pso p q R (-i)) x y = 1 x y
⊢ Pso p q R i * Pso p q R (-i) = 1

Tactic:
ext (x y)
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
a : ∀ (x : p), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y
a₁ : ∀ (x : q), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y

Tactic:
rcases x with ⟨x⟩ | ⟨x⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
a : ∀ (y : p), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
a₁ : ∀ (y : q), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inr y) = 1 (Sum.inl x) (Sum.inr y)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y

Tactic:
rcases y with ⟨y⟩ | ⟨y⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
a : ∀ (y : p), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inl y) = 1 (Sum.inr x) (Sum.inl y)
a₁ : ∀ (y : q), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y

Tactic:
rcases y with ⟨y⟩ | ⟨y⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
pos : ∀ (h : x = y), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
neg : ∀ (h : ¬x = y), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
by_cases h : x = y
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, h, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, h, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x : p
y : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inr y) = 1 (Sum.inl x) (Sum.inr y)

Tactic:
simp [Pso]

Premises used: LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x : q
y : p
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inl y) = 1 (Sum.inr x) (Sum.inl y)

Tactic:
simp [Pso]

Premises used: LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
pos : ∀ (h : x = y), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
neg : ∀ (h : ¬x = y), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
by_cases h : x = y
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, h, hi, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, h, hi, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
a : ∀ (x y : p ⊕ q), ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
⊢ (Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i = 1

Tactic:
ext (x y)
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
a : ∀ (x : p), ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y
a₁ : ∀ (x : q), ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y

Tactic:
rcases x with ⟨x⟩ | ⟨x⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : p
a :
  ∀ (y : p),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
a₁ :
  ∀ (y : q),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inr y) = 1 (Sum.inl x) (Sum.inr y)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y

Tactic:
rcases y with ⟨y⟩ | ⟨y⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
y : p ⊕ q
x : q
a :
  ∀ (y : p),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inl y) = 1 (Sum.inr x) (Sum.inl y)
a₁ :
  ∀ (y : q),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y

Tactic:
rcases y with ⟨y⟩ | ⟨y⟩
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
pos :
  ∀ (h : x = y),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
neg :
  ∀ (h : ¬x = y),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
by_cases h : x = y
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal, h, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : p
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal, h, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x : p
y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inr y) = 1 (Sum.inl x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal]

Premises used: LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x : q
y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inl y) = 1 (Sum.inr x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal]

Premises used: LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
pos :
  ∀ (h : x = y),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
neg :
  ∀ (h : ¬x = y),
    ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
by_cases h : x = y
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal, h, hi, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal, h, hi, one_apply]

Premises used: Matrix.one_apply, LieAlgebra.Orthogonal.indefiniteDiagonal, LieAlgebra.Orthogonal.Pso
-- 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
i : R
hi : i * i = -1
p₁ : ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)
⊢ ↥(so' p q R) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)

Tactic:
apply
    (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i)
        (invertiblePso p q R hi)).trans

Premises used: LieAlgebra.Orthogonal.invertiblePso, skewAdjointMatricesLieSubalgebraEquiv, LieAlgebra.Orthogonal.indefiniteDiagonal, LieEquiv.trans, LieAlgebra.Orthogonal.Pso
-- 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
i : R
hi : i * i = -1
h :
  (↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) :
      Set (Matrix (p ⊕ q) (p ⊕ q) R)) =
    (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) R))
⊢ ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) 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
i : R
hi : i * i = -1
h :
  ∀ (A : Matrix (p ⊕ q) (p ⊕ q) R),
    A ∈
        (↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) :
          Set (Matrix (p ⊕ q) (p ⊕ q) R)) ↔
      A ∈ (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) R))
⊢ (↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) :
      Set (Matrix (p ⊕ q) (p ⊕ q) R)) =
    (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) 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
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
h :
  A ∈ (↑(skewAdjointMatricesLieSubalgebra 1) : Set (Matrix (p ⊕ q) (p ⊕ q) R)) ↔
    A ∈ (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) R))
⊢ A ∈
      (↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) :
        Set (Matrix (p ⊕ q) (p ⊕ q) R)) ↔
    A ∈ (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) R))

Tactic:
rw [indefiniteDiagonal_transform p q R hi]

Premises used: LieAlgebra.Orthogonal.indefiniteDiagonal_transform
-- 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
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ (↑(skewAdjointMatricesLieSubalgebra 1) : Set (Matrix (p ⊕ q) (p ⊕ q) R)) ↔
    A ∈ (↑(so (p ⊕ q) R) : Set (Matrix (p ⊕ q) (p ⊕ q) R))

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
rw :
  (↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi) :
            (a : ↥(so' p q R)) →
              ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)))
          A) :
      Matrix (p ⊕ q) (p ⊕ q) R) =
    (Pso p q R i)⁻¹ * (↑A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i
⊢ (↑((soIndefiniteEquiv p q R hi : (a : ↥(so' p q R)) → ↥(so (p ⊕ q) R)) A) : Matrix (p ⊕ q) (p ⊕ q) R) =
    (Pso p q R i)⁻¹ * (↑A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i

Tactic:
rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]

Premises used: LieEquiv.ofEq_apply, LieEquiv.trans_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
p : Type u_2
q : Type u_3
R : Type u₂
inst : DecidableEq p
inst_1 : DecidableEq q
inst_2 : CommRing R
inst_3 : Fintype p
inst_4 : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ (↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi) :
            (a : ↥(so' p q R)) →
              ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)))
          A) :
      Matrix (p ⊕ q) (p ⊕ q) R) =
    (Pso p q R i)⁻¹ * (↑A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i

Tactic:
simp only [so', skewAdjointMatricesLieSubalgebraEquiv_apply]

Premises used: LieAlgebra.Orthogonal.so', skewAdjointMatricesLieSubalgebraEquiv_apply
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
rw : S l R = diagonal (Sum.elim (fun (x : l) ↦ 1) fun (i : l) ↦ -1)
⊢ S l R = fromBlocks 1 0 0 (-1)

Tactic:
rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]

Premises used: Matrix.fromBlocks_diagonal, Matrix.diagonal_one, Matrix.diagonal_neg
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
⊢ S l R = diagonal (Sum.elim (fun (x : l) ↦ 1) fun (i : l) ↦ -1)

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
⊢ (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)

Tactic:
simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]

Premises used: LieAlgebra.Orthogonal.JD, Matrix.fromBlocks_transpose, LieAlgebra.Orthogonal.PD, Matrix.fromBlocks_multiply