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

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f

Tactic:
exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
⊢ IsUnit f ∨ n = 0

Tactic:
by
  rw [or_iff_not_imp_right]
  rintro hn : n ≠ 0
  have hf2 : derivative (expand F (p ^ n) f) = 0 := by
    rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
  rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
  rcases hf with ⟨r, hr, hrf⟩
  rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
  rwa [hrf, isUnit_C]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative]
  · rintro ⟨⟩
  exact hf.natDegree_pos.ne'

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
⊢ M ≃ₗ[R] M

Tactic:
by_cases hR : Nontrivial R

Goal state after:
case pos
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : Nontrivial R
⊢ M ≃ₗ[R] M

case neg
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : ¬Nontrivial R
⊢ M ≃ₗ[R] M
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ (e.det v • (Basis.mk hli hsp).coord k) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v k) ((Basis.mk hli hsp) k)

Tactic:
simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ e.det v * ((Basis.mk hli hsp).coord k) (v k) = ↑e.det (update v k (v k))
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)

Tactic:
simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ e.det v * ((Basis.mk hli hsp).coord i) (v k) = ↑e.det (update v i (v k))
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
h₃ : IsNilpotent b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
⊢ exp (a + b) = exp a * exp b

Tactic:
obtain ⟨n₂, hn₂⟩ := h₃

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
⊢ exp (a + b) = exp a * exp b
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ P.newtonMap x = x - ↑h.unit⁻¹ * (aeval x) P

Tactic:
by
  simp [newtonMap_apply, Ring.inverse, h]

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : ¬IsUnit ((aeval x) (derivative P))
⊢ P.newtonMap x = x

Tactic:
by
  simp [newtonMap_apply, Ring.inverse, h]

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  eval (P.newtonMap^[n] x + -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P)
      (map (algebraMap R S) P) =
    eval (P.newtonMap^[n] x) (map (algebraMap R S) P) +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣ (aeval (P.newtonMap^[n + 1] x)) P

Tactic:
rw [eval_map_algebraMap, eval_map_algebraMap] at hd

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣ (aeval (P.newtonMap^[n + 1] x)) P
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
h : lowerCentralSeries R L M 1 = ⊥
⊢ IsTrivial L M

Tactic:
· rw [LieSubmodule.eq_bot_iff] at h; apply IsTrivial.mk; intro x m; apply h
    apply LieSubmodule.subset_lieSpan
    simp only [Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and, Set.mem_ofPred]
    exact ⟨x, m, rfl⟩

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

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ Submodule.map g ↑(lowerCentralSeries R L M (k + 1)) ≤ ↑(lowerCentralSeries R L₂ M₂ (k + 1))

Tactic:
rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
      Submodule.span_le]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ ⇑g '' {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} ⊆ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))
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
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
⊢ IsIntegral K x ∧ (map (algebraMap K E) (minpoly K x)).Splits

Tactic:
obtain ⟨hx, hhx⟩ := h.out x

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
hx : IsIntegral F x
hhx : (map (algebraMap F E) (minpoly F x)).Splits
⊢ IsIntegral K x ∧ (map (algebraMap K E) (minpoly K x)).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m✝ : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
⊢ m • (↑f * f') = ↑f * m • f'

Tactic:
rw [smul_mul', f.prop m]

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

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ IsAlgClosed k'

Tactic:
apply IsAlgClosed.of_exists_root
  intro p hmp hp
  have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
    rw [degree_map]
    exact ne_of_gt (degree_pos_of_irreducible hp)
  rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩
  use e x
  rw [IsRoot] at hx
  apply e.symm.injective
  rw [map_zero, ← hx]
  clear hx hpe hp hmp
  induction p using Polynomial.induction_on <;> simp_all

Goal state after:
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
⊢ x ∈ adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s

Tactic:
by
  rw [← mem_adjoin_range_iff, Subtype.range_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
n : ℕ
ih :
  ∀ m < n,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_dim : finrank K V = n
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
rcases n with - | n

Goal state after:
case h.zero
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ m < 0,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = 0
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
  have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
  rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix
  obtain ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK ((algHomAdjoinIntegralEquiv F ix).symm
    ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)
  exact ⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <|
    algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩

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

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -⁅f, e⁆ = h

Tactic:
lie_skew,

Goal state after:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅e, f⁆ = h
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
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ⁅x, m⁆ ∈ genWeightSpace M (χ₁ + χ₂)

Tactic:
rw [genWeightSpace, LieSubmodule.mem_iInf]

Goal state after:
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
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ∀ (i : ↥H), ⁅x, m⁆ ∈ genWeightSpaceOf M ((χ₁ + χ₂) i) i
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case add
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
x✝ y✝ : L
hx✝ : x✝ ∈ ⨆ i ∈ s, rootSpace H i
hy✝ : y✝ ∈ ⨆ i ∈ s, rootSpace H i
hu : ⁅x✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hv : ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x✝ + y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
| add _ _ _ _ hu hv =>

Goal state after:
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
χ : Weight R L M
x : L
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥

Tactic:
have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot

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
χ : Weight R L M
x : L
this : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥
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
inst✝ : Nontrivial ↥H
⊢ Nontrivial ↥(genWeightSpace L 0)

Tactic:
obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, e⟩ := exists_pair_ne H

Goal state after:
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
inst✝ : Nontrivial ↥H
x : L
hx : x ∈ H
y : L
hy : y ∈ H
e : ⟨x, hx⟩ ≠ ⟨y, hy⟩
⊢ Nontrivial ↥(genWeightSpace L 0)
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
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl M₀ M₁

Tactic:
← h₃,

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
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
h₄ : LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁
⊢ IsCompl (LieSubmodule.map M₀ₓ.incl 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
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
⊢ B.dualBasis hB (B.flip.dualBasis ⋯ b) = b

Tactic:
by
  ext i
  refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))
  simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]

Goal state after:
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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
⊢ InjOn (fun χ ↦ genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂)

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₂ : χ₂ ∈ {χ | genWeightSpace M χ ≠ ⊥}
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
⊢ χ₁ = χ₂
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
B : BilinForm R M
hB : B.IsRefl
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊤ ↔ x✝ ∈ ker B

Tactic:
simp [LinearMap.ext_iff, hB.eq_iff]

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ {a | IsAtom a} ⊆ S

Tactic:
intro a ha

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ∈ S
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toEnumFinset.card = m.card

Tactic:
rw [Finset.card, ← Multiset.card_map Prod.fst m.toEnumFinset.val]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ (map Prod.fst m.toEnumFinset.val).card = m.card
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ((fun a ↦ (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) a) ''
          {AdjoinRoot.root f.factor} ∪
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤

Tactic:
rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
by
  rw [f.mem_genEigenspace] at hm
  obtain ⟨l, -, hm⟩ := hm
  rw [← f.mem_genEigenspace_nat] at hm
  set p := f.genEigenspace μ l
  have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ l
  have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l
  have h₃ : MapsTo (f - g) p p :=
    mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ l
  have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l
  replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) :=
    (Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g)
  suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by
    replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
    simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩
  simpa [LinearMap.restrict_sub h₄ h₃] using (LinearMap.restrict_commute hfg h₄ h₃).isNilpotent_sub
    (f.isNilpotent_restrict_sub_algebraMap μ l) (Module.End.isNilpotent.restrict h₃ hnil)

Goal state after: