awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
hx₁ : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
mem₁ : ∀ (i : ι), ∀ y ∈ N i, motive y
⊢ motive 0

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
hx₁ : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
mem₁ : ∀ (i : ι), ∀ y ∈ N i, motive y
zero₁ : motive 0
⊢ ∀ (y z : M), motive y → motive z → motive (y + z)

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x

Tactic:
Submodule.iSup_induction (motive := motive) (fun i ↦ (N i : Submodule R M)) hx mem zero add

Premises used: LieSubmodule.toSubmodule, Submodule.iSup_induction
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x

Tactic:
exact Submodule.iSup_induction (motive := motive) (fun i ↦ (N i : Submodule R M)) hx mem zero add

Premises used: LieSubmodule.toSubmodule, Submodule.iSup_induction
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ motive x hx

Tactic:
Exists.elim ?_ fun (hx : x ∈ ⨆ i, N i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
refine : ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1
⊢ motive x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, N i) (hc : motive x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1

Tactic:
iSup_induction N (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, N i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: LieSubmodule.iSup_induction
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ N i),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x
refine_2 : ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) 0), motive 0 hx
refine_3 :
  ∀ (x y : M),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x →
      (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) y →
        (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) (x + y)
⊢ ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1

Tactic:
refine iSup_induction N (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, N i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_

Premises used: LieSubmodule.iSup_induction
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x_1
i : ι
x : M
hx : x ∈ N i
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x

Tactic:
⟨_, mem _ _ hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x_1
i : ι
x : M
hx : x ∈ N i
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x

Tactic:
exact ⟨_, mem _ _ hx⟩
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) 0

Tactic:
⟨_, zero⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) 0

Tactic:
exact ⟨_, zero⟩
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x_1
x y : M
w : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
Cx : motive x w
w_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y
Cy : motive y w_1
⊢ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) (x + y)), motive (x + y) hx

Tactic:
⟨_, add _ _ _ _ Cx Cy⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x_1 : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x_1
x y : M
w : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
Cx : motive x w
w_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y
Cy : motive y w_1
⊢ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) (x + y)), motive (x + y) hx

Tactic:
exact ⟨_, add _ _ _ _ Cx Cy⟩
-- Module: Mathlib.Algebra.Lie.Submodule
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
rw : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ Disjoint N N'
rw₁ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ N ⊓ N' = ⊥
rw₂ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑(N ⊓ N') : Submodule R M) = (↑⊥ : Submodule R M)
rw₃ :
  (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = (↑⊥ : Submodule R M)
rw₄ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥
rw₅ rw₆ : Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M)
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'

Tactic:
rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]

Premises used: LieSubmodule.bot_toSubmodule, disjoint_iff, LieSubmodule.toSubmodule_inj, LieSubmodule.inf_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
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
rw : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ Codisjoint N N'
rw₁ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ N ⊔ N' = ⊤
rw₂ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑(N ⊔ N') : Submodule R M) = (↑⊤ : Submodule R M)
rw₃ :
  (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = (↑⊤ : Submodule R M)
rw₄ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤
rw₅ rw₆ : Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M)
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]

Premises used: codisjoint_iff, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ IsCompl (↑N : Submodule R M) (↑N' : Submodule R M) ↔ IsCompl N N'

Tactic:
simp [isCompl_iff]

Premises used: isCompl_iff
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Type u_1
N : ι → LieSubmodule R L M
⊢ (iSupIndep.{u_1 + 1, w} (α := Submodule R M) fun (i : ι) ↦ (↑(N i) : Submodule R M)) ↔ iSupIndep N

Tactic:
simp [iSupIndep_def, ← disjoint_toSubmodule]

Premises used: LieSubmodule.disjoint_toSubmodule, iSupIndep_def
-- Module: Mathlib.Algebra.Lie.Submodule
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
N : ι → LieSubmodule R L M
rw :
  Eq.{w + 1} (α := Submodule R M) (↑(⨆ (i : ι), N i) : Submodule R M) ⊤ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
rw₁ :
  Eq.{w + 1} (α := Submodule R M) (↑(⨆ (i : ι), N i) : Submodule R M) (↑⊤ : Submodule R M) ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
rw₂ rw₃ :
  Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤ ↔ Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
⊢ Eq.{w + 1} (α := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) ⊤ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤

Tactic:
rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ N + N' = N ⊔ N'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
rw : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ N ∧ x ∈ N'
rw₁ : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ N'
rw₂ : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
rw₃ : x ∈ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
rw₄ rw₅ : x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

Tactic:
rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]

