mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ x✝ ∈ {x | ∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x} ↔
    x✝ ∈ ⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}

Tactic:
simp

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₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ (∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x✝) ↔ ∃ a, ⟨(b₂.h (eι a), b₁.h a), ⋯⟩ = x✝
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (vandermonde fun i ↦ ↑↑i).det = ↑(Nat.superFactorial 0)

Tactic:
simp

Goal state after:
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✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
⊢ ∀ (x y : ↥H₁ × ↥H₂), ⟨⟨(↑(x + y).1, ↑(x + y).2), ⋯⟩, ⋯⟩ = ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩ + ⟨⟨(↑y.1, ↑y.2), ⋯⟩, ⋯⟩

Tactic:
simp

Goal state after:
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✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
⊢ ∀ (m : K) (x : ↥H₁ × ↥H₂), ⟨⟨(↑(m • x).1, ↑(m • x).2), ⋯⟩, ⋯⟩ = (RingHom.id K) m • ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩

Tactic:
simp

Goal state after:
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
⊢ ((ad R L) x ^ 1) x = 0

Tactic:
simp

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
hvs : Set.InjOn v ↑s
P : F[X]
hP : ↑(#s) = P.degree + 1
⊢ P.degree ≠ ⊥

Tactic:
contrapose! hP; simp [hP]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (fun d ↦ d) ↑(image x univ)
v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
v_def : v = fun z ↦ if h : ∃ i, x i = z then y h.choose else 0
i : ι
⊢ x i ∈ image x univ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (bind₁ X) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
⊢ ((bind₂ C).comp C) x✝ = ((RingHom.id (MvPolynomial σ R)).comp C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hX
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((bind₂ C) (X i✝)) = coeff m✝ ((RingHom.id (MvPolynomial σ R)) (X i✝))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
x✝ : R
⊢ (((bind₂ g).comp (bind₂ f)).comp C) x✝ = ((bind₂ ((bind₂ g).comp f)).comp C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((bind₂ g).comp (bind₂ f)) (X i✝)) = coeff m✝ ((bind₂ ((bind₂ g).comp f)) (X i✝))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
i : σ
⊢ ((rename g).comp (bind₁ f)) (X i) = (bind₁ fun i ↦ (rename g) (f i)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ((bind₁ f).comp (rename g)) (X i) = (bind₁ (f ∘ g)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x✝ : R
⊢ (((eval₂Hom f g).comp (bind₂ h)).comp C) x✝ = ((eval₂Hom ((eval₂Hom f g).comp h) g).comp C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i✝ : σ
⊢ ((eval₂Hom f g).comp (bind₂ h)) (X i✝) = (eval₂Hom ((eval₂Hom f g).comp h) g) (X i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: 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

Tactic:
intro j

Goal state after:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (j ∈ φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars) → j ∈ φ.vars.biUnion fun i ↦ (f i).vars
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

Tactic:
simp

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
⊢ ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0

Tactic:
intro j

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 : ι
⊢ j ∈ s.erase i → (v i - v j)⁻¹ ≠ 0
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
⊢ y ∈ K[s]

Tactic:
adjoin_singleton_eq_range_aeval

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
⊢ y ∈ (aeval s).range
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
n : ℕ
⊢ IsWeightedHomogeneous w (φ ^ n) (n • m)

Tactic:
by
  induction n with
  | zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
  | succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ

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
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)

Tactic:
intro j

Goal state after:
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
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
⊢ j ∈ s → IsWeightedHomogeneous w (φ j) (n j)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case refine_1
ι : 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
⊢ IsHomogeneousElem 𝒜 ↑z

Tactic:
rcases z with ⟨z, hz2⟩
    apply h _ hz2

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

Goal state before:
pp: case e_f
R : Type u_3
inst✝ : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
x✝ : σ →₀ ℕ
⊢ ((fun s ↦ (linearCombination ℕ w).toAddMonoidHom s) ∘ mapDomain e) x✝ =
    (linearCombination ℕ (w ∘ e)).toAddMonoidHom x✝

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), 1 x ≠ 0

Tactic:
simp

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

Goal state before:
pp: case zero
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
⊢ (monomial 0) r ∈ homogeneousSubmodule σ R 1 ^ degree 0

Tactic:
simp

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
⊢ ∀ c ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) c) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
intro j

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
j : ι
⊢ j ∈ DFinsupp.support ((decompose 𝒜) r) → ↑(((decompose 𝒜) r) j) ∈ (homogeneousHull 𝒜 I).toIdeal
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2.zero
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
⊢ 0 ∈ homogeneousSubmodule σ R 1 ^ n

Tactic:
simp

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
    simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]

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 = ∏ _i ∈ Finset.range n, φ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ Finsupp.degree (Finsupp.single j 1) = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
N : ℕ
φ : MvPolynomial (Fin (N + 1)) R
n : ℕ
hφ : φ.IsHomogeneous n
i j : ℕ
h : i + j = n
d : Fin N →₀ ℕ
hd : coeff (cons i d) φ ≠ 0
⊢ ∀ x ∈ insert 0 (Finset.map (Fin.succEmb N) d.support) \ (cons i d).support, (cons i d) x = 0

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)
hφ : φ.IsHomogeneous n
⊢ (rename ⇑e) (p.coeff i) = (Polynomial.map (rename ⇑e).toRingHom p).coeff i

