awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (hypothesis)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
have hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
Tactic: have hs' : (F f).support ⊆ s := Finset.subset_union_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
have rw : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ s,
    HSMul.hSMul (β := R) x
      ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x)) :
              L →ₗ[R] R) :
            (a : L) → R)
          ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) x : L) :
        R))
  0
Tactic: rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ s,
      HSMul.hSMul (β := R) x
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) x : L) :
          R))
    0
have refine : Finset.map (Equiv.toEmbedding (Equiv.neg A)) s ⊆ s
Tactic: refine Function.Odd.finsetSum_eq_zero (fun n ↦ by simp [hΦ.eq]) (Finset.map_eq_of_subset ?_)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ s
have rw : Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
  Membership.mem (γ := Finset A)
    (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
    x
Tactic: rw [Finset.mem_union]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (hypothesis)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
have hx₁ : Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
  Membership.mem (γ := Finset A)
    (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
Tactic: replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx :
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
have inl : ∀
  (h :
    Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
      (-x)),
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
Tactic: obtain (h | h) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs :
  s =
    Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
      Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
hs' : Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ⊆ s
x : A
hx :
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) (-x) ∨
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)
inl :
  ∀
    (h :
      Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))
        (-x)),
    Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
      Membership.mem (γ := Finset A)
        (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
          (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
        x
⊢ Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
have inr : ∀
  (h :
    Membership.mem (γ := Finset A)
      (Finset.image Neg.neg (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))) (-x)),
  Membership.mem (γ := Finset A) (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)) x ∨
    Membership.mem (γ := Finset A)
      (Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
        (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f)))
      x
Tactic: obtain (h | h) := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
set set₁ :
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
have set₂ : let s : Finset A :=
  Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
    Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
      (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f));
∀
  (hs :
    s =
      Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f) ∪
        Finset.image (α := A) (⇑(Equiv.neg A) : (a : A) → A)
          (Finsupp.support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) f))),
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((F : (a : loopAlgebra R A L) → A →₀ L) f) fun (a : A) (v : L) ↦
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-a)) :
                L →ₗ[R] R) :
              (a : L) → R)
            v :
          R))
    0
Tactic: classical
    set s := (F f).support ∪ (F f).support.image (Equiv.neg A) with hs
    have hs' : (F f).support ⊆ s := Finset.subset_union_left
    rw [Finsupp.sum_of_support_subset _ hs' _ (by simp)]
    refine Function.Odd.finsetSum_eq_zero (fun n ↦ by simp [hΦ.eq]) (Finset.map_eq_of_subset ?_)
    intro x hx
    rw [Finset.mem_union]
    replace hx : -x ∈ (F f).support ∨ -x ∈ (F f).support.image Neg.neg := by simpa [hs] using hx
    obtain (h | h) := hx
    · exact Or.inr <| Finset.mem_image.mpr ⟨-x, by simp [h]⟩
    · exact Or.inl <| by simpa using h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
have pos : ∀ (h0 : a + b + c = 0),
  HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
Tactic: by_cases h0 : a + b + c = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
pos :
  ∀ (h0 : a + b + c = 0),
    HSMul.hSMul (β := R) b
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R)
            y :
          R) =
      HSMul.hSMul (β := R) c
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
              z :
            R) +
        HSMul.hSMul (β := R) a
          ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
              x :
            R)
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
have neg : ∀ (h0 : ¬a + b + c = 0),
  HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
Tactic: by_cases h0 : a + b + c = 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
have pos : HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
Tactic: suffices b • Φ ⁅x, z⁆ y = c • Φ ⁅x, y⁆ z + a • Φ ⁅y, z⁆ x by
        simpa only [show a + b = -c by grind, show a + c = -b by grind, show b + c = -a by grind,
          Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₁ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₂ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]