-- Mathlib/Algebra/Lie/Solvable.lean
theorem isSolvable_tensorProduct_iff : IsSolvable (A ⊗[R] L) ↔ IsSolvable L

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k = ⊥
⊢ derivedSeries R L k = ⊥

Tactic:
rw [eq_bot_iff] at h ⊢

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥

Proof state:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) ↔ IsSolvable L

Tactic:
refine ⟨?_, fun _ ↦ inferInstance⟩

Result:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) → IsSolvable L

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : x ∈ derivedSeries R L k
h : 1 ⊗ₜ[R] x = 0
⊢ x = 0

Tactic:
rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h

Result:
no goals

Proof state:
case intro
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k = ⊥
⊢ ∃ k, derivedSeries R L k = ⊥

Tactic:
use k

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k = ⊥
⊢ derivedSeries R L k = ⊥

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥

Tactic:
rw [derivedSeries_baseChange] at h

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : LieSubmodule.baseChange A (derivedSeries R L k) ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥

Proof state:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → ∃ k, derivedSeries R L k = ⊥

Tactic:
rintro ⟨k, h⟩

Result:
case intro
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k = ⊥
⊢ ∃ k, derivedSeries R L k = ⊥

Proof state:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) → IsSolvable L

Tactic:
rw [isSolvable_iff A, isSolvable_iff R]

Result:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → ∃ k, derivedSeries R L k = ⊥

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : LieSubmodule.baseChange A (derivedSeries R L k) ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥

Tactic:
specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : x ∈ derivedSeries R L k
h : 1 ⊗ₜ[R] x ∈ ⊥
⊢ x ∈ ⊥

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : x ∈ derivedSeries R L k
h : 1 ⊗ₜ[R] x ∈ ⊥
⊢ x ∈ ⊥

Tactic:
rw [LieSubmodule.mem_bot] at h ⊢

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
hx : x ∈ derivedSeries R L k
h : 1 ⊗ₜ[R] x = 0
⊢ x = 0

Proof state:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥

Tactic:
intro x hx

Result:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