awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
refine_1 :
  parallelPair (X := (KernelFork.ofι S.f ⋯).pt)
      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0 ≅
    parallelPair (Y := S.cycles) S.toCycles 0
⊢ IsColimit (CokernelCofork.ofπ π ⋯)
have refine_2 : (Cocone.precompose
        (parallelPair.ext
            (Iso.refl
              ((parallelPair (X := (KernelFork.ofι S.f sorry).pt)
                    ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) sorry)).lift (KernelFork.ofι S.f sorry)) 0).obj
                WalkingParallelPair.zero))
            (S.isoCyclesOfIsLimit hkf) sorry sorry).inv).obj
    (CokernelCofork.ofπ π sorry) ≅
  CokernelCofork.ofπ (Z := S.homology) S.homologyπ sorry
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ Eq (α := H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    (ι ≫ (hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0
have dsimp : Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g sorry) : H ⟶ S.X₃)
  (0 : H ⟶ (CokernelCofork.ofπ S.g sorry).pt)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g sorry) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g sorry).pt)
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₂ : (isoHomology S hkf hcc fac).inv ≫
    ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
  (isoHomology S hkf hcc fac).inv ≫ 0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
rw₂ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    (isoHomology S hkf hcc fac).inv ≫ 0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₃ : (isoHomology S hkf hcc fac).inv ≫
    ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
  0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
rw₂ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    (isoHomology S hkf hcc fac).inv ≫ 0
rw₃ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₄ : Eq (α := S.homology ⟶ S.X₃)
  (S.homologyι ≫
    Iso.inv (S.isoOpcyclesOfIsColimit hcc) ≫
      CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles)
  0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
rw₂ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    (isoHomology S hkf hcc fac).inv ≫ 0
rw₃ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    0
rw₄ :
  Eq (α := S.homology ⟶ S.X₃)
    (S.homologyι ≫
      Iso.inv (S.isoOpcyclesOfIsColimit hcc) ≫
        CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles)
    0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₅ : Eq (α := S.homology ⟶ S.X₃) (S.homologyι ≫ S.fromOpcycles) 0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
rw : Eq (α := H ⟶ S.X₃) (ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃) (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
rw₁ : ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles = 0
rw₂ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    (isoHomology S hkf hcc fac).inv ≫ 0
rw₃ :
  (isoHomology S hkf hcc fac).inv ≫
      ι ≫ CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles =
    0
rw₄ :
  Eq (α := S.homology ⟶ S.X₃)
    (S.homologyι ≫
      Iso.inv (S.isoOpcyclesOfIsColimit hcc) ≫
        CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles)
    0
rw₅ : Eq (α := S.homology ⟶ S.X₃) (S.homologyι ≫ S.fromOpcycles) 0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
have rw₆ : Eq.{v + 1} (α := S.homology ⟶ S.X₃) 0 0
Tactic: rw [id_comp, g'_eq, ← cancel_epi (isoHomology S hkf hcc fac).inv, comp_zero,
      isoHomology_hom_comp_ι_assoc, Iso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ IsLimit (KernelFork.ofι ι ⋯)
have refine_1 : parallelPair (Y := (CokernelCofork.ofπ S.g sorry).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry)) 0 ≅
  parallelPair (X := S.opcycles) S.fromOpcycles 0
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsKernel
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
refine_1 :
  parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0 ≅
    parallelPair (X := S.opcycles) S.fromOpcycles 0
⊢ IsLimit (KernelFork.ofι ι ⋯)
have refine_2 : (Cone.postcompose
        (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
            (Iso.refl
              ((parallelPair (Y := (CokernelCofork.ofπ S.g sorry).pt)
                    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry)) 0).obj
                WalkingParallelPair.one))
            sorry sorry).hom).obj
    (KernelFork.ofι ι sorry) ≅
  KernelFork.ofι (Z := S.homology) S.homologyι sorry
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsKernel
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (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
inst_5 : IsIrreducible R L M
⊢ ∃ (x : M) (y : M), x ≠ y
have aux : Ne.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤
Tactic: have aux : (⊥ : LieSubmodule R L M) ≠ ⊤ := bot_ne_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (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
inst_5 : IsIrreducible R L M
aux : Ne.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤
⊢ ∃ (x : M) (y : M), x ≠ y
have contrapose! : ∀ (aux : ∀ (x y : M), x = y), Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤
Tactic: contrapose! aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (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
inst_5 : IsIrreducible R L M
aux : ∀ (x y : M), x = y
⊢ Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤
have h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) ⊥ m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : HasTrivialRadical R L
⊢ LieModule.IsFaithful R L L
have rw : Eq (α := LieIdeal R L) (center R L) ⊥
Tactic: rw [isFaithful_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
have rw : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
Tactic: rw [hasTrivialRadical_iff_no_solvable_ideals]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
have mp : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) → ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
mp : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) → ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
⊢ (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
have mpr : (∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥) → ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable.{u_2} ↥I
⊢ I = ⊥
have mpr : derivedAbelianOfIdeal I = ⊥
Tactic: rw [← abelian_of_solvable_ideal_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ LieModule.IsIrreducible R L L
have suffices : Nontrivial.{u_2} (LieIdeal R L)
Tactic: suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ Nontrivial.{u_2} (LieIdeal R L)
have rw : ¬Subsingleton L
Tactic: rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ ¬Subsingleton L
have _i : ¬IsLieAbelian L
Tactic: have _i : ¬ IsLieAbelian L := IsSimple.non_abelian R
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
_i : ¬IsLieAbelian L
⊢ ¬Subsingleton L
have contrapose : ∀ (_i : Subsingleton L), IsLieAbelian L
Tactic: contrapose _i
Cleared hypotheses: _i
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
⊢ HasTrivialRadical R L
have rw : ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
Tactic: rw [hasTrivialRadical_iff_no_abelian_ideals]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian.{u_2} ↥I
⊢ I = ⊥
have apply : ¬I = ⊤
Tactic: apply (IsSimple.eq_bot_or_eq_top I).resolve_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSimple R L
hI : IsLieAbelian.{u_2} ↥⊤
⊢ False
have hI₁ : IsLieAbelian L
Tactic: rw [lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})
have nth_rewrite : Membership.mem (γ := LieIdeal R L) (sSup {I} ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) x
Tactic: nth_rewrite 1 [← sSup_singleton (a := I)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ Membership.mem (γ := LieIdeal R L) (sSup {I} ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) x
have rw : Membership.mem (γ := LieIdeal R L) ⊤ x
Tactic: rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left,
            IsSemisimple.sSup_atoms_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
rw : Membership.mem (γ := LieIdeal R L) ⊤ x
⊢ Membership.mem (γ := LieIdeal R L) (sSup {I} ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) x
have rw₁ : Subset (α := Set (LieIdeal R L)) {I} {I' : LieIdeal R L | IsAtom I'}
Tactic: rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left,
            IsSemisimple.sSup_atoms_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅x, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
have hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})
Tactic: have hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I}) := by
          nth_rewrite 1 [← sSup_singleton (a := I)]
          rw [← sSup_union, Set.union_diff_self, Set.union_eq_self_of_subset_left,
            IsSemisimple.sSup_atoms_eq_top]
          · apply LieSubmodule.mem_top
          · simp only [Set.singleton_subset_iff, Set.mem_setOf_eq, hI]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx : x ∈ I ⊔ sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅x, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
have hx₁ : ∃ y ∈ I,
  ∃ (z : L), Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) z ∧ y + z = x
Tactic: rw [LieSubmodule.mem_sup] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
hx :
  ∃ y ∈ I,
    ∃ (z : L), Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) z ∧ y + z = x
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅x, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
have obtain : ∀ (a : L) (ha : a ∈ I) (b : L)
  (hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b),
  Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅a + b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)).carrier
    (⁅a + b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
have simp : HAdd.hAdd (α := L) (β := L) (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
    (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L) ∈
  Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)
Tactic: simp only [Submodule.carrier_eq_coe, add_lie, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Basic (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ (↑(↑J : Submodule R ↥I) : Set ↥I)
a : L
ha : a ∈ I
b : L
hb : Membership.mem (γ := LieSubmodule R L L) (sSup ({I' : LieIdeal R L | IsAtom I'} \ {I})) b
⊢ HAdd.hAdd (α := L) (β := L) (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
      (⁅b, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L) ∈
    Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I)
have a₁ : Membership.mem (α := L) (Submodule.map (↑I.incl : ↥I →ₗ[R] L) (↑J : Submodule R ↥I))
  (⁅a, ((↑I.incl : ↥I →ₗ[R] L) : (a : ↥I) → L) y⁆ : L)
Tactic: apply add_mem