awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') y hy) : L) ∈ K
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hx) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') y hy) : L)⁆ ∈ K

Tactic:
exact h' x y hx hy'
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieSubalgebra R L) (toLieSubalgebra R L ⊤) ⊤

Tactic:
rfl

Premises used: LieIdeal.toLieSubalgebra, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
this : Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
simp :
  Membership.mem (α := L') (toLieSubalgebra R L' J)
    (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          Submodule.mem_toAddSubmonoid, Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie,
          LieSubalgebra.mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule, Submodule.mem_comap, LieHom.map_lie, AddSubsemigroup.mem_carrier, Submodule.mem_toAddSubmonoid, LieHom.coe_toLinearMap, AddSubmonoid.mem_toSubsemigroup
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
this : Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
⊢ Membership.mem (α := L') (toLieSubalgebra R L' J)
    (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')

Tactic:
this

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
this : Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
⊢ Membership.mem (α := L') (toLieSubalgebra R L' J)
    (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')

Tactic:
exact this
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
suffices :
  Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
suffices ⁅f x, f y⁆ ∈ J by
        simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          Submodule.mem_toAddSubmonoid, Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie,
          LieSubalgebra.mem_toSubmodule]
        exact this
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
⊢ Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')

Tactic:
apply J.lie_mem h

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : (↑(map f I) : Set L') = (⇑f : (a : L) → L') '' (↑I : Set L)
rw :
  Eq.{w₂ + 1} (α := Set L') ((⇑f : (a : L) → L') '' (↑I : Set L))
    ((⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(↑I : Submodule R L) : Set L))
⊢ (↑(map f I) : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)

Tactic:
rw [SetLike.ext'_iff, LieSubmodule.coe_toSubmodule, h, Submodule.map_coe]

Premises used: LieSubmodule.coe_toSubmodule, SetLike.ext'_iff, Submodule.map_coe
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : (↑(map f I) : Set L') = (⇑f : (a : L) → L') '' (↑I : Set L)
⊢ Eq.{w₂ + 1} (α := Set L') ((⇑f : (a : L) → L') '' (↑I : Set L))
    ((⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(↑I : Submodule R L) : Set L))

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
⊢ (↑(comap f J) : Submodule R L) = Submodule.comap (↑f : L →ₗ[R] L') (↑J : Submodule R L')

Tactic:
rfl

Premises used: Submodule.comap, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f I ≤ J ↔ (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑J : Set L')

Tactic:
LieSubmodule.lieSpan_le

Premises used: Set.Mem, setOf, Set.image, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
a :
  Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') x : L')
⊢ Membership.mem (α := L') (map f I) ((f : (a : L) → L') x : L')

Tactic:
apply LieSubmodule.subset_lieSpan

Premises used: LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
h :
  x ∈ (↑(toLieSubalgebra R L I).toSubmodule : Set L) ∧
    Eq.{w₂ + 1} (α := L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L') ((f : (a : L) → L') x : L')
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') x : L')

Tactic:
use x
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ x ∈ (↑(toLieSubalgebra R L I).toSubmodule : Set L) ∧
    Eq.{w₂ + 1} (α := L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L') ((f : (a : L) → L') x : L')

Tactic:
⟨hx, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ x ∈ (↑(toLieSubalgebra R L I).toSubmodule : Set L) ∧
    Eq.{w₂ + 1} (α := L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L') ((f : (a : L) → L') x : L')

