mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.OfAssociative

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
⊢ IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩

Goal state after:
case refine_1
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
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
⊢ x = 0

case refine_2
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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy : (toEnd R L M) x = (toEnd R L M) y
⊢ x = y
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ⊆ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) ↑(sInf S)

Tactic:
simp only [coe_sInf]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), ↑K ⊆ ↑K' ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, ↑s)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = ↑N
a✝ b✝ : M
x : a✝ ∈ ↑N
y : b✝ ∈ ↑N
⊢ a✝ + b✝ ∈ ↑N

Tactic:
exact N.add_mem' x y

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⨅ i, ↑(p i)

Tactic:
rw [iInf, sInf_toSubmodule]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sInf {x | ∃ s ∈ range fun i ↦ p i, ↑s = x} = ⨅ i, ↑(p i)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤

Tactic:
LieModuleHom.range_eq_top

Goal state after:
R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective ⇑e.toLieModuleHom
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ map f ⁅I, N⁆ = ⁅I, map f N⁆

Tactic:
rw [← toSubmodule_inj, toSubmodule_map, lieIdeal_oper_eq_linear_span,
    lieIdeal_oper_eq_linear_span, Submodule.map_span]
  congr
  ext m
  simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
⊢ minpoly A ((algebraMap A B) a) = X - C a

Tactic:
by
  nontriviality A
  refine (unique' A _ (monic_X_sub_C a) ?_ ?_).symm
  · rw [map_sub, aeval_C, aeval_X, sub_self]
  simp_rw [or_iff_not_imp_left]
  intro q hl h0
  rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl
  rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢
  rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
⊢ eval a (eval b P) = 0

Tactic:
rcases h with ⟨_, _, rfl⟩
    simp

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : f = 0
⊢ f.natDegree < d

Tactic:
simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢
      first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : f = 0
⊢ f.degree < ↑d

Tactic:
simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢
      first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : (minpoly R x).Monic
⊢ (aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = (aeval x) (f %ₘ minpoly R x)

Tactic:
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) = 1

Tactic:
simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ x ∈ s.attach, (X - C (f ↑x))).Separable

Tactic:
exact
      separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.ext <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ x ^ 1

Tactic:
by simpa using! bijective_id

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
hg3 : g.natDegree < N.succ
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩

Goal state after:
case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
n : ℕ
g : F[X]
hg4 : g.Separable
hg : Irreducible ((expand F (p ^ n)) g)
hgf : (expand F p) ((expand F (p ^ n)) g) = f
hg1 : ((expand F (p ^ n)) g).natDegree * p = N.succ
hg2 : ((expand F (p ^ n)) g).natDegree ≠ 0
hg3 : ((expand F (p ^ n)) g).natDegree < N.succ
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
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
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ ∀ (i : Fin f.natDegree), (powerBasisAux hf) i = root f ^ ↑i

Tactic:
by simp [powerBasisAux]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Function.Surjective ⇑(toAdjoin R x)

Tactic:
← AlgHom.range_eq_top,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (toAdjoin R x).range = ⊤
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_1
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
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ i ∈ R2N, (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j)

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Goal state after:
case calc_1
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
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
x✝ : i ∈ R2N
⊢ (↑i !)⁻¹ • (a + b) ^ i = (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j)
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case smul
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
x✝ : L
t : R
x : L
hx✝ : x ∈ LieSubalgebra.lieSpan R L s
hx : D1 x = D2 x
⊢ D1 (t • x) = D2 (t • x)

Tactic:
| smul t x _ hx =>

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 :
  (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] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P

Tactic:
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] 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
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = ↑((toModuleHom R L M).comp (mapIncl I N)).range

Tactic:
LieModuleHom.toSubmodule_range,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = (↑((toModuleHom R L M).comp (mapIncl I N))).range
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ((bracket' R A L L) x) x = 0

Tactic:
refine x.induction_on ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ((bracket' R A L L) 0) 0 = 0

case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x : A) (y : L), ((bracket' R A L L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0

case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) x = 0 → ((bracket' R A L L) y) y = 0 → ((bracket' R A L L) (x + y)) (x + y) = 0
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
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
    ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z)

Tactic:
refine x.induction_on ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : 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
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ((bracket' R A L M) 0) (((bracket' R A L M) y) z) =
    ((bracket' R A L M) (((bracket' R A L L) 0) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) 0) z)

case refine_2
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
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x : A) (y_1 : L),
    ((bracket' R A L M) (x ⊗ₜ[R] y_1)) (((bracket' R A L M) y) z) =
      ((bracket' R A L M) (((bracket' R A L L) (x ⊗ₜ[R] y_1)) y)) z +
        ((bracket' R A L M) y) (((bracket' R A L M) (x ⊗ₜ[R] y_1)) z)

case refine_3
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
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)
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:
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule, derivedSeries_def,
    derivedSeries_def]
  induction k with
  | zero => rfl
  | succ k ih =>
    rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
    rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
    rw [Set.ext_iff] at ih
    simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
    simp only [ih]
    apply le_antisymm
    · exact coe_derivedSeries_eq_int_aux _ _ L k ih
    · simp

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsLieAbelian L
⊢ IsSolvable L

Tactic:
by
  use 1
  rw [← abelian_iff_derived_one_eq_bot, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv]
  infer_instance

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
k✝ : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
    exact LieSubmodule.mono_lie_right ⊤ ih

Goal state after:
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Fintype V
b : Basis (↥(finsetBasisIndex K V)) K V := finsetBasis K V
⊢ Fintype.card K ^ Fintype.card ↥(finsetBasisIndex K V) = Fintype.card K ^ finrank K V

Tactic:
← Module.finrank_eq_card_basis b

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Fintype V
b : Basis (↥(finsetBasisIndex K V)) K V := finsetBasis K V
⊢ Fintype.card K ^ finrank K V = Fintype.card K ^ finrank K V
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
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 F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) (Algebra.adjoin F (f.rootSet K)))
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
adjoin_rootSet,

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 F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) ⊤)
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
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 F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K ((Polynomial.map (algebraMap F K) g).rootSet L)) = ⊤

Tactic:
adjoin_rootSet,

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 F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F ⊤ = ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ (aeval 0) p = 0 ∧ (aeval 0) q = 0

Tactic:
h.left,

Goal state after:
case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ (aeval 0) 0 = 0 ∧ (aeval 0) q = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : ¬FiniteDimensional K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
FiniteDimensional,

Goal state after:
case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : ¬Module.Finite K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ¬∀ (S : Finset E), ∃ τ ≥ y, ↑S ⊆ ↑τ.carrier
⊢ False

Tactic:
push Not at ϕ_max

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
⊢ False