mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ (Polynomial.map (algebraMap K L) p).Splits

pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤

Tactic:
· rw [← f.toAlgHom.comp_algebraMap, ← map_map]
    exact (splits F p).map _

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (p.rootSet L) = ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
⊢ ∃ z, z ^ n = x

Tactic:
by
  have : degree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn x]
    exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
  obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
  use z
  simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
  exact sub_eq_zero.1 hz

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

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
⊢ p.Splits

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp0 : p = 0
⊢ p.Splits

case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp0 : ¬p = 0
⊢ p.Splits
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
ha : (σ a).Nonempty
n : ℕ
⊢ σ (a ^ n) = (fun x ↦ x ^ n) '' σ a

Tactic:
by
  simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval_of_nonempty a (X ^ n) ha

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
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
this : ∀ (ω : Ω), ∃ π, ∀ θ ≥ ↑π, { carrier := adjoin F ↑S, emb := ω } ≤ θ → θ.carrier ≠ (↑π).carrier ⊔ adjoin F ↑S
⊢ False

Tactic:
choose π hπ using this

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
⊢ 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
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ ⨆ i, adjoin F ((minpoly F i.snd).rootSet E)

Tactic:
refine SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ ?_)
    (subset_adjoin F (rootSet (minpoly F x1) E) ?_)

Goal state after:
case refine_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ adjoin F ((minpoly F x1).rootSet E) ≤ adjoin F ((minpoly F ⟨i, ⟨x1, hx1⟩⟩.snd).rootSet E)

case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ (minpoly F x1).rootSet E
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
hp : Nat.Prime (finrank F E)
⊢ IsSimpleOrder (IntermediateField F E)

Tactic:
refine { toNontrivial := ?_, eq_bot_or_eq_top := ?_ }

Goal state after:
case refine_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
⊢ Nontrivial (IntermediateField F E)

case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
⊢ ∀ (a : IntermediateField F E), a = ⊥ ∨ a = ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
ih : ∃ L, FiniteDimensional F ↥L ∧ n < finrank F ↥L
⊢ ∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L

Tactic:
obtain ⟨L, fin, hn⟩ := ih
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
      contrapose! hnfd
      rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
      exact topEquiv.toLinearEquiv.finiteDimensional
    let L' := L ⊔ F⟮x⟯
    have := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
    refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
    have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
    have h2 : F⟮x⟯ ≤ L' := le_sup_right
    exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
⊢ s ∈ ↑φ.carrier

pp: case refine_2
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f

Tactic:
· rcases φ.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩
    exact (hφ h1).1 h2

Goal state after:
case refine_2
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
⊢ (φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
⊢ Irreducible (f.comp g)

Tactic:
suffices natDegree p = natDegree f * natDegree g from (associated_of_dvd_of_natDegree_le hp₂ H₁
    (this.trans natDegree_comp.symm).ge).irreducible hp₁

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
⊢ p.natDegree = f.natDegree * g.natDegree
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
⊢ p.natDegree = f.natDegree * g.natDegree

Tactic:
have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f := by
    rw [adjoin.finrank, ← key₁]
    exact IsIntegral.of_finite _ _

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
m₃ : M₃
⊢ m₃ ∈ (↑g ∘ₗ TensorProduct.mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x)).range → m₃ ∈ 𝕎(M₃, χ₁ + χ₂, x)

Tactic:
simp only [TensorProduct.mapIncl, LinearMap.mem_range, LinearMap.coe_comp,
    LieModuleHom.coe_toLinearMap, Function.comp_apply, exists_imp, Module.End.mem_maxGenEigenspace]

Goal state after:
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
m₃ : M₃
⊢ ∀ (x_1 : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)),
    g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) x_1) = m₃ →
      ∃ k, (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k) m₃ = 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
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
N : LieSubmodule K L M
inst✝ : IsTriangularizable K L M
y : L
⊢ ⨆ φ, ((toEnd K L ↥N) y).maxGenEigenspace φ = ⊤

Tactic:
← N.toEnd_restrict_eq_toEnd y

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
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
N : LieSubmodule K L M
inst✝ : IsTriangularizable K L M
y : L
⊢ ⨆ φ, End.maxGenEigenspace (LinearMap.restrict ((toEnd K L M) y) ⋯) φ = ⊤
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
rw [disjoint_iff, ← hI.lt_iff, lt_iff_le_and_ne]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ ∀ (b : α) (x : Set α),
    ∀ x_1 ∈ C, ∀ (x_2 : IsCompactElement x_1) (x_3 : x_1 ≤ sSup S), T x_1 x_2 x_3 = x → b ∈ x → b ≤ sSup C

Tactic:
rintro a T b hbC hb hbS rfl haT

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
a b : α
hbC : b ∈ C
hb : IsCompactElement b
hbS : b ≤ sSup S
haT : a ∈ T b hb hbS
⊢ a ≤ sSup C
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T = a

