mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅t • x, D⁆ a✝ = (t • ⁅x, D⁆) a✝

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅t • x, D⁆ a✝ = (t • ⁅x, D⁆) a✝
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅x, t • D⁆ a✝ = (t • ⁅x, D⁆) a✝

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅x, t • D⁆ a✝ = (t • ⁅x, D⁆) a✝
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x x✝ : L
⊢ ↑((ad R L) x) x✝ = ((LieAlgebra.ad R L) x) x✝

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x x✝ : L
⊢ ↑((ad R L) x) x✝ = ((LieAlgebra.ad R L) x) x✝
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
a✝ : L
⊢ ⁅(ad R L) x, D⁆ a✝ = ⁅x, D⁆ a✝

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
a✝ : L
⊢ ⁅(ad R L) x, D⁆ a✝ = ⁅x, D⁆ a✝
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ Ring.inverse ((aeval x) (derivative P)) * (aeval x) P = 0 ↔ (aeval x) P = 0

Tactic:
Ring.inverse_mul_eq_iff_eq_mul _ _ _ h,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ (aeval x) P = (aeval x) (derivative P) * 0 ↔ (aeval x) P = 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_3
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∑ i ∈ R2N, ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j)) =
    ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
rw [hR2N, sum_sigma']
      apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
      · simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
        lia
      · simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
        rintro ⟨x₁, y₁⟩ - h₁ ⟨x₂, y₂⟩ - h₂ h₃ h₄
        simp_all
        lia
      · simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]
        exact fun x y _ _ _ ↦ ⟨x + y, x, by lia⟩
      · simp only [mem_sigma, mem_range, implies_true]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
⊢ q.natDegree < (X - C (AdjoinRoot.root p)).natDegree + q.natDegree

Tactic:
;

Goal state after:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
⊢ q.natDegree < (X - C (AdjoinRoot.root p)).natDegree + q.natDegree
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
⊢ a.IsSemisimple

Tactic:
let R := K[X] ⧸ Ideal.span {minpoly K f}
  let S := AdjoinRoot ((minpoly K g).map <| algebraMap K R)
  have : Module.Finite K R :=
    (AdjoinRoot.powerBasis' <| minpoly.monic <| IsIntegral.isIntegral f).finite
  have : Module.Finite R S :=
    (AdjoinRoot.powerBasis' <| (minpoly.monic <| IsIntegral.isIntegral g).map _).finite
  have : Module.Finite K S := .trans R S
  have : IsArtinianRing R := .of_finite K R
  have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
  have : IsReduced S := by
    simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
    exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical
  let φ : S →ₐ[K] End K M := Ideal.Quotient.liftₐ _ (eval₂AlgHom (Ideal.Quotient.liftₐ _ (aeval f)
    fun a ↦ ?_) g ?_) ((Ideal.span_singleton_le_iff_mem _).mpr ?_ : _ ≤ RingHom.ker _)
  rotate_left 1
  · rw [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly]; exact id
  · rintro ⟨p⟩; exact p.induction_on (fun k ↦ by simp [R, commute_algebraMap_left])
      (fun p q hp hq ↦ by simpa [R] using! hp.add_left hq)
      fun n k ↦ by simpa [R, pow_succ, ← mul_assoc _ _ X] using! (·.mul_left comm)
  · simpa only [RingHom.mem_ker, eval₂AlgHom_apply, eval₂_map, AlgHom.comp_algebraMap_of_tower]
      using! minpoly.aeval K g
  have : K[f, g] ≤ φ.range := adjoin_le fun x ↦ by
    rintro (hx | hx) <;> rw [hx]
    · exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
    · exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩
  obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)
  refine isSemisimple_of_squarefree_aeval_eq_zero
    ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p) ?_
  rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case refl
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
x✝¹ x✝ : (_ : ℕ) × ℕ
i j : ℕ
⊢ ⟨i, j⟩ = ⟨i, j⟩

Tactic:
;

Goal state after:
case refl
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
x✝¹ x✝ : (_ : ℕ) × ℕ
i j : ℕ
⊢ ⟨i, j⟩ = ⟨i, j⟩
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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 N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this : hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x
⊢ (hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x) t =
    (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)

Tactic:
;

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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 N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
this : hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x
⊢ (hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x) t =
    (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D l J

Tactic:
;

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D l J
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J

Tactic:
;

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J

Tactic:
;

Goal state after:
case succ.inr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l ≤ k
⊢ ⁅D k I, D k I⁆ ≤ D l J
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case refine_3
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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 N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t t₁ t₂ : M ⊗[R] N
ht₁ : (TensorProduct.map ↑f ↑g) ⁅x, t₁⁆ = ⁅x, (TensorProduct.map ↑f ↑g) t₁⁆
ht₂ : (TensorProduct.map ↑f ↑g) ⁅x, t₂⁆ = ⁅x, (TensorProduct.map ↑f ↑g) t₂⁆
⊢ (TensorProduct.map ↑f ↑g) ⁅x, t₁ + t₂⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (t₁ + t₂)⁆

Tactic:
;

Goal state after:
case refine_3
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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 N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t t₁ t₂ : M ⊗[R] N
ht₁ : (TensorProduct.map ↑f ↑g) ⁅x, t₁⁆ = ⁅x, (TensorProduct.map ↑f ↑g) t₁⁆
ht₂ : (TensorProduct.map ↑f ↑g) ⁅x, t₂⁆ = ⁅x, (TensorProduct.map ↑f ↑g) t₂⁆
⊢ (TensorProduct.map ↑f ↑g) ⁅x, t₁ + t₂⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (t₁ + t₂)⁆
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case h
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
h : IsNilpotent a
⊢ exp a * exp (-a) = 1 ∧ exp (-a) * exp a = 1

Tactic:
exact ⟨exp_mul_exp_neg_self h, exp_neg_mul_exp_self h⟩

Goal state after:
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x m : L
n : M
⊢ ((↑(toEnd R L M)).toFun ⁅x, m⁆) n = ⁅x, (↑(toEnd R L M)).toFun m⁆ n

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x m : L
n : M
⊢ ((↑(toEnd R L M)).toFun ⁅x, m⁆) n = ⁅x, (↑(toEnd R L M)).toFun m⁆ n
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ D k ⊥ ≤ ⊥

Tactic:
;

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ D k ⊥ ≤ ⊥
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦
    ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = x

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦
    ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = x
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) ↔ ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) ↔ ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} ∧ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
;

Goal state after:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} ∧ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩ = x ⊗ₜ[R] n

Tactic:
;

Goal state after:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩ = x ⊗ₜ[R] n
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ∃ x n, ⁅↑x, ↑n⁆ = m

Tactic:
;

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ∃ x n, ⁅↑x, ↑n⁆ = m
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R (↥I) k ⊤, derivedSeriesOfIdeal R (↥I) k ⊤⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
;

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅derivedSeriesOfIdeal R (↥I) k ⊤, derivedSeriesOfIdeal R (↥I) k ⊤⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ∃ x_1 n_1, ⁅↑x_1, ↑n_1⁆ = ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩)

Tactic:
;

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ∃ x_1 n_1, ⁅↑x_1, ↑n_1⁆ = ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩)
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩)

Tactic:
;

Goal state after:
case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆ = ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩)