mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∏ j_1 ∈ s.erase i, eval (v j) (basisDivisor (v i) (v j_1)) = 0

Tactic:
prod_eq_zero_iff

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
⊢ (s.sup fun b ↦ ((interpolate (insert b (t \ s)) v) r * Lagrange.basis s v b).degree) < ↑(#t)

Tactic:
simp_rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #t), degree_mul]
    intro i hi
    have hs : 1 ≤ #s := Nonempty.card_pos ⟨_, hi⟩
    have hst' : #s ≤ #t := card_le_card hst
    have H : #t = 1 + (#t - #s) + (#s - 1) := by
      rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
    rw [degree_basis (Set.InjOn.mono hst hvt) hi, H, WithBot.coe_add, Nat.cast_withBot,
      WithBot.add_lt_add_iff_right (@WithBot.coe_ne_bot _ (#s - 1))]
    convert!
      degree_interpolate_lt _
        (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset⟩)))
    rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]

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

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this✝² : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
this✝¹ : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
this✝ : Nontrivial ↥(s.eigenspace ν)
hν : ν ∈ E
this : Subsingleton ↥E
⊢ ν = 0

Tactic:
simpa using! Subsingleton.elim (⟨ν, hν⟩ : E) 0

Goal state after:
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
⊢ ((bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i ↦ (f i).vars

Tactic:
calc (bind₁ f φ).vars
    _ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
      rw [← map_sum, ← φ.as_sum]
    _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars :=
      (vars_sum_subset _ _)
    _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) := by
      simp only [bind₁_monomial]
    _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) := ?_
    -- proof below
    _ ≤ φ.vars.biUnion fun i : σ => vars (f i) := ?_
    -- proof below
  · apply Finset.biUnion_mono
    intro d _hd
    calc
      vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) ≤
          (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars :=
        vars_mul _ _
      _ ≤ (∏ i ∈ d.support, f i ^ d i).vars := by
        simp only [Finset.empty_union, vars_C, Finset.Subset.refl]
      _ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := vars_prod _
      _ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_
    apply Finset.biUnion_mono
    intro i _hi
    apply vars_pow
  · intro j
    simp_rw [Finset.mem_biUnion]
    rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
    exact ⟨i, (mem_vars_iff_mem_support _).mpr ⟨d, hd, hi⟩, hj⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ ∑ i_1 ∈ t, (X - C (v i)) * nodal (t.erase i_1) v = ∑ x ∈ t, nodal ((insert i t).erase x) v

Tactic:
refine sum_congr rfl fun j hjt => ?_

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
j : ι
hjt : j ∈ t
⊢ (X - C (v i)) * nodal (t.erase j) v = nodal ((insert i t).erase j) v
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ LinearMap.charpoly (e.conj φ) = ((LinearMap.toMatrix b b) φ).charpoly

Tactic:
← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ ((LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ)).charpoly = ((LinearMap.toMatrix b b) φ).charpoly
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
w : σ → M
m : M
a b : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
hb : b ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : coeff c (a + b) ≠ 0
⊢ (weight w) c = m

Tactic:
rw [coeff_add] at hc

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
hb : b ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
⊢ (weight w) c = m
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
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
h : ∀ (a : R), motive (C a * p) ⋯
⊢ motive p hp

Tactic:
simpa using h 1

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case h₀
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ∀ b ∈ Finset.univ,
    b ≠ ij →
      (monomial (Finsupp.single b 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij b) = 0

pp: case h₁
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ij ∉ Finset.univ →
    (monomial (Finsupp.single ij 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij ij) = 0

Tactic:
· rintro kl - H
        rw [this, if_neg H, map_zero]

Goal state after:
case h₁
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ij ∉ Finset.univ →
    (monomial (Finsupp.single ij 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij ij) = 0
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
⊢ finrank K ↥(φ.maxGenEigenspace 0) = (charpoly φ).natTrailingDegree

Tactic:
set V := φ.maxGenEigenspace 0

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
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree
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
inst✝² : LinearOrder M
inst✝¹ : OrderBot M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
rw [← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsWeightedHomogeneous]
  apply forall_congr'
  intro m
  rw [mem_support_iff]
  apply forall_congr'
  intro _
  exact weightedDegree_eq_zero_iff hw

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
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
I : Ideal (MvPolynomial σ R)
h : Ideal.IsHomogeneous (weightedHomogeneousSubmodule R w) I
p : MvPolynomial σ R
⊢ p ∈ I ↔ ∀ (m : M), (weightedHomogeneousComponent w m) p ∈ I

Tactic:
simp_rw [← weightedDecomposition.decompose'_apply]
  exact h.mem_iff

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree

Tactic:
apply nilRankAux_le

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b

Tactic:
apply nilRankAux_le

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
⊢ ∃ r, (eval r) ((polyCharpoly (?m.208 r) b).coeff φ.nilRank) ≠ 0

Tactic:
by_contra! h₀

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ : ∀ (r : ChooseBasisIndex R L → R), (eval r) ((polyCharpoly (?m.208 r) b).coeff φ.nilRank) = 0
⊢ False
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : ∀ i < r, χ.coeff i = 0
⊢ χ = X ^ r

Tactic:
by
    simp_rw [r, ← lieCharpoly_natDegree K E x' u] at this ⊢
    rw [(lieCharpoly_monic K E x' u).eq_X_pow_iff_natDegree_le_natTrailingDegree]
    exact le_natTrailingDegree (lieCharpoly_monic K E x' u).ne_zero this

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R

Tactic:
rw [mem_iff] at h ⊢
  simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_1
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : fromBlocks A B C D ∈ symplecticGroup l R
⊢ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1

Tactic:
have h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D)
        (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R := by
      simpa [mem_iff, fromBlocks_transpose, J, fromBlocks_multiply,
        sub_eq_add_neg] using transpose_mem h

Goal state after:
case refine_1
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : fromBlocks A B C D ∈ symplecticGroup l R
h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D) (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R
⊢ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
r : R
d e : Derivation R A A
a : A
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a

Tactic:
simp only [commutator_apply, map_smul, smul_sub, smul_apply]

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

Goal state before:
pp: case h.refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ ((toEnd K (↥U) Q) v ^ k) z' ≠ 0

Tactic:
apply Nat.find_min hz'

Goal state after:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
α : K
hα : α ∈ s
v : ↥U := ⋯
z : L
hz : z ∈ engel K ↑v
z' : Q := ⋯
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := ⋯
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
⊢ k < Nat.find hz'
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
⊢ ∀ (hx : single m b + y ∈ gradeBy R (⇑f) i),
    (decomposeAux f) ↑⟨single m b + y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hx⟩

Tactic:
hmby

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) i
⊢ (decomposeAux f) ↑⟨single m b + y, hmby⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : ι
x y : S ⊗[R] ↥(ℳ i)
h : (Submodule.toBaseChange S (ℳ i)) x = (Submodule.toBaseChange S (ℳ i)) y
⊢ Function.Bijective
    ⇑(↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
        ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)))

Tactic:
by rw [← LinearEquiv.coe_trans]; exact LinearEquiv.bijective _

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ s.formPerm.toCycle ⋯ = ↑s

Tactic:
toCycle_eq_toList _ _ x

Goal state after:
case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ ↑(s.formPerm.toList x) = ↑s

case mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
val✝ : Cycle α
s : List α
hn✝ : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ s.formPerm x ≠ x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ (∑ k, if ↑i < ↑k then f ↑k else 0) = ∑ k > i, f ↑k

Tactic:
by simp [← Finset.sum_filter, Finset.filter_lt_eq_Ioi]

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

Goal state before:
pp: case h
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := ⋯
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := ⋯
π₂ : L →ₗ[k] ↥(k ∙ z) := ⋯
W : LieSubmodule k L V := ⋯
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ Nontrivial ↥(weightSpace V ⇑(χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂))

Tactic:
refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_

Goal state after:
case h.refine_1
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ v ∈ weightSpace V ⇑(χ₀ ∘ₗ π₁ + c • ↑e ∘ₗ π₂)

case h.refine_2
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
⊢ ⟨v, ?h.refine_1⟩ ≠ 0