mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
refine hs.symm.imp (fun ⟨n, hn₀, hn⟩ ↦ ?_) (fun ⟨n, hn₀, hn⟩ ↦ ?_)

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
⊢ Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs :
  (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
x✝ : ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
n : ι → ℕ
hn₀ : n ≠ 0
hn : Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i
⊢ -Weight.toLinear K (↥H) L χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: a b : ℕ
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

Tactic:
rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

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

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

Tactic:
norm_cast
  rw [ascPochhammer_nat_eq_descFactorial]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f 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
⊢ (fun k ↦ P.pairingIn ℤ j ↑k) = g' ᵥ* b.cartanMatrix

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

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

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

Tactic:
apply_fun Polynomial.map (algebraMap ℤ R) at h

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

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

Tactic:
Nat.descFactorial_eq_zero_iff_lt.mpr h,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * ↑0 = ↑((n - k) * 0)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
⊢ a ∈ Set.Ici (↑(n + 1) - 1) →
    ∀ ⦃b : S⦄,
      b ∈ Set.Ici (↑(n + 1) - 1) →
        a ≤ b → (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b

Tactic:
ha

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
ha : a ∈ Set.Ici (↑(n + 1) - 1)
⊢ ∀ ⦃b : S⦄,
    b ∈ Set.Ici (↑(n + 1) - 1) →
      a ≤ b → (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ eval x (basisDivisor x y) = 1

Tactic:
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X]

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
j : Fin n.succ
a✝ : j ∈ univ
hj0 : j ≠ 0
⊢ (-1) ^ ↑j * W 0 j * (W.submatrix succ j.succAbove).det = 0

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ (-1) ^ ↑j.succ * W 0 j.succ * (W.submatrix succ j.succ.succAbove).det = 0
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₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
⊢ Disjoint p₁.ker p₂.ker

Tactic:
rw [disjoint_iff, _root_.eq_bot_iff]

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹¹ : Finite ι₁
inst✝¹⁰ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁹ : LieRing L₁
inst✝⁸ : LieRing L₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
⊢ p₁.ker ⊓ p₂.ker ≤ ⊥
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = ((bind₁ f) (∑ x ∈ φ.support, (monomial x) (coeff x φ))).vars

Tactic:
← φ.as_sum

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = ((bind₁ f) φ).vars
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:

Tactic:
(bind₁ f φ).vars
    _ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
      rw [← map_sum, ← φ.as_sum]
    _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars :=
      (vars_sum_subset _ _)
    _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) := by
      simp only [bind₁_monomial]
    _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) := ?_
    -- proof below
    _ ≤ φ.vars.biUnion fun i : σ => vars (f i) := ?_

Goal state after:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ⊆
    φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars

case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars) ⊆ φ.vars.biUnion fun i ↦ (f i).vars
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
⊢ Function.Injective fun X ↦ ↑X.toSubmodule

Tactic:
rintro ⟨p, hp⟩ ⟨q, hq⟩ (h : (p : Set M) = q)

Goal state after:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
p : Submodule A M
hp : p.IsHomogeneous ℳ
q : Submodule A M
hq : q.IsHomogeneous ℳ
h : ↑p = ↑q
⊢ { toSubmodule := p, is_homogeneous' := hp } = { toSubmodule := q, is_homogeneous' := hq }
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
x : F
hvs : Set.InjOn v ↑s
hx : ∀ i ∈ s, x ≠ v i
hs : s.Nonempty
⊢ eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ = 1

Tactic:
simpa only [Pi.one_apply, interpolate_one hvs hs, eval_one, mul_one] using
      (eval_interpolate_not_at_node 1 hx).symm

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ IsNilpotent (↥(derivedSeries R L 1)) M

Tactic:
have _i : FaithfulSMul R A := FaithfulSMul.trans R (FractionRing R) A

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
⊢ IsNilpotent (↥(derivedSeries R L 1)) M
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case e'_3
ι : 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
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {b | b.toIdeal ≤ I}

Tactic:
mem_image,

Goal state after:
case e'_3
ι : 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
coe_mono : Monotone toIdeal
x : Ideal A
⊢ x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ ∃ x_1 ∈ {b | b.toIdeal ≤ I}, x_1.toIdeal = x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1.zero
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ homogeneousSubmodule σ R 1 ^ 0 ≤ homogeneousSubmodule σ R 0

Tactic:
simp [homogeneousSubmodule_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (φ ^ n).IsHomogeneous (m * n)

Tactic:
rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]
  rw [show m * n = ∑ _i ∈ Finset.range n, m by simp [mul_comm]]
  apply IsHomogeneous.prod _ _ _ (fun _ _ ↦ hφ)

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
⊢ ((rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n

Tactic:
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.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : n - i ≠ 0
⊢ 0 ≠ n - i

Tactic:
exact hi.symm

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 (⨆ n, ker (φ ^ n)) W

Tactic:
exact LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
h : LinearIndependent R (col 1)
⊢ Module.rank R ↥(span R (range (col 1))) = lift.{uR, um} #m

Tactic:
rank_span h,

Goal state after:
m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
h : LinearIndependent R (col 1)
⊢ #↑(range (col 1)) = lift.{uR, um} #m
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
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
hcomp : (c • B).mulVecLin = f ∘ₗ B.mulVecLin
⊢ (c • B).rank = B.rank

Tactic:
rw [rank, rank, hcomp, LinearMap.range_comp]

Goal state after:
m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
hcomp : (c • B).mulVecLin = f ∘ₗ B.mulVecLin
⊢ finrank R ↥(Submodule.map f B.mulVecLin.range) = finrank R ↥B.mulVecLin.range
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * M * U =
    diagonal fun i ↦ if i ∈ s then 1 else 0

Tactic:
U_def,

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
⊢ diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * M *
      (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod =
    diagonal fun i ↦ if i ∈ s then 1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
⊢ ∃ V U e, IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Tactic:
refine ⟨V, U, e, (isUnit_iff_isUnit_det _).2 hVdet, isUnit_prod_comp_inverse _, ?_⟩

Goal state after:
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
⊢ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
f : oneCochain R L M
x : L
x✝¹ : R
x✝ : L
⊢ ⁅x, f (x✝¹ • x✝)⁆ - ⁅x✝¹ • x✝, f x⁆ - f ⁅x, x✝¹ • x✝⁆ = (RingHom.id R) x✝¹ • (⁅x, f x✝⁆ - ⁅x✝, f x⁆ - f ⁅x, x✝⁆)

Tactic:
simp [smul_sub]

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

Goal state before:
pp: 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
f : oneCochain R L M
x✝² : R
x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝² • x✝¹, f y⁆ - ⁅y, f (x✝² • x✝¹)⁆ - f ⁅x✝² • x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id R) x✝² • { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ }) x✝

Tactic:
simp [smul_sub]

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

Goal state before:
pp: 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
x✝³ : R
x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ (↑⟨{
              toFun := fun x ↦
                { toFun := fun y ↦ ⁅x, (x✝³ • x✝²) y⁆ - ⁅y, (x✝³ • x✝²) x⁆ - (x✝³ • x✝²) ⁅x, y⁆, map_add' := ⋯,
                  map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑((RingHom.id R) x✝³ •
            ⟨{
                toFun := fun x ↦
                  { toFun := fun y ↦ ⁅x, x✝² y⁆ - ⁅y, x✝² x⁆ - x✝² ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝

Tactic:
simp [smul_sub]

Goal state after: