awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂'
x 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⁆
have a : (↑((↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule sorry) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
        ⁅x, y⁆) :
    L₂) =
  (↑⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule sorry) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
          x,
        (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule sorry) :
              ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
          y⁆ :
    L₂)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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_1 N' N O : LieSubmodule R L M
h :
  Eq.{w + 1} (α := Set M) ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) N)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)
⊢ N = O
have mk : ∀ (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier)
  (h :
    Eq.{w + 1} (α := Set M)
      ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
        { toSubmodule := toSubmodule, lie_mem := @lie_mem })
      ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)),
  { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = O
Tactic: cases N
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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' O : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = O
have mk : ∀ (toSubmodule_1 : Submodule R M)
  (lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier)
  (h :
    Eq.{w + 1} (α := Set M)
      ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
        { toSubmodule := toSubmodule, lie_mem := @lie_mem })
      ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
        { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })),
  { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
    { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }
Tactic: cases O
Cleared hypotheses: O, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
toSubmodule_1 : Submodule R M
lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
    { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }
have mk : toSubmodule = toSubmodule_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
x : L
m : M
h :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) ⁅x, m⁆
have rw : Membership.mem (γ := Set M)
  (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) ⁅x, 0⁆
Tactic: rw [(Submodule.mem_bot R).1 h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
⊢ (↑{ toSubmodule := p, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = p
have mk : ∀ (toAddSubmonoid : AddSubmonoid M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
  (h :
    ∀ {x : L} {m : M},
      m ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier →
        ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier),
  (↑{ toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem := @h : LieSubmodule R L M } : Submodule R M) =
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' }
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
x y : LieSubmodule R L M
h : (↑x : Submodule R M) = (↑y : Submodule R M)
⊢ x = y
have mk : ∀ (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier)
  (h :
    (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) = (↑y : Submodule R M)),
  { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
y : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
h : (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) = (↑y : Submodule R M)
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = y
have mk : ∀ (toSubmodule_1 : Submodule R M)
  (lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier)
  (h :
    (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) =
      (↑{ toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 : LieSubmodule R L M } : Submodule R M)),
  { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
    { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
s : Set M
hs : s = (↑N : Set M)
a b : M
x : a ∈ s
y : b ∈ s
⊢ a + b ∈ s
have rw : ∀ (x : a ∈ (↑N : Set M)) (y : b ∈ (↑N : Set M)), a + b ∈ (↑N : Set M)
Tactic: rw [hs] at x y ⊢
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
x y : L
m : ↥N
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x + y, (↑m : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x + y, (↑m : M)⁆ sorry) : M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ sorry + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ sorry) : M)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
x : L
m n : ↥N
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(m + n) : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑n : M)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(m + n) : M)⁆ sorry) : M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ sorry + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑n : M)⁆ sorry) : M)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
x y : L
m : ↥N
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅⁅x, y⁆, (↑m : M)⁆ ⋯ +
      Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯) : M)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ sorry) : M)⁆ sorry) : M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅⁅x, y⁆, (↑m : M)⁆ sorry +
        Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ sorry) : M)⁆ sorry) :
    M)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
⊢ ⁅t • x, y⁆ = t • ⁅x, y⁆
have a : (↑⁅t • x, y⁆ : M) = (↑(t • ⁅x, y⁆) : M)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have a : (↑⁅x, t • y⁆ : M) = (↑(t • ⁅x, y⁆) : M)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
p : Submodule R M
⊢ (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
have mp : (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
p : Submodule R M
mp : (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
have mpr : (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p
have w : LieSubmodule R L M
Tactic: use { p with lie_mem := @h }
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
w : LieSubmodule R L M
⊢ ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p
have h₁ : (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Submodule R M) = p
Tactic: use { p with lie_mem := @h }
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
⊢ (↑N : Submodule R M) = ⊥ ↔ N = ⊥
have rw : (↑N : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) = (↑⊥ : Submodule R M)
Tactic: rw [← toSubmodule_inj, bot_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
rw : (↑N : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) = (↑⊥ : Submodule R M)
⊢ (↑N : Submodule R M) = ⊥ ↔ N = ⊥
have rw₁ : (↑N : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) = ⊥
Tactic: rw [← toSubmodule_inj, bot_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊥ ↔ N = ⊥
have rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊥ : Submodule R M) ↔ N = ⊥
Tactic: rw [← toSubmodule_inj, bot_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊥ : Submodule R M) ↔ N = ⊥
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊥ ↔ N = ⊥
have rw₁ : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = ⊥ ↔ N = ⊥
Tactic: rw [← toSubmodule_inj, bot_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
⊢ (↑N : Submodule R M) = ⊤ ↔ N = ⊤
have rw : (↑N : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) = (↑⊤ : Submodule R M)
Tactic: rw [← toSubmodule_inj, top_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
rw : (↑N : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) = (↑⊤ : Submodule R M)
⊢ (↑N : Submodule R M) = ⊤ ↔ N = ⊤
have rw₁ : (↑N : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) = ⊤
Tactic: rw [← toSubmodule_inj, top_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊤ ↔ N = ⊤
have rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊤ : Submodule R M) ↔ N = ⊤
Tactic: rw [← toSubmodule_inj, top_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊤ : Submodule R M) ↔ N = ⊤
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊤ ↔ N = ⊤
have rw₁ : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = ⊤ ↔ N = ⊤
Tactic: rw [← toSubmodule_inj, top_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
x : L
m : M
h :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, w} (R := R) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x}))))
    m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, w} (R := R) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x}))))
    ⁅x, m⁆
have simp : ∀ (h : ∀ a ∈ S, m ∈ (↑(↑a : Submodule R M) : Set M)), ∀ a ∈ S, ⁅x, m⁆ ∈ (↑(↑a : Submodule R M) : Set M)
Tactic: simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_setOf_eq,
          forall_apply_eq_imp_iff₂, forall_exists_index, and_imp] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
⊢ (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (↑N : Submodule R M)
have rw : Eq.{w + 1} (α := Submodule R M) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x})
  (⨅ N ∈ S, (↑N : Submodule R M))
Tactic: rw [sInf_toSubmodule, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
rw :
  Eq.{w + 1} (α := Submodule R M) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x})
    (⨅ N ∈ S, (↑N : Submodule R M))
⊢ (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (↑N : Submodule R M)
have rw₁ : sInf (toSubmodule '' S) = ⨅ N ∈ S, (↑N : Submodule R M)
Tactic: rw [sInf_toSubmodule, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
rw :
  Eq.{w + 1} (α := Submodule R M) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x})
    (⨅ N ∈ S, (↑N : Submodule R M))
rw₁ : sInf (toSubmodule '' S) = ⨅ N ∈ S, (↑N : Submodule R M)
⊢ (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (↑N : Submodule R M)
have rw₂ : Eq.{w + 1} (α := Submodule R M) (⨅ a ∈ S, (↑a : Submodule R M)) (⨅ N ∈ S, (↑N : Submodule R M))
Tactic: rw [sInf_toSubmodule, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ Eq.{w + 1} (α := Submodule R M)
    (sInf
      {x : Submodule R M |
        ∃ (s : LieSubmodule R L M),
          Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s ∧ (↑s : Submodule R M) = x})
    (⨅ (i : ι), (↑(p i) : Submodule R M))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule R M)
      (sInf
        {x : Submodule R M |
          ∃ (s : LieSubmodule R L M),
            Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s ∧ (↑s : Submodule R M) = x})
      x ↔
    Membership.mem (γ := Submodule R M) (⨅ (i : ι), (↑(p i) : Submodule R M)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
⊢ Eq.{w + 1} (α := Set M)
    (⋂ (p : Submodule R M),
      ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x} p),
        (↑p : Set M))
    (⋂ s ∈ S, (↑s : Set M))
have h : ∀ (m : M),
  Membership.mem (γ := Set M)
      (⋂ (p : Submodule R M),
        ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x} p),
          (↑p : Set M))
      m ↔
    Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ (↑(⨅ (i : ι), p i) : Set M) = ⋂ (i : ι), (↑(p i) : Set M)
have rw : Eq.{w + 1} (α := Set M)
  (⋂ (s : LieSubmodule R L M),
    ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s), (↑s : Set M))
  (⋂ (i : ι), (↑(p i) : Set M))
Tactic: rw [iInf, coe_sInf]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ Membership.mem (γ := LieSubmodule R L M) (⨅ (i : ι), p i) x ↔ ∀ (i : ι), x ∈ p i
have rw : (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i
Tactic: rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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_1 N'_1 N N' : LieSubmodule R L M
x : L
m : M
hm : m ∈ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M)
⊢ ⁅x, m⁆ ∈ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M)
have rw : ∀ (hm : ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = m),
  ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = ⁅x, m⁆
Tactic: rw [Submodule.mem_sup] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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_1 N'_1 N N' : LieSubmodule R L M
x : L
m : M
hm : ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = m
⊢ ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = ⁅x, m⁆
have obtain : ∀ (y : M) (hy : y ∈ (↑N : Submodule R M)) (z : M) (hz : z ∈ (↑N' : Submodule R M)),
  ∃ y_1 ∈ (↑N : Submodule R M), ∃ z_1 ∈ (↑N' : Submodule R M), y_1 + z_1 = ⁅x, y + z⁆
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := hm
Cleared hypotheses: m, hm