awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have left : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
Tactic: constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have right : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
Tactic: constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₁ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₁ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₂ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₂ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₃ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₃ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have left₄ : N ⊓ N' ≤ N
Tactic: constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₁ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₁ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₂ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₂ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₃ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆
right₃ : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
left₄ : N ⊓ N' ≤ N
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have right₄ : N ⊓ N' ≤ N'
Tactic: constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆
have rw : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
Tactic: rw [le_inf_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have right : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
have left : I ⊓ J ≤ I
Tactic: apply mono_lie_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have right : I ⊓ J ≤ J
Tactic: apply mono_lie_left
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
Tactic: constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have right : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
Tactic: constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₁ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₁ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₂ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₂ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₃ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₃ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have left₄ : I ⊓ J ≤ I
Tactic: constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₁ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₁ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₂ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₂ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₃ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₃ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₄ : I ⊓ J ≤ I
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
have right₄ : I ⊓ J ≤ J
Tactic: constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
⊢ map f ⁅I, N⁆ = ⁅I, map f N⁆
have rw : Eq.{w₁ + 1} (α := Submodule R M₂)
  (Submodule.span R
    (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
      {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}))
  (Submodule.span R {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x})
Tactic: rw [← toSubmodule_inj, toSubmodule_map, lieIdeal_oper_eq_linear_span,
    lieIdeal_oper_eq_linear_span, Submodule.map_span]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
⊢ Eq.{w₁ + 1} (α := Submodule R M₂)
    (Submodule.span R
      (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
        {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}))
    (Submodule.span R {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x})
have e_s : Eq.{w₁ + 1} (α := Set M₂)
  (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
    {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
  {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x}
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
⊢ Eq.{w₁ + 1} (α := Set M₂)
    (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
      {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x}
have e_s : ∀ (m : M₂),
  Membership.mem (γ := Set M₂)
      (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
        {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
      m ↔
    Membership.mem (γ := Set M₂) {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x} m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
| comap f ⁅I, N₂⁆
have rw : comap f ⁅I, map f (comap f N₂)⁆
Tactic: rw [← map_comap_eq N₂ f hf₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆
have conv_lhs : comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
Tactic: conv_lhs => rw [← map_comap_eq N₂ f hf₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
have rw : comap f (map f ⁅I, comap f N₂⁆) = ⁅I, comap f N₂⁆
Tactic: rw [← map_bracket_eq, comap_map_eq _ f hf₁]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
rw : comap f (map f ⁅I, comap f N₂⁆) = ⁅I, comap f N₂⁆
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
have rw₁ : ⁅I, comap f N₂⁆ = ⁅I, comap f N₂⁆
Tactic: rw [← map_bracket_eq, comap_map_eq _ f hf₁]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆
have rw : {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
Tactic: rw [map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
x : L
hx : Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x} x
⊢ x ∈ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
have obtain : ∀ (y₁ : L) (hy₁ : y₁ ∈ I₁) (y₂ : L) (hy₂ : y₂ ∈ I₂)
  (hx :
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₁) y₁ hy₁) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) y₂ hy₂) : L)⁆ =
      x),
  x ∈ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
Tactic: obtain ⟨⟨y₁, hy₁⟩, ⟨y₂, hy₂⟩, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx :
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₁) y₁ hy₁) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) y₂ hy₂) : L)⁆ = x
⊢ x ∈ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
have rw : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₁) y₁ hy₁) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) y₂ hy₂) : L)⁆ ∈
  (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx :
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₁) y₁ hy₁) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) y₂ hy₂) : L)⁆ = x
fy₁ : ↥(map f I₁) := Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₁) ((f : (a : L) → L') y₁) ⋯
fy₂ : ↥(map f I₂) := Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₂) ((f : (a : L) → L') y₂) ⋯
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₁) y₁ hy₁) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I₂) y₂ hy₂) : L)⁆ ∈
    comap f ⁅map f I₁, map f I₂⁆
have simp : Membership.mem (α := L') ⁅map f I₁, map f I₂⁆
  (Bracket.bracket (L := L') ((f : (a : L) → L') y₁ : L') ((f : (a : L) → L') y₂) : L')
