mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ (((Pi.basis fun x ↦ b).reindex
            ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
              (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
                  (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
              (j₁, j₂)))))
      (i₁, i₂) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Basis.repr_reindex_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
                  (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
              (j₁, j₂)))))
      (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
        (i₁, i₂)) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 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

Tactic:
· exact 1

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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
    convert! this using 2
    ext x
    exact h x
  rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]
  exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Tactic:
by
  rw [quotMapOfEquivQuotMapCMapMk, Ideal.quotEquivOfEq_symm]
  exact Ideal.quotEquivOfEq_mk _ _

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ T ⊗[R] AdjoinRoot p ≃ₐ[T] AdjoinRoot q

Tactic:
refine .ofAlgHom
    (Algebra.TensorProduct.lift (algHom T T _)
      (mapAlgHom includeRight p q <| by exact h.symm.dvd) fun _ _ ↦ .all ..)
    (liftAlgHom _ (Algebra.TensorProduct.map (AlgHom.id T T)
      (((Algebra.ofId S (AdjoinRoot p))).restrictScalars R)) (1 ⊗ₜ root _) ?_) ?_ ?_

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))))
      (1 ⊗ₜ[R] root p) q =
    0

case refine_2
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯).comp
      (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
        (1 ⊗ₜ[R] root p) ?refine_1) =
    AlgHom.id T (AdjoinRoot q)

case refine_3
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
          (1 ⊗ₜ[R] root p) ?refine_1).comp
      (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯) =
    AlgHom.id T (T ⊗[R] AdjoinRoot p)
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
⊢ (ad R L) (D x) = 0

Tactic:
rw [LieModule.mem_maxTrivSubmodule] at hD

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : ∀ (x : L), ⁅x, D⁆ = 0
x : L
⊢ (ad R L) (D x) = 0
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
x : L
hx : x ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
m : M
⊢ ⁅t • x, m⁆ ∈ N

Tactic:
by rw [smul_lie]; exact N.smul_mem t (hx m)

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑(derivedSeries R L k) = ↑(derivedSeries ℤ L k)

Tactic:
← LieSubmodule.coe_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑↑(derivedSeries R L k) = ↑(derivedSeries ℤ L k)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑↑(derivedSeries R L k) = ↑(derivedSeries ℤ L k)

Tactic:
← LieSubmodule.coe_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑↑(derivedSeries R L k) = ↑↑(derivedSeries ℤ L k)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
⊢ derivedSeries R L 1 < ⊤

Tactic:
by
  obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)
  rw [lt_top_iff_ne_top]
  intro contra
  rw [LieIdeal.derivedSeries_eq_top n contra] at hn
  exact top_ne_bot hn

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

Goal state before:
pp: 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
k : ℕ
⊢ ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries ℤ L M k)

Tactic:
← LieSubmodule.coe_toSubmodule,

Goal state after:
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
k : ℕ
⊢ ↑↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries ℤ L M k)
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✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x✝ y✝ : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) x) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
            ((TensorProduct.map f.toLinearMap ↑g) x) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) x) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
              ((TensorProduct.map f.toLinearMap ↑g) x) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) x) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
              ((TensorProduct.map f.toLinearMap ↑g) x)) →
      ((TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) y) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
              ((TensorProduct.map f.toLinearMap ↑g) y) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) y) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
                ((TensorProduct.map f.toLinearMap ↑g) y) →
            (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) y) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
                ((TensorProduct.map f.toLinearMap ↑g) y)) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) (x + y)) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
              ((TensorProduct.map f.toLinearMap ↑g) (x + y)) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) (x + y)) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
                ((TensorProduct.map f.toLinearMap ↑g) (x + y)) →
            (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) (x + y)) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
                ((TensorProduct.map f.toLinearMap ↑g) (x + y))

Tactic:
by simp_all

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

Goal state before:
pp: 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
l k : ℕ
⊢ l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l

Tactic:
induction k generalizing l with
  | zero => exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl
  | succ k ih =>
    intro h
    rcases Nat.of_le_succ h with (hk | hk)
    · rw [lowerCentralSeries_succ]
      exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
    · exact hk.symm ▸ le_rfl

Goal state after:
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
N : LieSubmodule R L M
m : A ⊗[R] M
⊢ m ∈ baseChange A N ↔ m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)