Premises used: LieSubmodule.mem_toSubmodule, Submodule.mem_inf, LieSubmodule.inf_toSubmodule
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
rw : (∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
⊢ x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
rw [← mem_toSubmodule, sup_toSubmodule, Submodule.mem_sup]

Premises used: LieSubmodule.mem_toSubmodule, LieSubmodule.sup_toSubmodule, Submodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
⊢ (∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
⊢ (∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
hx : x ∈ N
⊢ x ∈ N ⊔ N'

Tactic:
le_sup_left (a := N) hx

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
hx : x ∈ N'
⊢ 0 ∈ N

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
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 : M
hx : x ∈ N'
⊢ 0 + x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
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 ≤ ⊥ ↔ ∀ m ∈ N, m = 0
⊢ N = ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
rw [eq_bot_iff]

Premises used: LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Submodule
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 ≤ ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Algebra.Lie.Submodule
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 ≤ ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
hα : Eq.{w + 1} (α := LieSubmodule R L ↥⊥) ⊥ ⊤
⊢ Subsingleton.{w + 1} (LieSubmodule R L ↥⊥)

Tactic:
apply subsingleton_of_bot_eq_top

Premises used: subsingleton_of_bot_eq_top
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ Eq.{w + 1} (α := LieSubmodule R L ↥⊥) ⊥ ⊤

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Lie.Submodule
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' x x_1 x_2 : LieSubmodule R L M
⊢ (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M) →
    ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⊓ (↑x_2 : Submodule R M) ≤
      (↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M) ⊓ (↑x_2 : Submodule R M)

Tactic:
IsModularLattice.sup_inf_le_assoc_of_le _

Premises used: IsModularLattice.sup_inf_le_assoc_of_le, Set.Mem, setOf
-- Module: Mathlib.Algebra.Lie.Submodule
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' x x_1 x_2 : LieSubmodule R L M
⊢ (↑x : Submodule R M) ≤ (↑x_2 : Submodule R M) →
    ((↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M)) ⊓ (↑x_2 : Submodule R M) ≤
      (↑x : Submodule R M) ⊔ (↑x_1 : Submodule R M) ⊓ (↑x_2 : Submodule R M)

Tactic:
exact IsModularLattice.sup_inf_le_assoc_of_le _

Premises used: IsModularLattice.sup_inf_le_assoc_of_le
-- Module: Mathlib.Algebra.Lie.Submodule
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 : IsNoetherian R M
⊢ WellFoundedGT.{w} (LieSubmodule R L M)

Tactic:
RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).dual.ltEmbedding

Premises used: LieSubmodule.toSubmodule_orderEmbedding, OrderEmbedding.ltEmbedding, RelHomClass.isWellFounded, OrderEmbedding.dual
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : IsArtinian R M
⊢ WellFoundedLT.{w} (LieSubmodule R L M)

Tactic:
RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).ltEmbedding

Premises used: LieSubmodule.toSubmodule_orderEmbedding, OrderEmbedding.ltEmbedding, RelHomClass.isWellFounded
-- Module: Mathlib.Algebra.Lie.Submodule
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 : IsArtinian R M
⊢ IsAtomic.{w} (LieSubmodule R L M)

Tactic:
isAtomic_of_orderBot_wellFounded_lt <| (wellFoundedLT_of_isArtinian R L M).wf

Premises used: IsWellFounded.wf, isAtomic_of_orderBot_wellFounded_lt
-- Module: Mathlib.Algebra.Lie.Submodule
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
rw : Eq.{w + 1} (α := LieSubmodule R L M) ⊥ ⊤ ↔ Subsingleton.{w + 1} (Submodule R M)
rw₁ : Eq.{w + 1} (α := LieSubmodule R L M) ⊥ ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
rw₂ : Eq.{w + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M) ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
rw₃ : Eq.{w + 1} (α := Submodule R M) (↑⊥ : Submodule R M) ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
rw₄ rw₅ : Eq.{w + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)

Tactic:
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
      top_toSubmodule, bot_toSubmodule]

Premises used: LieSubmodule.bot_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, subsingleton_iff_bot_eq_top