-- Mathlib/Algebra/Lie/Solvable.lean
theorem Injective.lieAlgebra_isSolvable [hL : IsSolvable L] (h : Injective f) :
    IsSolvable L'

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k

Tactic:
apply LieIdeal.derivedSeries_map_le

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : IsSolvable L
h : Injective ⇑f
⊢ IsSolvable L'

Tactic:
rw [isSolvable_iff R] at hL ⊢

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∃ k, derivedSeries R L' k = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ derivedSeries R L' k = ⊥

Tactic:
apply LieIdeal.bot_of_map_eq_bot h

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L a = ⊥ → derivedSeries R L' a = ⊥

Tactic:
intro k hk

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ derivedSeries R L' k = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∃ k, derivedSeries R L' k = ⊥

Tactic:
apply hL.imp

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L a = ⊥ → derivedSeries R L' a = ⊥

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥

Tactic:
rw [eq_bot_iff, ← hk]

Result:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k