awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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')
⊢ f.ker = ⊥ ↔ Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
have 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')
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
have rw : (↑f : L →ₗ[R] L').range = ⊤ ↔ Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
Tactic: rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieSubalgebra.top_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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.idealRange = ⊤
have h₁ : f.range = ⊤
Tactic: rw [← f.range_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 = ⊤
⊢ f.idealRange = ⊤
have rw : ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = ⊤
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 = ⊤
⊢ ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = ⊤
have h₁ : Eq.{w₂ + 1} (α := Submodule R L') (↑⊤ : Submodule R L') ⊤
Tactic: use ⊤
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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.IsIdealMorphism
have rw : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
Tactic: rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ f.IsIdealMorphism
have rw₁ : LieIdeal.toLieSubalgebra R L' ⊤ = f.range
Tactic: rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ f.IsIdealMorphism
have rw₂ : Eq (α := LieSubalgebra R L') (LieIdeal.toLieSubalgebra R L' ⊤) ⊤
Tactic: rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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' ⊤) ⊤
⊢ f.IsIdealMorphism
have rw₃ : Eq.{w₂ + 1} (α := LieSubalgebra R L') ⊤ ⊤
Tactic: rw [isIdealMorphism_def, f.idealRange_eq_top_of_surjective h, f.range_eq_top.mpr h,
    LieIdeal.top_toLieSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
have rw : map f I ≤ ⊥ ↔ I ≤ f.ker
Tactic: rw [← le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
have hy' : ∃ x ∈ I, (f : (a : L) → L') x = y
Tactic: have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
have 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')
Tactic: obtain ⟨z₂, hz₂, rfl⟩ := hy'
Cleared hypotheses: y, hy, hy'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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')
⊢ Membership.mem (α := L') (Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule).carrier
    (⁅x, (f : (a : L) → L') z₂⁆ : L')
have 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')
Tactic: obtain ⟨z₁, rfl⟩ := h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ 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')
have 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')
Tactic: simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, Submodule.mem_carrier,
          Submodule.map_coe]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ ∃ 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')
have 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')
Tactic: use ⁅z₁, z₂⁆
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 := ⋯ }
⊢ (↑(map f I) : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)
have rw : ∃ (N : LieSubmodule R L' L'), (↑N : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)
Tactic: rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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
⊢ ∃ (x : ↥I), (f : (a : L) → L') (↑x : L) = y
have h₃ : ∃ 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₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ ∃ (x : ↥I), (f : (a : L) → L') (↑x : L) = y
have 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')
Tactic: obtain ⟨x, hx, rfl⟩ := h₂
Cleared hypotheses: y, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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)
⊢ ∃ (x_1 : ↥I), Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') (↑x_1 : L) : L') (((↑f : L →ₗ[R] L') : (a : L) → L') x : L')
have 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')
Tactic: use ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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)
⊢ 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')
have 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')
Tactic: rw [LieHom.coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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 = ⊥
⊢ I = ⊥
have h₃ : comap f ⊥ = ⊥
Tactic: rw [← f.ker_eq_bot, LieHom.ker] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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 = ⊥
have h₃ : I ≤ ⊥
Tactic: rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
have refine : map f (I ⊔ f.ker) ≤ map f I
Tactic: refine le_antisymm ?_ (LieIdeal.map_mono le_sup_left)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
have 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')
Tactic: apply LieSubmodule.lieSpan_mono
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ x ∈ (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
have 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')
Tactic: rw [← hy₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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
⊢ 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')
have hy₃ : ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y
Tactic: erw [LieSubmodule.mem_sup] at hy₁
Cleared hypotheses: hy₁, hy₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ 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')
have 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')
Tactic: obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁
Cleared hypotheses: hy₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 : L →ₗ[R] L') : (a : L) → L') y : L')
have 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')
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 : L →ₗ[R] L') : (a : L) → L') (z₁ + z₂) : L')
have h : Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
  ((f : (a : L) → L') z₁ : L')
Tactic: rw [map_add, f.coe_toLinearMap, LieHom.mem_ker.mp hz₂, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 ⊓ J
have a : map f (comap f J) ≤ f.idealRange ⊓ J
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ map f (comap f J) = f.idealRange ⊓ J
have a₁ : f.idealRange ⊓ J ≤ map f (comap f J)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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 ⊓ J
have a : map f (comap f J) ≤ f.idealRange ∧ map f (comap f J) ≤ J
Tactic: rw [le_inf_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (hypothesis)
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
⊢ f.idealRange ⊓ J ≤ map f (comap f J)
have h₁ : toLieSubalgebra R L' f.idealRange = f.range
Tactic: rw [f.isIdealMorphism_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ f.idealRange ⊓ J ≤ map f (comap f J)
have a : (↑f.range : Set L') ∩ (↑J : Set L') ⊆ (↑(map f (comap f J)) : Set L')
Tactic: rw [← SetLike.coe_subset_coe, LieSubmodule.coe_inf, ← coe_toLieSubalgebra, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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
⊢ y ∈ (↑(map f (comap f J)) : Set L')
have 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')
Tactic: rw [← h₁] at h₂ ⊢
Cleared hypotheses: h₂, h₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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)
⊢ comap f (map f I) = I ⊔ f.ker
have rw : (↑(comap f (map f I)) : Submodule R L) = (↑(I ⊔ f.ker) : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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)
⊢ comap f (map f I) = I ⊔ f.ker
have rw₁ : Submodule.comap (↑f : L →ₗ[R] L') (↑(map f I) : Submodule R L') = (↑(I ⊔ f.ker) : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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)
⊢ comap f (map f I) = I ⊔ f.ker
have rw₂ : Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
  (↑(I ⊔ f.ker) : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]