awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
⊢ ∀
    (hu :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx))
    (hv :
      Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
        (lieSpan R (↥(lieSpan R L s))
          (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy)),
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁅u, v⁆ ⋯)

Tactic:
exact LieSubalgebra.lie_mem _

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
a : comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) ≤ lieSpan R (↥K) (range f)
a₁ : lieSpan R (↥K) (range f) ≤ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
⊢ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) = lieSpan R (↥K) (range f)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
hx' :
  Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx ∈
    comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) x

Tactic:
simp only [mem_comap, coe_incl] at hx'

Premises used: LieSubalgebra.mem_comap, LieSubalgebra.coe_incl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
hx' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) x
this : x ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ Membership.mem (γ := LieSubalgebra R ↥K) (lieSpan R (↥K) (range f)) (Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx)

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
hx' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) x
a : x ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ Membership.mem (γ := LieSubalgebra R ↥K) (lieSpan R (↥K) (range f)) (Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx)

Tactic:
suffices x ∈ (lieSpan R K (range f)).map K.incl by aesop
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u : L
hu : u ∈ range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)
⊢ ∀ (i : ι), Membership.mem (γ := LieSubalgebra R ↥K) (lieSpan R (↥K) (range f)) (f i)

Tactic:
have (i : ι) : f i ∈ lieSpan R K (range f) := subset_lieSpan <| mem_range_self i
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u : L
hu : u ∈ range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)
this : ∀ (i : ι), Membership.mem (γ := LieSubalgebra R ↥K) (lieSpan R (↥K) (range f)) (f i)
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
⊢ 0 ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
⊢ 0 ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
hv : v ∈ map K.incl (lieSpan R (↥K) (range f))
a :
  ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    u + v ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ u + v ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu hv
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    u + v ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    u + v ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
a : ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))), t • u ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ t • u ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))), t • u ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
LieSubalgebra.smul_mem _ _

Premises used: LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))), t • u ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact LieSubalgebra.smul_mem _ _

Premises used: LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
hv : v ∈ map K.incl (lieSpan R (↥K) (range f))
a :
  ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu hv
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
lie_mem _

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v
⊢ ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
    ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact lie_mem _

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) x
a : ∀ (u : L) (hu : u ∈ range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)), u ∈ map K.incl (lieSpan R (↥K) (range f))
a₁ : 0 ∈ map K.incl (lieSpan R (↥K) (range f))
a₂ :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v →
        ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
          u + v ∈ map K.incl (lieSpan R (↥K) (range f))
a₃ :
  ∀ (t : R) (u : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u →
      ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))), t • u ∈ map K.incl (lieSpan R (↥K) (range f))
a₄ :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) u →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) v →
        ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))) (hv : v ∈ map K.incl (lieSpan R (↥K) (range f))),
          ⁅u, v⁆ ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
induction hx' using lieSpan_induction with
    | mem u hu =>
      have (i : ι) : f i ∈ lieSpan R K (range f) := subset_lieSpan <| mem_range_self i
      aesop
    | zero => exact zero_mem _
    | add u v _ _ hu hv => revert hu hv; exact add_mem
    | smul t u _ hu => revert hu; exact LieSubalgebra.smul_mem _ _
    | lie u v _ _ hu hv => revert hu hv; exact lie_mem _

Premises used: AddMemClass.add_mem, ZeroMemClass.zero_mem, LieSubalgebra.smul_mem, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
a : range f ⊆ (↑(comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))) : Set ↥K)
⊢ lieSpan R (↥K) (range f) ≤ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))

Tactic:
rw [lieSpan_le]

Premises used: LieSubalgebra.lieSpan_le
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
i : ι
a :
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
    (↑(f i) : L)
⊢ f i ∈ (↑(comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))) : Set ↥K)

Tactic:
simp only [SetLike.mem_coe, mem_comap, coe_incl]

Premises used: LieSubalgebra.mem_comap, SetLike.mem_coe, LieSubalgebra.coe_incl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
i : ι
⊢ (↑(f i) : L) ∈ range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
i : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
    (↑(f i) : L)

Tactic:
exact subset_lieSpan <| by simp

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 rwa rwa₁ rwa₂ rwa₃ : Function.Injective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
⊢ Function.Injective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑(↑f : L₁ →ₗ[R] L₂) : (a : L₁) → L₂)

Tactic:
rwa [LieHom.coe_toLinearMap]

Premises used: LieHom.coe_toLinearMap
-- Module: Mathlib.Algebra.Lie.Subalgebra
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.Injective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
x : L₁
⊢ Eq.{w + 1} (α := L₂) ((↑((ofInjective f h : (a : L₁) → ↥f.range) x) : L₂) : L₂) ((f : (a : L₁) → L₂) x : L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : (↑L₁' : Set L₁) = (↑L₁'' : Set L₁)
h₁ : ∀ (x : L₁), x ∈ L₁'.toSubmodule ↔ x ∈ L₁''.toSubmodule
⊢ L₁'.toSubmodule = L₁''.toSubmodule

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : (↑L₁' : Set L₁) = (↑L₁'' : Set L₁)
x : L₁
h₁ h₂ : x ∈ (↑L₁'' : Set L₁) ↔ x ∈ (↑L₁'' : Set L₁)
⊢ x ∈ (↑L₁' : Set L₁) ↔ x ∈ (↑L₁'' : Set L₁)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L₁ : Type v
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
L L' : LieSubalgebra R L₁
h : (↑L : Set L₁) = (↑L' : Set L₁)
x : ↥L
⊢ (↑((ofEq L L' h : (a : ↥L) → ↥L') x) : L₁) = (↑x : L₁)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
a :
  (↑(AddHom.toFun
          (LinearMap.toAddHom
            (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
              ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
          ⁅x, y⁆) :
      L₂) =
    (↑⁅AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            x,
          AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            y⁆ :
      L₂)
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
          ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
      ⁅x, y⁆ =
    ⁅AddHom.toFun
        (LinearMap.toAddHom
          (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
            ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
        x,
      AddHom.toFun
        (LinearMap.toAddHom
          (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
            ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
        y⁆

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
⊢ (↑(AddHom.toFun
          (LinearMap.toAddHom
            (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
              ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
          ⁅x, y⁆) :
      L₂) =
    (↑⁅AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            x,
          AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            y⁆ :
      L₂)

Tactic:
LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y

Premises used: LieEquiv.toLieHom, LieHom.map_lie, Subtype.val
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
⊢ (↑(AddHom.toFun
          (LinearMap.toAddHom
            (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
              ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
          ⁅x, y⁆) :
      L₂) =
    (↑⁅AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            x,
          AddHom.toFun
            (LinearMap.toAddHom
              (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule) :
                ↥L₁''.toSubmodule →ₗ[R] ↥(Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁''.toSubmodule)))
            y⁆ :
      L₂)

Tactic:
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y

Premises used: LieEquiv.toLieHom, LieHom.map_lie, Subtype.val
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁'' : LieSubalgebra R L₁
e : L₁ ≃ₗ⁅R⁆ L₂
x : ↥L₁''
⊢ Eq.{w + 1} (α := L₂) ((↑((lieSubalgebraMap L₁'' e : (a : ↥L₁'') → ↥(LieSubalgebra.map e.toLieHom L₁'')) x) : L₂) : L₂)
    ((e : (a : L₁) → L₂) (↑x : L₁) : L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
rw : Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁'.toSubmodule = (LieSubalgebra.map e.toLieHom L₁').toSubmodule
⊢ Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁'.toSubmodule = L₂'.toSubmodule

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁'.toSubmodule = (LieSubalgebra.map e.toLieHom L₁').toSubmodule

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
a :
  (↑((↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
          ⁅x, y⁆) :
      L₂) =
    (↑⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            x,
          (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            y⁆ :
      L₂)
⊢ (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
      ⁅x, y⁆ =
    ⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
        x,
      (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
            ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
        y⁆

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Subalgebra
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
⊢ (↑((↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
          ⁅x, y⁆) :
      L₂) =
    (↑⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            x,
          (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            y⁆ :
      L₂)

Tactic:
LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y

Premises used: LieEquiv.toLieHom, LieHom.map_lie, Subtype.val