awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
N N' : LieSubmodule R L M
h : map f N = map f N'
⊢ Eq.{w₁ + 1} (α := Set M') ((⇑f : (a : M) → M') '' (↑N : Set M)) ((⇑f : (a : M) → M') '' (↑N' : Set M))

Tactic:
simp only [← coe_map, h]

Premises used: LieSubmodule.coe_map
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : L
m : M
hm : m ∈ N
⊢ (↑(AddHom.toFun
            (LinearMap.toAddHom
                ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                    LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                  LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                    ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
              AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
            ⁅x, Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm⁆ :
          ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
      M') =
    (↑(⁅x,
            AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                      LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                        ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                    LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
              (Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm)⁆ :
          ↥(map f N)) :
      M')

Tactic:
f.map_lie x m

Premises used: LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : L
m : M
hm : m ∈ N
⊢ (↑(AddHom.toFun
            (LinearMap.toAddHom
                ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                    LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                  LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                    ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
              AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
            ⁅x, Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm⁆ :
          ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
      M') =
    (↑(⁅x,
            AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                      LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                        ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                    LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
              (Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm)⁆ :
          ↥(map f N)) :
      M')

Tactic:
exact f.map_lie x m

Premises used: LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ ↥(map f N) → ↥N

Tactic:
exact DFunLike.coe (Submodule.equivMapOfInjective (f : M →ₗ[R] M') hf N).symm

Premises used: LinearEquiv.symm, LieSubmodule.toSubmodule, LieModuleHom.toLinearMap, Submodule.equivMapOfInjective, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m ∈ N
⊢ comap e.toLieModuleHom (map e.toLieModuleHom N) = N

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
m : M
⊢ m ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m ∈ N

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
h : ∀ (m : M'), m ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m ∈ N
⊢ map e.toLieModuleHom (comap e.toLieModuleHom N) = N

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
m : M'
⊢ m ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m ∈ N

Tactic:
simp [e.apply_eq_iff_eq_symm_apply]

Premises used: LieModuleEquiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ (↑f.ker : Submodule R M) = (↑f : M →ₗ[R] N).ker

Tactic:
rfl

Premises used: LinearMap.ker, Submodule.comap, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw :
  (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  (↑f : M →ₗ[R] N).ker = (↑⊥ : Submodule R M) ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ : (↑f : M →ₗ[R] N).ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₃ :
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑(↑f : M →ₗ[R] N) : (a : M) → N) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₄ rw₅ :
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]

Premises used: LieSubmodule.bot_toSubmodule, LinearMap.ker_eq_bot, LieModuleHom.coe_toLinearMap, LieSubmodule.toSubmodule_inj, LieModuleHom.ker_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
⊢ m ∈ f.ker ↔ Eq.{w₁ + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
⊢ Eq.{w + 1} (α := LieSubmodule R L M) (ker id) ⊥

Tactic:
rfl

Premises used: Set.Mem, setOf, LieSubmodule.comap, Submodule.comap, Set.preimage, LieModuleHom.ker, Set.singleton, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
h :
  ∀ (m : M) (hm : m ∈ f.ker),
    Eq.{w₁ + 1} (α := N) ((f.comp f.ker.incl : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
      ((0 : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
⊢ f.comp f.ker.incl = 0

Tactic:
ext ⟨m, hm⟩
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ Eq.{w₁ + 1} (α := N) ((f.comp f.ker.incl : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
    ((0 : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)

Tactic:
mem_ker.mp hm

Premises used: LieModuleHom.mem_ker, Iff.mp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ Eq.{w₁ + 1} (α := N) ((f.comp f.ker.incl : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
    ((0 : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)

Tactic:
exact mem_ker.mp hm

Premises used: LieModuleHom.mem_ker, Iff.mp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
rw : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' = ⊥
rw₁ : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' ≤ ⊥
rw₂ rw₃ : M' ≤ LieSubmodule.comap f ⊥ ↔ M' ≤ LieSubmodule.comap f ⊥
⊢ M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥

Tactic:
rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]

Premises used: LieModuleHom.ker, LieSubmodule.map_le_iff_le_comap, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ (↑f.range : Set N) = Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ (↑f.range : Submodule R N) = (↑f : M →ₗ[R] N).range

Tactic:
rfl

Premises used: LinearMap.range, rfl, Submodule.copy
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
n : N
⊢ n ∈ f.range ↔ ∃ (m : M), (f : (a : M) → N) m = n

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : N), m ∈ LieSubmodule.map f ⊤ ↔ m ∈ f.range
⊢ LieSubmodule.map f ⊤ = f.range

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : N
⊢ m ∈ LieSubmodule.map f ⊤ ↔ m ∈ f.range

Tactic:
simp [LieSubmodule.mem_map]

Premises used: LieSubmodule.mem_map
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ :
  Eq.{w₁ + 1} (α := Set N) (Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₃ rw₄ :
  Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]

Premises used: Set.range_eq_univ, LieModuleHom.coe_range, LieSubmodule.top_coe, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f_1 : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), Membership.mem (α := N) P ((f : (a : M) → N) m : N)
x : L
m : M
a :
  Eq.{w₁ + 1} (α := N)
    (↑((LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) ⁅x, m⁆) : N)
    (↑⁅x, (LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) m⁆ : N)
⊢ Eq.{w₁ + 1} (α := ↥P)
    ((LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) ⁅x, m⁆ :
      ↥(↑P : Submodule R N))
    (⁅x, (LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) m⁆ : ↥P)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f_1 : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), Membership.mem (α := N) P ((f : (a : M) → N) m : N)
x : L
m : M
⊢ Eq.{w₁ + 1} (α := N)
    (↑((LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) ⁅x, m⁆) : N)
    (↑⁅x, (LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) m⁆ : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), Membership.mem (α := N) P ((f : (a : M) → N) m : N)
m : M
⊢ Eq.{w₁ + 1} (α := N) ((↑((codRestrict P f h : (a : M) → ↥P) m) : N) : N) ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ N.incl.ker = ⊥

Tactic:
(LieModuleHom.ker_eq_bot N.incl).mpr <| injective_incl N

Premises used: Iff.mpr, LieModuleHom.ker_eq_bot, LieSubmodule.incl, LieSubmodule.injective_incl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
simp : (↑N : Submodule R M).subtype.range = (↑N : Submodule R M)
⊢ N.incl.range = N

Tactic:
simp only [← toSubmodule_inj, LieModuleHom.toSubmodule_range, incl_coe]

Premises used: LieModuleHom.toSubmodule_range, LieSubmodule.toSubmodule_inj, LieSubmodule.incl_coe
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
rw rw₁ : (↑N : Submodule R M) = (↑N : Submodule R M)
⊢ (↑N : Submodule R M).subtype.range = (↑N : Submodule R M)

Tactic:
rw [Submodule.range_subtype]

Premises used: Submodule.range_subtype
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
simp : Submodule.comap (↑N : Submodule R M).subtype (↑N : Submodule R M) = ⊤
⊢ comap N.incl N = ⊤

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, top_toSubmodule]

Premises used: LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
rw rw₁ : Eq.{w + 1} (α := Submodule R ↥N) ⊤ ⊤
⊢ Submodule.comap (↑N : Submodule R M).subtype (↑N : Submodule R M) = ⊤

Tactic:
rw [Submodule.comap_subtype_self]

Premises used: Submodule.comap_subtype_self
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ map N.incl ⊤ = N

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ (m : M), m ∈ map (N.incl.restrictLie H) ⊤ ↔ m ∈ N.restr H
⊢ map (N.incl.restrictLie H) ⊤ = N.restr H

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
H : LieSubalgebra R L
m : M
⊢ m ∈ map (N.incl.restrictLie H) ⊤ ↔ m ∈ N.restr H

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
rw : map f N ≤ map f ⊤
⊢ map f N ≤ f.range

Tactic:
rw [← LieModuleHom.map_top]

Premises used: LieModuleHom.map_top
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ map f ⊤

Tactic:
LieSubmodule.map_mono le_top

Premises used: le_top, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ map f ⊤

Tactic:
exact LieSubmodule.map_mono le_top

Premises used: le_top, LieSubmodule.map_mono
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ LT.lt (α := LieSubmodule R L M)
      ((mapOrderEmbedding (f := N.incl) ⋯ : (a : LieSubmodule R L ↥N) → LieSubmodule R L M) N' : LieSubmodule R L M)
      ((mapOrderEmbedding (f := N.incl) ⋯ : (a : LieSubmodule R L ↥N) → LieSubmodule R L M) ⊤ : LieSubmodule R L M) ↔
    N' < ⊤

Tactic:
(LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt

Premises used: Subtype.coe_injective, LieSubmodule.mapOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
h : N = (mapOrderEmbedding (f := N.incl) ⋯ : (a : LieSubmodule R L ↥N) → LieSubmodule R L M) ⊤
⊢ map N.incl N' < N ↔ N' < ⊤

Tactic:
convert! (LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt

Premises used: Subtype.coe_injective, LieSubmodule.mapOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ N = (mapOrderEmbedding (f := N.incl) ⋯ : (a : LieSubmodule R L ↥N) → LieSubmodule R L M) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
rw : map N.incl ⊤
| N

Tactic:
rw [← N.map_incl_top]

Premises used: LieSubmodule.map_incl_top