awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1
have 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)
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 => ?_
-- 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
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw : (↑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]
-- 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
rw : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ Disjoint N N'
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw₁ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ N ⊓ N' = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]
-- 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
rw : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ Disjoint N N'
rw₁ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ N ⊓ N' = ⊥
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw₂ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑(N ⊓ N') : Submodule R M) = (↑⊥ : Submodule R M)
Tactic: rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]
-- 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
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)
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw₃ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = (↑⊥ : Submodule R M)
Tactic: rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]
-- 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
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)
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw₄ : (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]
-- 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
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) = ⊥
⊢ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint N N'
have rw₅ : Disjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Disjoint (↑N : Submodule R M) (↑N' : Submodule R M)
Tactic: rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
    ← disjoint_iff]
-- 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
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw : (↑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]
-- 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
rw : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ Codisjoint N N'
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw₁ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ N ⊔ N' = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]
-- 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
rw : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ Codisjoint N N'
rw₁ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ N ⊔ N' = ⊤
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw₂ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑(N ⊔ N') : Submodule R M) = (↑⊤ : Submodule R M)
Tactic: rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]
-- 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
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)
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw₃ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = (↑⊤ : Submodule R M)
Tactic: rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]
-- 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
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)
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw₄ : (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M) = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]
-- 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
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) = ⊤
⊢ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint N N'
have rw₅ : Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M) ↔ Codisjoint (↑N : Submodule R M) (↑N' : Submodule R M)
Tactic: rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]
-- 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
N : ι → LieSubmodule R L M
⊢ Eq.{w + 1} (α := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) ⊤ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
have rw : 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]
-- 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
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) ⊤
⊢ Eq.{w + 1} (α := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) ⊤ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
have 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) ⊤
Tactic: rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]
-- 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
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) ⊤
⊢ Eq.{w + 1} (α := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) ⊤ ↔
    Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
have rw₂ : Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤ ↔ Eq.{w + 1} (α := LieSubmodule R L M) (⨆ (i : ι), N i) ⊤
Tactic: rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]
-- 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 : M
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
have rw : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ N ∧ x ∈ N'
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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 : M
rw : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ N ∧ x ∈ N'
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
have rw₁ : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ N'
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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 : 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'
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
have rw₂ : x ∈ (↑(N ⊓ N') : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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 : 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)
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
have rw₃ : x ∈ (↑N : Submodule R M) ⊓ (↑N' : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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 : 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)
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
have rw₄ : x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M) ↔ x ∈ (↑N : Submodule R M) ∧ x ∈ (↑N' : Submodule R M)
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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 : M
⊢ x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
have rw : (∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = x) ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
Tactic: rw [← mem_toSubmodule, sup_toSubmodule, Submodule.mem_sup]
-- 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 = ⊥ ↔ ∀ m ∈ N, m = 0
have rw : N ≤ ⊥ ↔ ∀ m ∈ N, m = 0
Tactic: rw [eq_bot_iff]
-- 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
⊢ Subsingleton.{w + 1} (LieSubmodule R L ↥⊥)
have hα : Eq.{w + 1} (α := LieSubmodule R L ↥⊥) ⊥ ⊤
Tactic: apply subsingleton_of_bot_eq_top
-- 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
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)
have rw : Eq.{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]
-- 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
rw : Eq.{w + 1} (α := LieSubmodule R L M) ⊥ ⊤ ↔ Subsingleton.{w + 1} (Submodule R M)
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)
have rw₁ : Eq.{w + 1} (α := LieSubmodule R L M) ⊥ ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
      top_toSubmodule, 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
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) ⊥ ⊤
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)
have rw₂ : Eq.{w + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M) ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
      top_toSubmodule, 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
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) ⊥ ⊤
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)
have rw₃ : Eq.{w + 1} (α := Submodule R M) (↑⊥ : Submodule R M) ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
      top_toSubmodule, 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
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) ⊥ ⊤
⊢ Subsingleton.{w + 1} (LieSubmodule R L M) ↔ Subsingleton.{w + 1} (Submodule R M)
have rw₄ : Eq.{w + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{w + 1} (α := Submodule R M) ⊥ ⊤
Tactic: rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toSubmodule_inj,
      top_toSubmodule, 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
⊢ Nontrivial.{w} ↥N ↔ N ≠ ⊥
have mp : Nontrivial.{w} ↥N → N ≠ ⊥
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
N : LieSubmodule R L M
mp : Nontrivial.{w} ↥N → N ≠ ⊥
⊢ Nontrivial.{w} ↥N ↔ N ≠ ⊥
have mpr : N ≠ ⊥ → Nontrivial.{w} ↥N
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
N : LieSubmodule R L M
⊢ N ≠ ⊥ → Nontrivial.{w} ↥N
have mpr : Subsingleton.{w + 1} ↥N → N = ⊥
Tactic: contrapose!
-- 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
⊢ Subsingleton.{w + 1} ↥N → N = ⊥
have mpr : Subsingleton.{w + 1} ↥N → ∀ m ∈ N, m = 0
Tactic: rw [LieSubmodule.eq_bot_iff]
-- 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 M
x : M
⊢ Membership.mem (γ := LieSubmodule R L M) (lieSpan R L s) x ↔ ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N
have rw : Membership.mem (γ := Set M)
    (⋂ (s_1 : LieSubmodule R L M),
      ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) {N : LieSubmodule R L M | s ⊆ (↑N : Set M)} s_1),
        (↑s_1 : Set M))
    x ↔
  ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → x ∈ N
Tactic: rw [← SetLike.mem_coe, lieSpan, 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
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ (↑(lieSpan R L s) : Set M)
have rw : ∀ (N : LieSubmodule R L M), s ⊆ (↑N : Set M) → m ∈ N
Tactic: rw [SetLike.mem_coe, mem_lieSpan]
-- 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 M
⊢ LE.le (α := Submodule R M) (Submodule.span R s) (↑(lieSpan R L s) : Submodule R M)
have rw : s ⊆ (↑(↑(lieSpan R L s) : Submodule R M) : Set M)
Tactic: rw [Submodule.span_le]
-- 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 M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N ↔ s ⊆ (↑N : Set M)
have mp : lieSpan R L s ≤ N → s ⊆ (↑N : Set M)
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
s : Set M
N : LieSubmodule R L M
mp : lieSpan R L s ≤ N → s ⊆ (↑N : Set M)
⊢ lieSpan R L s ≤ N ↔ s ⊆ (↑N : Set M)
have mpr : s ⊆ (↑N : Set M) → lieSpan R L s ≤ N
Tactic: constructor