mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
⊢ ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
r : R
⊢ (pderiv i) ((map φ) (C r)) = (map φ) ((pderiv i) (C r))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p q : MvPolynomial σ R
hp : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
hq : (pderiv i) ((map φ) q) = (map φ) ((pderiv i) q)
⊢ (pderiv i) ((map φ) (p + q)) = (map φ) ((pderiv i) (p + q))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_5
M : Type u_6
N : Type u_7
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
inst✝⁸ : Module.Finite R M
inst✝⁷ : FinitePresentation R N
f : M →ₗ[R] N
p : Ideal R
inst✝⁶ : p.IsPrime
Mₚ : Type u_3
Nₚ : Type u_4
inst✝⁵ : AddCommGroup Mₚ
inst✝⁴ : AddCommGroup Nₚ
inst✝³ : Module R Mₚ
inst✝² : Module R Nₚ
fM : M →ₗ[R] Mₚ
fN : N →ₗ[R] Nₚ
inst✝¹ : IsLocalizedModule p.primeCompl fM
inst✝ : IsLocalizedModule p.primeCompl fN
hf : Function.Bijective ⇑((IsLocalizedModule.map p.primeCompl fM fN) f)
⊢ ∃ g ∉ p, Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ (map S f g) l' = (s • LinearMap.id) ∘ₗ ↑l

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
⊢ (pderiv i) ((map φ) f) = (map φ) ((pderiv i) f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
⊢ Function.Bijective ⇑((map S f g) l')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
h' : Module.Finite R M
⊢ ∃ d k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i ↦ torsionBy R M (p i ^ e i)
⊢ ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R M (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ R ∙ p i ^ k j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i ↦ torsionBy R M (p i ^ e i)
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R M (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ R ∙ p i ^ k j)
i : (x : I) × Fin ⋯.choose
⊢ R ∙ p i.fst ^ ⋯.choose i.snd =
    R ∙
      (fun x ↦
            match x with
            | ⟨i, snd⟩ => p i)
          i ^
        (fun x ↦
            match x with
            | ⟨i, j⟩ => ⋯.choose j)
          i

Tactic:
simp only

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
⊢ (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h' : Module.Finite R M
hM : IsTorsion R M
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] ⨁ (i : ι), R ⧸ R ∙ p i ^ e i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h' : Module.Finite R M
⊢ ∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ e i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝² : CommSemiring R
S : Type u_1
τ : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
j : σ
⊢ (aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
σ : Type u_1
ι : Type u_2
p : MvPolynomial (σ ⊕ ι) R
i : σ
⊢ (pderiv i) ((sumRingEquiv R σ ι) p) = (sumRingEquiv R σ ι) ((pderiv (Sum.inl i)) p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝ : CommSemiring R
f g : R[X]
⊢ { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } (f * g) =
    f • { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } g +
      g • { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = D (C a * f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = a • D f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D₁ D₂ : Derivation R R[X] A
h : D₁ X = D₂ X
f : R[X]
⊢ f ∈ ↑R[ X]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ (LinearMap.toSpanSingleton R[X] A (a + b)).compDer derivative' =
    (LinearMap.toSpanSingleton R[X] A a).compDer derivative' + (LinearMap.toSpanSingleton R[X] A b).compDer derivative'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ (LinearMap.toSpanSingleton R[X] A (t • a)).compDer derivative' =
    (RingHom.id R) t • (LinearMap.toSpanSingleton R[X] A a).compDer derivative'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ((mkDerivation R) a) f = derivative f • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ((mkDerivation R) a) X = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (mkDerivation R) 1 = derivative'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ((mkDerivation R) 1) f = derivative f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ (mkDerivationEquiv R) a = (mkDerivation R) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (x y : R[X]),
    (AEval.of R M a) (d ((aeval a) (x + y))) = (AEval.of R M a) (d ((aeval a) x)) + (AEval.of R M a) (d ((aeval a) y))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (m : R) (x : R[X]), (AEval.of R M a) (d ((aeval a) (m • x))) = (RingHom.id R) m • (AEval.of R M a) (d ((aeval a) x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (a_1 b : R[X]),
    { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } (a_1 * b) =
      a_1 • { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } b +
        b • { toFun := fun f ↦ (AEval.of R M a) (d ((aeval a) f)), map_add' := ⋯, map_smul' := ⋯ } a_1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = derivative f • (AEval.of R M a) (d a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (AEval.of R M a).symm ((d.compAEval a) f) = (aeval a) (derivative f) • d a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
⊢ x_χ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L α)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_pos : x_χ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L α)
⊢ ⟨e, he⟩ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_pos : x_χ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L α)
c : K
hc : c • ⟨e, he⟩ = ⟨x_χ, hx_χ_pos⟩
⊢ x_χ = c • e + 0 • f + 0 • ⁅e, f⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
⊢ ∃ x, (toSpanSingleton R M x).ker = annihilator R M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
⊢ x_χ ∈ sl2SubalgebraOfRoot hα₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
⊢ Function.LeftInverse
    (⇑(Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x)))
    (MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
⊢ Function.RightInverse
    (⇑(Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x)))
    (MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
⊢ (mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
M' : Type u_1
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
f : M →ₗ[R] M'
inst✝⁴ : IsLocalizedModule S f
N' : Type u_2
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g
inst✝ : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ g ∘ₗ h' = (IsLocalizedModule.map S f g) (h', s).1 ∘ₗ f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
i : σ
x : MvPolynomial σ R
⊢ (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (D R (MvPolynomial σ R)) (MvPolynomial.X i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : R[X]
⊢ (D R R[X]) P = derivative P • (D R R[X]) X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ Function.LeftInverse (⇑((lsmul R R Ω[R[X]⁄R]).toLinearMap.flip ((D R R[X]) X)))
    derivative'.liftKaehlerDifferential.toFun

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R[X]
⊢ derivative'.liftKaehlerDifferential.toFun (((lsmul R R Ω[R[X]⁄R]).toLinearMap.flip ((D R R[X]) X)) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
N'✝ : Type ?u.18
inst✝¹⁴ : CommRing R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommGroup N'✝
inst✝⁸ : Module R N'✝
S : Submonoid R
f✝ : N →ₗ[R] N'✝
inst✝⁷ : IsLocalizedModule S f✝
M' : Type u_1
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
f : M →ₗ[R] M'
inst✝⁴ : IsLocalizedModule S f
N' : Type u_2
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g
inst✝ : FinitePresentation R M
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
y : M'
⊢ (y, 1).2 • y = LinearMap.id (y, 1).1

Tactic:
by

Goal state after: