case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy }
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ Function.Surjective ↑(rangeRestrict f)
rintro ⟨y, hy⟩
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ range f
hy : ∃ y_1, ↑f y_1 = y
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy✝ }
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy }
erw [mem_range] at hy
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := ↑f x, property := hy }
case mk
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ range f
hy : ∃ y_1, ↑f y_1 = y
⊢ ∃ a, ↑(rangeRestrict f) a = { val := y, property := hy✝ }
obtain ⟨x, rfl⟩ := hy
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ↑(rangeRestrict f) x = { val := ↑f x, property := hy }
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ∃ a, ↑(rangeRestrict f) a = { val := ↑f x, property := hy }
use x
no goals
case mk.intro
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : ↑f x ∈ range f
⊢ ↑(rangeRestrict f) x = { val := ↑f x, property := hy }
simp only [Subtype.mk_eq_mk, rangeRestrict_apply]