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

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i j : ι
⊢ (algebraMap ℤ K) ((reindex b.baseSupportEquiv.symm b.baseSupportEquiv.symm) b.base.cartanMatrix i j) =
    (algebraMap ℤ K) (b.A i j)

Tactic:
reindex_apply,

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i j : ι
⊢ (algebraMap ℤ K) (b.base.cartanMatrix.submatrix (⇑b.baseSupportEquiv.symm.symm) (⇑b.baseSupportEquiv.symm.symm) i j) =
    (algebraMap ℤ K) (b.A i j)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n) * k + ↑n * eval k (ascPochhammer S n) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
Nat.cast_comm,

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n) * k + eval k (ascPochhammer S n) * ↑n = eval k (ascPochhammer S n) * (k + ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * s + ↑n * eval s (ascPochhammer S n)

Tactic:
Nat.cast_comm,

Goal state after:
case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * s + eval s (ascPochhammer S n) * ↑n
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: r : ℕ
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
by_cases h : r = 0

Goal state after:
case pos
r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

case neg
r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Tactic:
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
      rw [tsub_eq_zero_iff_le.mpr h, zero_add]

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

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S n) * k - ↑n * eval k (descPochhammer S n) = eval k (descPochhammer S n) * (k - ↑n)

Tactic:
Nat.cast_comm,

Goal state after:
S : Type u_1
inst✝ : Ring S
n : ℕ
k : S
⊢ eval k (descPochhammer S n) * k - eval k (descPochhammer S n) * ↑n = eval k (descPochhammer S n) * (k - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k) * -r + ↑k * eval (-r) (ascPochhammer R k) =
    (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
Nat.cast_comm,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * ↑k =
    (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (eval r (descPochhammer R k) * -r - -1 * (↑k * eval r (descPochhammer R k)))

Tactic:
Nat.cast_comm,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (eval r (descPochhammer R k) * -r - -1 * (eval r (descPochhammer R k) * ↑k))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
⊢ MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))

Tactic:
by
  induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
    have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
    simp_rw [descPochhammer_succ_eval]
    exact mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S))
      (sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)

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 : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ (Lagrange.basis s v i).leadingCoeff = (∏ j ∈ s.erase i, (v i - v j))⁻¹

Tactic:
by
  have : (∏ j ∈ s.erase i, (X - C (v j))).coeff (#s - 1) = 1 := by
    simpa [hi] using (monic_prod_X_sub_C v (s.erase i)).coeff_natDegree
  simp_rw [leadingCoeff, natDegree_basis hvs hi, Lagrange.basis]
  simp [basisDivisor, Finset.prod_mul_distrib, ← map_prod, this]

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

Goal state before:
pp: 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
x : L
⊢ ∀ {x_1 y : L},
    x_1 ∈ (((ad R L) x).maxGenEigenspace 0).carrier →
      y ∈ (((ad R L) x).maxGenEigenspace 0).carrier → ⁅x_1, y⁆ ∈ (((ad R L) x).maxGenEigenspace 0).carrier

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid, Module.End.mem_maxGenEigenspace, zero_smul,
        sub_zero, forall_exists_index]

Goal state after:
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
x : L
⊢ ∀ {x_1 y : L} (x_2 : ℕ),
    ((ad R L) x ^ x_2) x_1 = 0 → ∀ (x_3 : ℕ), ((ad R L) x ^ x_3) y = 0 → ∃ k, ((ad R L) x ^ k) ⁅x_1, y⁆ = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
h : ¬∃ i_1, x i_1 = x i
⊢ 0 = y i

Tactic:
· aesop

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

Goal state before:
pp: case inl
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
h : coeff c a ≠ 0
⊢ (weight w) c = m

pp: case inr
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
h : coeff c b ≠ 0
⊢ (weight w) c = m

Tactic:
· exact ha h

Goal state after:
case inr
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
h : coeff c b ≠ 0
⊢ (weight w) c = m
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ homogeneousCore' 𝒜 I = sSup {J | IsHomogeneous 𝒜 J ∧ J ≤ I}

Tactic:
refine (IsLUB.sSup_eq ?_).symm
  apply IsGreatest.isLUB
  have coe_mono : Monotone (toIdeal : HomogeneousIdeal 𝒜 → Ideal A) := fun x y => id
  convert! coe_mono.map_isGreatest (Ideal.homogeneousCore.gc 𝒜).isGreatest_u using 1
  ext x
  rw [mem_image, mem_ofPred_eq]
  refine ⟨fun hI => ⟨⟨x, hI.1⟩, ⟨hI.2, rfl⟩⟩, ?_⟩
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact ⟨x.isHomogeneous, hx⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
c : n → R
⊢ (eval c) (M.toMvPolynomial i) = (M *ᵥ c) i

Tactic:
simp only [toMvPolynomial, map_sum, eval_monomial, pow_zero, Finsupp.prod_single_index, pow_one,
    mulVec, dotProduct]

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
ι : 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
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (basis A bₘ) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)

Tactic:
simp only [polyCharpolyAux]

Goal state after:
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
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (charpoly.univ A ιM) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ι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
inst✝ : DecidableEq M
n : M
p : MvPolynomial σ R
⊢ ((weightedHomogeneousComponent w n) p).support = {c ∈ p.support | (weight w) c = n}

Tactic:
ext c
  simp [coeff_weightedHomogeneousComponent, And.comm]

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
⊢ ⊥ < ker φ → ∃ m, m ≠ 0 ∧ φ m = 0

Tactic:
contrapose!

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
⊢ (∀ (m : M), m ≠ 0 → φ m ≠ 0) → ¬⊥ < ker φ
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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
h : ∀ (m : M), m ≠ 0 → φ m ≠ 0
x : M
⊢ φ x = 0 → x = 0

Tactic:
contrapose!

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
tfae_3_to_4 : constantCoeff (charpoly φ) = 0 → LinearMap.det φ = 0
tfae_4_to_5 : LinearMap.det φ = 0 → ⊥ < ker φ
h : ∀ (m : M), m ≠ 0 → φ m ≠ 0
x : M
⊢ x ≠ 0 → φ x ≠ 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
⊢ [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ker φ = ⊥,
      ∀ (m : M), φ m = 0 → m = 0].TFAE

Tactic:
have := (hasEigenvalue_zero_tfae φ).not
  dsimp only [List.map] at this
  push Not at this
  have aux₁ : ∀ m, (m ≠ 0 → φ m ≠ 0) ↔ (φ m = 0 → m = 0) := by intro m; apply not_imp_not
  have aux₂ : ker φ = ⊥ ↔ ¬ ⊥ < ker φ := by rw [bot_lt_iff_ne_bot, not_not]
  simpa only [aux₁, aux₂] using this

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

Goal state before:
pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
⊢ d i = 0

Tactic:
by_cases hi : i ∈ d.support

Goal state after:
case pos
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∈ d.support
⊢ d i = 0

case neg
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∉ d.support
⊢ d i = 0
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

Tactic:
apply LieEquiv.ofSubalgebras _ _ e.lieConj

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ LieSubalgebra.map e.lieConj.toLieHom (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) =
    skewAdjointLieSubalgebra B
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij) 1
B : ↥(sl n R) := (single j i ⋯) 1
c : IsLieAbelian ↥(sl n R)
⊢ ↑A * ↑B = ↑B * ↑A

Tactic:
← sub_eq_zero,

Goal state after:
n : Type u_1
R : Type u₂
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
i j : n
hij : i ≠ j
A : ↥(sl n R) := (single i j hij) 1
B : ↥(sl n R) := (single j i ⋯) 1
c : IsLieAbelian ↥(sl n R)
⊢ ↑A * ↑B - ↑B * ↑A = 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1

Tactic:
← neg_zero,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) (-0) (-0) (-1) = -1
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (reindex s s) (Qᵀ * P) = (reindex s s) (Pᵀ * Q)
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
reindex_apply,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (Qᵀ * P).submatrix ⇑s.symm ⇑s.symm = (reindex s s) (Pᵀ * Q)
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (Qᵀ * P).submatrix ⇑s.symm ⇑s.symm = (reindex s s) (Pᵀ * Q)
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
reindex_apply,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (Qᵀ * P).submatrix ⇑s.symm ⇑s.symm = (Pᵀ * Q).submatrix ⇑s.symm ⇑s.symm
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
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
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
⊢ ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0

Tactic:
rw [mem_engel_iff] at hz

Goal state after:
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
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : ∃ n, ((ad K L) ↑v ^ n) z = 0
z' : Q := (LieSubmodule.Quotient.mk' E) z
⊢ ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ (toLin' (replicateCol (Fin 1) w)).rank ≤ 1

Tactic:
refine (LinearMap.rank_le_domain _).trans_eq ?_

Goal state after:
K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
a✝ : Nontrivial K
⊢ Module.rank K (Fin 1 → K) = 1