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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
hf' : ∀ (i : ι), f (P.root i) ≠ 0
aux :
  ∀ (i : ι),
    P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f) ∨
      -P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f)
⊢ (baseOf (⇑P.root) f).ncard = finrank R M

Tactic:
P.ncard_eq_finrank_of_linearIndepOn_of
      (P.linearIndepOn_root_baseOf f hf') aux

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
hf' : ∀ (i : ι), f (P.root i) ≠ 0
aux :
  ∀ (i : ι),
    P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f) ∨
      -P.root i ∈ AddSubmonoid.closure (⇑P.root '' baseOf (⇑P.root) f)
⊢ finrank R M = finrank R M
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
⊢ ↑(chainBotCoeff i (chainTopIdx i j)) - ↑(chainTopCoeff i (chainTopIdx i j)) = P.pairingIn ℤ (chainTopIdx i j) i

Tactic:
rw [P.chainBotCoeff_sub_chainTopCoeff h]

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

Goal state before:
pp: case inl
ι : 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
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
obtain ⟨j, hj, hj₀⟩ := hi.exists_mem_support_pos_pairingIn
    exact ⟨j, hj, hj₀.ne'⟩

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

Goal state before:
pp: R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
⊢ B.Nondegenerate ↔ ker B = ⊥

Tactic:
by
  refine ⟨Nondegenerate.ker_eq_bot, fun h ↦ .ofSeparatingLeft ?_⟩
  rwa [separatingLeft_iff_ker_eq_bot]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ + a₂ - (b₁ + b₂)) < ε

Tactic:
grw [add_sub_add_comm, abv_add abv, h₁, h₂, add_halves]

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

Goal state before:
pp: f g : Cauchy abs
⊢ { cauchy := f } * { cauchy := g⁻¹ } = { cauchy := f } * { cauchy := g }⁻¹

Tactic:
ofCauchy_inv

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
⊢ f 1 ≤ 1

Tactic:
rcases eq_zero_or_one_of_sq_eq_self hf1 with h | h <;> rw [h]

Goal state after:
case inl
R : Type u_1
inst✝ : Monoid R
f : R → ℝ
hf : IsPowMul f
hf1 : f 1 ^ 2 = f 1
h : f 1 = 0
⊢ 0 ≤ 1
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : k • Aᴴ = k • A
hk : IsSelfAdjoint k
⊢ A.IsHermitian

Tactic:
simpa using! congr(⅟k • $h)

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
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit (A ^ z.succ).det ↔ IsUnit A.det ∨ ↑z.succ = 0

Tactic:
det_pow,

Goal state after:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ ↑z).det ↔ IsUnit A.det ∨ ↑z = 0
⊢ IsUnit (A.det ^ z.succ) ↔ IsUnit A.det ∨ ↑z.succ = 0
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit (A ^ z.succ).det ↔ IsUnit A.det ∨ -↑z.succ = 0

Tactic:
det_pow,

Goal state after:
case pred
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (A ^ (-↑z)).det ↔ IsUnit A.det ∨ -↑z = 0
⊢ IsUnit (A.det ^ z.succ) ↔ IsUnit A.det ∨ -↑z.succ = 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
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
⊢ A ^ z ≠ 0

Tactic:
have := ha.det_zpow z
  contrapose this
  rw [this, det_zero]
  exact not_isUnit_zero

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

Goal state before:
pp: case refine_1
n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
⊢ Function.Injective fun v ↦ v ᵥ* M⁻¹

Tactic:
· simp only [Matrix.vecMul_injective_iff_isUnit, isUnit_nonsing_inv_iff, hM.isUnit]

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.degree ≤ q.degree
⊢ q ≠ 0

Tactic:
· rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)

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

Goal state before:
pp: S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (ascPochhammer S n) = ↑(r + n)!

Tactic:
rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n : ℕ
v w : Fin n → K
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
  /- We can assume not all `w i` are zero, and therefore that `w 0 ≠ 0`,
  since otherwise we can swap row `0` with another nonzero row. -/
  wlog h0 : w 0 ≠ 0 generalizing v w with aux
  · obtain h0' | ⟨i₀, hi₀ : w i₀ ≠ 0⟩ := forall_or_exists_not (w · = 0)
    · obtain rfl | hne := eq_or_ne n 0
      · simp [projVandermonde_apply]
      rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]
    rw [← mul_right_inj' (a := ((Equiv.swap 0 i₀).sign : K))
      (by simp [show 0 ≠ i₀ by rintro rfl; contradiction]), ← det_permute, ← projVandermonde_comp,
      aux _ _ (by simpa), ← (Equiv.swap 0 i₀).prod_Ioi_comp_eq_sign_mul_prod (by simp)]
    rfl
  /- Let `W` be obtained from the matrix by subtracting `r = (v 0) / (w 0)` times each column
  from the next column, starting from the penultimate column. This doesn't change the determinant.-/
  set r := v 0 / w 0 with hr
  set W : Matrix (Fin (n + 1)) (Fin (n + 1)) K := .of fun i ↦ (cons (projVandermonde v w i 0)
    (fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc))
  -- deleting the first row and column of `W` gives a row-scaling of a Vandermonde matrix.
  have hW_eq : (W.submatrix succ succ) = .of fun i j ↦ (v (succ i) - r * w (succ i)) *
      projVandermonde (v ∘ succ) (w ∘ succ) i j := by
    ext i j
    simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]
    simp
    ring
  /- The first row of `W` is `[(w 0)^n, 0, ..., 0]` - take a cofactor expansion along this row,
  and apply induction. -/
  rw [det_eq_of_forall_col_eq_smul_add_pred (B := W) (c := fun _ ↦ r) (by simp [W])
    (fun i j ↦ by simp [W, r, projVandermonde_apply]), det_succ_row_zero,
    Finset.sum_eq_single 0 _ (by simp)]
  · rw [succAbove_zero, hW_eq, det_mul_column, ih]
    simp only [Nat.succ_eq_add_one, coe_ofNat_eq_mod, Nat.zero_mod,
      pow_zero, show W 0 0 = w 0 ^ n by simp [W, projVandermonde_apply], one_mul, hr]
    field_simp
    simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]
    field_simp
    simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]
  intro j _ hj0
  obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0
  rw [mul_eq_zero, mul_eq_zero]
  refine .inl (.inr ?_)
  simp only [of_apply, projVandermonde_apply_of_ne_zero h0, val_succ, val_castSucc, cons_succ, W, r]
  ring

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

Goal state before:
pp: case add
ι₁ : 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₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this : IsLieAbelian ↥H₁
u v : ↥(prod eι b₁ b₂)
hu : u ∈ lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
hv : v ∈ lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
hu' : ⁅(↑u).1, ↑x⁆ = 0
hv' : ⁅(↑v).1, ↑x⁆ = 0
⊢ ⁅(↑(u + v)).1, ↑x⁆ = 0

Tactic:
simp [hu', hv']

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

Goal state before:
pp: case lie
ι₁ : 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₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this : IsLieAbelian ↥H₁
u v : ↥(prod eι b₁ b₂)
hu : u ∈ lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
hv : v ∈ lieSpan R ↥(prod eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
hu' : ⁅(↑u).1, ↑x⁆ = 0
hv' : ⁅(↑v).1, ↑x⁆ = 0
⊢ ⁅(↑⁅u, v⁆).1, ↑x⁆ = 0

Tactic:
simp [hu', hv']

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f ⟨a (i, j).1, ⋯⟩ - f ⟨a (i, j).2, ⋯⟩) = (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩ - f ⟨a (k, l).2, ⋯⟩)

Tactic:
← map_sub,

Goal state after:
ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f (⟨a (i, j).1, ⋯⟩ - ⟨a (i, j).2, ⋯⟩)) = (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩ - f ⟨a (k, l).2, ⋯⟩)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f (⟨a (i, j).1, ⋯⟩ - ⟨a (i, j).2, ⋯⟩)) = (algebraMap R K) (f ⟨a (k, l).1, ⋯⟩ - f ⟨a (k, l).2, ⋯⟩)

Tactic:
← map_sub,

Goal state after:
ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq : ⟨a i, ⋯⟩ - ⟨a j, ⋯⟩ = ⟨a k, ⋯⟩ - ⟨a l, ⋯⟩
⊢ (algebraMap R K) (f (⟨a (i, j).1, ⋯⟩ - ⟨a (i, j).2, ⋯⟩)) = (algebraMap R K) (f (⟨a (k, l).1, ⋯⟩ - ⟨a (k, l).2, ⋯⟩))
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
hy : y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) m
⊢ y ∈ (fun n ↦ LinearMap.ker ((ad R ↥H) x ^ n)) n

Tactic:
rw [LinearMap.mem_ker] at 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 : ((ad R ↥H) x ^ m) y = 0
⊢ ((ad R ↥H) x ^ n) y = 0
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(algEquivMatrix (chooseBasis R M)) ((aeval f) f.charpoly) = 0

Tactic:
AlgEquiv.toLinearEquiv_apply,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (algEquivMatrix (chooseBasis R M)) ((aeval f) f.charpoly) = 0
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 : ι
⊢ nodalWeight s v i = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹

Tactic:
nodalWeight,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
⊢ ∏ j ∈ s.erase i, (v i - v j)⁻¹ = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
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
⊢ nodalWeight s v i ≠ 0

Tactic:
nodalWeight,

Goal state after:
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
⊢ ∏ j ∈ s.erase i, (v i - v j)⁻¹ ≠ 0
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 : ι
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, C (v i - v j)⁻¹ * (X - C (v j)) = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))

Tactic:
nodalWeight,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, C (v i - v j)⁻¹ * (X - C (v j)) = C (∏ j ∈ s.erase i, (v i - v j)⁻¹) * (nodal s v / (X - C (v i)))
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ↑(weightedTotalDegree w p) ≤ weightedTotalDegree' w p

Tactic:
· simp only [weightedTotalDegree]
    have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm
    rw [← hm]
    simpa [weightedTotalDegree'] using hm'

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ (weightedHomogeneousSubmodule R w n).FG

Tactic:
rw [weightedHomogeneousSubmodule_eq_finsupp_supported, ← Module.Finite.iff_fg]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
⊢ Module.Finite R ↥(AddMonoidAlgebra.supported R R {d | (weight w) d = n})
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
⊢ Submodule.IsHomogeneous (span {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}) 𝒜

Tactic:
refine Ideal.homogeneous_span _ _ fun x hx => ?_
    obtain ⟨i, x, rfl⟩ := hx
    apply SetLike.isHomogeneousElem_coe

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 𝒜
⊢ ⨆ i, ⨆ (_ : i > 0), ofClass (𝒜 i) = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))

Tactic:
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.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : (φ ^ k) x = 0
⊢ x ∈ ⨆ m, (φ ^ m).ker

Tactic:
← mem_ker

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
k : ℕ
hk : x ∈ ker (φ ^ k)
⊢ x ∈ ⨆ m, (φ ^ m).ker
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
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x : ι → R
⊢ Polynomial.map (eval x) (φ.polyCharpolyAux b bₘ) = charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))

Tactic:
by
  simp only [← polyCharpolyAux_map_eq_charpoly φ b bₘ, LinearEquiv.apply_symm_apply,
    Finsupp.equivFunOnFinite, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]

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
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✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
⊢ Polynomial.map (eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)

Tactic:
rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]

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✝ : Nontrivial R
x : L
⊢ φ.nilRank ≤ (charpoly (φ x)).natTrailingDegree

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero
  intro h
  apply_fun (MvPolynomial.eval ((chooseBasis R L).repr x)) at h
  rw [polyCharpoly_coeff_eval, map_zero] at h
  apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h
  apply (LinearMap.charpoly_monic _).ne_zero

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

Goal state before:
pp: case inl.inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : p
y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inl x) (Sum.inr y) = 1 (Sum.inl x) (Sum.inr y)

Tactic:
simp [Pso, indefiniteDiagonal]

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

Goal state before:
pp: case inr.inl
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x : q
y : p
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inl y) = 1 (Sum.inr x) (Sum.inl y)

Tactic:
simp [Pso, indefiniteDiagonal]

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
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f * (J l R).map ⇑f * Aᵀ.map ⇑f = (J l R).map ⇑f

Tactic:
← Matrix.map_mul,

Goal state after:
l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ (A * J l R * Aᵀ).map ⇑f = (J l R).map ⇑f
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
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range = finrank R ↥B.mulVecLin.range

Tactic:
LinearMap.range_comp,

Goal state after:
m : Type um
n : Type un
inst✝³ : Fintype n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ finrank R ↥(Submodule.map A.mulVecLin B.mulVecLin.range) = finrank R ↥B.mulVecLin.range
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(LinearMap.funLeft R R r ∘ₗ A.mulVecLin ∘ₗ LinearMap.funLeft R R ⇑(Equiv.refl n).symm).range ≤
    finrank R ↥A.mulVecLin.range

Tactic:
LinearMap.range_comp,

Goal state after:
case calc.step
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R
      ↥(Submodule.map (LinearMap.funLeft R R r) (A.mulVecLin ∘ₗ LinearMap.funLeft R R ⇑(Equiv.refl n).symm).range) ≤
    finrank R ↥A.mulVecLin.range