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

Goal state before:
pp: x a b : ℝ
⊢ a * b = b * a

Tactic:
apply ext_cauchy

Goal state after:
x a b : ℝ
⊢ (a * b).cauchy = (b * a).cauchy
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x

Tactic:
obtain ⟨x⟩ := x

Goal state after:
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy abs
⊢ C { cauchy := x }
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk y✝¹ ⊔ mk y✝

Tactic:
← mk_sup,

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk (y✝¹ ⊔ y✝)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk y✝¹ ⊔ mk y✝

Tactic:
← mk_sup,

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk (y✝¹ ⊔ y✝)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝ → mk y✝¹ ≤ mk y✝ → mk y✝² ⊔ mk y✝¹ ≤ mk y✝

Tactic:
← mk_sup,

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝ → mk y✝¹ ≤ mk y✝ → mk (y✝² ⊔ y✝¹) ≤ mk y✝
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = ∑ i, ∑ j, Aᵀ i j * B j i

Tactic:
dotProduct,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ ∑ i, A.vec i * B.vec i = ∑ i, ∑ j, Aᵀ i j * B j i
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ (fun j ↦ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = ∑ j, (∑ j_1, A l j_1 * X j_1 j) * Bᵀ j k

Tactic:
dotProduct,

Goal state after:
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, kroneckerMap (fun x1 x2 ↦ x1 * x2) B A (k, l) x * X.vec x = ∑ j, (∑ j_1, A l j_1 * X j_1 j) * Bᵀ j k
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ (X.vec ⬝ᵥ fun i ↦ kroneckerMap (fun x1 x2 ↦ x1 * x2) B A i (k, l)) = ∑ j, (∑ j_1, Aᵀ l j_1 * X j_1 j) * B j k

Tactic:
dotProduct,

Goal state after:
l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ ∑ x, X.vec x * kroneckerMap (fun x1 x2 ↦ x1 * x2) B A x (k, l) = ∑ j, (∑ j_1, Aᵀ l j_1 * X j_1 j) * B j k
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ (A * B).vec = A.vec ᵥ* kroneckerMap (fun x1 x2 ↦ x1 * x2) B 1

Tactic:
by
  rw [vec_vecMul_kronecker_of_commute, transpose_one, Matrix.one_mul]
  intro x i j
  obtain rfl | hij := eq_or_ne i j <;> simp [*]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : NonUnitalSemiring R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x : m → R
A B : Matrix m n R
x' : n → R
⊢ x ⬝ᵥ A ⊙ B *ᵥ x' = (diagonal x).vec ⬝ᵥ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B *ᵥ (diagonal x').vec

Tactic:
simp [diagonal, mulVec, dotProduct, Fintype.sum_prod_type]

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 : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ m

Tactic:
rcases m with m | m
    · simp
    rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
    · calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
    · simp [h]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
aux : (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal (d - μ • 1))
⊢ (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0

Tactic:
aux,

Goal state after:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : ((toLin b b) (diagonal (d - μ • 1)) ^ k) x = 0
j : n
aux : (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal (d - μ • 1))
⊢ (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ (A ^ k).IsSymm

Tactic:
by
  rw [IsSymm, transpose_zpow, h]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ μ * ∑ i, d i * |v i| ^ 2 ≤ |v| ᵥ* diagonal d ⬝ᵥ N *ᵥ |v|

Tactic:
dotProduct,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
⊢ μ * ∑ i, d i * |v i| ^ 2 ≤ ∑ i, (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬(toLin' (4 - b.cartanMatrix)).ker ≠ ⊥

Tactic:
aux,

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬(-(toLin' b.cartanMatrix - 4 • 1)).ker ≠ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : f x = μ • x
⊢ ((aeval f) p) x = eval μ p • x

Tactic:
rcases eq_or_ne x 0 with rfl | hne
  · simp
  · exact aeval_apply_of_hasEigenvector ⟨mem_eigenspace_iff.mpr hx, hne⟩

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

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0)))

Tactic:
rw [C_mul', aeval_def]; simp [algebraMap, Algebra.algebraMap]

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

Goal state before:
pp: case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (∑ i ∈ cons a s has, f i)!

Tactic:
Finset.sum_cons

Goal state after:
case cons
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (ascPochhammer S n) = ascPochhammer T n
⊢ map f (ascPochhammer S (n + 1)) = ascPochhammer T (n + 1)

Tactic:
simp [ih, ascPochhammer_succ_left, map_comp]

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

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ P.pairing i k = (algebraMap ℤ R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k)

Tactic:
map_sum,

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ P.pairing i k = ∑ x ∈ b.support, (algebraMap ℤ R) (f x * P.pairingIn ℤ x k)
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
k : ι
⊢ P.pairing j k = (algebraMap ℤ R) (∑ l ∈ b.support, g l * P.pairingIn ℤ l k)

Tactic:
map_sum,

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
k : ι
⊢ P.pairing j k = ∑ x ∈ b.support, (algebraMap ℤ R) (g x * P.pairingIn ℤ x k)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
induction b with
  | zero => simp
  | succ b =>
    simp_rw [add_succ, Nat.add_one_sub_one]
    obtain h | h := le_total a b
    · 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]
    · rw [tsub_add_cancel_of_le h]

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
aux : {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} = (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ
⊢ ∀ x ∈ span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}, (LinearMap.fst R L₁ L₂) x = 0 → x = 0

Tactic:
aux,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
aux : {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} = (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ
⊢ ∀ x ∈ span R ((fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ), (LinearMap.fst R L₁ L₂) x = 0 → x = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
⊢ rectVandermonde v w (n + 1) i = Pi.single (last n) (v i ^ n)

Tactic:
ext j
  obtain rfl | hlt := j.le_last.eq_or_lt
  · simp [rectVandermonde_apply]
  rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
  simpa [Nat.sub_eq_zero_iff_le] using! hlt

Goal state after:
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
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ ((interpolate (insert i (t \ s)) v) r).degree + (Lagrange.basis s v i).degree < ↑(#t)

Tactic:
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))]

Goal state after:
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
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ ((interpolate (insert i (t \ s)) v) r).degree < ↑(1 + (#t - #s))
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ (φ (P * A * Q)).charpoly = (φ₁ P * φ₂ A * φ₃ Q).charpoly

Tactic:
by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1
hbc_inj : Injective ⇑(End.baseChangeHom R A M)
aux : (End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩) = baseChange A ((toEnd R L M) x)
⊢ _root_.IsNilpotent ((End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩))

Tactic:
aux,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1
hbc_inj : Injective ⇑(End.baseChangeHom R A M)
aux : (End.baseChangeHom R A M) ((toEnd R (↥(derivedSeries R L 1)) M) ⟨x, hx⟩) = baseChange A ((toEnd R L M) x)
⊢ _root_.IsNilpotent (baseChange A ((toEnd R L M) x))
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
a : R
x : MvPolynomial σ R
x✝ : x ∈ {p | ∃ (hp : IsWeightedHomogeneous w p m), ∀ (a : R), motive (C a * p) ⋯}
w✝ : IsWeightedHomogeneous w x m
hx : ∀ (a : R), motive (C a * x) ⋯
⊢ IsWeightedHomogeneous w (a • x) m

Tactic:
simp [Algebra.smul_def, C_mul ‹_› a]

Goal state after:
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
h : IsHomogeneous 𝒜 I
i : ι
x : ↥I
⊢ ↑(((decompose 𝒜) ↑x) i) ∈ ↑I

Tactic:
exact h _ x.prop

Goal state after:
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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ 𝒜₊.toAddSubmonoid = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))

Tactic:
by
  rw [irrelevant_eq_iSup]
  exact le_antisymm (iSup_le fun i ↦ iSup_le fun hi _ hx ↦ subset_closure <| mem_biUnion hi hx) <|
    closure_le.mpr <| iUnion_subset fun i ↦ iUnion_subset fun hi ↦ le_biSup (ofClass <| 𝒜 ·) hi

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

Goal state before:
pp: case e_f
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
⊢ (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
      (MvPolynomial.map (algebraMap R A)) =
    (MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))

Tactic:
apply MvPolynomial.ringHom_ext

Goal state after:
case e_f.hC
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
⊢ ∀ (r : R),
    ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
          (MvPolynomial.map (algebraMap R A)))
        (C r) =
      ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (C r)

case e_f.hX
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
⊢ ∀ (i : ιM × ιM),
    ((↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ)))).comp
          (MvPolynomial.map (algebraMap R A)))
        (X i) =
      ((MvPolynomial.map (algebraMap R A)).comp ↑(bind₁ (toMvPolynomial b bₘ.end φ))) (X i)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

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

Tactic:
map_sum,

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