awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
x : L'
⊢ (∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x) ↔
    ∃ (a : L),
      Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x} a ∧
        ((↑f : L →ₗ[R] L') : (a : L) → L') a = x
have e_p : (∃ (a : L'),
    ((∃ (x : L), (f : (a : L) → L') x = a) ∧ a ∈ J₁) ∧
      ∃ (a_1 : L'), ((∃ (x : L), (f : (a : L) → L') x = a_1) ∧ a_1 ∈ J₂) ∧ ⁅a, a_1⁆ = x) ↔
  ∃ (a : L),
    Membership.mem (α := L') J₁ ((f : (a : L) → L') a : L') ∧
      ∃ (b : L),
        Membership.mem (α := L') J₂ ((f : (a : L) → L') b : L') ∧
          Bracket.bracket (L := L') ((f : (a : L) → L') a : L') ((f : (a : L) → L') b) = x
Tactic: simp_all only [Subtype.exists, LieSubmodule.mem_inf, LieHom.mem_idealRange_iff, exists_prop,
    Set.mem_setOf_eq, LieHom.coe_toLinearMap, mem_comap,
    exists_exists_and_exists_and_eq_and, LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆
have rw : ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange
Tactic: rw [← map_sup_ker_eq_map, ← comap_bracket_eq h, map_comap_eq h, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
have congr : I.incl
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
congr : I.incl
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
have J : ⁅I ⊓ I₁, I ⊓ I₂⁆
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆
have J : ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
Tactic: rw [← I.incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
have J : ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
Tactic: congr
    next => skip
    rw [← I.incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
have conv_rhs : ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
Tactic: conv_rhs =>
    congr
    next => skip
    rw [← I.incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
have rw : ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker
Tactic: rw [comap_bracket_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
rw : ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
have rw₁ : I.incl.IsIdealMorphism
Tactic: rw [comap_bracket_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆
have rw : comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Tactic: rw [comap_bracket_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
have h₃ : I ⊓ I₁ = I₁
Tactic: rw [← inf_eq_right] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
h₃ : I ⊓ I₁ = I₁
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
have h₄ : I ⊓ I₂ = I₂
Tactic: rw [← inf_eq_right] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
have rw : comap I.incl ⁅I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
rw : comap I.incl ⁅I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
have rw₁ : comap I.incl ⁅I₁, I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
⊢ LinearMap.BilinForm.lieInvariant L Φ ↔
    Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
      (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ
have refine_1 : ∀ (h : LinearMap.BilinForm.lieInvariant L Φ) (x : L), ⁅x, Φ⁆ = 0
Tactic: refine ⟨fun h x ↦ ?_, fun h x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
refine_1 : ∀ (h : LinearMap.BilinForm.lieInvariant L Φ) (x : L), ⁅x, Φ⁆ = 0
⊢ LinearMap.BilinForm.lieInvariant L Φ ↔
    Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
      (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ
have refine_2 : ∀
  (h :
    Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
      (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ)
  (x : L) (y z : M),
  Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
    (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
Tactic: refine ⟨fun h x ↦ ?_, fun h x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
⊢ ⁅x, Φ⁆ = 0
have refine_1 : ∀ (y z : M),
  Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
Tactic: ext y z
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1 : Eq.{u_1 + 1} (α := R)
  ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
          ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
        (a : M) → R)
      z :
    R)
  ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₁ : HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
  (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₂ : HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
  (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₂ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₃ : HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
  (0 : (a : M) → R) z
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₂ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₃ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (0 : (a : M) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₄ : HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
  0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₂ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₃ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (0 : (a : M) → R) z
refine_1₄ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₅ : HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
    (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R) =
  0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
refine_1 :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := M →ₗ[R] R) (β := M →ₗ[R] R) (⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R)
            ((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) :
          (a : M) → R)
        z :
      R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
refine_1₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (Φ : (a : M) → M →ₗ[R] R) y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₂ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z
refine_1₃ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    (0 : (a : M) → R) z
refine_1₄ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R) =
    0
refine_1₅ :
  HSub.hSub (α := R) (β := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
      (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
have refine_1₆ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
      LinearMap.zero_apply, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
h :
  Membership.mem (γ := LieSubmodule R L (LinearMap.BilinForm R M))
    (LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)) Φ
x : L
y z : M
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
    (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
have h₁ : Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
  ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
Tactic: replace h := LinearMap.congr_fun₂ (h x) y z
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
x : L
y z : M
h :
  Eq.{u_1 + 1} (α := R) ((((⁅x, Φ⁆ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
    ((((0 : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
    (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
have h₁ : Eq.{u_1 + 1} (α := R) (-(((Φ : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) ⁅x, z⁆ : R)
  ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, y⁆ : M →ₗ[R] R) : (a : M) → R) z : R)
Tactic: simp only [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply,
      LinearMap.zero_apply, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
⊢ y ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal (↑N : Submodule R M)).carrier
have suffices : (∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)) →
  ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) ⁅x, y⁆ : R) (0 : R)
Tactic: suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
      simpa only [LinearMap.BilinForm.isOrtho_def, -- and some default simp lemmas
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
a : M
ha : a ∈ N
⊢ Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) a : M →ₗ[R] R) : (a : M) → R) ⁅x, y⁆ : R) (0 : R)
have rw : Eq.{u_1 + 1} (α := R) ((((Φ : (a : M) → M →ₗ[R] R) ⁅x, a⁆ : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: rw [← neg_eq_zero, ← hΦ_inv]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)
have rw : I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I
Tactic: rw [disjoint_iff, ← hI.lt_iff, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian.{u_2} ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I
have suffices : ¬I ≤ orthogonal Φ hΦ_inv I
Tactic: suffices ¬I ≤ orthogonal Φ hΦ_inv I by simpa