Tactic:
have : a ≤ sSup T := le_sSup haT

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ sSup T = a
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✝ : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
⊢ I = ⊥

Tactic:
apply (IsSimple.eq_bot_or_eq_top I).resolve_right

Goal state after:
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 : IsLieAbelian ↥I
⊢ ¬I = ⊤
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, ↑I.incl y⁆ ∈ Submodule.map ↑I.incl ↑J

Tactic:
simp only [Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists]

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 ∧ ↑I.incl ⟨a_1, b⟩ = ⁅a, ↑I.incl y⁆
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B ↑m) (y + z) = 0

pp: case refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (x_1 : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) x_1) m = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B (y + z)) ↑m = 0

Tactic:
· rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]

Goal state after:
case refine_2
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (x_1 : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) x_1) m = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B (y + z)) ↑m = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem
ι : 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
z : L
hz : z ∈ lieSpan R L (range b.f)
i : ι
⊢ ⁅b.e i, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact LieSubmodule.mem_sup_left <| this i z hz

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
let s' := s.erase J
  have hs' : s' ⊂ s := Finset.erase_ssubset hJs
  have hs'S : ↑s' ⊆ S := Set.Subset.trans (Finset.coe_subset.mpr hs'.subset) hs
  -- If we show that `I` is contained in the supremum `K` of the complement of `J` in `s`,
  -- then we are done by recursion.
  set K := s'.sup id
  suffices I ≤ K by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩
  -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
  -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
  intro x hx
  obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y ∈ id J, ∃ z ∈ K, y + z = x := by
    rw [← LieSubmodule.mem_sup, ← Finset.sup_insert, Finset.insert_erase hJs]
    exact hI.le hx
  -- If we show that `y` is contained in the center of `J`,
  -- then we find `x = z`, and hence `x` is contained in the supremum of `s'`.
  -- Since `x` was arbitrary, we have shown that `I` is contained in the supremum of `s'`.
  suffices ⟨y, hy⟩ ∈ LieAlgebra.center R J by
    have _inst := isSimple_of_isAtom J (hs hJs)
    simp_all
  -- To show that `y` is in the center of `J`,
  -- we show that any `j ∈ J` brackets to `0` with `z` and with `x = y + z`.
  -- By a simple computation, that implies `⁅j, y⁆ = 0`, for all `j`, as desired.
  intro j
  suffices ⁅(j : L), z⁆ = 0 ∧ ⁅(j : L), y + z⁆ = 0 by
    rw [lie_add, this.1, add_zero] at this
    ext
    exact this.2
  rw [← LieSubmodule.mem_bot (R := R) (L := L), ← LieSubmodule.mem_bot (R := R) (L := L)]
  constructor
  -- `j` brackets to `0` with `z`, since `⁅j, z⁆` is contained in `⁅J, K⁆ ≤ J ⊓ K`,
  -- and `J ⊓ K = ⊥` by the independence of the atoms.
  · apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.notMem_erase _ _)).le_bot
    apply LieSubmodule.lie_le_inf
    apply LieSubmodule.lie_mem_lie j.2
    simpa only [K, Finset.sup_id_eq_sSup] using hz
  -- By similar reasoning, `j` brackets to `0` with `x = y + z ∈ I`, if we show `J ⊓ I = ⊥`.
  suffices J ⊓ I = ⊥ by
    apply this.le
    apply LieSubmodule.lie_le_inf
    exact LieSubmodule.lie_mem_lie j.2 hx
  -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`.
  apply ((hs hJs).le_iff.mp _).resolve_right
  · contrapose hJI
    rw [← hJI]
    exact inf_le_right
  exact inf_le_left

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

Goal state before:
pp: case neg
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainTopCoeff α β
hα : ¬α = 0
⊢ genWeightSpace M (n • α + ⇑β) ≠ ⊥

Tactic:
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, chainTopCoeff_add_one _ _ hα] at hn
  exact Nat.find_min (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists hn

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ (map (↑e.flip.flip) (map (↑e.symm) p)).dualCoannihilator = map (↑e.flip.symm) (map (↑e.flip) p.dualCoannihilator)

Tactic:
LinearEquiv.flip_flip,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R M)
this : IsReflexive R N
⊢ (map (↑e) (map (↑e.symm) p)).dualCoannihilator = map (↑e.flip.symm) (map (↑e.flip) p.dualCoannihilator)
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
in_span : ↑S n ∈ span R (↑S '' Set.Iio m)
⊢ head ∈ span R (↑S '' Set.Iio m)

Tactic:
have smul_span := smul_mem (span R (S '' Set.Iio m)) (P.leadingCoeff • u) in_span

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
in_span : ↑S n ∈ span R (↑S '' Set.Iio m)
smul_span : (P.leadingCoeff • u) • ↑S n ∈ span R (↑S '' Set.Iio m)
⊢ head ∈ span R (↑S '' Set.Iio m)