Tactic:
by
  rw [← Submodule.baseChange_eq_span]; rfl

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ (minpoly G F x).Monic

Tactic:
simp only [minpoly]

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ ((prodXSubSMul G F x).toSubring (subfield G F).toSubring ⋯).Monic
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

Goal state after:
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 : ∃ a ∈ f.roots.toFinset, (algebraMap K L) a = y
⊢ y ∈ ↑⊥
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this : Module.rank R ↥(toSubmodule A) ≤ Module.rank R ↥(toSubmodule (A ⊔ B))
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,

Goal state after:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this : Module.rank R ↥(toSubmodule A) ≤ Module.rank R ↥(toSubmodule (A ⊔ B))
⊢ finrank R ↥(A ⊔ B) ≤ 0 * finrank R ↥B
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 K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : ¬f = 0
⊢ ↥⊤ →ₐ[K] F

Tactic:
← adjoin_rootSet L f

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 K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : ¬f = 0
⊢ ↥(Algebra.adjoin K (f.rootSet L)) →ₐ[K] F
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ E' ≤ adjoin L ↑s

Tactic:
← restrictScalars_le_iff K,

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ restrictScalars K E' ≤ restrictScalars K (adjoin L ↑s)
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
i : ι → E
x : E
⊢ (∃ r ∈ Algebra.adjoin F (Set.range i), ∃ s ∈ Algebra.adjoin F (Set.range i), x = r / s) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
Algebra.adjoin_range_eq_range_aeval,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ (∃ r ∈ (MvPolynomial.aeval i).range, ∃ s ∈ (MvPolynomial.aeval i).range, x = r / s) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s
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
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯

Tactic:
apply minpoly.dvd

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := ⋯
K' : IntermediateField F E := ⋯
hsub : K' ≤ K
⊢ (aeval α) (g.toSubring K'.toSubring ⋯) = 0
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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional F ↥F⟮x⟯
h : ¬n + 1 < finrank F ↥L'
⊢ False

Tactic:
have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)

Goal state after:
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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional F ↥F⟮x⟯
h : ¬n + 1 < finrank F ↥L'
h1 : L = L'
⊢ False
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

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:
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
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F (AdjoinSimple.gen F α)) = 0

Tactic:
minpoly_gen

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0
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
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0

Tactic:
exact (mem_aroots.mp x.2).2

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ minpoly K (AdjoinSimple.gen K pb.gen) = minpoly K pb.gen

Tactic:
minpoly_gen

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ minpoly K pb.gen = minpoly K pb.gen
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (max #↑(Set.range ⇑(algebraMap F E) ∪ s) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
lift_max,

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ max (Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s)) (Cardinal.lift.{u, v} ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} (max (max #↑(Set.range ⇑(algebraMap F E)) #↑s) ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
lift_max,

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ max (max (Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E))) (Cardinal.lift.{u, v} #↑s))
      (Cardinal.lift.{u, v} ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule

Tactic:
← Nat.sub_add_cancel hl,

Goal state after:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs (l - k + k) ⊥ = H.toLieSubmodule
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
inst✝ : IsNoetherian R L
⊢ H.toLieSubmodule = rootSpace H 0 ↔ H.IsCartanSubalgebra

Tactic:
rw [← zeroRootSubalgebra_eq_iff_is_cartan, ← LieSubalgebra.toSubmodule_inj,
    ← LieSubmodule.toSubmodule_inj]

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
inst✝ : IsNoetherian R L
⊢ ↑H.toLieSubmodule = ↑(rootSpace H 0) ↔ (zeroRootSubalgebra R L H).toSubmodule = H.toSubmodule
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule 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
inst✝ : IsTriangularizable K L M
N : LieSubmodule K L M
χ_N : Weight K L ↥N
hN : LieSubmodule.map N.incl (genWeightSpace ↥N ⇑χ_N) ≤ N
⊢ N ⊓ genWeightSpace M ⇑χ_N ≤ ⨆ χ, N ⊓ genWeightSpace M ⇑χ

Tactic:
by
    by_cases h : genWeightSpace M (χ_N : L → K) = ⊥
    · simp [h]
    · exact le_iSup_of_le ⟨_, h⟩ le_rfl

Goal state after: