R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ IsIdealMorphism f ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
simp only [isIdealMorphism_def, idealRange_eq_lieSpan_range, ←
  LieSubalgebra.coe_to_submodule_eq_iff, ← f.range.coe_to_submodule,
  LieIdeal.coe_to_lieSubalgebra_to_submodule, LieSubmodule.coe_lieSpan_submodule_eq_iff,
  LieSubalgebra.mem_coe_submodule, mem_range, exists_imp,
  Submodule.exists_lieSubmodule_coe_eq_iff]
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) → ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z

case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z) → ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
constructor
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y : L
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆) → ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
intro h x y
case mp.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
case mp
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y : L
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
obtain ⟨z, hz⟩ := h x (f y) y rfl
case mp.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ⁅x, ↑f y⁆ = ↑f z
case mp.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ∃ z, ⁅x, ↑f y⁆ = ↑f z
use z
no goals
case mp.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
x : L'
y z : L
hz : ↑f z = ⁅x, ↑f y⁆
⊢ ⁅x, ↑f y⁆ = ↑f z
exact hz.symm
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z) → ∀ (x m : L') (x_1 : L), ↑f x_1 = m → ∃ y, ↑f y = ⁅x, m⁆
intro h x y z hz
case mpr.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
case mpr
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
obtain ⟨w, hw⟩ := h x z
case mpr.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ↑f w = ⁅x, y⁆
case mpr.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ∃ y_1, ↑f y_1 = ⁅x, y⁆
use w
no goals
case mpr.intro
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : LieRing L'
inst✝⁸ : LieAlgebra R L'
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, ↑f y⁆ = ↑f z
x y : L'
z : L
hz : ↑f z = y
w : L
hw : ⁅x, ↑f z⁆ = ↑f w
⊢ ↑f w = ⁅x, y⁆
rw [← hw, hz]