awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
rw : ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)
⊢ (↑(map f I) : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)

Tactic:
rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule, LieIdeal.map, LieSubmodule.coe_lieSpan_submodule_eq_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
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)

Tactic:
⟨J, rfl⟩

Premises used: Exists.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
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)

Tactic:
exact ⟨J, 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
y : L'
h₁ : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h₂ : y ∈ map f I
⊢ ∃ y_1 ∈ (↑I : Submodule R L), ((↑f : L →ₗ[R] L') : (a : L) → L') y_1 = y

Tactic:
rw [← LieSubmodule.mem_toSubmodule, coe_map_of_surjective h₁, Submodule.mem_map] at h₂

Premises used: LieSubmodule.mem_toSubmodule, Submodule.mem_map, LieIdeal.coe_map_of_surjective
-- 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
y : L'
h₁ : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h₂ : ∃ y_1 ∈ (↑I : Submodule R L), ((↑f : L →ₗ[R] L') : (a : L) → L') y_1 = y
obtain :
  ∀ (x : L) (hx : x ∈ (↑I : Submodule R L)),
    ∃ (x_1 : ↥I), Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑x_1 : L) : L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
⊢ ∃ (x : ↥I), (f : (a : L) → L') (↑x : L) = y

Tactic:
obtain ⟨x, hx, rfl⟩ := h₂

Premises used: 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
h₁ : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
x : L
hx : x ∈ (↑I : Submodule R L)
h :
  Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L) : L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
⊢ ∃ (x_1 : ↥I), Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑x_1 : L) : L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')

Tactic:
use ⟨x, hx⟩
-- 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₁ : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
x : L
hx : x ∈ (↑I : Submodule R L)
h h₂ :
  Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L) : L')
    ((f : (a : L) → L') x : L')
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L) : L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')

Tactic:
rw [LieHom.coe_toLinearMap]

Premises used: LieHom.coe_toLinearMap
-- 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₁ : Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h₂ : map f I = ⊥
⊢ comap f ⊥ = ⊥

Tactic:
rw [← f.ker_eq_bot, LieHom.ker] at h₁

Premises used: LieHom.ker_eq_bot, LieHom.ker
-- 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₁ : Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
h₂ : map f I = ⊥
h₃ : comap f ⊥ = ⊥
⊢ map f I = ⊥

Tactic:
rw [← f.ker_eq_bot, LieHom.ker] at h₁

Premises used: LieHom.ker_eq_bot, LieHom.ker
-- 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₁ : comap f ⊥ = ⊥
h₂ : map f I = ⊥
⊢ I ≤ ⊥

Tactic:
rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂

Premises used: LieIdeal.map_le_iff_le_comap, eq_bot_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
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
rw : I ≤ ⊥
⊢ I = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_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
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥

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 : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I ≤ ⊥

Tactic:
exact h₂
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
x : ↥I₁
⊢ (↑((inclusion h : (a : ↥I₁) → ↥I₂) x) : L) = (↑x : L)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
x : ↥I₁
⊢ (inclusion h : (a : ↥I₁) → ↥I₂) x = Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) (↑x : L) ⋯

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
x y : ↥I₁
⊢ Eq (α := ↥I₂) ((inclusion h : (a : ↥I₁) → ↥I₂) x : ↥I₂) ((inclusion h : (a : ↥I₁) → ↥I₂) y : ↥I₂) → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe, imp_self, Subtype.mk_eq_mk, LieIdeal.inclusion_apply
-- 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
⊢ map f (I ⊔ f.ker) = map f I

Tactic:
le_antisymm ?_ (LieIdeal.map_mono le_sup_left)

Premises used: le_sup_left, LieIdeal.map_mono, 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
refine : map f (I ⊔ f.ker) ≤ map f I
⊢ map f (I ⊔ f.ker) = map f I

Tactic:
refine le_antisymm ?_ (LieIdeal.map_mono le_sup_left)

Premises used: le_sup_left, LieIdeal.map_mono, 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
h :
  (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule) : Set L') ⊆
    (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
⊢ map f (I ⊔ f.ker) ≤ map f I

Tactic:
apply LieSubmodule.lieSpan_mono

Premises used: LieSubmodule.lieSpan_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
x : L'
y : L
hy₁ : y ∈ (↑(toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule : Set L)
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
h :
  Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') y : L')
⊢ x ∈ (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')

Tactic:
rw [← hy₂]
-- 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'
y : L
hy₁ : y ∈ (↑(toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule : Set L)
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
⊢ ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y

Tactic:
erw [LieSubmodule.mem_sup] at hy₁

Premises used: LieSubmodule.mem_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'
I : LieIdeal R L
x : L'
y : L
hy₁ : y ∈ (↑(toLieSubalgebra R L (I ⊔ f.ker)).toSubmodule : Set L)
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
hy₃ : ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y
⊢ ((↑f : L →ₗ[R] L') : (a : L) → L') y = x

Tactic:
erw [LieSubmodule.mem_sup] at hy₁

Premises used: LieSubmodule.mem_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'
I : LieIdeal R L
x : L'
y : L
hy₁ : ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
h :
  ∀ (z₁ : L) (hz₁ : z₁ ∈ I) (z₂ : L) (hz₂ : z₂ ∈ f.ker) (hy : z₁ + z₂ = y),
    Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
      (((↑f : L →ₗ[R] L') : (a : L) → L') y : L')
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') y : L')

Tactic:
obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁
-- 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'
y : L
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
h :
  Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') (z₁ + z₂) : L')
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') y : L')

Tactic:
rw [← hy]
-- 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'
y : L
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
h :
  Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') z₁ : L')
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    (((↑f : L →ₗ[R] L') : (a : L) → L') (z₁ + z₂) : L')

Tactic:
rw [map_add, f.coe_toLinearMap, LieHom.mem_ker.mp hz₂, add_zero]

Premises used: map_add, LieHom.coe_toLinearMap, LieHom.mem_ker, Iff.mp, add_zero
-- 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'
y : L
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') z₁ : L')

Tactic:
⟨z₁, hz₁, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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'
y : L
hy₂ : ((↑f : L →ₗ[R] L') : (a : L) → L') y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') z₁ : L')

Tactic:
exact ⟨z₁, hz₁, 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
⊢ map f I ⊔ map f f.ker = map f I

Tactic:
simpa using map_sup_ker_eq_map (f := f)

Premises used: LieIdeal.map_sup_ker_eq_map
-- 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'
h : f.IsIdealMorphism
a : map f (comap f J) ≤ f.idealRange ⊓ J
a₁ : f.idealRange ⊓ J ≤ map f (comap f J)
⊢ map f (comap f J) = f.idealRange ⊓ 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'
J : LieIdeal R L'
h : f.IsIdealMorphism
a : map f (comap f J) ≤ f.idealRange ∧ map f (comap f J) ≤ J
⊢ map f (comap f J) ≤ f.idealRange ⊓ J

Tactic:
rw [le_inf_iff]

Premises used: le_inf_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'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) ≤ f.idealRange ∧ map f (comap f J) ≤ J

Tactic:
⟨f.map_le_idealRange _, map_comap_le⟩

Premises used: And.intro, LieHom.map_le_idealRange, LieIdeal.map_comap_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'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) ≤ f.idealRange ∧ map f (comap f J) ≤ J

Tactic:
exact ⟨f.map_le_idealRange _, map_comap_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'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ toLieSubalgebra R L' f.idealRange = f.range

Tactic:
rw [f.isIdealMorphism_def] at h

Premises used: LieHom.isIdealMorphism_def
-- 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'
h : toLieSubalgebra R L' f.idealRange = f.range
a : (↑f.range : Set L') ∩ (↑J : Set L') ⊆ (↑(map f (comap f J)) : Set L')
⊢ f.idealRange ⊓ J ≤ map f (comap f J)

Tactic:
rw [← SetLike.coe_subset_coe, LieSubmodule.coe_inf, ← coe_toLieSubalgebra, h]

Premises used: LieIdeal.coe_toLieSubalgebra, SetLike.coe_subset_coe, LieSubmodule.coe_inf
-- 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'
h : toLieSubalgebra R L' f.idealRange = f.range
y : L'
h₂ : y ∈ (↑J : Set L')
x : L
h₁ : ((↑f : L →ₗ[R] L') : (a : L) → L') x = y
a :
  ∀ (h₂ : Membership.mem (α := L') (↑J : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L'))
    (h₁ : ((↑f : L →ₗ[R] L') : (a : L) → L') x = y),
    Membership.mem (α := L') (↑(map f (comap f J)) : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
⊢ y ∈ (↑(map f (comap f J)) : Set L')

Tactic:
rw [← h₁] at 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 : LieIdeal R L'
h : toLieSubalgebra R L' f.idealRange = f.range
y : L'
x : L
h₂ : Membership.mem (α := L') (↑J : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
h₁ : ((↑f : L →ₗ[R] L') : (a : L) → L') x = y
⊢ Membership.mem (α := L') (↑(map f (comap f J)) : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')

Tactic:
mem_map h₂

Premises used: Set.Mem, LieIdeal.mem_map
-- 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'
h : toLieSubalgebra R L' f.idealRange = f.range
y : L'
x : L
h₂ : Membership.mem (α := L') (↑J : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
h₁ : ((↑f : L →ₗ[R] L') : (a : L) → L') x = y
⊢ Membership.mem (α := L') (↑(map f (comap f J)) : Set L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')

Tactic:
exact mem_map h₂

Premises used: LieIdeal.mem_map
-- 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 : (↑(comap f (map f I)) : Submodule R L) = (↑(I ⊔ f.ker) : Submodule R L)
rw₁ : Submodule.comap (↑f : L →ₗ[R] L') (↑(map f I) : Submodule R L') = (↑(I ⊔ f.ker) : Submodule R L)
rw₂ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑(I ⊔ f.ker) : Submodule R L)
rw₃ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑I : Submodule R L) ⊔ (↑f.ker : Submodule R L)
rw₄ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker
rw₅ rw₆ : (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker = (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker
⊢ comap f (map f I) = I ⊔ f.ker

Tactic:
rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]

Premises used: LieIdeal.map_toSubmodule, LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule, LieHom.ker_toSubmodule, LieIdeal.comap_toSubmodule, Submodule.comap_map_eq
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.range = toLieSubalgebra R L I

Tactic:
(I : LieSubalgebra R L).incl_range

Premises used: Set.Mem, LieSubalgebra.incl_range, LieIdeal.toLieSubalgebra, LieIdeal.incl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : ↥I
⊢ (I.incl : (a : ↥I) → L) x = (↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ (↑I.incl : ↥I →ₗ[R] L) = (toLieSubalgebra R L I).subtype

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ Function.Injective (α := ↥I) (β := L) (⇑I.incl : (a : ↥I) → L)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : ∀ (m : ↥I), m ∈ comap I.incl I ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊤ m
⊢ comap I.incl I = ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
m : ↥I
⊢ m ∈ comap I.incl I ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊤ m

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : ∀ (m : ↥I), m ∈ I.incl.ker ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊥ m
⊢ I.incl.ker = ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
m : ↥I
⊢ m ∈ I.incl.ker ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊥ m

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
rw : ∃ (N : LieSubmodule R L L), (↑N : Submodule R L) = (↑I : Submodule R L)
⊢ I.incl.idealRange = I

Tactic:
rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, incl_range, toLieSubalgebra_toSubmodule,
    LieSubmodule.coe_lieSpan_submodule_eq_iff]

Premises used: LieSubalgebra.coe_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieIdeal.incl_range, LieSubmodule.toSubmodule_inj, LieSubmodule.coe_lieSpan_submodule_eq_iff, LieHom.idealRange_eq_lieSpan_range
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
w : LieSubmodule R L L
h : (↑I : Submodule R L) = (↑I : Submodule R L)
⊢ ∃ (N : LieSubmodule R L L), (↑N : Submodule R L) = (↑I : Submodule R L)

Tactic:
use I
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
rw : toLieSubalgebra R L I = I.incl.range
⊢ I.incl.IsIdealMorphism

Tactic:
rw [I.incl.isIdealMorphism_def, incl_idealRange]

Premises used: LieHom.isIdealMorphism_def, LieIdeal.incl_idealRange, LieIdeal.incl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ toLieSubalgebra R L I = I.incl.range

Tactic:
(I : LieSubalgebra R L).incl_range.symm

Premises used: Set.Mem, LieSubalgebra.incl_range, LieIdeal.toLieSubalgebra, LieIdeal.incl, Eq.symm
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ toLieSubalgebra R L I = I.incl.range

Tactic:
exact (I : LieSubalgebra R L).incl_range.symm

Premises used: LieSubalgebra.incl_range, LieIdeal.toLieSubalgebra, Eq.symm
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
rw : Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
⊢ comap I.incl I₂ = ⊤ ↔ I ≤ I₂

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule, LieSubmodule.top_toSubmodule,
    incl_coe]

Premises used: LieIdeal.incl_coe, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule