awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsLieAbelian L
ψ : Module.Dual R L
x y : L
rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw₂ : ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsLieAbelian L
ψ : Module.Dual R L
x y : L
rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
rw₂ : ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw₃ : ψ.toFun 0 = 0
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsLieAbelian L
ψ : Module.Dual R L
x y : L
rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
rw₂ : ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x
rw₃ : ψ.toFun 0 = 0
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw₄ : Eq.{u + 1} (α := R) ((ψ : (a : L) → R) 0 : R) (0 : R)
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsLieAbelian L
ψ : Module.Dual R L
x y : L
rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
rw₂ : ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x
rw₃ : ψ.toFun 0 = 0
rw₄ : Eq.{u + 1} (α := R) ((ψ : (a : L) → R) 0 : R) (0 : R)
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw₅ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)) =
    (singleSubSingle i k : (a : R) → ↥(sl n R)) r
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)) =
    (singleSubSingle j k : (a : R) → ↥(sl n R)) r
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)) =
    (singleSubSingle i j : (a : R) → ↥(sl n R)) r
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ¬IsLieAbelian ↥(sl n R)
have rcases : ∀ (i j : n) (hij : i ≠ j), ¬IsLieAbelian ↥(sl n R)
Tactic: rcases Fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
have rw : (↑A : Matrix n n R) * (↑B : Matrix n n R) - (↑B : Matrix n n R) * (↑A : Matrix n n R) = 0
Tactic: rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)
have rw₁ : (↑⁅A, B⁆ : Matrix n n R) = 0
Tactic: rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)
have rw₂ : Eq (α := Matrix n n R) (↑0 : Matrix n n R) 0
Tactic: rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (↑A : Matrix n n R) * (↑B : Matrix n n R) = (↑B : Matrix n n R) * (↑A : Matrix n n R)
have rw₃ : Eq (α := Matrix n n R) 0 0
Tactic: rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (hypothesis)
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)
⊢ False
have c' : (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
A : Matrix n n R
⊢ Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (so n R) A ↔ Aᵀ = -A
have rw : Matrix.IsSkewAdjoint 1 A ↔ Aᵀ = -A
Tactic: rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ Pso p q R i * Pso p q R (-i) = 1
have a : ∀ (x y : p ⊕ q), (Pso p q R i * Pso p q R (-i)) x y = 1 x y
Tactic: ext (x y)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y
have a : ∀ (x : p), (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y
Tactic: rcases x with ⟨x⟩ | ⟨x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y
have a₁ : ∀ (x : q), (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y
Tactic: rcases x with ⟨x⟩ | ⟨x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) y = 1 (Sum.inl x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) y = 1 (Sum.inr x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inl x) (Sum.inl y) = 1 (Sum.inl x) (Sum.inl y)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ (Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i = 1
have a : ∀ (x y : p ⊕ q), ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
Tactic: ext (x y)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
have 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
Tactic: rcases x with ⟨x⟩ | ⟨x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
have 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
Tactic: rcases x with ⟨x⟩ | ⟨x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) y = 1 (Sum.inl x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) y = 1 (Sum.inr x) y
have 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)
Tactic: rcases y with ⟨y⟩ | ⟨y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((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)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ ((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)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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
⊢ ((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)
have 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)
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ ((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)
have 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)
Tactic: by_cases h : x = y
-- 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
i : R
hi : i * i = -1
⊢ ↥(so' p q R) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)
have p₁ : ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)
Tactic: apply
    (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i)
        (invertiblePso p q R hi)).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
i : R
hi : i * i = -1
⊢ ↥(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)
have 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))
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
i : R
hi : i * i = -1
⊢ (↑(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))
have 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))
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
i : R
hi : i * i = -1
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))
have h : A ∈ (↑(skewAdjointMatricesLieSubalgebra 1) : 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
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)
⊢ (↑((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
have 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
Tactic: rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]
-- 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
⊢ S l R = fromBlocks 1 0 0 (-1)
have rw : S l R = diagonal (Sum.elim (fun (x : l) ↦ 1) fun (i : l) ↦ -1)
Tactic: rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]