Tactic:
exact ⟨hx, rfl⟩
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
x : L
⊢ x ∈ comap f J ↔ Membership.mem (α := L') J ((f : (a : L) → L') x : L')

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
rw : (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑J : Set L') ↔ I ≤ comap f J
⊢ map f I ≤ J ↔ I ≤ comap f J

Tactic:
rw [map_le]

Premises used: LieIdeal.map_le
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑J : Set L') ↔ I ≤ comap f J

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image_subset_iff
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑J : Set L') ↔ I ≤ comap f J

Tactic:
exact Set.image_subset_iff

Premises used: Set.image_subset_iff
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: LieIdeal.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
⊢ map f (I ⊔ I₂) = map f I ⊔ map f I₂

Tactic:
(gc_map_comap f).l_sup

Premises used: LieIdeal.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
rw rw₁ : comap f J ≤ comap f J
⊢ map f (comap f J) ≤ J

Tactic:
rw [map_le_iff_le_comap]

Premises used: LieIdeal.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
rw rw₁ : map f I ≤ map f I
⊢ I ≤ comap f (map f I)

Tactic:
rw [← map_le_iff_le_comap]

Premises used: LieIdeal.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
h₁ : (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule
⊢ LE.le (α := LieIdeal R L')
    (LieSubmodule.lieSpan R L' (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I₁).toSubmodule) : Set L'))
    (LieSubmodule.lieSpan R L' (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I₂).toSubmodule) : Set L'))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule

Tactic:
exact h
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : J₁ ≤ J₂
⊢ (↑J₁ : Set L') ⊆ (↑J₂ : Set L')

Tactic:
rw [← SetLike.coe_subset_coe] at h ⊢

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : (↑J₁ : Set L') ⊆ (↑J₂ : Set L')
⊢ (↑(comap f J₁) : Submodule R L).carrier ⊆ (↑(comap f J₂) : Submodule R L).carrier

Tactic:
Set.preimage_mono h

Premises used: setOf, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : (↑J₁ : Set L') ⊆ (↑J₂ : Set L')
⊢ (↑(comap f J₁) : Submodule R L).carrier ⊆ (↑(comap f J₂) : Submodule R L).carrier

Tactic:
exact Set.preimage_mono h

Premises used: Set.preimage_mono
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
a : map f I ≤ J
a₁ : J ≤ map f I
⊢ map f I = J

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
a : (⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(toLieSubalgebra R L I).toSubmodule : Set L) ⊆ (↑J : Set L')
⊢ map f I ≤ J

Tactic:
rw [map, LieSubmodule.lieSpan_le, Submodule.map_coe]

Premises used: LieIdeal.map, LieSubmodule.lieSpan_le, Submodule.map_coe
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
a a₁ : (↑J : Set L') ⊆ (↑J : Set L')
⊢ (⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(toLieSubalgebra R L I).toSubmodule : Set L) ⊆ (↑J : Set L')

Tactic:
erw [h]
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
a : (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑(map f I) : Set L')
⊢ J ≤ map f I

Tactic:
rw [← SetLike.coe_subset_coe, ← h]

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑(map f I) : Set L')

Tactic:
LieSubmodule.subset_lieSpan

Premises used: Set.Mem, setOf, LieSubmodule.subset_lieSpan, Set.image
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑(map f I) : Set L')

Tactic:
exact LieSubmodule.subset_lieSpan

Premises used: LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
hα : Eq.{v + 1} (α := LieIdeal R ↥⊥) ⊥ ⊤
⊢ Subsingleton.{v + 1} (LieIdeal R ↥⊥)

Tactic:
apply subsingleton_of_bot_eq_top

Premises used: subsingleton_of_bot_eq_top
-- Module: Mathlib.Algebra.Lie.Ideal
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'
inst_10 : LieAlgebra R L
inst_11 : LieModule R L M
inst_12 : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
⊢ Eq.{v + 1} (α := LieIdeal R ↥⊥) ⊥ ⊤

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ f.idealRange = LieSubmodule.lieSpan R L' (↑f.range : Set L')

Tactic:
rfl

Premises used: LieHom.idealRange, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (m : L'), m ∈ f.idealRange ↔ m ∈ LieIdeal.map f ⊤
⊢ f.idealRange = LieIdeal.map f ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
m : L'
h :
  Membership.mem (γ := LieSubmodule R L' L') (LieSubmodule.lieSpan R L' (↑(LieSubalgebra.map f ⊤) : Set L')) m ↔
    m ∈ LieIdeal.map f ⊤
⊢ m ∈ f.idealRange ↔ m ∈ LieIdeal.map f ⊤

Tactic:
simp only [idealRange, range_eq_map]

Premises used: LieHom.range_eq_map, LieHom.idealRange
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
m : L'
⊢ Membership.mem (γ := LieSubmodule R L' L') (LieSubmodule.lieSpan R L' (↑(LieSubalgebra.map f ⊤) : Set L')) m ↔
    m ∈ LieIdeal.map f ⊤

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ f.IsIdealMorphism ↔ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range

Tactic:
Iff.rfl

Premises used: Iff.rfl, LieHom.IsIdealMorphism
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
hf : f.IsIdealMorphism
⊢ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range

Tactic:
hf

Premises used: LieHom.IsIdealMorphism
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
simp :
  (∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆) ↔
    ∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
⊢ f.IsIdealMorphism ↔
    ∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
simp only [isIdealMorphism_def, idealRange_eq_lieSpan_range, ←
    LieSubalgebra.toSubmodule_inj, ← f.range.coe_toSubmodule,
    LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff,
    LieSubalgebra.mem_toSubmodule, mem_range, exists_imp,
    Submodule.exists_lieSubmodule_coe_eq_iff]

Premises used: Submodule.exists_lieSubmodule_coe_eq_iff, LieHom.isIdealMorphism_def, LieSubalgebra.mem_toSubmodule, LieSubalgebra.coe_toSubmodule, LieHom.range, LieIdeal.toLieSubalgebra_toSubmodule, LieSubalgebra.toSubmodule_inj, LieSubmodule.coe_lieSpan_submodule_eq_iff, LieHom.idealRange_eq_lieSpan_range, LieHom.mem_range, exists_imp
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
mp :
  (∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆) →
    ∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
mpr :
  (∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')) →
    ∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆
⊢ (∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆) ↔
    ∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆
x : L'
y : L
mp :
  ∀ (z : L) (hz : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') z : L') (⁅x, (f : (a : L) → L') y⁆ : L')),
    ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
⊢ ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
obtain ⟨z, hz⟩ := h x (f y) y rfl

Premises used: DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : ∀ (x m : L') (x_1 : L), (f : (a : L) → L') x_1 = m → ∃ (y : L), (f : (a : L) → L') y = ⁅x, m⁆
x : L'
y z : L
hz : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') z : L') (⁅x, (f : (a : L) → L') y⁆ : L')
h₁ : Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
⊢ ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
use z