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

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

Tactic:
by simp [hf₂, contra]

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
f : CauSeq β abv
n : ℕ
⊢ ∀ (i : ℕ), ↑(npowRec n f) i = ↑f i ^ n

Tactic:
by induction n <;> simp [*, npowRec, pow_succ]

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
f g : CauSeq β abv
hf : f ≈ g
⊢ -f ≈ -g

Tactic:
by
  simpa only [neg_sub'] using! neg_limZero hf

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - g - (f - g)).Pos
⊢ f < h

Tactic:
sub_sub_sub_cancel_right

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : (h - f).Pos
⊢ f < h
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: case mpr
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
a✝ : Nontrivial R
i : n
⊢ v i ≠ 0 → 0 < star (v i) * v i

Tactic:
· exact (star_mul_self_pos <| .of_ne_zero ·)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
⊢ a ⊓ b ≈ b

pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b

Tactic:
· intro _ _
    refine ⟨i, fun j hj => ?_⟩
    dsimp
    rw [← min_sub_sub_right]
    rwa [sub_self, min_eq_right, abs_zero]
    exact ε0.le.trans (h _ hj)

Goal state after:
case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b
Module: Mathlib.LinearAlgebra.Matrix.Hadamard

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
A : Matrix n n α
d : n → α
⊢ A ⊙ 1 = diagonal d ↔ A.diag = d

Tactic:
simpa using hadamard_diagonal_eq_diagonal_iff (A := A) (d := 1)

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
f : n ≃ m
h : ((reindex f f) A).IsHermitian
⊢ A.IsHermitian

Tactic:
simpa using h.reindex f.symm

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

Tactic:
have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := isHermitian_conjTranspose_mul_mul _ hA.inv

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hA : A.IsHermitian
hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))

Tactic:
exact h.pow _

Goal state after:
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 : IsUnit A.det
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹

Tactic:
by rw [← zpow_add_one h, sub_add_cancel]

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

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
⊢ A ^ (-↑k + n) = A ^ (-↑k) * A ^ n

Tactic:
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (n + 1)))

Tactic:
exact h.pow _

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
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ ∃ s g, ∑ i ∈ s, g i • P.root ↑i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
refine ⟨⟨{i, j}, by simpa⟩, Finsupp.single i (1 : R) + Finsupp.single j (2 : R), ?_⟩

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 ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ ∑ i_1 ∈ { val := {i, j}, nodup := ⋯ }, (⇑(Finsupp.single i 1) + ⇑(Finsupp.single j 2)) i_1 • P.root ↑i_1 = 0 ∧
    ∃ i_1 ∈ { val := {i, j}, nodup := ⋯ }, (⇑(Finsupp.single i 1) + ⇑(Finsupp.single j 2)) i_1 ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case refine_1
ι : 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
_i : Fintype ι
d : ↥b.support → ℤ := fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
hd : d = fun i ↦ ((P.RootFormIn ℤ) (P.rootSpanMem ℤ ↑i)) (P.rootSpanMem ℤ ↑i)
i : ↥b.support
⊢ 0 < d i

Tactic:
rw [hd, ← posRootForm_eq]
    exact RootPositiveForm.zero_lt_posForm_apply_root _ _

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

Goal state before:
pp: S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h : ↑n - 1 ≤ s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
by
  rcases eq_or_lt_of_le h with heq | h
  · rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
    positivity
  · exact (descPochhammer_pos h).le

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
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = #s - 1

Tactic:
← card_erase_of_mem hi,

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
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = #(s.erase i)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ 0 < #s

Tactic:
exact Nonempty.card_pos hs

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), ∑ i, v i * f j ^ ↑i = 0
⊢ v = 0

Tactic:
apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf
  simp_rw [mul_comm]
  exact hfv

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h : (vandermonde fun i ↦ ↑(w' i)).det = (of fun i j ↦ eval (↑(w' i)) (descPochhammer ℤ ↑j)).det
⊢ ↑n.superFactorial ∣ (vandermonde v).det

Tactic:
conv_lhs at h => simp only [hw', det_vandermonde_sub]

Goal state after:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h : (vandermonde v).det = (of fun i j ↦ eval (↑(w' i)) (descPochhammer ℤ ↑j)).det
⊢ ↑n.superFactorial ∣ (vandermonde v).det
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v)

Tactic:
rw [derivative_nodal, eval_finsetSum, ← add_sum_erase _ _ hi, add_eq_left]
  exact sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

Goal state after:
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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
⊢ False

Tactic:
obtain ⟨P, hP⟩ := X_dvd_iff.2 h

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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ False
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 = (eval (v i) (nodal (s.erase i) v))⁻¹

Tactic:
rw [eval_nodal, nodalWeight, prod_inv_distrib]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : IsEmpty σ
w : σ → M
f : MvPolynomial σ R
⊢ IsWeightedHomogeneous w (C (coeff 0 f)) 0

Tactic:
exact isWeightedHomogeneous_C _ _

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

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

Tactic:
his

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
⊢ ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
    (∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)) →
      IsWeightedHomogeneous w (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
⊢ (MvPolynomial.eval₂Hom f M) ((univ R n).coeff i) = (of (Function.curry M)).charpoly.coeff i

Tactic:
by
  rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]

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
⊢ Submodule.IsHomogeneous (span {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}) 𝒜

Tactic:
by
    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✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ r ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
← DirectSum.sum_support_decompose 𝒜 r

Goal state after:
ι : 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
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal
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
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ coeff d ((weightedHomogeneousComponent w n) φ) = 0

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg hd]

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
⊢ i ∉ s →
    ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
      (∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)) →
        (∏ i ∈ insert i s, φ i).IsHomogeneous (∑ i ∈ insert i s, n i)

Tactic:
his

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
⊢ ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
    (∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)) → (∏ i ∈ insert i s, φ i).IsHomogeneous (∑ i ∈ insert i s, n i)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
⊢ ((rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n

Tactic:
by
  refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩
  convert! ← @h (d.mapDomain f) _
  · simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]
    exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf
  · rwa [coeff_rename_mapDomain f hf]

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

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
⊢ IsCompl V W

Tactic:
hV

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
⊢ IsCompl (⨆ n, ker (φ ^ n)) W
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝¹ : CommRing R
inst✝ : IsDomain R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
hnR : ↑n ≤ #R
⊢ ∀ (r : σ → R), (eval r) (F - G) = 0

Tactic:
simpa [sub_eq_zero] using h

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

Goal state before:
pp: m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (toLin' (diagonal w)).range = ⨆ i ∈ {i | w i ≠ 0}, (LinearMap.single K (fun x ↦ K) i).range

Tactic:
dsimp only [mem_ofPred_eq]
  rw [← Submodule.map_top, ← iSup_range_single, Submodule.map_iSup]
  congr; funext i
  rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']

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

Goal state before:
pp: case inr.inr
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
⊢ Ex ≤ Ey

Tactic:
suffices χ = X ^ r by
    -- Indeed, by evaluating the coefficients at `1`
    apply_fun (fun p ↦ p.map (evalRingHom 1)) at this
    -- we find that the characteristic polynomial `χ 1` of `⁅y, _⁆` is equal to `X ^ r`
    simp_rw [Polynomial.map_pow, map_X, χ, lieCharpoly_map_eval, one_smul, u, sub_add_cancel,
      -- and therefore the endomorphism `⁅y, _⁆` acts nilpotently on `E`.
      r, LinearMap.charpoly_eq_X_pow_iff,
      Subtype.ext_iff, coe_toEnd_pow _ _ _ E, ZeroMemClass.coe_zero] at this
    -- We ultimately want to show `engel K x ≤ engel K y`
    intro z hz
    -- which holds by definition of Engel subalgebra and the nilpotency that we just established.
    rw [mem_engel_iff]
    exact this ⟨z, hz⟩

Goal state after:
case inr.inr
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
⊢ χ = X ^ r
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)

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)

pp: case inr.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 y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
· -- x : p, y : q
    simp [Pso, indefiniteDiagonal]

Goal state after:
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)

case inr.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 y : q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case intro
m : Type um
n : Type un
R : Type uR
inst✝⁷ : Fintype n
inst✝⁶ : Finite m
inst✝⁵ : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
i : n
aux₁ : A.mulVecLin ((Pi.basisFun R n) i) = ∑ j, A j i • (Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) ((Pi.basisFun R n) i) = v₂ (e i)
⊢ ((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i ↦ R) i) 1 =
    (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i ↦ R) i) 1

Tactic:
Pi.basisFun_apply

Goal state after:
case intro
m : Type um
n : Type un
R : Type uR
inst✝⁷ : Fintype n
inst✝⁶ : Finite m
inst✝⁵ : DecidableEq n
M₁ : Type u_1
M₂ : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
A : Matrix m n R
v₁ : Basis m R M₁
v₂ : Basis n R M₂
val✝ : Fintype m
e₁ : (m → R) ≃ₗ[R] M₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl m)
e₂ : (n → R) ≃ₗ[R] M₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl n)
i : n
aux₁ : A.mulVecLin (Pi.single i 1) = ∑ j, A j i • (Pi.basisFun R m) j
aux₂ : ∀ (e : n ≃ n), ((Pi.basisFun R n).equiv v₂ e) (Pi.single i 1) = v₂ (e i)
⊢ ((↑e₁ ∘ₗ A.mulVecLin) ∘ₗ LinearMap.single R (fun i ↦ R) i) 1 =
    (((toLin v₂ v₁) A ∘ₗ ↑e₂) ∘ₗ LinearMap.single R (fun i ↦ R) i) 1
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ x ∈ couple R A A' → ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2

Tactic:
intro hx; ext a; exact congrArg (· a) hx

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
⊢ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2 → x ∈ couple R A A'

Tactic:
intro hx; ext a; exact congrArg (· a) hx

Goal state after: