-- Mathlib/Algebra/Lie/Killing.lean
/-- Given a Killing Lie algebra `L`, if `L'` is isomorphic to `L`, then `L'` is Killing too. -/
lemma isKilling_of_equiv [IsKilling R L] (e : L ≃ₗ⁅R⁆ L') : IsKilling R L'

Proof state:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ x' ∈ ⊥

Tactic:
suffices e.symm x' ∈ LinearMap.ker (killingForm R L) by
  rw [IsKilling.ker_killingForm_eq_bot] at this
  simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this

Result:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ e.symm x' ∈ LinearMap.ker (killingForm R L)

Proof state:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ IsKilling R L'

Tactic:
constructor

Result:
case killingCompl_top_eq_bot
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ LieIdeal.killingCompl R L' ⊤ = ⊥

Proof state:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ (∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0) ↔ x' ∈ ⊥

Tactic:
refine ⟨fun hx' ↦ ?_, fun hx y _ ↦ hx ▸ LinearMap.map_zero₂ (killingForm R L') y⟩

Result:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ x' ∈ ⊥

Proof state:
case killingCompl_top_eq_bot
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ LieIdeal.killingCompl R L' ⊤ = ⊥

Tactic:
ext x'

Result:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ x' ∈ LieIdeal.killingCompl R L' ⊤ ↔ x' ∈ ⊥

Proof state:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Tactic:
replace hx' : ∀ y', killingForm R L' x' y' = 0 := by simpa using hx'

Result:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' : ∀ (y' : L'), ((killingForm R L') x') y' = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Proof state:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ e.symm x' ∈ LinearMap.ker (killingForm R L)

Tactic:
ext y

Result:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Proof state:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ x' ∈ LieIdeal.killingCompl R L' ⊤ ↔ x' ∈ ⊥

Tactic:
simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]

Result:
case killingCompl_top_eq_bot.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ (∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0) ↔ x' ∈ ⊥

Proof state:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' : ∀ (y' : L'), ((killingForm R L') x') y' = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Tactic:
specialize hx' (e y)

Result:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' : ((killingForm R L') x') (e y) = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Proof state:
case killingCompl_top_eq_bot.h.h
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' : ((killingForm R L') x') (e y) = 0
⊢ ((killingForm R L) (e.symm x')) y = 0 y

Tactic:
rwa [← e.apply_symm_apply x', killingForm_of_equiv_apply] at hx'

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ LinearMap.ker (killingForm R L)
⊢ x' ∈ ⊥

Tactic:
rw [IsKilling.ker_killingForm_eq_bot] at this

Result:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' ∈ ⊥

Proof state:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' ∈ ⊥

Tactic:
simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ∀ (y' : L'), ((killingForm R L') x') y' = 0

Tactic:
simpa using hx'

Result:
no goals