Tactic:
simp

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
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
x : DirectSum M fun i ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (decompose' R w ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) x)) m = x m

Tactic:
rw [← Subtype.coe_inj, decompose'_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
x : DirectSum M fun i ↦ ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ (weightedHomogeneousComponent w m) ((DirectSum.coeAddMonoidHom (weightedHomogeneousSubmodule R w)) x) = ↑(x m)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ d ∈ φ.support, degree d ≠ n

Tactic:
rw [totalDegree, Finset.sup_lt_iff (lt_of_le_of_lt (Nat.zero_le _) h)] at h

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : ∀ b ∈ φ.support, (b.sum fun x e ↦ e) < n
⊢ ∀ d ∈ φ.support, degree d ≠ n
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ χ ⁅x, y⁆ = 0

Tactic:
LieHom.map_lie,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅χ x, χ y⁆ = 0
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅χ x, χ y⁆ = 0

Tactic:
by
  rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x✝¹ : Matrix n n R
i✝ x✝ : n
⊢ ((toEnd R (Matrix n n R) (n → R)) x✝¹ ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝ =
    (lieEquivMatrix'.symm.toLieHom x✝¹ ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
n : Type w
inst✝¹ : CommRing R
inst✝ : Fintype n
A B : Matrix n n R
⊢ (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ

Tactic:
simp

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

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)

Tactic:
suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔
        A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P) by
      simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
      exact this

Goal state after:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ (P.lieConj h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
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)).ker = ⨆ i ∈ {i | w i = 0}, (LinearMap.single K (fun x ↦ K) i).range

Tactic:
rw [← comap_bot]
  simpa [← ker_comp, proj_diagonal, ker_smul', ← iInf_ker_proj] using
    (iSup_range_single_eq_iInf_ker_proj K _ isCompl_compl {i | w i = 0}.toFinite).symm

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 n
i j k : n
r : R
⊢ (traceLinearMap n R R) ((singleLinearMap R i i) r) = (traceLinearMap n R R) ((singleLinearMap R j j) r)

Tactic:
simp

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i j) r + (singleSubSingle j k) r) = ↑((singleSubSingle i k) r)

Tactic:
simp

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle i j) r) = ↑((singleSubSingle j k) r)

Tactic:
simp

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle j k) r) = ↑((singleSubSingle i j) r)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ 1 ∈ {A | A * J l R * Aᵀ = J l R}

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 * 0 + -1 * 1) * 0ᵀ + (0 * -1 + -1 * 0) * (-1)ᵀ) ((0 * 0 + -1 * 1) * 1ᵀ + (0 * -1 + -1 * 0) * 0ᵀ)
      ((1 * 0 + 0 * 1) * 0ᵀ + (1 * -1 + 0 * 0) * (-1)ᵀ) ((1 * 0 + 0 * 1) * 1ᵀ + (1 * -1 + 0 * 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0

Tactic:
simp

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
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ)
      (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) =
    1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ Aᵀ * J l R * A = -Aᵀ * -J l R * A

Tactic:
simp

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

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ rank 1 = Fintype.card n

Tactic:
rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r c).rank = ((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ.rank

Tactic:
simp

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r id)ᵀᵀ.rank = (A.submatrix r ⇑(Equiv.refl n)).rank

Tactic:
simp

Goal state after: