mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
x : k[G]
y : α →₀ k[G]
⊢ (free k G α).asModuleEquiv.symm.toAddEquiv.toFun (x • y) =
    (RingHom.id k[G]) x • (free k G α).asModuleEquiv.symm.toAddEquiv.toFun y

Tactic:
by
    simp only [AddHom.toFun_eq_coe, coe_toAddHom, LinearEquiv.coe_coe, RingHom.id_apply,
      (free k G α).asModuleEquiv.symm_apply_eq, asModuleEquiv_map_smul,
      LinearEquiv.apply_symm_apply]
    induction x using MonoidAlgebra.induction_linear with
    | zero => simp
    | add => simp [*, add_smul]
    | single g a =>
    induction y using Finsupp.induction_linear with
    | zero => simp
    | add => simp [*]
    | single h y =>
    induction y using MonoidAlgebra.induction_linear with
    | zero => simp
    | add => simp [*]
    | single i b => simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝¹ : Nonempty ι
inst✝ : NeZero 2
contra : b.support = ∅
inhabited_h : Inhabited ι
⊢ False

Tactic:
simpa [P.ne_zero default, contra] using b.root_mem_or_neg_mem default

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
⊢ f ≠ 0 → 0 < f

Tactic:
hf'

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
f✝ : ι → ℤ
hf✝ : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
⊢ 0 < f
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
x✝ : 0 ≤ f ∧ ∃ i, 0 i < f i
contra : f ≤ 0
h : 0 ≤ f
i : ι
hi : 0 i < f i
⊢ False

Tactic:
by simp [le_antisymm contra h] at hi

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Star

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x * y = y * x

Tactic:
← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx),

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x * y = star (y * x)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
rcases Classical.em (LimZero f) with h | h
  · simp [*]
  simp only [false_or, h]
  rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
  rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
  refine (le_total 0 (f i)).imp ?_ ?_ <;>
    refine fun h => ⟨K, K0, i, fun j ij => ?_⟩ <;>
    have := (hi _ ij).1 <;>
    obtain ⟨h₁, h₂⟩ := hi _ le_rfl
  · rwa [abs_of_nonneg] at this
    rw [abs_of_nonneg h] at h₁
    exact
      (le_add_iff_nonneg_right _).1
        (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)
  · rwa [abs_of_nonpos] at this
    rw [abs_of_nonpos h] at h₁
    rw [← sub_le_sub_iff_right, zero_sub]
    exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
⊢ mk (if h : f.LimZero then 0 else f.inv h) = mk (if h : g.LimZero then 0 else g.inv h)

Tactic:
by
      have := limZero_congr fg
      by_cases hf : LimZero f
      · simp [hf, this.1 hf]
      · have hg := mt this.2 hf
        simp only [hf, dite_false, hg]
        have If : mk (inv f hf) * mk f = 1 := mk_eq.2 (inv_mul_cancel hf)
        have Ig : mk (inv g hg) * mk g = 1 := mk_eq.2 (inv_mul_cancel hg)
        have Ig' : mk g * mk (inv g hg) = 1 := mk_eq.2 (mul_inv_cancel hg)
        rw [mk_eq.2 fg, ← Ig] at If
        rw [← mul_one (mk (inv f hf)), ← Ig', ← mul_assoc, If, mul_assoc, Ig', mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε

Tactic:
exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr
x a b : ℝ
h✝ : a < b
⊢ ∀ (c : ℝ), a + c = b + c ∨ a + c < b + c

Tactic:
· refine fun c => Or.inr ?_
      induction a using Real.ind_mk with | _ a =>
      induction b using Real.ind_mk with | _ b =>
      induction c using Real.ind_mk with | _ c =>
      simp only [mk_lt, ← mk_add] at *
      change Pos _ at *
      rwa [add_sub_add_right_eq_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x

Tactic:
← dotProduct_single_one v x,

Goal state after:
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v ⬝ᵥ Pi.single x 1 = w x
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
obtain ha | ha := ha
  · obtain hb | hb := hb
    · exact Or.inl (CauSeq.sup_lt ha hb)
    · replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
      refine le_of_le_of_eq (Or.inr ?_) hb
      exact CauSeq.sup_eq_right ha
  · replace hb := le_of_le_of_eq hb (Setoid.symm ha)
    refine le_of_le_of_eq (Or.inr ?_) ha
    exact CauSeq.sup_eq_left hb

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹

Tactic:
pow_succ A,

Goal state after:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
⊢ False

Tactic:
have h_iSup : ⨆ μ ∈ Set.range d, eigenspace (toLin b b (diagonal d)) μ = ⊤ := by
      rw [eq_top_iff, ← b.span_eq, Submodule.span_le]
      rintro - ⟨i, rfl⟩
      simp only [SetLike.mem_coe]
      apply Submodule.mem_iSup_of_mem (d i)
      apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩
      rw [mem_eigenspace_iff]
      exact (hasEigenvector_toLin_diagonal d i b).apply_eq_smul

Goal state after:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
d : n → R
μ : R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ ?m.73

Tactic:
by simpa [Finsupp.ext_iff] using hx

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
← Finset.prod_int_mod,

Goal state after:
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ (∏ i ∈ range k, (n % ↑k ! + ↑i)) % ↑k ! = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
by
  rcases eq_or_ne f 0 with rfl | hf
  · rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
  · exact eq_of_degree_sub_lt_of_eval_finset_eq s
      (lt_of_lt_of_le (degree_sub_lt_left h_deg_eq hf hlc) h_deg_le) h_eval

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v) r

Tactic:
constructor <;> intro h

Goal state after:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r

case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ ∑ i_1 ∈ {i, j}, (interpolate (insert i_1 (s \ {i, j})) v) r * Lagrange.basis {i, j} v i_1 =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s

Tactic:
sum_insert (notMem_singleton.mpr hij),

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * Lagrange.basis {i, j} v i +
      ∑ x ∈ {j}, (interpolate (insert x (s \ {i, j})) v) r * Lagrange.basis {i, j} v x =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
⊢ y ∈ (engel R x).normalizer → y ∈ engel R x

Tactic:
hy

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hy : y ∈ (engel R x).normalizer
⊢ y ∈ engel R x
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ Submodule.map N.subtype ⊤ ≤ (engel R x).toSubmodule ⊔ H.toSubmodule

Tactic:
Submodule.map_le_iff_le_comap

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ ⊤ ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)
Module: Mathlib.Algebra.Lie.EngelSubalgebra

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✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ Submodule.map N.subtype (dx ^ (k + 1)).ker ≤ (engel R x).toSubmodule

Tactic:
Submodule.map_le_iff_le_comap

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).ker ≤ Submodule.comap N.subtype (engel R x).toSubmodule
Module: Mathlib.Algebra.Lie.EngelSubalgebra

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✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
⊢ y ∈ (dx ^ (k + 1)).ker → y ∈ Submodule.comap N.subtype (engel R x).toSubmodule

Tactic:
hy

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
y : ↥N
hy : y ∈ (dx ^ (k + 1)).ker
⊢ y ∈ Submodule.comap N.subtype (engel R x).toSubmodule
Module: Mathlib.Algebra.Lie.EngelSubalgebra

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✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := ⋯
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := ⋯
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ Submodule.map N.subtype (dx ^ (k + 1)).range ≤ H.toSubmodule

Tactic:
Submodule.map_le_iff_le_comap

Goal state after:
case a
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H
aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N
dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂
k : ℕ
hk : Codisjoint (dx ^ (k + 1)).ker (dx ^ (k + 1)).range
⊢ (dx ^ (k + 1)).range ≤ Submodule.comap N.subtype H.toSubmodule
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
⊢ y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) m → y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) n

Tactic:
hy

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
H : LieSubalgebra R L
h : ∀ x ∈ H, H ≤ engel R x
x : ↥H
m n : ℕ
hmn : m ≤ n
y : ↥H
hy : y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) m
⊢ y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) n
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun i ↦ ((bind₁ f) ((monomial i) (coeff i φ))).vars) =
    φ.support.biUnion fun d ↦ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars

Tactic:
simp only [bind₁_monomial]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
classical
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
  · intro i s his IH h
    simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
    apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
    intro j hjs
    exact h j (Finset.mem_insert_of_mem hjs)

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ ⟨x, ⋯⟩ ∈ comap DI.incl (derivedSeriesOfIdeal R L 1 DI)

Tactic:
mem_comap

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
x : L
hx : x ∈ DDI
⊢ DI.incl ⟨x, ⋯⟩ ∈ derivedSeriesOfIdeal R L 1 DI
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
r : R
⊢ (C r * φ).IsHomogeneous m

Tactic:
simpa only [zero_add] using (isHomogeneous_C _ _).mul hφ

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

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Tactic:
let b := bV.prod bW

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := ⋯
G : ↥W →ₗ[K] ↥W := ⋯
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := ⋯
e : (↥V × ↥W) ≃ₗ[K] M := ⋯
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := ⋯
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := ⋯
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := ⋯
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
⊢ ∀ (m : ↥V), ∃ n, (F ^ n) m = 0

Tactic:
simp only [Subtype.forall, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V, F]

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
hG : G.charpoly.natTrailingDegree = 0
⊢ ∀ (a : M) (b : ∃ k, (φ ^ k) a = 0), ∃ n, (restrict φ hφV ^ n) ⟨a, ⋯⟩ = 0
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A

case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
⊢ (c • B).rank = B.rank

Tactic:
have hcomp : (c • B).mulVecLin = f.comp B.mulVecLin := by aesop

Goal state after:
m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
hcomp : (c • B).mulVecLin = f ∘ₗ B.mulVecLin
⊢ (c • B).rank = B.rank