mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x : ↥(toAlgHom F E K₁).range
⊢ ϕ ↑x ∈ (toAlgHom F E K₂).range

Tactic:
suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
      rintro x ⟨y, ⟨z, hy⟩, hx⟩
      rw [← hx, ← hy]
      apply minpoly.mem_range_of_degree_eq_one E
      refine ((h.splits z).of_dvd (map_ne_zero (minpoly.ne_zero (h.isIntegral z)))
        (minpoly.dvd E _ (by simp [aeval_algHom_apply]))).degree_eq_one_of_irreducible
        (minpoly.irreducible ?_)
      simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
      suffices IsIntegral F _ by exact this.tower_top
      exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ

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)
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
have : FaithfulSMul Q F := ⟨fun {q₁ q₂} ↦ by
    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:
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)
this : FaithfulSMul Q F
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)
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 F K) f).rootSet L)) =
    Subalgebra.restrictScalars F ⊤

Tactic:
by
      rw [rootSet, aroots, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top,
        eq_top_iff, ← adjoin_rootSet L f, Algebra.adjoin_le_iff]
      exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ restrictScalars F (extendScalars h) = restrictScalars F (adjoin (↥K) S)

Tactic:
by
  rw [extendScalars_restrictScalars, restrictScalars_adjoin]
  exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))

Tactic:
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
hcomm : Commute ((aeval a) (C k - X)) ((aeval a) (-(q / (X - C k))))
⊢ ¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
E : Type u_2
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
⊢ FiniteDimensional K ↥(E1 ⊔ E2)

Tactic:
have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range

Goal state after:
F : Type u_1
inst✝⁷ : Field F
E : Type u_2
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
h : FiniteDimensional K ↥(Subalgebra.toSubmodule g.range)
⊢ FiniteDimensional K ↥(E1 ⊔ E2)
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
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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : adjoin F ↑S ≤ θ.carrier
θ₀ : ↥(adjoin F ↑S) →ₐ[F] K := θ.emb.comp (inclusion hθ)
⊢ False

Tactic:
have := (hπ₀ θ₀).trans hθπ

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
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
hπ : ∀ (ω : Ω), ∀ θ ≥ ↑(π ω), { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑(π ω)).carrier ⊔ adjoin F ↑S
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
π₀ : { a // a ∈ c }
hπ₀ : ∀ (i : Ω), ↑(π i) ≤ ↑π₀
θ : Lifts F E K
hθπ : θ ≥ ↑π₀
hθ : adjoin F ↑S ≤ θ.carrier
θ₀ : ↥(adjoin F ↑S) →ₐ[F] K := θ.emb.comp (inclusion hθ)
this : ↑(π θ₀) ≤ θ
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
⊢ FiniteDimensional K ↥(⨆ i, t i)

Tactic:
rw [← iSup_univ]

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
⊢ FiniteDimensional K ↥(⨆ x ∈ Set.univ, t x)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ⨆ i ∈ s, F⟮↑i⟯ ≤ adjoin F ↑(Finset.image Subtype.val s)

Tactic:
simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∀ i ∈ s, {↑i} ⊆ ↑(adjoin F (Subtype.val '' ↑s))
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
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
χ : R
x y : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
m

Goal state after:
K : Type u_1
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
χ : R
x y : L
m : M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
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
χ : R
x : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro y m hm
      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid] at hm ⊢
      rw [← zero_add χ]
      exact lie_mem_maxGenEigenspace_toEnd (by simp) hm

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0)).carrier
hy : y ∈ (↑(rootSpace H 0)).carrier
⊢ ⁅x, y⁆ ∈ (↑(rootSpace H 0)).carrier

Tactic:
by
      let xy : rootSpace H 0 ⊗[R] rootSpace H 0 := ⟨x, hx⟩ ⊗ₜ ⟨y, hy⟩
      suffices (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy : L) ∈ rootSpace H 0 by
        rwa [rootSpaceProduct_tmul, Subtype.coe_mk, Subtype.coe_mk] at this
      exact (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy).property

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

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
⊢ ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
let f : Module.End R H := toEnd R H H y

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
⊢ ((toEnd R (↥H) L) y ^ k) x = 0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
⊢ ∀ {m : M}, m ∈ (⨅ k, (φ ^ k).range).carrier → ⁅y, m⁆ ∈ (⨅ k, (φ ^ k).range).carrier

Tactic:
m

Goal state after:
K : Type u_1
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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
m : M
⊢ m ∈ (⨅ k, (φ ^ k).range).carrier → ⁅y, m⁆ ∈ (⨅ k, (φ ^ k).range).carrier
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
x : L
k : ℕ
hk : ∀ (b : ℕ), k ≤ b → ⨅ m, ((toEnd R L M) x ^ m).range = ((toEnd R L M) x ^ b).range
m : M
F : LieSubmodule R L M := ⋯
x✝ : M ⧸ F
⊢ ((toEnd R L M) x ^ k) m ∈ posFittingCompOf R M x

Tactic:
simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]

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
x : L
k : ℕ
hk : ∀ (b : ℕ), k ≤ b → ⨅ m, ((toEnd R L M) x ^ m).range = ((toEnd R L M) x ^ b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x✝ : M ⧸ F
⊢ ((toEnd R L M) x ^ k) m ∈ ((toEnd R L M) x ^ k).range
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case inr
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
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
⊢ IsCompl M₀ M₁

Tactic:
set M₀ₓ₀ := genWeightSpace M₀ₓ (0 : L → R)

Goal state after:
case inr
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
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
⊢ IsCompl M₀ M₁
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((B₂.toDual b₂).symm (B₁ v)) = B₁ v

Tactic:
erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ IsAtomistic α

Tactic:
refine CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_
  obtain ⟨s, hs, hs'⟩ := hS.atomistic a (h ▸ le_top)
  exact ⟨s, hs', fun I hI ↦ hS.isAtom I (hs hI)⟩

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
⊢ ker (B.restrict p) = Submodule.comap p.subtype (ker B)

Tactic:
by
  ext ⟨z, hz⟩
  simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · ext w
    obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w
    simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩
  · ext ⟨x, hx⟩
    simpa using LinearMap.congr_fun h x

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

Goal state before:
pp: 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
x : L
y : ↥I
hy : y ∈ ↑↑J
⊢ x ∈ ⊤

Tactic:
apply LieSubmodule.mem_top

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

Goal state before:
pp: case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI₁ : IsAtom I
⊢ ¬IsLieAbelian ↥I

Tactic:
hI₂

Goal state after:
case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI₁ : IsAtom I
hI₂ : IsLieAbelian ↥I
⊢ False
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case C
k : Type u
inst✝ : Field k
a✝ : k
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.C a✝) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.C a✝))

Tactic:
exact isIntegral_algebraMap

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

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (-↑p • χ₁ + χ₂) = ⊥

Tactic:
rw [neg_smul, ← smul_neg, natCast_zsmul]
    exact hp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Tactic:
have : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q := by simp
  simp_rw [genWeightSpaceChain_def, this]

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

Goal state before:
pp: case mem
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
hu : u ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) = 0

Tactic:
obtain ⟨y, hy, z, hz, hyz⟩ := hu
    let f : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(y : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M α χ p q hq hy hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    let g : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(z : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left M α χ p q hp hz hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    have hfg : toEnd R H _ u = ⁅f, g⁆ := by
      ext
      rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
      simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
        AddSubgroupClass.coe_sub, f, g]
    simp [hfg]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k ↦ ↑(genWeightSpace M (k • α + χ))
⊢ iSupIndep fun i ↦ genWeightSpace M (↑i • α + χ)

Tactic:
refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun k ↦ ↑(genWeightSpace M (k • α + χ))
i j : ↥(Finset.Ioo p q)
hij : ↑i • α + χ = ↑j • α + χ
⊢ i = j
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case mem
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x u : L
hu : u ∈ {x | ∃ u v, ⁅u, v⁆ = x}
⊢ (trace R M) (φ u * y) = 0

Tactic:
obtain ⟨a, b, rfl⟩ := hu

Goal state after:
case mem
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b : L
⊢ (trace R M) (φ ⁅a, b⁆ * y) = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: case mem
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b : L
⊢ (trace R M) (φ ⁅a, b⁆ * y) = 0

Tactic:
obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)

Goal state after:
case mem
R : Type u_1
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
h : traceForm R L M = 0
y : End R M
hy : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
x a b c : L
hbc : φ c = ⁅y, φ b⁆
⊢ (trace R M) (φ ⁅a, b⁆ * y) = 0