awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₅ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 : S.X₁ ⟶ S.homology)
rw₆ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf)) ≫
      Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ)
    0
rw₇ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles
      (Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ))
    0
rw₈ : Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.homologyπ) 0
rw₉ rw₁₀ : Eq.{v + 1} (α := S.X₁ ⟶ S.homology) 0 0
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)

Tactic:
rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]

Premises used: CategoryTheory.ShortComplex.toCycles_comp_homologyπ, CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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
refine_2 :
  (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair (X := (KernelFork.ofι S.f ⋯).pt)
                      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ π ⋯) ≅
    CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯
⊢ IsColimit (CokernelCofork.ofπ π ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.ShortComplex.homologyIsCokernel, Equiv.invFun
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ 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

Tactic:
exact parallelPair.ext (Iso.refl _) (S.isoCyclesOfIsLimit hkf)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext
                  (Iso.refl
                    ((parallelPair (X := (KernelFork.ofι S.f ⋯).pt)
                          ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                      WalkingParallelPair.zero))
                  (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
          (CokernelCofork.ofπ π ⋯)) ≫
      (isoHomology S hkf hcc fac).hom =
    Cofork.π (CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯)

Tactic:
simp [Cofork.π]

Premises used: CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair (X := (KernelFork.ofι S.f ⋯).pt)
                      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ π ⋯) ≅
    CokernelCofork.ofπ (Z := S.homology) S.homologyπ ⋯

Tactic:
exact Cofork.ext (isoHomology S hkf hcc fac) (by simp [Cofork.π])

Premises used: CategoryTheory.Limits.Cofork.ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ Cofork.π cc ≫ Iso.hom (Iso.refl cc.pt) = Cofork.π (CokernelCofork.ofπ (Cofork.π cc) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
dsimp :
  Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
⊢ Eq (α := H ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    (ι ≫ (hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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
rw₆ rw₇ : Eq.{v + 1} (α := S.homology ⟶ S.X₃) 0 0
⊢ Eq (α := H ⟶ S.X₃) (ι ≫ 𝟙 cc.pt ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) : H ⟶ S.X₃)
    (0 : H ⟶ (CokernelCofork.ofπ S.g ⋯).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]

Premises used: CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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
refine_2 :
  (Cone.postcompose
          (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
              (Iso.refl
                ((parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).hom).obj
      (KernelFork.ofι ι ⋯) ≅
    KernelFork.ofι (Z := S.homology) S.homologyι ⋯
⊢ IsLimit (KernelFork.ofι ι ⋯)

Tactic:
refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsKernel

Premises used: CategoryTheory.ShortComplex.homologyIsKernel, Equiv.invFun, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ 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

Tactic:
exact parallelPair.ext (S.isoOpcyclesOfIsColimit hcc) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.parallelPair.ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 (α :=
    ((Cone.postcompose
              (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
                  (Iso.refl
                    ((parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                          ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0).obj
                      WalkingParallelPair.one))
                  ⋯ ⋯).hom).obj
          (KernelFork.ofι ι ⋯)).pt ⟶
      S.opcycles)
    ((isoHomology S hkf hcc fac).hom ≫ Fork.ι (KernelFork.ofι (Z := S.homology) S.homologyι ⋯))
    (Fork.ι
      ((Cone.postcompose
            (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
                (Iso.refl
                  ((parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                        ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0).obj
                    WalkingParallelPair.one))
                ⋯ ⋯).hom).obj
        (KernelFork.ofι ι ⋯)))

Tactic:
simp [Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
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 ι
⊢ (Cone.postcompose
          (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
              (Iso.refl
                ((parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
                      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) 0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).hom).obj
      (KernelFork.ofι ι ⋯) ≅
    KernelFork.ofι (Z := S.homology) S.homologyι ⋯

Tactic:
exact Fork.ext (isoHomology S hkf hcc fac) (by simp [Fork.ι])

Premises used: CategoryTheory.Limits.Fork.ext
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ Ne.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤

Tactic:
have aux : (⊥ : LieSubmodule R L M) ≠ ⊤ := bot_ne_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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) ⊥ ⊤
contrapose! : ∀ (aux : ∀ (x y : M), x = y), Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤
⊢ ∃ (x : M) (y : M), x ≠ y

Tactic:
contrapose! aux
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
h : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) ⊥ m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m
⊢ Eq.{u_3 + 1} (α := LieSubmodule R L M) ⊥ ⊤

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
m : M
⊢ Membership.mem (γ := LieSubmodule R L M) ⊥ m ↔ Membership.mem (γ := LieSubmodule R L M) ⊤ m

Tactic:
simpa using aux m 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
I : LieIdeal R L
hI : IsSolvable.{u_2} ↥I
⊢ I = ⊥

Tactic:
sSup_eq_bot.mp radical_eq_bot _ hI

Premises used: sSup_eq_bot, LieAlgebra.HasTrivialRadical.radical_eq_bot, Iff.mp
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
rw : Eq (α := LieIdeal R L) (center R L) ⊥
⊢ LieModule.IsFaithful R L L

Tactic:
rw [isFaithful_self_iff]

Premises used: LieAlgebra.isFaithful_self_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ Eq (α := LieIdeal R L) (center R L) ⊥

Tactic:
HasTrivialRadical.eq_bot_of_isSolvable _

Premises used: LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ Eq (α := LieIdeal R L) (center R L) ⊥

Tactic:
exact HasTrivialRadical.eq_bot_of_isSolvable _

Premises used: LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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), IsSolvable.{u_2} ↥I → I = ⊥
⊢ HasTrivialRadical R L

Tactic:
⟨sSup_eq_bot.mpr h⟩

Premises used: Iff.mpr, LieAlgebra.HasTrivialRadical.mk, sSup_eq_bot
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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), IsSolvable.{u_2} ↥I → I = ⊥

Tactic:
⟨@HasTrivialRadical.eq_bot_of_isSolvable _ _ _ _ _, hasTrivialRadical_of_no_solvable_ideals⟩

Premises used: LieAlgebra.hasTrivialRadical_of_no_solvable_ideals, Iff.intro, LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
rw : (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
⊢ HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥

Tactic:
rw [hasTrivialRadical_iff_no_solvable_ideals]

Premises used: LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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 = ⊥
mpr : (∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥) → ∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥
⊢ (∀ (I : LieIdeal R L), IsSolvable.{u_2} ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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), IsSolvable.{u_2} ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian.{u_2} ↥I
⊢ I = ⊥

Tactic:
h₁ _ <| LieAlgebra.ofAbelianIsSolvable I

Premises used: LieAlgebra.ofAbelianIsSolvable, Membership.mem, Subtype
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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), IsSolvable.{u_2} ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian.{u_2} ↥I
⊢ I = ⊥

Tactic:
exact h₁ _ <| LieAlgebra.ofAbelianIsSolvable I

Premises used: LieAlgebra.ofAbelianIsSolvable, Membership.mem, Subtype
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
mpr : derivedAbelianOfIdeal I = ⊥
⊢ I = ⊥

Tactic:
rw [← abelian_of_solvable_ideal_eq_bot_iff]

Premises used: LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ derivedAbelianOfIdeal I = ⊥

Tactic:
h₁ _ <| abelian_derivedAbelianOfIdeal I

Premises used: LieAlgebra.abelian_derivedAbelianOfIdeal
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ derivedAbelianOfIdeal I = ⊥

Tactic:
exact h₁ _ <| abelian_derivedAbelianOfIdeal I

Premises used: LieAlgebra.abelian_derivedAbelianOfIdeal
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
suffices : Nontrivial.{u_2} (LieIdeal R L)
⊢ LieModule.IsIrreducible R L L

Tactic:
suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
rw : ¬Subsingleton L
⊢ Nontrivial.{u_2} (LieIdeal R L)

Tactic:
rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial]

Premises used: LieSubmodule.nontrivial_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ ¬IsLieAbelian L

Tactic:
have _i : ¬ IsLieAbelian L := IsSimple.non_abelian R
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
contrapose : ∀ (_i : Subsingleton L), IsLieAbelian L
⊢ ¬Subsingleton L

Tactic:
contrapose _i
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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 : Subsingleton L
⊢ IsLieAbelian L

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ IsAtom.{u_2} (α := LieIdeal R L) ⊤

Tactic:
isAtom_top

Premises used: isAtom_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
⊢ IsAtom I ↔ I = ⊤

Tactic:
isAtom_iff_eq_top

Premises used: isAtom_iff_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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 : IsAtom I
⊢ I = ⊤

Tactic:
isAtom_iff_eq_top.mp hI

Premises used: Iff.mp, isAtom_iff_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
rw : ∀ (I : LieIdeal R L), IsLieAbelian.{u_2} ↥I → I = ⊥
⊢ HasTrivialRadical R L

Tactic:
rw [hasTrivialRadical_iff_no_abelian_ideals]

Premises used: LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals
-- Module: Mathlib.Algebra.Lie.Semisimple.Basic
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
apply : ¬I = ⊤
⊢ I = ⊥

Tactic:
apply (IsSimple.eq_bot_or_eq_top I).resolve_right

Premises used: Or.resolve_right, LieAlgebra.IsSimple.eq_bot_or_eq_top