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
N N₂ : LieSubmodule R L M
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₂ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₃ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊤ ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw₄ : (↑N : Submodule R M) ≤ (↑N₂ : Submodule R M) ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_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
rw : (↑(comap N.incl N₂) : Submodule R ↥N) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₁ : Submodule.comap (↑N.incl : ↥N →ₗ[R] M) (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₂ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = (↑⊤ : Submodule R ↥N) ↔ N ≤ N₂
rw₃ : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊤ ↔ N ≤ N₂
rw₄ : (↑N : Submodule R M) ≤ (↑N₂ : Submodule R M) ↔ N ≤ N₂
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂
have rw₅ : N ≤ N₂ ↔ N ≤ N₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_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
⊢ comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
have simp : Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊥ ↔
  (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
Tactic: simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
    inf_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
⊢ Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊥ ↔
    (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
have rw : Disjoint (↑N : Submodule R M) (↑N₂ : Submodule R M) ↔ (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
Tactic: rw [← Submodule.disjoint_iff_comap_eq_bot, 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 : Disjoint (↑N : Submodule R M) (↑N₂ : Submodule R M) ↔ (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
⊢ Submodule.comap (↑N : Submodule R M).subtype (↑N₂ : Submodule R M) = ⊥ ↔
    (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
have rw₁ : (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) ⊓ (↑N₂ : Submodule R M) = ⊥
Tactic: rw [← Submodule.disjoint_iff_comap_eq_bot, 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 : LieSubmodule R L M
⊢ map LieModuleHom.id N = N
have h : ∀ (m : M), m ∈ map LieModuleHom.id N ↔ m ∈ N
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
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 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f ⊥ = ⊥
have h : ∀ (m : M'), m ∈ map f ⊥ ↔ Membership.mem (γ := LieSubmodule R L M') ⊥ m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
⊢ comap e.toLieModuleHom (map e.toLieModuleHom N) = N
have h : ∀ (m : M), m ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m ∈ N
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N_1 N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
⊢ map e.toLieModuleHom (comap e.toLieModuleHom N) = N
have h : ∀ (m : M'), m ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m ∈ N
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw : (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw :
  (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₁ : (↑f : M →ₗ[R] N).ker = (↑⊥ : Submodule R M) ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw :
  (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  (↑f : M →ₗ[R] N).ker = (↑⊥ : Submodule R M) ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₂ : (↑f : M →ₗ[R] N).ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw :
  (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  (↑f : M →ₗ[R] N).ker = (↑⊥ : Submodule R M) ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ : (↑f : M →ₗ[R] N).ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₃ : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑(↑f : M →ₗ[R] N) : (a : M) → N) ↔
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw :
  (↑f.ker : Submodule R M) = (↑⊥ : Submodule R M) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  (↑f : M →ₗ[R] N).ker = (↑⊥ : Submodule R M) ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ : (↑f : M →ₗ[R] N).ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₃ :
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑(↑f : M →ₗ[R] N) : (a : M) → N) ↔
    Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.ker = ⊥ ↔ Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₄ : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔
  Function.Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.comp f.ker.incl = 0
have h : ∀ (m : M) (hm : m ∈ f.ker),
  Eq.{w₁ + 1} (α := N) ((f.comp f.ker.incl : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
    ((0 : (a : ↥f.ker) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.ker) m hm) : N)
Tactic: ext ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
⊢ M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
have rw : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' = ⊥
Tactic: rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
rw : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' = ⊥
⊢ M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
have rw₁ : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' ≤ ⊥
Tactic: rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
rw : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' = ⊥
rw₁ : M' ≤ LieSubmodule.comap f ⊥ ↔ LieSubmodule.map f M' ≤ ⊥
⊢ M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
have rw₂ : M' ≤ LieSubmodule.comap f ⊥ ↔ M' ≤ LieSubmodule.comap f ⊥
Tactic: rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ LieSubmodule.map f ⊤ = f.range
have h : ∀ (m : N), m ∈ LieSubmodule.map f ⊤ ↔ m ∈ f.range
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₁ : Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
  Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₂ : Eq.{w₁ + 1} (α := Set N) (Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
  Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ :
  Eq.{w₁ + 1} (α := Set N) (Set.range.{w₁, w + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
    Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₃ : Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔
  Function.Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, coe_range, LieSubmodule.top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_6 : Module R N
inst_7 : LieRingModule L N
f_1 : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), Membership.mem (α := N) P ((f : (a : M) → N) m : N)
x : L
m : M
⊢ Eq.{w₁ + 1} (α := ↥P)
    ((LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) ⁅x, m⁆ :
      ↥(↑P : Submodule R N))
    (⁅x, (LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) m⁆ : ↥P)
have a : Eq.{w₁ + 1} (α := N)
  (↑((LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) ⁅x, m⁆) : N)
  (↑⁅x, (LinearMap.codRestrict (↑P : Submodule R N) (↑f : M →ₗ[R] N) h : (a : M) → ↥(↑P : Submodule R N)) m⁆ : N)
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
N : LieSubmodule R L M
⊢ N.incl.range = N
have simp : (↑N : Submodule R M).subtype.range = (↑N : Submodule R M)
Tactic: simp only [← toSubmodule_inj, LieModuleHom.toSubmodule_range, incl_coe]
-- 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).subtype.range = (↑N : Submodule R M)
have rw : (↑N : Submodule R M) = (↑N : Submodule R M)
Tactic: rw [Submodule.range_subtype]
-- 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
⊢ comap N.incl N = ⊤
have simp : Submodule.comap (↑N : Submodule R M).subtype (↑N : Submodule R M) = ⊤
Tactic: simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, 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
⊢ Submodule.comap (↑N : Submodule R M).subtype (↑N : Submodule R M) = ⊤
have rw : Eq.{w + 1} (α := Submodule R ↥N) ⊤ ⊤
Tactic: rw [Submodule.comap_subtype_self]
-- 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
inst_5 : LieAlgebra R L
H : LieSubalgebra R L
⊢ map (N.incl.restrictLie H) ⊤ = N.restr H
have h : ∀ (m : M), m ∈ map (N.incl.restrictLie H) ⊤ ↔ m ∈ N.restr H
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
N : LieSubmodule R L M
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
⊢ map f N ≤ f.range
have rw : map f N ≤ map f ⊤
Tactic: rw [← LieModuleHom.map_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
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' < N ↔ N' < ⊤
have h : N = (mapOrderEmbedding (f := N.incl) sorry : (a : LieSubmodule R L ↥N) → LieSubmodule R L M) ⊤
Tactic: convert! (LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt
-- 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' : LieSubmodule R L ↥N
| N
have rw : map N.incl ⊤
Tactic: rw [← N.map_incl_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
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ N
have conv_rhs : map N.incl N' ≤ map N.incl ⊤
Tactic: conv_rhs => rw [← N.map_incl_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
M : Type u_1
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
M' : Type u_2
inst_5 : AddCommGroup M'
inst_6 : Module R M'
inst_7 : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤
have rw : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := M') (⇑e.toLieModuleHom : (a : M) → M')
Tactic: rw [LieModuleHom.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TensorProduct (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
inst_11 : AddCommGroup P
inst_12 : Module R P
inst_13 : LieRingModule L P
inst_14 : LieModule R L P
inst_15 : AddCommGroup Q
inst_16 : Module R Q
inst_17 : LieRingModule L Q
inst_18 : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ (hasBracketAux (x + y) : (a : M ⊗[R] N) → M ⊗[R] N) t =
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((hasBracketAux x : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
      ((hasBracketAux y : (a : M ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
have simp : HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N)
      ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N) +
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N)
      ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N) =
  HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N)
      ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) x) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N) +
    HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
      ((LinearMap.rTensor N (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N)
      ((LinearMap.lTensor M (((toEnd R L N : LieHom.{u, v, w₁} R L (Module.End R N)) : (a : L) → Module.End R N) y) :
            (a : M ⊗[R] N) → M ⊗[R] N)
          t :
        M ⊗[R] N)
Tactic: simp only [hasBracketAux, LinearMap.lTensor_add, LinearMap.rTensor_add, map_add,
      LinearMap.add_apply]