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₂
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
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L') (toLieSubalgebra R L' J).toSubmodule).carrier
have suffices : Membership.mem (α := L') J (Bracket.bracket (L := L') ((f : (a : L) → L') x : L') ((f : (a : L) → L') y) : L')
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
-- 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)
⊢ (↑(map f I) : Submodule R L') = Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)
have 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))
Tactic: rw [SetLike.ext'_iff, LieSubmodule.coe_toSubmodule, h, 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
x : L
hx : x ∈ I
⊢ Membership.mem (α := L') (map f I) ((f : (a : L) → L') x : L')
have a : Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
  ((f : (a : L) → L') x : L')
Tactic: apply LieSubmodule.subset_lieSpan
-- 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
hx : x ∈ I
⊢ Membership.mem (α := L') (↑(Submodule.map (↑f : L →ₗ[R] L') (toLieSubalgebra R L I).toSubmodule) : Set L')
    ((f : (a : L) → L') x : L')
have 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')
Tactic: use 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
J : LieIdeal R L'
⊢ map f I ≤ J ↔ I ≤ comap f J
have rw : (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑J : Set L') ↔ I ≤ comap f J
Tactic: rw [map_le]
-- 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'
⊢ map f (comap f J) ≤ J
have rw : comap f J ≤ comap f J
Tactic: rw [map_le_iff_le_comap]
-- 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
⊢ I ≤ comap f (map f I)
have rw : map f I ≤ map f I
Tactic: rw [← map_le_iff_le_comap]
-- 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₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ 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'))
have h₁ : (toLieSubalgebra R L I₁).toSubmodule ≤ (toLieSubalgebra R L I₂).toSubmodule
Tactic: gcongr
-- 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₁ J₂ : LieIdeal R L'
h : J₁ ≤ J₂
⊢ comap f J₁ ≤ comap f J₂
have h₁ : (↑J₁ : Set L') ⊆ (↑J₂ : Set L')
Tactic: rw [← SetLike.coe_subset_coe] 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
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ map f I = J
have a : map f I ≤ 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'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
a : map f I ≤ J
⊢ map f I = J
have a₁ : J ≤ map f I
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'
I : LieIdeal R L
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ map f I ≤ J
have a : (⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(toLieSubalgebra R L I).toSubmodule : Set L) ⊆ (↑J : Set L')
Tactic: rw [map, LieSubmodule.lieSpan_le, 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
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ (⇑(↑f : L →ₗ[R] L') : (a : L) → L') '' (↑(toLieSubalgebra R L I).toSubmodule : Set L) ⊆ (↑J : Set L')
have a : (↑J : Set L') ⊆ (↑J : Set L')
Tactic: erw [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
J : LieIdeal R L'
h : (⇑f : (a : L) → L') '' (↑I : Set L) = (↑J : Set L')
⊢ J ≤ map f I
have a : (⇑f : (a : L) → L') '' (↑I : Set L) ⊆ (↑(map f I) : Set L')
Tactic: rw [← SetLike.coe_subset_coe, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
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'
⊢ Subsingleton.{v + 1} (LieIdeal R ↥⊥)
have hα : Eq.{v + 1} (α := LieIdeal R ↥⊥) ⊥ ⊤
Tactic: apply subsingleton_of_bot_eq_top
-- 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.idealRange = LieIdeal.map f ⊤
have h : ∀ (m : L'), m ∈ f.idealRange ↔ m ∈ LieIdeal.map f ⊤
Tactic: ext
-- 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'
m : L'
⊢ m ∈ f.idealRange ↔ m ∈ LieIdeal.map f ⊤
have h : Membership.mem (γ := LieSubmodule R L' L') (LieSubmodule.lieSpan R L' (↑(LieSubalgebra.map f ⊤) : Set L')) m ↔
  m ∈ LieIdeal.map f ⊤
Tactic: simp only [idealRange, range_eq_map]
-- 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.IsIdealMorphism ↔
    ∀ (x : L') (y : L), ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
have 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')
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]
-- 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'
⊢ (∀ (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')
have 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')
Tactic: constructor
-- 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'
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')
⊢ (∀ (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')
have 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⁆
Tactic: constructor
-- 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 : ∀ (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')
have 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')
Tactic: obtain ⟨z, hz⟩ := h x (f y) y rfl
-- 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 : ∀ (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')
⊢ ∃ (z : L), Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
have h₁ : Eq (α := L') (⁅x, (f : (a : L) → L') y⁆ : L') ((f : (a : L) → L') z : L')
Tactic: use 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'
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
⊢ ∃ (y_1 : L), (f : (a : L) → L') y_1 = ⁅x, y⁆
have 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⁆
Tactic: obtain ⟨w, hw⟩ := h x 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'
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')
⊢ ∃ (y_1 : L), (f : (a : L) → L') y_1 = ⁅x, y⁆
have h₁ : (f : (a : L) → L') w = ⁅x, y⁆
Tactic: use w
-- 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 : ∀ (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')
⊢ (f : (a : L) → L') w = ⁅x, y⁆
have h₁ : ⁅x, (f : (a : L) → L') z⁆ = ⁅x, y⁆
Tactic: rw [← hw, hz]
-- 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 : ∀ (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⁆
⊢ (f : (a : L) → L') w = ⁅x, y⁆
have h₂ : ⁅x, y⁆ = ⁅x, y⁆
Tactic: rw [← hw, hz]
-- 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
⊢ LieIdeal.map f I ≤ f.idealRange
have rw : LieIdeal.map f I ≤ LieIdeal.map f ⊤
Tactic: rw [f.idealRange_eq_map]
-- 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'
x : L
⊢ Membership.mem (α := L') f.idealRange ((f : (a : L) → L') x : L')
have rw : Membership.mem (α := L') (LieIdeal.map f ⊤) ((f : (a : L) → L') x : L')
Tactic: rw [idealRange_eq_map]
-- 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.IsIdealMorphism
y : L'
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw : ∀ (h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range) {y : L'},
  y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [f.isIdealMorphism_def] at h
Cleared hypotheses: h, y
-- 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 : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw : y ∈ (↑f.idealRange : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]
-- 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 : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
rw : y ∈ (↑f.idealRange : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw₁ : y ∈ (↑(LieIdeal.toLieSubalgebra R L' f.idealRange) : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]
-- 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 : 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
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw₂ : y ∈ (↑f.range : Set L') ↔ ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]
-- 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 : 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
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw₃ : Membership.mem (γ := Set L') (Set.range.{w₂, v + 1} (ι := L) (⇑f : (a : L) → L')) y ↔
  ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]
-- 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 : 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
⊢ y ∈ f.idealRange ↔ ∃ (x : L), (f : (a : L) → L') x = y
have rw₄ : (∃ (y_1 : L), (f : (a : L) → L') y_1 = y) ↔ ∃ (x : L), (f : (a : L) → L') x = y
Tactic: rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.coe_range, Set.mem_range]
-- 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
⊢ I ≤ f.ker ↔ ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
have mp : I ≤ f.ker → ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
Tactic: constructor
-- 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
mp : I ≤ f.ker → ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
⊢ I ≤ f.ker ↔ ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
have mpr : (∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')) → I ≤ f.ker
Tactic: constructor
-- 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 : I ≤ f.ker
x : L
hx : x ∈ I
⊢ Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
have h₁ : x ∈ f.ker
Tactic: specialize h hx
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
h : ∀ x ∈ I, Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
x : L
hx : x ∈ I
⊢ x ∈ f.ker
have mpr : Eq.{w₂ + 1} (α := L') ((f : (a : L) → L') x : L') (0 : L')
Tactic: rw [mem_ker]
-- 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.ker = ⊥ ↔ Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
have rw : (↑f.ker : Submodule R L) = (↑⊥ : Submodule R 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'
rw :
  (↑f.ker : Submodule R L) = (↑⊥ : Submodule R 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₁ : (↑f : L →ₗ[R] L').ker = (↑⊥ : Submodule R 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'
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')
⊢ f.ker = ⊥ ↔ Function.Injective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
have rw₂ : (↑f : L →ₗ[R] L').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]
-- 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')
⊢ 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 : L →ₗ[R] L') : (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]