awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 ⁅I, map f (comap f N₂)⁆
| comap f ⁅I, N₂⁆

Tactic:
rw [← map_comap_eq N₂ f hf₂]

Premises used: LieSubmodule.map_comap_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
conv_lhs : comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
⊢ comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆

Tactic:
conv_lhs => rw [← map_comap_eq N₂ f hf₂]

Premises used: LieSubmodule.map_comap_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂⁆
rw₁ rw₂ : ⁅I, comap f N₂⁆ = ⁅I, comap f N₂⁆
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆

Tactic:
rw [← map_bracket_eq, comap_map_eq _ f hf₁]

Premises used: LieSubmodule.comap_map_eq, LieSubmodule.map_bracket_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : {x : L | ∃ (x_1 : ↥I₁) (n : ↥I₂), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)
⊢ map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆

Tactic:
rw [map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Premises used: LieIdeal.map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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)
⊢ x ∈ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)

Tactic:
obtain ⟨⟨y₁, hy₁⟩, ⟨y₂, hy₂⟩, hx⟩ := hx
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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)
⊢ x ∈ (↑(comap f ⁅map f I₁, map f I₂⁆) : Set L)

Tactic:
rw [← hx]
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂) ⋯
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')
⊢ ⁅(↑(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₂⁆

Tactic:
simp only [mem_comap, LieHom.map_lie]

Premises used: LieHom.map_lie, LieIdeal.mem_comap
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂) ⋯
⊢ 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:
LieSubmodule.lie_coe_mem_lie fy₁ fy₂

Premises used: Set.Mem, LieSubmodule.lie_coe_mem_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂) ⋯
⊢ 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:
exact LieSubmodule.lie_coe_mem_lie fy₁ fy₂

Premises used: LieSubmodule.lie_coe_mem_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
this : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Tactic:
le_antisymm (map_bracket_le f) this

Premises used: LieIdeal.map_bracket_le, le_antisymm
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
this : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Tactic:
exact le_antisymm (map_bracket_le f) this

Premises used: LieIdeal.map_bracket_le, le_antisymm
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
suffices : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆

Tactic:
suffices ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆ by exact le_antisymm (map_bracket_le f) this
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
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}))
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆

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]

Premises used: LieSubmodule.toSubmodule_le_toSubmodule, LieIdeal.coe_map_of_surjective, LinearMap.map_span, LieSubmodule.lieIdeal_oper_eq_linear_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
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})
⊢ 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:
apply Submodule.span_mono

Premises used: Submodule.span_mono
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂
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'))
⊢ 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')⁆

Tactic:
obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁

Premises used: LieIdeal.mem_map_of_surjective, rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
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')
⊢ 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₂

Premises used: LieIdeal.mem_map_of_surjective, rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
y₁ : ↥I₁
h₁ : Membership.mem (α := L') (map f I₁) ((f : (a : L) → L') (↑y₁ : L) : L')
y₂ : ↥I₂
h₂ : Membership.mem (α := L') (map f I₂) ((f : (a : L) → L') (↑y₂ : L) : L')
⊢ Eq.{w₂ + 1} (α := L') (((↑f : L →ₗ[R] L') : (a : L) → L') ⁅(↑y₁ : L), (↑y₂ : L)⁆ : L')
    (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:
apply f.map_lie

Premises used: LieHom.map_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')
y₁ : ↥I₁
h₁ : Membership.mem (α := L') (map f I₁) ((f : (a : L) → L') (↑y₁ : L) : L')
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:
exact ⟨⁅(y₁ : L), (y₂ : L)⁆, ⟨y₁, y₂, rfl⟩, by apply f.map_lie⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'
rw : map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆
⊢ ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆

Tactic:
rw [← map_le_iff_le_comap]

Premises used: LieIdeal.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'
⊢ map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆

Tactic:
le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, LieIdeal.map_comap_le, le_trans
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'
⊢ map f ⁅comap f J₁, comap f J₂⁆ ≤ ⁅J₁, J₂⁆

Tactic:
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

Premises used: LieIdeal.map_bracket_le, LieSubmodule.mono_lie, LieIdeal.map_comap_le, le_trans
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
rw : I₁.incl.idealRange ⊓ I₂
| I₁ ⊓ I₂

Tactic:
rw [← I₁.incl_idealRange]

Premises used: LieIdeal.incl_idealRange
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
conv_rhs : map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂
⊢ map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂

Tactic:
conv_rhs => rw [← I₁.incl_idealRange]

Premises used: LieIdeal.incl_idealRange
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I₁ I₂ : LieIdeal R L
rw : I₁.incl.IsIdealMorphism
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂

Tactic:
rw [← map_comap_eq]

Premises used: LieIdeal.map_comap_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₁.incl.IsIdealMorphism

Tactic:
I₁.incl_isIdealMorphism

Premises used: LieIdeal.incl_isIdealMorphism
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₁.incl.IsIdealMorphism

Tactic:
exact I₁.incl_isIdealMorphism

Premises used: LieIdeal.incl_isIdealMorphism
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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}))
⊢ comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker

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]