Tactic: simp only [mem_comap, LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆
have suffices : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
Tactic: suffices ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆ by exact le_antisymm (map_bracket_le f) this
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
have rw : LE.le.{w₂} (α := Submodule R L')
  (Submodule.span R {x : L' | ∃ (x_1 : ↥(map f I₁)) (n : ↥(map f I₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x})
  (Submodule.span R
    (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
      {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x}))
Tactic: rw [← LieSubmodule.toSubmodule_le_toSubmodule, coe_map_of_surjective h,
    LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LinearMap.map_span]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
⊢ LE.le.{w₂} (α := Submodule R L')
    (Submodule.span R {x : L' | ∃ (x_1 : ↥(map f I₁)) (n : ↥(map f I₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x})
    (Submodule.span R
      (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
        {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x}))
have h₁ : Subset.{w₂} (α := Set L') {x : L' | ∃ (x_1 : ↥(map f I₁)) (n : ↥(map f I₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x}
  (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
    {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
Tactic: apply Submodule.span_mono
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ Membership.mem (γ := Set L')
    (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
      {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
    ⁅(↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₁) z₁ h₁) : L'),
      (↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₂) z₂ h₂) : L')⁆
have h₃ : ∀ (y₁ : ↥I₁) (h₁ : Membership.mem (α := L') (map f I₁) ((f : (a : L) → L') (↑y₁ : L) : L')),
  Membership.mem (γ := Set L')
    (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
      {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
    (Bracket.bracket (L := L')
      ((↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₁) ((f : (a : L) → L') (↑y₁ : L)) h₁) : L') : L')
      (↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₂) z₂ h₂) : L'))
Tactic: obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁
Cleared hypotheses: z₁, h₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective.{v + 1, w₂ + 1} (α := L) (β := L') (⇑f : (a : L) → L')
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : ↥I₁
h₁ : Membership.mem (α := L') (map f I₁) ((f : (a : L) → L') (↑y₁ : L) : L')
⊢ Membership.mem (γ := Set L')
    (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
      {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
    (Bracket.bracket (L := L')
      ((↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₁) ((f : (a : L) → L') (↑y₁ : L)) h₁) : L') : L')
      (↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₂) z₂ h₂) : L'))
have h₃ : ∀ (y₂ : ↥I₂) (h₂ : Membership.mem (α := L') (map f I₂) ((f : (a : L) → L') (↑y₂ : L) : L')),
  Membership.mem.{w₂, w₂} (α := L') (γ := Set L')
    (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
      {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
    (Bracket.bracket (L := L')
        ((↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₁) ((f : (a : L) → L') (↑y₁ : L)) h₁) : L') : L')
        (↑(Subtype.mk (p := fun (x : L') ↦ x ∈ map f I₂) ((f : (a : L) → L') (↑y₂ : L)) h₂) : L') :
      L')
Tactic: obtain ⟨y₂, rfl⟩ := mem_map_of_surjective h h₂
Cleared hypotheses: z₂, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
⊢ ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆
have rw : map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆
Tactic: rw [← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
| I₁ ⊓ I₂
have rw : I₁.incl.idealRange ⊓ I₂
Tactic: rw [← I₁.incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂
have conv_rhs : map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂
Tactic: conv_rhs => rw [← I₁.incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂
have rw : I₁.incl.IsIdealMorphism
Tactic: rw [← map_comap_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker
have rw : Submodule.comap (↑f : L →ₗ[R] L')
    (Submodule.span R
      {x : L' | ∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x}) =
  Submodule.comap (↑f : L →ₗ[R] L')
    (Submodule.span R
      (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
        {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x}))
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, ← Submodule.comap_map_eq,
    LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
    LinearMap.map_span]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f : L →ₗ[R] L')
      (Submodule.span R
        {x : L' | ∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x}) =
    Submodule.comap (↑f : L →ₗ[R] L')
      (Submodule.span R
        (Set.image.{v, w₂} (α := L) (⇑(↑f : L →ₗ[R] L') : (a : L) → L')
          {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x}))
have e_p : Eq.{w₂ + 1} (α := L' → Prop)
  (fun (x : L') ↦ ∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x)
  fun (x : L') ↦
  ∃ (a : L),
    Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x} a ∧
      ((↑f : L →ₗ[R] L') : (a : L) → L') a = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Eq.{w₂ + 1} (α := L' → Prop)
    (fun (x : L') ↦ ∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x)
    fun (x : L') ↦
    ∃ (a : L),
      Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x} a ∧
        ((↑f : L →ₗ[R] L') : (a : L) → L') a = x
have e_p : ∀ (x : L'),
  (∃ (x_1 : ↥(f.idealRange ⊓ J₁)) (n : ↥(f.idealRange ⊓ J₂)), ⁅(↑x_1 : L'), (↑n : L')⁆ = x) ↔
    ∃ (a : L),
      Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥(comap f J₁)) (n : ↥(comap f J₂)), ⁅(↑x_1 : L), (↑n : L)⁆ = x} a ∧
        ((↑f : L →ₗ[R] L') : (a : L) → L') a = x
Tactic: ext