awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
⊢ (↑(⨆ (x : { x : LieSubmodule R L M // x ∈ s }), (↑(↑x : LieSubmodule R L M) : Submodule R M)) : Set M) =
    ⋃ (i : { x : LieSubmodule R L M // x ∈ s }), (↑(↑(↑i : LieSubmodule R L M) : Submodule R M) : Set M)

Tactic:
have := Submodule.coe_iSup_of_directed _ hdir.directed_val
-- 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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this :
  (↑(⨆ (x : { x : LieSubmodule R L M // x ∈ s }), (↑(↑x : LieSubmodule R L M) : Submodule R M)) : Set M) =
    ⋃ (i : { x : LieSubmodule R L M // x ∈ s }), (↑(↑(↑i : LieSubmodule R L M) : Submodule R M) : Set M)
⊢ (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)

Tactic:
simp_rw [← iSup_toSubmodule, Set.iUnion_coe_set, coe_toSubmodule] at this

Premises used: LieSubmodule.iSup_toSubmodule, Set.iUnion_coe_set, LieSubmodule.coe_toSubmodule
-- 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
m : M
s : Set (LieSubmodule R L M)
hdir : DirectedOn (fun (x1 x2 : LieSubmodule R L M) ↦ x1 ≤ x2) s
hsup : m ∈ (↑(sSup s) : Set M)
hne : Nonempty.{w + 1} (↑s : Type w)
this : (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M) = ⋃ i ∈ s, (↑i : Set M)
rw : (↑(sSup s) : Set M) = (↑(⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)) : Set M)
rw₁ : sSup s = ⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M)
rw₂ :
  Eq.{w + 1} (α := LieSubmodule R L M) (⨆ a ∈ s, a)
    (⨆ (i : { x : LieSubmodule R L M // x ∈ s }), (↑i : LieSubmodule R L M))
rw₃ rw₄ :
  Eq.{w + 1} (α := LieSubmodule R L M) (⨆ a ∈ s, a)
    (⨆ (i : LieSubmodule R L M),
      ⨆ (h : i ∈ s), (↑(Subtype.mk (p := fun (x : LieSubmodule R L M) ↦ x ∈ s) i h) : LieSubmodule R L M))
⊢ (↑(sSup s) : Set M) = ⋃ N ∈ s, (↑N : Set M)

Tactic:
rw [← this, SetLike.coe_set_eq, sSup_eq_iSup, iSup_subtype]

Premises used: iSup_subtype, sSup_eq_iSup, SetLike.coe_set_eq
-- 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
⊢ ∀ (b : LieSubmodule R L M),
    Membership.mem (γ := Set (LieSubmodule R L M)) ((fun (x : M) ↦ lieSpan R L {x}) '' (↑N : Set M)) b → b ≤ 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
refine : N ≤ sSup ((fun (x : M) ↦ lieSpan R L {x}) '' (↑N : Set M))
⊢ sSup ((fun (x : M) ↦ lieSpan R L {x}) '' (↑N : Set M)) = N

Tactic:
refine le_antisymm (sSup_le <| by simp) ?_

Premises used: le_antisymm, sSup_le
-- 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 : Submodule R M) ≤
    sSup {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x}

Tactic:
fun m hm ↦ Submodule.mem_sSup.mpr fun N' hN' ↦ ?_

Premises used: Iff.mpr, Submodule.mem_sSup
-- 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
refine :
  ∀ (m : M) (hm : m ∈ (↑N : Submodule R M)) (N' : Submodule R M)
    (hN' :
      ∀ (p : Submodule R M),
        Membership.mem (γ := Set (Submodule R M))
            {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x}
            p →
          p ≤ N'),
    m ∈ N'
⊢ (↑N : Submodule R M) ≤
    sSup {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x}

Tactic:
refine fun m hm ↦ Submodule.mem_sSup.mpr fun N' hN' ↦ ?_

Premises used: Iff.mpr, Submodule.mem_sSup
-- 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 : M
hm : m ∈ (↑N : Submodule R M)
N' : Submodule R M
hN' :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x} p →
      p ≤ N'
⊢ ∀ m ∈ N, (↑(lieSpan R L {m}) : Submodule R M) ≤ N'

Tactic:
simpa using hN'
-- 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 : M
hm : m ∈ (↑N : Submodule R M)
N' : Submodule R M
hN' :
  ∀ (p : Submodule R M),
    Membership.mem (γ := Set (Submodule R M))
        {x : Submodule R M | ∃ (s : LieSubmodule R L M), (∃ x ∈ N, lieSpan R L {x} = s) ∧ (↑s : Submodule R M) = x} p →
      p ≤ N'
⊢ ∀ m ∈ N, (↑(lieSpan R L {m}) : Submodule R M) ≤ N'

Tactic:
replace hN' : ∀ m ∈ N, lieSpan R L {m} ≤ N' := by simpa using hN'
-- 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 : M
hm : m ∈ (↑N : Submodule R M)
N' : Submodule R M
hN' : ∀ m ∈ N, (↑(lieSpan R L {m}) : Submodule R M) ≤ N'
⊢ m ∈ N'

Tactic:
hN' _ hm (subset_lieSpan rfl)

Premises used: LieSubmodule.subset_lieSpan, 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
m : M
hm : m ∈ (↑N : Submodule R M)
N' : Submodule R M
hN' : ∀ m ∈ N, (↑(lieSpan R L {m}) : Submodule R M) ≤ N'
⊢ m ∈ N'

Tactic:
exact hN' _ hm (subset_lieSpan rfl)

Premises used: LieSubmodule.subset_lieSpan, 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 N' : LieSubmodule R L M
s : Set M
⊢ IsCompactlyGenerated.{w} (LieSubmodule R L M)

Tactic:
⟨fun N ↦ ⟨(fun x ↦ lieSpan R L {x}) '' N, fun _ ⟨m, _, hm⟩ ↦
    hm ▸ isCompactElement_lieSpan_singleton R L m, N.sSup_image_lieSpan_singleton⟩⟩

Premises used: LieSubmodule.isCompactElement_lieSpan_singleton, IsCompactlyGenerated.mk, Eq.rec, _private.0.LieSubmodule.instIsCompactlyGenerated.match_1, LieSubmodule.sSup_image_lieSpan_singleton, SetLike.coe, LieSubmodule.lieSpan, And.intro, Exists.intro, Set.image, IsCompactElement, Singleton.singleton
-- 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'
x : L
m' : M'
h : m' ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
rcases :
  ∀ (m : M) (hm : m ∈ (↑(↑N : Submodule R M) : Set M)) (hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'),
    ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier
⊢ ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier

Tactic:
rcases h with ⟨m, hm, hfm⟩
-- 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'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
h : ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M) ∧ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
⊢ ⁅x, m'⁆ ∈ (Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)).carrier

Tactic:
use ⁅x, m⁆
-- 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'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
h : ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M)
h₁ : ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆
⊢ ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M) ∧ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆

Tactic:
constructor
-- 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'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : ((↑f : M →ₗ[R] M') : (a : M) → M') m = m'
⊢ ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M)

Tactic:
apply N.lie_mem hm

Premises used: LieSubmodule.lie_mem
-- 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'
x : L
m' : M'
m : M
hm : m ∈ (↑(↑N : Submodule R M) : Set M)
hfm : (f : (a : M) → M') m = m'
⊢ ((↑f : M →ₗ[R] M') : (a : M) → M') ⁅x, m⁆ = ⁅x, m'⁆

Tactic:
simp [hfm]
-- 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'
N : LieSubmodule R L M
⊢ (↑(map f N) : Set M') = (⇑f : (a : M) → M') '' (↑N : Set M)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- 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'
N : LieSubmodule R L M
⊢ (↑(map f N) : Submodule R M') = Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)

Tactic:
rfl

Premises used: Submodule.map, rfl
-- 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'
x : L
m : M
h : m ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier
this : Membership.mem (α := M') N' (⁅x, (f : (a : M) → M') m⁆ : M')
⊢ ⁅x, m⁆ ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier

Tactic:
simp [this]
-- 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'
x : L
m : M
h : m ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier
suffices : Membership.mem (α := M') N' (⁅x, (f : (a : M) → M') m⁆ : M')
⊢ ⁅x, m⁆ ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier

Tactic:
suffices ⁅x, f m⁆ ∈ N' by simp [this]
-- 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'
x : L
m : M
h : m ∈ (Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')).carrier
⊢ Membership.mem (α := M') N' (⁅x, (f : (a : M) → M') m⁆ : M')

Tactic:
apply N'.lie_mem h

Premises used: LieSubmodule.lie_mem
-- 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'
N' : LieSubmodule R L M'
⊢ (↑(comap f N') : Submodule R M) = Submodule.comap (↑f : M →ₗ[R] M') (↑N' : Submodule R M')

Tactic:
rfl

Premises used: Submodule.comap, rfl
-- 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'
N : LieSubmodule R L M
N' : LieSubmodule R L M'
⊢ map f N ≤ N' ↔ N ≤ comap f N'

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- 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'
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: LieSubmodule.map_le_iff_le_comap, GaloisConnection
-- 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'
N N₂ : LieSubmodule R L M
⊢ map f (N ⊓ N₂) ≤ map f N ⊓ map f N₂

Tactic:
Set.image_inter_subset f N N₂

Premises used: Set.Mem, setOf, Set.image_inter_subset, Set.inter, Set.Subset, SetLike.coe, Set.image, DFunLike.coe
-- 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'
N N₂ : LieSubmodule R L M
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ map f (N ⊓ N₂) = map f N ⊓ map f N₂

Tactic:
SetLike.coe_injective <| Set.image_inter hf

Premises used: Set.image_inter, SetLike.coe_injective
-- 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'
N N₂ : LieSubmodule R L M
⊢ map f (N ⊔ N₂) = map f N ⊔ map f N₂

Tactic:
(gc_map_comap f).l_sup

Premises used: LieSubmodule.gc_map_comap, GaloisConnection.l_sup
-- 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'
N' N₂' : LieSubmodule R L M'
⊢ comap f (N' ⊓ N₂') = comap f N' ⊓ comap f N₂'

Tactic:
rfl

Premises used: Set.Mem, setOf, LieSubmodule.comap, Set.inter, Submodule.comap, Set.preimage, rfl
-- 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'
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ map f (⨆ (i : ι), N i) = ⨆ (i : ι), map f (N i)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

Premises used: GaloisConnection.l_iSup, LieSubmodule.gc_map_comap
-- 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'
N : LieSubmodule R L M
m' : M'
⊢ m' ∈ map f N ↔ ∃ m ∈ N, (f : (a : M) → M') m = m'

Tactic:
Submodule.mem_map

Premises used: Set.Mem, Submodule.mem_map
-- 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'
N : LieSubmodule R L M
m : M
h : m ∈ N
⊢ Membership.mem (α := M') (map f N) ((f : (a : M) → M') m : M')

Tactic:
Set.mem_image_of_mem _ h

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image
-- 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'
N' : LieSubmodule R L M'
m : M
⊢ m ∈ comap f N' ↔ Membership.mem (α := M') N' ((f : (a : M) → M') m : M')

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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 N₂ : LieSubmodule R L M
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₂ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₃ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊤ ↔ N ≤ N₂
rw₄ : (↑N : Submodule R M) ≤ (↑N₂ : Submodule R M) ↔ N ≤ N₂
rw₅ rw₆ : N ≤ N₂ ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]

Premises used: LieSubmodule.toSubmodule_le_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, Submodule.comap_subtype_eq_top, 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 N₂ : LieSubmodule R L M
simp :
  Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊥ ↔
    (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
⊢ comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
    inf_toSubmodule]

Premises used: LieSubmodule.bot_toSubmodule, LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe, LieSubmodule.inf_toSubmodule
-- 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 N₂ : LieSubmodule R L M
rw : Disjoint (↑N : Submodule R M) (↑N₂ : Submodule R M) ↔ (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
rw₁ rw₂ : (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
⊢ Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊥ ↔
    (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥

Tactic:
rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

Premises used: disjoint_iff, Submodule.disjoint_iff_comap_eq_bot
-- 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'
N N₂ : LieSubmodule R L M
h : N ≤ N₂
⊢ map f N ≤ map f N₂

Tactic:
Set.image_mono h

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- 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'
N : LieSubmodule R L M
M'' : Type u_1
inst_8 : AddCommGroup M''
inst_9 : Module R M''
inst_10 : LieRingModule L M''
g : M' →ₗ⁅R,L⁆ M''
⊢ (↑(map (g.comp f) N) : Set M'') = (↑(map g (map f N)) : Set M'')

Tactic:
simp only [← Set.image_comp, coe_map, LieModuleHom.coe_comp]

Premises used: LieSubmodule.coe_map, LieModuleHom.coe_comp, Set.image_comp
-- 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
h : ∀ (m : M), m ∈ map LieModuleHom.id N ↔ m ∈ N
⊢ map LieModuleHom.id N = N

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
m : M
⊢ m ∈ map LieModuleHom.id N ↔ m ∈ N

Tactic:
simp
-- 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'
h : ∀ (m : M'), m ∈ map f ⊥ ↔ Membership.mem (γ := LieSubmodule R L M') ⊥ m
⊢ map f ⊥ = ⊥

Tactic:
ext m
-- 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'
m : M'
⊢ m ∈ map f ⊥ ↔ Membership.mem (γ := LieSubmodule R L M') ⊥ m

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- 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'
N N₂ : LieSubmodule R L M
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ map f N ≤ map f N₂ ↔ N ≤ N₂

Tactic:
Set.image_subset_image_iff hf

Premises used: Set.Mem, setOf, Set.Subset, Set.image_subset_image_iff, Set.image