mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case add
R : Type u
inst✝ : CommRing R
x y : R[X] →₀ R[X]
hx :
  derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) x) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) x
hy :
  derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) y) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) y
⊢ derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) x) • (D R R[X]) X +
      derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) y) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) x + (Finsupp.linearCombination R[X] ⇑(D R R[X])) y

Tactic:
;

Goal state after:
case add
R : Type u
inst✝ : CommRing R
x y : R[X] →₀ R[X]
hx :
  derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) x) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) x
hy :
  derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) y) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) y
⊢ derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) x) • (D R R[X]) X +
      derivative'.liftKaehlerDifferential ((Finsupp.linearCombination R[X] ⇑(D R R[X])) y) • (D R R[X]) X =
    (Finsupp.linearCombination R[X] ⇑(D R R[X])) x + (Finsupp.linearCombination R[X] ⇑(D R R[X])) y
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
w_chi : Weight.toLinear K (↥H) L χ = 0
⊢ 0 = ⇑χ

Tactic:
;

Goal state after:
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
w_chi : Weight.toLinear K (↥H) L χ = 0
⊢ 0 = ⇑χ
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
w_chi : Weight.toLinear K (↥H) L χ = 0
h : ↥H
⊢ 0 h = χ h

Tactic:
;

Goal state after:
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
w_chi : Weight.toLinear K (↥H) L χ = 0
h : ↥H
⊢ 0 h = χ h
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
w_chi : ¬Weight.toLinear K (↥H) L χ = 0
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
⊢ ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + -Weight.toLinear K (↥H) L α)

Tactic:
;

Goal state after:
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
w_chi : ¬Weight.toLinear K (↥H) L χ = 0
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
⊢ ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + -Weight.toLinear K (↥H) L α)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ (aeval fun x ↦ f (X x)) = f

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ (aeval fun x ↦ f (X x)) = f
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ (aeval fun x ↦ f (X x)) (X i✝) = f (X i✝)

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ (aeval fun x ↦ f (X x)) (X i✝) = f (X i✝)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ f = aeval fun x ↦ f (X x)

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
⊢ f = aeval fun x ↦ f (X x)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ f (X i✝) = (aeval fun x ↦ f (X x)) (X i✝)

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
H : ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG := FinitePresentation.out
n : ℕ := H.choose
f : MvPolynomial (Fin n) R →ₐ[R] S := ⋯.choose
hf : Function.Surjective ⇑f
hf' : (RingHom.ker f).FG
H' : ∃ n_1 s, Submodule.span (MvPolynomial (Fin n) R) (Set.range s) = RingHom.ker f :=
  Submodule.fg_iff_exists_fin_generating_family.mp hf'
m : ℕ := H'.choose
v : Fin m → MvPolynomial (Fin n) R := ⋯.choose
hv : Ideal.span (Set.range v) = RingHom.ker f
i✝ : Fin n
⊢ f (X i✝) = (aeval fun x ↦ f (X x)) (X i✝)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : R
⊢ (algebraMap R (T ⊗[R] P.Ring)) x = (algebraMap R T) x ⊗ₜ[R] 1

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Extension R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : R
⊢ (algebraMap R (T ⊗[R] P.Ring)) x = (algebraMap R T) x ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ (Hom.id P).toAlgHom x✝ = (AlgHom.id R P.Ring) x✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ (Hom.id P).toAlgHom x✝ = (AlgHom.id R P.Ring) x✝
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ (f.comp (Hom.id P)).toRingHom x✝ = f.toRingHom x✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ (f.comp (Hom.id P)).toRingHom x✝ = f.toRingHom x✝
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ ((Hom.id P').comp f).toRingHom x✝ = f.toRingHom x✝

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ ((Hom.id P').comp f).toRingHom x✝ = f.toRingHom x✝
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P✝ : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝² : CommRing R''
inst✝¹ : CommRing S''
inst✝ : Algebra R'' S''
P'' : Extension R'' S''
P : Extension R S
x : S
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) S) ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ x)) = x

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P✝ : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝² : CommRing R''
inst✝¹ : CommRing S''
inst✝ : Algebra R'' S''
P'' : Extension R'' S''
P : Extension R S
x : S
⊢ (algebraMap (P.Ring ⧸ P.ker ^ 2) S) ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ x)) = x
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
⊢ ∀ (x : R₁) (y : R₂) (z : P.Cotangent), (x • y) • z = x • y • z

Tactic:
intro r

Goal state after:
R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
r : R₁
⊢ ∀ (y : R₂) (z : P.Cotangent), (r • y) • z = r • y • z
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ -Weight.toLinear K (↥H) L β ∈ q

Tactic:
;

Goal state after:
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
x✝ : { α // Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }
β : Weight K (↥H) L
hβ_mem : Weight.toLinear K (↥H) L β ∈ q
hβ_nz : β.IsNonZero
⊢ -Weight.toLinear K (↥H) L β ∈ q
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα : (rootSystem H).root α ∈ q
⊢ rootSpace H ⇑↑α ≤ genWeightSpace L ⇑↑α ⊔ genWeightSpace L (-⇑↑α) ⊔ corootSubmodule ↑α

Tactic:
;

Goal state after:
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα : (rootSystem H).root α ∈ q
⊢ rootSpace H ⇑↑α ≤ genWeightSpace L ⇑↑α ⊔ genWeightSpace L (-⇑↑α) ⊔ corootSubmodule ↑α
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝¹ : Ideal.span (Set.range s) = P.ker
hs✝ : Submodule.span P.Ring (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤
⊢ Submodule.span P.Ring (⇑mk '' Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
ι : Type u_1
s : ι → P.Ring
hs✝¹ : Ideal.span (Set.range s) = P.ker
hs✝ : Submodule.span P.Ring (Set.range s) = P.ker
hs : Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩) = ⊤
⊢ Submodule.map mk (Submodule.span P.Ring (Set.range fun i ↦ ⟨s i, ⋯⟩)) = ⊤
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
⊢ ((map (Hom.id P)) (mk x)).val = (LinearMap.id (mk x)).val

Tactic:
simp only [map_mk, Hom.toAlgHom_id, AlgHom.coe_id, id_eq, Subtype.coe_eta, val_mk,
    LinearMap.id_coe]

Goal state after: