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'
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')
⊢ Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
hz.symm

Premises used: Eq.symm
-- 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')
⊢ Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')

Tactic:
exact hz.symm

Premises used: Eq.symm
-- 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 : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
x y : L'
z : L
hz : (f : (a : L) → L') z = y
mpr :
  ∀ (w : L) (hw : Eq (α := L') (⁅x, (f : (a : L) → L') z⁆ : L') ((f : (a : L) → L') w : L')),
    ∃ (y_1 : L), (f : (a : L) → L') y_1 = ⁅x, y⁆
⊢ ∃ (y_1 : L), (f : (a : L) → L') y_1 = ⁅x, y⁆

Tactic:
obtain ⟨w, hw⟩ := h x z
-- 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 : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
x y : L'
z : L
hz : (f : (a : L) → L') z = y
w : L
hw : Eq (α := L') (⁅x, (f : (a : L) → L') z⁆ : L') ((f : (a : L) → L') w : L')
h₁ : (f : (a : L) → L') w = ⁅x, y⁆
⊢ ∃ (y_1 : L), (f : (a : L) → L') y_1 = ⁅x, y⁆

Tactic:
use w
-- 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 : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
x y : L'
z : L
hz : (f : (a : L) → L') z = y
w : L
hw : Eq (α := L') (⁅x, (f : (a : L) → L') z⁆ : L') ((f : (a : L) → L') w : L')
h₁ : ⁅x, (f : (a : L) → L') z⁆ = ⁅x, y⁆
h₂ h₃ : ⁅x, y⁆ = ⁅x, y⁆
⊢ (f : (a : L) → L') w = ⁅x, y⁆

Tactic:
rw [← hw, hz]
-- 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.range : Set L') ⊆ (↑f.idealRange : Set L')

Tactic:
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
rw : LieIdeal.map f I ≤ LieIdeal.map f ⊤
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
rw [f.idealRange_eq_map]

Premises used: LieHom.idealRange_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'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤

Tactic:
LieIdeal.map_mono le_top

Premises used: LieIdeal.map_mono, le_top
-- 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
⊢ LieIdeal.map f I ≤ LieIdeal.map f ⊤

Tactic:
exact LieIdeal.map_mono le_top

Premises used: LieIdeal.map_mono, le_top
-- 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'
⊢ f.ker ≤ LieIdeal.comap f J

Tactic:
LieIdeal.comap_mono bot_le

Premises used: Set.Mem, LieIdeal.comap_mono, bot_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'
⊢ (↑f.ker : Submodule R L) = (↑f : L →ₗ[R] L').ker

Tactic:
rfl

Premises used: LinearMap.ker, 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'
x : L
⊢ x ∈ (↑f.ker : Submodule R L) ↔ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')

Tactic:
simp only [ker_toSubmodule, LinearMap.mem_ker, coe_toLinearMap]

Premises used: LinearMap.mem_ker, LieHom.coe_toLinearMap, LieHom.ker_toSubmodule
-- 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'
x : L
rw : Membership.mem (α := L') (LieIdeal.map f ⊤) ((f : (a : L) → L') x : L')
⊢ Membership.mem (α := L') f.idealRange ((f : (a : L) → L') x : L')

Tactic:
rw [idealRange_eq_map]

Premises used: LieHom.idealRange_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'
x : L
⊢ Membership.mem (α := L') (LieIdeal.map f ⊤) ((f : (a : L) → L') x : L')

Tactic:
LieIdeal.mem_map (LieSubmodule.mem_top x)

Premises used: LieSubmodule.mem_top, 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'
x : L
⊢ Membership.mem (α := L') (LieIdeal.map f ⊤) ((f : (a : L) → L') x : L')

Tactic:
exact LieIdeal.mem_map (LieSubmodule.mem_top x)

Premises used: LieSubmodule.mem_top, 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'
h : f.IsIdealMorphism
y : L'
rw :
  ∀ (h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range) {y : L'},
    y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y

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'
h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
rw : y ∈ (↑f.idealRange : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
rw₁ : y ∈ (↑(LieIdeal.toLieSubalgebra R L' f.idealRange) : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
rw₂ : y ∈ (↑f.range : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
rw₃ :
  Membership.mem (γ := Set L') (Set.range.{w₂, v + 1} (ι := L) (⇑f : (a : L) → L')) y ↔
    ∃ (x : L), (f : (a : L) → L') x = y
rw₄ rw₅ : (∃ (y_1 : L), (f : (a : L) → L') y_1 = y) ↔ ∃ (x : L), (f : (a : L) → L') x = y
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y

Tactic:
rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]

Premises used: Set.mem_range, LieIdeal.coe_toLieSubalgebra, LieHom.coe_range, LieSubmodule.mem_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
mp : I ≤ f.ker → ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
mpr : (∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')) → I ≤ f.ker
⊢ I ≤ f.ker ↔ ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : 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'
I : LieIdeal R L
h : I ≤ f.ker
x : L
hx : x ∈ I
⊢ x ∈ f.ker

Tactic:
specialize h 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
x : L
hx : x ∈ I
h : x ∈ f.ker
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')

Tactic:
rw [mem_ker] at h

Premises used: LieHom.mem_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
x : L
hx : x ∈ I
h : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')

Tactic:
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
x : L
hx : x ∈ I
h : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')

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'
I : LieIdeal R L
h : ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
x : L
hx : x ∈ I
mpr : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
⊢ x ∈ f.ker

Tactic:
rw [mem_ker]

Premises used: LieHom.mem_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 : ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
x : L
hx : x ∈ I
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')

Tactic:
apply h 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'
rw :
  (↑f.ker : Submodule R L) = (↑⊥ : Submodule R L) ↔
    Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw₁ :
  (↑f : L →ₗ[R] L').ker = (↑⊥ : Submodule R L) ↔
    Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw₂ : (↑f : L →ₗ[R] L').ker = ⊥ ↔ Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw₃ :
  Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑(↑f : L →ₗ[R] L') : (a : L) → L') ↔
    Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw₄ rw₅ :
  Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L') ↔
    Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ f.ker = ⊥ ↔ Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')

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, LieSubmodule.toSubmodule_inj, LieHom.coe_toLinearMap, LieHom.ker_toSubmodule
-- 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.range.toSubmodule = (↑f : L →ₗ[R] L').range

Tactic:
rfl

Premises used: LinearMap.range, rfl, Submodule.copy
-- 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'
rw : (↑f : L →ₗ[R] L').range = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ f.range = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieSubalgebra.top_toSubmodule]

Premises used: LieSubalgebra.top_toSubmodule, LieSubalgebra.toSubmodule_inj, LieHom.range_toSubmodule
-- 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 : L →ₗ[R] L').range = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')

Tactic:
LinearMap.range_eq_top

Premises used: LinearMap.range_eq_top
-- 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 : L →ₗ[R] L').range = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')

Tactic:
exact LinearMap.range_eq_top

Premises used: LinearMap.range_eq_top
-- 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 : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ f.range = ⊤

Tactic:
rw [← f.range_eq_top] at h

Premises used: LieHom.range_eq_top
-- 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 : f.range = ⊤
rw : ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = ⊤
⊢ f.idealRange = ⊤

Tactic:
rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, LieSubmodule.top_toSubmodule,
    LieSubalgebra.top_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]

Premises used: LieSubalgebra.top_toSubmodule, LieSubalgebra.coe_toSubmodule, LieSubmodule.top_toSubmodule, 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
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 : f.range = ⊤
h₁ : Eq.{w₂ + 1} (α := Submodule R L') (↑⊤ : Submodule R L') ⊤
⊢ ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = ⊤

Tactic:
use ⊤
-- 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 : f.range = ⊤
⊢ Eq.{w₂ + 1} (α := Submodule R L') (↑⊤ : Submodule R L') ⊤

Tactic:
LieSubmodule.top_toSubmodule

Premises used: LieSubmodule.top_toSubmodule
-- 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 : f.range = ⊤
⊢ Eq.{w₂ + 1} (α := Submodule R L') (↑⊤ : Submodule R L') ⊤

Tactic:
exact LieSubmodule.top_toSubmodule

Premises used: LieSubmodule.top_toSubmodule
-- 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 : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
rw : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
rw₁ : LieIdeal.toLieSubalgebra R L' ⊤ = f.range
rw₂ : Eq (α := LieSubalgebra R L') (LieIdeal.toLieSubalgebra R L' ⊤) ⊤
rw₃ rw₄ : Eq.{w₂ + 1} (α := LieSubalgebra R L') ⊤ ⊤
⊢ f.IsIdealMorphism

Tactic:
rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]

Premises used: Iff.mpr, LieHom.isIdealMorphism_def, LieHom.range_eq_top, LieIdeal.top_toLieSubalgebra, LieHom.idealRange_eq_top_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
rw : map f I ≤ ⊥ ↔ I ≤ f.ker
⊢ map f I = ⊥ ↔ I ≤ f.ker

Tactic:
rw [← le_bot_iff]

Premises used: le_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
⊢ map f I ≤ ⊥ ↔ I ≤ f.ker

Tactic:
LieIdeal.map_le_iff_le_comap

Premises used: Set.Mem, 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
⊢ map f I ≤ ⊥ ↔ I ≤ f.ker

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

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

Tactic:
have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [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
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
x y : L'
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
hy' : ∃ x ∈ I, (f : (a : L) → L') x = y
obtain :
  ∀ (z₂ : L) (hz₂ : z₂ ∈ I)
    (hy :
      Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
        ((f : (a : L) → L') z₂ : L')),
    Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
      (⁅x, (f : (a : L) → L') z₂⁆ : L')
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier

Tactic:
obtain ⟨z₂, hz₂, rfl⟩ := hy'

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'
z₂ : L
hz₂ : z₂ ∈ I
hy :
  Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    ((f : (a : L) → L') z₂ : L')
obtain :
  ∀ (z₁ : L),
    Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')
⊢ Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    (⁅x, (f : (a : L) → L') z₂⁆ : L')

Tactic:
obtain ⟨z₁, rfl⟩ := h x

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')
z₂ : L
hz₂ : z₂ ∈ I
hy :
  Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    ((f : (a : L) → L') z₂ : L')
z₁ : L
simp :
  ∃ x ∈ (toLieSubalgebra R L I).toSubmodule,
    Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L')
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')
⊢ Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')

Tactic:
simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, Submodule.mem_carrier,
          Submodule.map_coe]

Premises used: Set.mem_image, LieHom.coe_toLinearMap, SetLike.mem_coe, Submodule.mem_carrier, 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 : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
z₂ : L
hz₂ : z₂ ∈ I
hy :
  Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    ((f : (a : L) → L') z₂ : L')
z₁ : L
h₁ :
  ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧
    Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') ⁅z₁, z₂⁆ : L')
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')
⊢ ∃ x ∈ (toLieSubalgebra R L I).toSubmodule,
    Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L')
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')

Tactic:
use ⁅z₁, z₂⁆
-- 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')
z₂ : L
hz₂ : z₂ ∈ I
hy :
  Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    ((f : (a : L) → L') z₂ : L')
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧
    Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') ⁅z₁, z₂⁆ : L')
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')

Tactic:
⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩

Premises used: LieHom.map_lie, LieSubmodule.lie_mem, And.intro
-- 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')
z₂ : L
hz₂ : z₂ ∈ I
hy :
  Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    ((f : (a : L) → L') z₂ : L')
z₁ : L
⊢ ⁅z₁, z₂⁆ ∈ (toLieSubalgebra R L I).toSubmodule ∧
    Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') ⁅z₁, z₂⁆ : L')
      (Bracket.bracket (L := L') ((f : (a : L) → L') z₁ : L') ((f : (a : L) → L') z₂) : L')

Tactic:
exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