awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤
h : Subsingleton L
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have h : Nontrivial.{u_3} ↥(weightSpace V (⇑0 : (a : L) → k))
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤
h : Nontrivial L
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have H₁ : Eq (α := LieSubmodule k L L) (derivedSeries k L 1) ⊤
Tactic: rw [LieSubmodule.toSubmodule_eq_top] at H
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have lift : ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A
Tactic: lift A to LieIdeal k L
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A
lift : ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have inr : ∀ (A : LieSubmodule k L L) (hA : IsCoatom (↑A : Submodule k L))
  (hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)),
  ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: lift A to LieIdeal k L
Cleared hypotheses: A, hA, hAL
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
A : LieSubmodule k L L
hA : IsCoatom (↑A : Submodule k L)
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have inr : ∀ (χ' : Module.Dual.{u_1, u_4} k ↥A),
  Nontrivial.{u_3} ↥(weightSpace V (⇑χ' : (a : ↥A) → k)) →
    ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: obtain ⟨χ', _⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite A
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have have : ∀ (χ : Module.Dual.{u_1, u_3} k ↥imL) (h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))),
  ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have h₁ : Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
Tactic: use χ.comp toEndo
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
have h₁ : ∀ (v : V) (hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v)
  (hv0 :
    Subtype.mk (p := fun (x : V) ↦
        Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x) v hv ≠
      0),
  Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
Tactic: obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
have h₁ : Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) v
Tactic: refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
h₁ : Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) v
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
have h₂ : Ne (α := ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)))
  (Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) x) v sorry)
  0
Tactic: refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
⊢ Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) v
have h₁ : ∀ (hv_1 : ∀ (x : ↥imL), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ : (a : ↥imL) → k) x : k) v)
  (hv0 :
    Subtype.mk (p := fun (x : V) ↦
        Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x) v hv ≠
      0)
  (x : L), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ ∘ₗ toEndo : (a : L) → k) x : k) v
Tactic: rw [mem_weightSpace] at hv ⊢
Cleared hypotheses: hv0
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
    HAdd.hAdd (α := R)
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) x) 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))
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
have hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
Tactic: have hu₁ : (F x).support ⊆ u := Finset.subset_union_left
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
    HAdd.hAdd (α := R)
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) x) 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))
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
have hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
Tactic: have hu₂ : (F y).support ⊆ u := Finset.subset_union_right
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
a : A
ha : Membership.mem (γ := Finset A) (support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y))) a
⊢ a ∈ u
have ha₁ : HAdd.hAdd (α := L) (β := L) ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) a : L)
    ((((F : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) : (a : A) → L) a : L) ≠
  0
Tactic: replace ha : F x a + F y a ≠ 0 := by simpa using ha
Cleared hypotheses: ha
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) 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)) =
    HAdd.hAdd (α := R)
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) x) 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))
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) y) 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))
have hu₃ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) ⊆ u
Tactic: have hu₃ : (F (x + y)).support ⊆ u := fun a ha ↦ by
          replace ha : F x a + F y a ≠ 0 := by simpa using ha
          grind
-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
r : R
x : loopAlgebra R A L
⊢ (sum ((F : (a : loopAlgebra R A L) → A →₀ L) (r • x)) 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)) =
    HSMul.hSMul (α := R) (β := R) ((RingHom.id R : (a : R) → R) r : R)
      (sum ((F : (a : loopAlgebra R A L) → A →₀ L) x) 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))
have rw : Eq.{u_1 + 1} (α := R)
  (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
    HSMul.hSMul (β := R) x_1
      ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
              L →ₗ[R] R) :
            (a : L) → R)
          ((HSMul.hSMul (β := A →₀ L) r ((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
        R))
  (∑ x_1 ∈ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x),
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (HSMul.hSMul (β := R) x_1
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-x_1)) :
                L →ₗ[R] R) :
              (a : L) → R)
            ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) x_1 : L) :
          R)))
Tactic: rw [map_smul, sum_of_support_subset _ support_smul _ (by simp), sum, Finset.smul_sum]
-- 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
⊢ Membership.mem (γ :=
    Submodule R (loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))
    (Cohomology.twoCochain R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))
    (LinearMap.compr₂ (residuePairing R A L Φ)
      (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
        R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R))
have refine : ∀ (f : loopAlgebra R A L),
  Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((LinearMap.compr₂ (residuePairing R A L Φ)
                  (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
                    R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
              f :
            loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
        f :
      TrivialLieModule R (loopAlgebra R A L) R)
    (0 : TrivialLieModule R (loopAlgebra R A L) R)
Tactic: refine Cohomology.mem_twoCochain_iff.mpr fun f ↦ ?_
-- 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
⊢ Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((LinearMap.compr₂ (residuePairing R A L Φ)
                  (↑(LinearEquiv.symm (TrivialLieModule.equiv R (loopAlgebra R A L) R)) :
                    R →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                (a : loopAlgebra R A L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
              f :
            loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
          (a : loopAlgebra R A L) → TrivialLieModule R (loopAlgebra R A L) R)
        f :
      TrivialLieModule R (loopAlgebra R A L) R)
    (0 : TrivialLieModule R (loopAlgebra R A L) R)
have suffices : 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: suffices ((F f).sum fun a v ↦ a • Φ (F f (-a)) v) = 0 by simpa
-- 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
⊢ 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 : 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));
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))
Tactic: set s := (F f).support ∪ (F f).support.image (Equiv.neg A) with hs