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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
⊢ ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)

Tactic:
exact fun x y ↦ rfl

Goal state after:
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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ i, 0 i < f i

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at hi⟩

Goal state after:
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✝ : CharZero R
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
h : ¬f ≤ 0
⊢ 0 ≤ f

case refine_2
ι : 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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
h : ¬f ≤ 0
⊢ ∃ i, 0 i < f i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case pos
ι : 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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
suffices P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1 by
      rcases this with h₁ | h₁
      · replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
      · replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        rw [← neg_mem_range_root_iff, neg_sub]
        exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩
    have : P.coxeterWeightIn ℤ i j ∈ ({1, 2, 3} : Set _) := by
      have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
      have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
      have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
        simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
      simp_all
    simp_rw [coxeterWeightIn, Int.mul_mem_one_two_three_iff, mem_insert_iff, mem_singleton_iff,
      Prod.mk.injEq] at this
    lia

Goal state after:
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 : ι
h : i ∈ b.support
⊢ 0 < 1

Tactic:
exact Int.one_pos

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

Goal state before:
pp: R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ toBilin (Pi.basisFun R₁ n) = toBilin'

Tactic:
ext M
  simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr,
    toBilin'_apply]

Goal state after:
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
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
hi : 0 < b.height (-j)
contra : i = -j
⊢ False

Tactic:
height_reflectionPerm_self,

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✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
i j k : ι
z : ℤ
hij : i ≠ j
hj : j ∈ b.support
hk : P.root k = P.root i + z • P.root j
this : InvolutiveNeg ι := P.indexNeg
hi : 0 < -b.height j
contra : i = -j
⊢ False
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✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos i
⊢ p i

Tactic:
exact hi.induction_on_add h₁ h₂

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

Goal state before:
pp: case inr
ι : 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✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p (-i)

Tactic:
exact hi.induction_on_add h₁ h₂

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

Goal state before:
pp: x : ℝ
⊢ Ring ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ CommSemiring ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ Semiring ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ CommMonoidWithZero ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ MonoidWithZero ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddCommGroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddGroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddCommMonoid ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddMonoid ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddLeftCancelSemigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddRightCancelSemigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddCommSemigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ AddSemigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ CommMonoid ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ Monoid ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ CommSemigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x : ℝ
⊢ Semigroup ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x a b c : ℝ
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
by
    induction a using Real.ind_mk
    induction b using Real.ind_mk
    induction c using Real.ind_mk
    simpa using le_trans

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

Goal state before:
pp: x : ℝ
⊢ Preorder ℝ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ (1 - f * f.inv hf) * g = g * (1 - f * f.inv hf)

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
⊢ g * (1 - f * f.inv hf) = g * (1 - f * f.inv hf)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
a : Cauchy abs
h : { cauchy := a } ≠ 0
⊢ { cauchy := a } * { cauchy := a }⁻¹ = 1

Tactic:
mul_comm

Goal state after:
x : ℝ
a : Cauchy abs
h : { cauchy := a } ≠ 0
⊢ { cauchy := a }⁻¹ * { cauchy := a } = 1
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ DivisionRing ℝ

Tactic:
infer_instance

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

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a < b)

Tactic:
infer_instance

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

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a ≤ b)

Tactic:
infer_instance

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

Goal state before:
pp: x a b : ℝ
⊢ Decidable (a = b)

Tactic:
infer_instance

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
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
i : n
⊢ 0 ≤ A i i

Tactic:
by
  simpa using hA.2 <| .single i 1

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

Goal state before:
pp: n : ℕ
⊢ (sf n) * ((n + 1) * n !) = n.succ * n ! * sf n

Tactic:
mul_comm

Goal state after:
n : ℕ
⊢ (n + 1) * n ! * sf n = n.succ * n ! * sf n
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (ascPochhammer ℕ n)) = eval (↑k) (map (algebraMap ℕ S) (ascPochhammer ℕ n))

Tactic:
eval_map,

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

Goal state before:
pp: n t : ℕ
⊢ n.ascFactorial t * (n + t) = (n + t) * n.ascFactorial t

Tactic:
mul_comm

Goal state after:
n t : ℕ
⊢ (n + t) * n.ascFactorial t = (n + t) * n.ascFactorial t
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
eval_natCast_mul,

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ ↑(eval k (descPochhammer ℤ n)) = eval (↑k) (map (algebraMap ℤ R) (descPochhammer ℤ n))

Tactic:
eval_map,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ ↑(eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| descPochhammer ℤ (n + 1 + 1)

Tactic:
rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| descPochhammer ℤ (n + 1) * (X - 1 - ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
eval_natCast_mul,

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

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

Tactic:
eval_natCast_mul,

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R k) * ↑n - eval (↑n) (↑k * descPochhammer R k) = ↑((n - k) * n.descFactorial k)

Tactic:
eval_natCast_mul,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
⊢ eval (↑n) (descPochhammer R k) * ↑n - ↑k * eval (↑n) (descPochhammer R k) = ↑((n - k) * n.descFactorial k)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case inl
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 (last n) = Pi.single (last n) (v i ^ n) (last n)

Tactic:
simp [rectVandermonde_apply]

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
⊢ ∀ (j : Fin n), ∑ i, f j ^ ↑i * v i = 0

Tactic:
mul_comm

Goal state after:
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
⊢ ∀ (j : Fin n), ∑ x, v x * f j ^ ↑x = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ j > 0, (↑↑j - ↑↑0) = ↑n.succ.factorial

Tactic:
simp only [Fin.val_zero, Nat.cast_zero, sub_zero]

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ x > 0, ↑↑x = ↑n.succ.factorial
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
x : L
⊢ (engel R x).normalizer = engel R x

Tactic:
by
  apply le_antisymm _ (le_normalizer _)
  intro y hy
  rw [mem_normalizer_iff] at hy
  specialize hy x (self_mem_engel R x)
  rw [← lie_skew, neg_mem_iff (G := L), mem_engel_iff] at hy
  rcases hy with ⟨n, hn⟩
  rw [mem_engel_iff]
  use n + 1
  rw [pow_succ, Module.End.mul_apply]
  exact hn

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
P : R[X]
hP : minpoly R f = X * P
⊢ P.degree < (X * P).degree

Tactic:
mul_comm

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
⊢ P.degree < (P * X).degree
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
⊢ (f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly

Tactic:
let b₁ := chooseBasis R M₁

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ (f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly
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
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
⊢ IsWeightedHomogeneous w (C r * φ) m

Tactic:
rw [← zero_add m]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
⊢ IsWeightedHomogeneous w (C r * φ) (0 + m)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case refine_1
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 ∈ ∅, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)

Tactic:
intro

Goal state after:
case refine_1
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
a✝ : ∀ i ∈ ∅, IsWeightedHomogeneous w (φ i) (n i)
⊢ IsWeightedHomogeneous w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : 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 𝒜
I : Ideal A
⊢ IsHomogeneous 𝒜 I ↔ ∃ S, I = span (Subtype.val '' S)

Tactic:
by
  rw [Ideal.IsHomogeneous.iff_eq, eq_comm]
  exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm

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

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

Tactic:
intro

Goal state after:
case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h✝ : ∀ i ∈ ∅, (φ i).IsHomogeneous (n i)
⊢ (∏ i ∈ ∅, φ i).IsHomogeneous (∑ i ∈ ∅, n i)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (charpoly.univ A ιM) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM))

Tactic:
rw [← charpoly.univ_map_map _ (algebraMap R A)]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Polynomial.map (↑(bind₁ (toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ))))
      (Polynomial.map (MvPolynomial.map (algebraMap R A)) (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM))
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r = finrank K L
this : engel K x = ⊤
⊢ engel K y ≤ ⊤

Tactic:
le_top

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

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PD l R)

Tactic:
infer_instance

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

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PB l R)

Tactic:
infer_instance

Goal state after: