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

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
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ ↑g = ↑g'

Tactic:
apply Hom.coweightHom_injective P

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
g g' : P.Aut
hgg' : ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g = ((fun a ↦ MulOpposite.op a) ∘ ⇑(coweightHom P)) g'
h : MulOpposite.unop ((Hom.coweightHom P) ↑g) = MulOpposite.unop ((Hom.coweightHom P) ↑g')
⊢ (Hom.coweightHom P) ↑g = (Hom.coweightHom P) ↑g'
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K⁻¹ * (K * ε * K * K⁻¹) ≤ ε

Tactic:
simp [K0.ne']

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

Goal state before:
pp: case refine_1
ι : 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
inst✝ : P.IsReduced
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)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ 0 < ((P.posRootForm ℚ).posForm (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)

Tactic:
exact (P.posRootForm ℚ).zero_lt_posForm_apply_root i (P.rootSpanMem ℚ i).property

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

Goal state before:
pp: case inr.h.h.h
x : ℝ
a b : CauSeq ℚ abs
h✝ : mk a < mk b
c : CauSeq ℚ abs
⊢ mk a + mk c < mk b + mk c

Tactic:
simp only [mk_lt, ← mk_add] at *

Goal state after:
case inr.h.h.h
x : ℝ
a b c : CauSeq ℚ abs
h✝ : a < b
⊢ a + c < b + c
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 n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
← isHermitian_submatrix_equiv (Equiv.sumComm n m),

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ ((Matrix.fromBlocks A B Bᴴ D).submatrix ⇑(Equiv.sumComm n m) ⇑(Equiv.sumComm n m)).IsHermitian ↔
    (A - B * D⁻¹ * Bᴴ).IsHermitian
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])

Tactic:
have hy' : IsUnit (Y ^ n.succ).det := by
      rw [det_pow]
      exact hy.pow n.succ

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
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
u : Mˣ
k : ℕ
⊢ ↑(u⁻¹ ^ (k + 1)) = (↑u ^ (k + 1))⁻¹

Tactic:
u⁻¹.val_pow_eq_pow_val,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑u⁻¹ ^ (k + 1) = (↑u ^ (k + 1))⁻¹
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case neg
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ M⁻¹.PosSemidef

Tactic:
nonsing_inv_apply_not_isUnit _ h

Goal state after:
case neg
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef 0
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
⊢ (4 - b.cartanMatrix).det ≠ 0

Tactic:
suffices ¬ HasEigenvalue b.cartanMatrix.toLin' 4 by
    have aux : (4 - b.cartanMatrix).toLin' = - (b.cartanMatrix.toLin' - (4 : ℤ) • 1) := by ext; simp
    rwa [ne_eq, ← det_toLin', det_eq_zero_iff_ker_ne_bot, aux, ker_neg, ← eigenspace_def,
      ← hasEigenvalue_iff]

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
⊢ ¬HasEigenvalue (toLin' b.cartanMatrix) 4
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
this : f' = g'
k : ι
hk : k ∈ b.support
⊢ f k • P.root k = g k • P.root k

Tactic:
replace this : f k = g k := congr_fun this ⟨k, hk⟩

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 : ι
hk : k ∈ b.support
this : f k = g k
⊢ f k • P.root k = g k • P.root 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
this : ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k
x✝ : ↥b.support
⊢ P.pairingIn ℤ j ↑x✝ = (g' ᵥ* b.cartanMatrix) x✝

Tactic:
simp [g', this, cartanMatrixIn, Matrix.vecMul_eq_sum, b.support.sum_subtype (by tauto)]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
i : ι
⊢ ∃ x ∈ p, (f (Sum.inl i)) x ≠ 0

Tactic:
obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i
    refine ⟨fun i ↦ P.pairingIn ℤ i j, subset_span ⟨⟨j, hj⟩, rfl⟩, ?_⟩
    rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀
    simpa [f, ne_eq, Int.cast_eq_zero]

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

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

Tactic:
induction n with
  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, ↑k = -r
⊢ eval r (ascPochhammer R n) = 0

Tactic:
obtain ⟨rn, hrn, rnn⟩ := hrn

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ eval r (ascPochhammer R n) = 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
k n : ℕ
h : k < n
⊢ eval (-(↑n - ↑(k + 1))) (ascPochhammer R n) = 0

Tactic:
← Nat.cast_sub h

Goal state after:
R : Type u
inst✝ : Ring R
k n : ℕ
h : k < n
⊢ eval (-↑(n - k.succ)) (ascPochhammer R n) = 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 : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬basisDivisor (v i) (v j) = 0

Tactic:
basisDivisor_eq_zero_iff,

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 : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬v i = v j
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₂
L : LieSubalgebra R (L₁ × L₂) := prod eι b₁ b₂
p₂ : ↥L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
h₁ : range b₂.e = range (⇑p₂ ∘ prodE eι b₁ b₂)
⊢ range b₂.f = range (⇑p₂ ∘ prodF eι b₁ b₂)

Tactic:
simp [show p₂ ∘ prodF eι b₁ b₂ = b₂.f ∘ eι from rfl]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : ↥s → F
i : ι
hi : i ∈ s
⊢ (fun f i ↦ eval (v ↑i) ↑f) ((fun r ↦ ⟨(interpolate s v) fun x ↦ if hx : x ∈ s then r ⟨x, hx⟩ else 0, ⋯⟩) f) ⟨i, hi⟩ =
    f ⟨i, hi⟩

Tactic:
simp only [eval_interpolate_at_node _ hvs hi]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : ↥s → F
i : ι
hi : i ∈ s
⊢ (if hx : i ∈ s then f ⟨i, hx⟩ else 0) = f ⟨i, hi⟩
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: 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
⊢ #t = 1 + (#t - #s) + (#s - 1)

Tactic:
rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
⊢ degree 1 < (X ^ Fintype.card ↥G).degree

Tactic:
simp [Fintype.card_pos]

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]
  have := (Finsupp.finite_of_nat_weight_eq w hw n).to_subtype
  exact Module.Finite.of_basis (basisRestrictSupport R {d | Finsupp.weight w d = n})

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝

Tactic:
· exact Ideal.subset_span z.2

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 𝒜
κ : Sort u_4
f : κ → Ideal A
s : κ → Set ↥(homogeneousSubmonoid 𝒜)
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ i, f i = span (Subtype.val '' ⋃ i, s i)

Tactic:
simp_rw [Set.image_iUnion, Ideal.span_iUnion]

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 𝒜
κ : Sort u_4
f : κ → Ideal A
s : κ → Set ↥(homogeneousSubmonoid 𝒜)
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ⨆ i, f i = ⨆ i, span (Subtype.val '' s i)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
f : MvPolynomial σ R
⊢ f.IsHomogeneous 0

Tactic:
by
  rw [eq_C_of_isEmpty f]
  exact isHomogeneous_C _ _

Goal state after:
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
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ((mapDomain f d).sum fun i c ↦ c) = d.sum fun i c ↦ c

Tactic:
exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf

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✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpolyAux b bₘ = Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)

Tactic:
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✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : DecidableEq ιM
bₘ : Basis ιM R M
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM) =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)
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
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H : (φ.polyCharpoly b).coeff k = 0
⊢ (φ.polyCharpoly b').coeff k = 0

Tactic:
by
  rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map] at H ⊢
  set B := (Module.Free.chooseBasis R M).end
  set g := toMvPolynomial b' b LinearMap.id
  apply_fun (MvPolynomial.bind₁ g) at H
  have : toMvPolynomial b' B φ = fun i ↦ (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i) :=
    funext <| toMvPolynomial_comp b' b B φ LinearMap.id
  rwa [map_zero, RingHom.coe_coe, MvPolynomial.bind₁_bind₁, ← this] at H

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

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ S l R = fromBlocks 1 0 0 (-1)

Tactic:
by
  rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]
  rfl

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
⊢ ∀ (i : m), (if w i = 0 then 1 else w i) ≠ 0

Tactic:
by simp [ite_eq_iff']

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
⊢ (∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆) → a ∈ twoCocycle R L M

Tactic:
· intro h
    ext x y z
    simp only [d₂₃_apply, trivial_lie_zero, sub_self, add_zero, zero_sub, LinearMap.zero_apply]
    rw [← twoCochain_skew a x, ← twoCochain_skew a y, h x y z]
    abel

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

Goal state before:
pp: case inl
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x✝ y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
i : ι
y x : L i
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L i) x, (of L i) y⁆ =
    ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆

Tactic:
simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]

Goal state after:
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
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
this : finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
⊢ Ex ≤ ⟨engel K y, ⋯⟩

Tactic:
suffices engel K y = engel K x from this.ge
    apply LieSubalgebra.toSubmodule_injective
    exact Submodule.eq_of_le_of_finrank_le hyx this

Goal state after:
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
h : ↑(finrank K L) ≤ #K
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
by
  obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h
  use x
  refine ⟨?_, normalizer_engel _ _⟩
  apply isNilpotent_of_forall_le_engel
  intro y hy
  set Ex : {engel K z | z ∈ engel K x} := ⟨engel K x, x, self_mem_engel _ _, rfl⟩
  suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩
  apply engel_isBot_of_isMin h (engel K x) Ex le_rfl
  rintro ⟨_, y, hy, rfl⟩ hyx
  suffices finrank K (engel K x) ≤ finrank K (engel K y) by
    suffices engel K y = engel K x from this.ge
    apply LieSubalgebra.toSubmodule_injective
    exact Submodule.eq_of_le_of_finrank_le hyx this
  rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]
  apply rank_le_finrank_engel

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

Goal state before:
pp: case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ + c') = (liftAux R f) (b✝ + c')

Tactic:
| add_right c' _ h₂ =>

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
⊢ ∀ {x y : FreeLieAlgebra R X},
    Quot.liftOn ⁅x, y⁆ ⇑(liftAux R f) ⋯ = ⁅Quot.liftOn x ⇑(liftAux R f) ⋯, Quot.liftOn y ⇑(liftAux R f) ⋯⁆

Tactic:
by rintro ⟨a⟩ ⟨b⟩; rw [← liftAux_map_mul]; rfl

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

Goal state before:
pp: case hadd
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f i = 0
a✝ : a ≠ 0
⊢ ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, y⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) y⁆
          j) -
      ↑(⁅y, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)

Tactic:
induction y using DirectSum.induction_on' with

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).formPerm ((f ^ k) x) = (f ^ (k + 1)) x

Tactic:
List.formPerm_apply_mem_eq_next (nodup_toList f x),

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f.toList x).next ((f ^ k) x) ?pos.hx✝ = (f ^ (k + 1)) x

case pos.hx
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
k : ℕ
left✝ : k < (f.cycleOf x).support.card
hy : f.SameCycle x ((f ^ k) x)
⊢ (f ^ k) x ∈ f.toList x
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
⊢ m.card ≤ n + 1

Tactic:
by
  classical
    have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c := by
      intro r hr
      obtain ⟨i, hi⟩ := h₂.1 hr
      exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
    rw [← Finset.card_fin (n + 1)]
    exact (Finset.card_le_card fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le

Goal state after: