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

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (C.comp (Ideal.Quotient.mk I)) X p) =
    (Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
        (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (C.comp (Ideal.Quotient.mk I)) X p) *
      (Ideal.Quotient.mk (Ideal.map C I)) (X i) =
    (Ideal.Quotient.mk (Ideal.map C I)) p * (Ideal.Quotient.mk (Ideal.map C I)) (X i)

Tactic:
simp only [hp]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q ^ 2 ∣ p

Tactic:
apply pow_dvd_of_le_emultiplicity

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ ↑2 ≤ emultiplicity q p
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
s : Finset M
hs : Basis (↥s) A M
⊢ Module.Finite A M

Tactic:
exact Module.Finite.of_basis hs

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 0) x = x

Tactic:
rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis (↥s) R M
⊢ Module.Finite R M

Tactic:
exact Module.Finite.of_basis hs

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) g₂ = g₂

Tactic:
· rw [add_zero, pow_zero, expand_one]
    constructor <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))

Tactic:
rw [det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
    LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]
  congr 1; ext i j
  rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]

Goal state after:
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 : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ IsRadical (minpoly K f)

Tactic:
rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (annihilator K[X] (AEval' f)).IsRadical
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
D✝ D1 D2 : LieDerivation R L M
a✝ b✝ : L
S : Type u_4
T : Type u_5
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulBracketCommClass S L M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulBracketCommClass T L M
r : S
D : LieDerivation R L M
a b : L
⊢ (r • ↑D) ⁅a, b⁆ = ⁅a, (r • ↑D) b⁆ - ⁅b, (r • ↑D) a⁆

Tactic:
simp only [LinearMap.smul_apply, coeFn_coe, apply_lie_eq_sub,
        smul_sub, SMulBracketCommClass.smul_bracket_comm]

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

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
⊢ (exp D) (x * y) = (exp D) x * (exp D) y

Tactic:
have h_nilL : IsNilpotent DL := h_nil.map <| lTensorAlgHom R B B

Goal state after:
R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
⊢ (exp D) (x * y) = (exp D) x * (exp D) y
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
⊢ IsSolvable (A ⊗[R] L)

Tactic:
by
  obtain ⟨k, hk⟩ := IsSolvable.solvable R L
  rw [isSolvable_iff A]
  use k
  rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]

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

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
⊢ ∑ x ∈ c.support, c x • ⁅a ⊗ₜ[R] y, ↑x⁆ ∈ Submodule.baseChange A ↑N

Tactic:
refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
x✝¹ : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
val✝ : A ⊗[R] M
n : M
hn : n ∈ ↑↑N
h : ((TensorProduct.mk R A M) 1) n = val✝
x✝ : ⟨val✝, ⋯⟩ ∈ c.support
⊢ ⁅a ⊗ₜ[R] y, ↑⟨val✝, ⋯⟩⁆ ∈ Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ baseChange A ⊤ = ⊤

Tactic:
by
  simp only [baseChange, top_toSubmodule, Submodule.baseChange_top]
  rfl

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

Goal state before:
pp: case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M

pp: case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M

Tactic:
· rw [nilpotencyLength_eq_zero_iff] at h; infer_instance

Goal state after:
case inr
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 1
⊢ IsTrivial L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent ↥(ad R L).range

Tactic:
exact (ad R L).isNilpotent_range

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂
    intro h
    rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin K ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) f).roots.toFinset) =
    Subalgebra.restrictScalars F ⊤

Tactic:
← IsScalarTower.algebraMap_eq,

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Polynomial.map (algebraMap F L) f).roots.toFinset) =
    Subalgebra.restrictScalars F ⊤
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
y : L
hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset
⊢ y ∈ ↑⊥

Tactic:
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
x : E
hx : x ∈ ↑(↑π₁).carrier
⊢ (θ π₂).emb ((inclusion ⋯) ((inclusion ⋯) ⟨x, hx⟩)) = (θ π₁).emb ((inclusion ⋯) ⟨x, hx⟩)

Tactic:
rw [(ge π₁).2, (ge π₂).2, h.2]

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
⊢ Nonempty (E →ₐ[F] K)

Tactic:
suffices ϕ.carrier = ⊤ from ⟨ϕ.emb.comp <| ((equivOfEq this).trans topEquiv).symm⟩

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
⊢ ϕ.carrier = ⊤
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case h
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
φ : K
j k : ι
⊢ ∀ (φ_1 : K),
    MapsTo ⇑(LinearMap.restrict (f j) ⋯) ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) φ_1)
      ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) φ_1)

Tactic:
μ

Goal state after:
case h
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
φ : K
j k : ι
μ : K
⊢ MapsTo ⇑(LinearMap.restrict (f j) ⋯) ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ)
    ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ)
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this : ∀ (χ : ι → K), χ i ≠ φ → ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊥
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤

Tactic:
by
        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
hx : x ∈ H
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
hv' : ⁅x, v⁆ ∈ lieSpan R L (range b.e)
⊢ -⁅v, ⁅x, u⁆⁆ + ⁅u, ⁅x, v⁆⁆ ∈ lieSpan R L (range b.e)

Tactic:
neg_add_eq_sub

Goal state after:
case lie
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
hx : x ∈ H
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
hv' : ⁅x, v⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
this : IsCompl (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0) (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
this :
  IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥N') 0))
    (LieSubmodule.map e.toLieModuleHom (posFittingComp R L ↥N'))
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ B.orthogonal ⊤

Tactic:
rw [orthogonal_top_eq_ker b]
  exact toLin_restrict_ker_eq_inf_ker ..

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
⊢ ∀ x_1 ∈ I, (Φ x_1) ⁅↑x, ↑y⁆ = 0

Tactic:
intro z hz

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ (Φ z) ⁅↑x, ↑y⁆ = 0
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ∃ a_1, ∃ (b : a_1 ∈ I), ⟨a_1, b⟩ ∈ J ∧ ↑I.incl ⟨a_1, b⟩ = ⁅a, ↑I.incl y⁆

Tactic:
Submodule.coe_subtype

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ∃ a_1, ∃ (b : a_1 ∈ I), ⟨a_1, b⟩ ∈ J ∧ ↑⟨a_1, b⟩ = ⁅a, ↑y⁆
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hv : x.fst = v
h : ¬↑x.snd = count v m
⊢ count v m + 1 = count x.fst (v ::ₘ m)

Tactic:
simp [hv]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hx.a.a
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅u, yl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact hu' hyl

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (AlgebraicClosure k)) ↑f).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Tactic:
dsimp [AlgebraicClosure]

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (algebraMap k (MvPolynomial (Vars k) k ⧸ maxIdeal k)) ↑f).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅⁅u, v⁆, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rw [lie_lie]
    apply sub_mem
    · obtain ⟨yc, hyc, yl, hyl, yu, hyu, aux⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
        yc + yl + yu = ⁅v, z⁆ := by simpa [LieSubmodule.mem_sup] using! hv' hz
      simp only [← aux, lie_add]
      repeat apply add_mem
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hu
      · exact hu' hyl
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hu
    · obtain ⟨yc, hyc, yl, hyl, yu, hyu, aux⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
        yc + yl + yu = ⁅u, z⁆ := by simpa [LieSubmodule.mem_sup] using! hu' hz
      simp only [← aux, lie_add]
      repeat apply add_mem
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hv
      · exact hv' hyl
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hv

Goal state after: