awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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⁆ ⋯)
have lie : ∀
  (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⁆ sorry)
Tactic: revert hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
⊢ 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) x hx)
have mem : ∀ (u : L) (hu : u ∈ s),
  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 sorry)
Tactic: induction hx using lieSpan_induction with
  | mem u hu => exact subset_lieSpan <| by simpa
  | 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 LieSubalgebra.lie_mem _
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
mem :
  ∀ (u : L) (hu : u ∈ s),
    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 ⋯)
⊢ 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) x hx)
have zero : 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) 0 sorry)
Tactic: induction hx using lieSpan_induction with
  | mem u hu => exact subset_lieSpan <| by simpa
  | 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 LieSubalgebra.lie_mem _
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
mem :
  ∀ (u : L) (hu : u ∈ s),
    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 ⋯)
zero :
  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) 0 ⋯)
⊢ 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) x hx)
have add : ∀ (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) sorry)
Tactic: induction hx using lieSpan_induction with
  | mem u hu => exact subset_lieSpan <| by simpa
  | 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 LieSubalgebra.lie_mem _
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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
⊢ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) = lieSpan R (↥K) (range f)
have a : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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)
⊢ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) = lieSpan R (↥K) (range f)
have a₁ : lieSpan R (↥K) (range f) ≤ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (hypothesis)
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 ↥K) (lieSpan R (↥K) (range f)) (Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx)
have hx'₁ : 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'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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
⊢ Membership.mem (γ := LieSubalgebra R ↥K) (lieSpan R (↥K) (range f)) (Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx)
have a : x ∈ map K.incl (lieSpan R (↥K) (range f))
Tactic: suffices x ∈ (lieSpan R K (range f)).map K.incl by aesop
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (hypothesis)
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)
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
have 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))
Tactic: revert hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
have a : ∀ (hu : u ∈ map K.incl (lieSpan R (↥K) (range f))), t • u ∈ map K.incl (lieSpan R (↥K) (range f))
Tactic: revert hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
have 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))
Tactic: revert hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))
have a : ∀ (u : L) (hu : u ∈ range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)), u ∈ 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 _
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))
have a₁ : 0 ∈ 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 _
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))
have 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))
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 _
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))
have 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))
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 _
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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))
⊢ x ∈ map K.incl (lieSpan R (↥K) (range f))
have 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))
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 _
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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
⊢ lieSpan R (↥K) (range f) ≤ comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))
have a : range f ⊆ (↑(comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))) : Set ↥K)
Tactic: rw [lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
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 ∈ (↑(comap K.incl (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f)))) : Set ↥K)
have a : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range (Subtype.val (p := fun (x : L) ↦ x ∈ K) ∘ f))) (↑(f i) : L)
Tactic: simp only [SetLike.mem_coe, mem_comap, coe_incl]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : (↑L₁' : Set L₁) = (↑L₁'' : Set L₁)
⊢ L₁'.toSubmodule = L₁''.toSubmodule
have h₁ : ∀ (x : L₁), x ∈ L₁'.toSubmodule ↔ x ∈ L₁''.toSubmodule
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
h : (↑L₁' : Set L₁) = (↑L₁'' : Set L₁)
x : L₁
⊢ x ∈ (↑L₁' : Set L₁) ↔ x ∈ (↑L₁'' : Set L₁)
have h₁ : x ∈ (↑L₁'' : Set L₁) ↔ x ∈ (↑L₁'' : Set L₁)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (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₂
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⁆ =
    ⁅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⁆
have 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₂)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (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₂
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 = L₂'.toSubmodule
have rw : Submodule.map (↑e.toLinearEquiv : L₁ →ₗ[R] L₂) L₁'.toSubmodule = (LieSubalgebra.map e.toLieHom L₁').toSubmodule
Tactic: rw [← h]