Premises used: LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule, LinearMap.map_span, LieSubmodule.lieIdeal_oper_eq_linear_span, LieHom.ker_toSubmodule, LieIdeal.comap_toSubmodule, Submodule.comap_map_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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
⊢ 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:
congr
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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
⊢ 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:
ext
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L'
e_p :
  (∃ (a : L'),
      ((∃ (x : L), (f : (a : L) → L') x = a) ∧ a ∈ J₁) ∧
        ∃ (a_1 : L'), ((∃ (x : L), (f : (a : L) → L') x = a_1) ∧ a_1 ∈ J₂) ∧ ⁅a, a_1⁆ = x) ↔
    ∃ (a : L),
      Membership.mem (α := L') J₁ ((f : (a : L) → L') a : L') ∧
        ∃ (b : L),
          Membership.mem (α := L') J₂ ((f : (a : L) → L') b : L') ∧
            Bracket.bracket (L := L') ((f : (a : L) → L') a : L') ((f : (a : L) → L') b) = x
⊢ (∃ (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:
simp_all only [Subtype.exists, LieSubmodule.mem_inf, LieHom.mem_idealRange_iff, exists_prop,
    Set.mem_setOf_eq, LieHom.coe_toLinearMap, mem_comap,
    exists_exists_and_exists_and_eq_and, LieHom.map_lie]

Premises used: LieSubmodule.mem_inf, LieHom.map_lie, Subtype.exists, Set.mem_setOf_eq, exists_prop, LieHom.coe_toLinearMap, exists_exists_and_exists_and_eq_and, LieIdeal.mem_comap, LieHom.mem_idealRange_iff
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L'
⊢ (∃ (a : L'),
      ((∃ (x : L), (f : (a : L) → L') x = a) ∧ a ∈ J₁) ∧
        ∃ (a_1 : L'), ((∃ (x : L), (f : (a : L) → L') x = a_1) ∧ a_1 ∈ J₂) ∧ ⁅a, a_1⁆ = x) ↔
    ∃ (a : L),
      Membership.mem (α := L') J₁ ((f : (a : L) → L') a : L') ∧
        ∃ (b : L),
          Membership.mem (α := L') J₂ ((f : (a : L) → L') b : L') ∧
            Bracket.bracket (L := L') ((f : (a : L) → L') a : L') ((f : (a : L) → L') b) = x

Tactic:
grind
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange
⊢ map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆

Tactic:
rw [← map_sup_ker_eq_map, ← comap_bracket_eq h, map_comap_eq h, inf_eq_right]

Premises used: LieIdeal.map_comap_eq, inf_eq_right, LieIdeal.comap_bracket_eq, LieIdeal.map_sup_ker_eq_map
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange

Tactic:
le_trans (LieSubmodule.lie_le_left _ _) inf_le_left

Premises used: inf_le_left, LieSubmodule.lie_le_left, le_trans
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange

Tactic:
exact le_trans (LieSubmodule.lie_le_left _ _) inf_le_left

Premises used: inf_le_left, LieSubmodule.lie_le_left, le_trans
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
congr : I.incl
J : ⁅I ⊓ I₁, I ⊓ I₂⁆
| comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| I.incl

Tactic:
next => skip