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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x (f - g) = 0

Tactic:
eval_sub,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x f - eval x g = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) (f - g) = 0

Tactic:
eval_sub,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f - eval (v i) g = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y

Tactic:
exact hxy

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (vandermonde v).det ≠ 0 ↔ Function.Injective v

Tactic:
unfold Function.Injective
  simp only [det_vandermonde_eq_zero_iff, Ne, not_exists, not_and, Classical.not_not]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
⊢ ∀ (x_1 : ℕ), ((ad R L) x ^ x_1) z = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, z⁆ = 0

Tactic:
n

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
⊢ ((ad R L) x ^ n) z = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, z⁆ = 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
⊢ s = 0

Tactic:
let μ : I → K := Sigma.fst

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
⊢ s = 0
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ (n + 1)) y = 0

Tactic:
rw [pow_succ, Module.End.mul_apply]

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
n : ℕ
hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0
⊢ ((ad R L) x ^ n) (((ad R L) x) y) = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
⊢ ∑ x ∈ s, C (r x / ∏ j ∈ s.erase x, (v x - v j)) * (⇑derivative)^[k] (∏ j ∈ s.erase x, (X - C (v j))) =
    ∑ x ∈ s,
      C (r x / ∏ j ∈ s.erase x, (v x - v j)) *
        (↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase x), ∏ j ∈ t, (X - C (v j)))

Tactic:
congr! 2 with i hi

Goal state after:
case a
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
⊢ (⇑derivative)^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ j ∈ t, (X - C (v j))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
⊢ ∏ j ∈ s, eval x (X - C (v j)) = ∏ i ∈ s, (x - v i)

Tactic:
eval_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
⊢ ∏ x_1 ∈ s, (eval x X - eval x (C (v x_1))) = ∏ i ∈ s, (x - v i)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, eval x (X - C (v a)) ≠ 0

Tactic:
eval_sub,

Goal state after:
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, eval x X - eval x (C (v a)) ≠ 0
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ (P * A * Q).charpoly = A.charpoly

Tactic:
let φ₃ := reindexLinearEquiv R R (Equiv.refl ι') e

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ (P * A * Q).charpoly = A.charpoly
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 𝒜 ℳ
x✝¹ x✝ : HomogeneousSubmodule 𝒜 ℳ
x : Submodule A M
hx : x.IsHomogeneous ℳ
y : Submodule A M
hy : y.IsHomogeneous ℳ
h : x = y
⊢ { toSubmodule := x, is_homogeneous' := hx } = { toSubmodule := y, is_homogeneous' := hy }

Tactic:
by simp [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
inst✝ : SemilatticeSup M
w : σ → M
⊢ weightedTotalDegree' w 0 = ⊥

Tactic:
simp only [weightedTotalDegree', support_zero, Finset.sup_empty]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommSemiring R
M : Matrix m n R
N : Matrix n o R
i : m
⊢ (M * N).toMvPolynomial i = (bind₁ N.toMvPolynomial) (M.toMvPolynomial i)

Tactic:
simp only [toMvPolynomial, mul_apply, map_sum, Finset.sum_comm (γ := o), bind₁, aeval,
    AlgHom.coe_mk, coe_eval₂Hom, eval₂_monomial, algebraMap_apply, Algebra.algebraMap_self,
    RingHom.id_apply, C_apply, pow_zero, Finsupp.prod_single_index, pow_one, Finset.mul_sum,
    monomial_mul, zero_add]

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)
hVW : IsCompl V W
x : M
⊢ ∀ (x_1 : ℕ), (φ ^ x_1) x = 0 → ∃ k, (φ ^ k) (φ x) = 0

Tactic:
n

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
x : M
n : ℕ
⊢ (φ ^ n) x = 0 → ∃ k, (φ ^ k) (φ x) = 0
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)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
x : M
H : ∀ (i : ℕ), ∃ y, (φ ^ i) y = x
⊢ ∀ (i : ℕ), ∃ y, (φ ^ i) y = φ x

Tactic:
n

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
x : M
H : ∀ (i : ℕ), ∃ y, (φ ^ i) y = x
n : ℕ
⊢ ∃ y, (φ ^ n) y = φ x
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✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R (⇑f '' A.col '' Set.univ) = span R ((A.submatrix r id).col '' Set.univ)

Tactic:
image_image,

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R ((fun x ↦ f (A.col x)) '' Set.univ) = span R ((A.submatrix r id).col '' Set.univ)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Fintype n
inst✝ : CommSemiring R
A : Matrix m n R
⊢ toNat A.cRank = A.rank

Tactic:
by
  rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : (f A * f U) • x = 0
heq2 : f V • (f C * f U) • x = 0
⊢ IsUnit (f V)

pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : f Vᵀ⁻¹ • (f A * f U) • x = 0
heq2 : f V • (f C * f U) • x = 0
⊢ IsUnit (f Vᵀ⁻¹)

Tactic:
· exact f_unit hV

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : f Vᵀ⁻¹ • (f A * f U) • x = 0
heq2 : f V • (f C * f U) • x = 0
⊢ IsUnit (f Vᵀ⁻¹)
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d + e, f⁆ a = (⁅d, f⁆ + ⁅e, f⁆) a
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, e + f⁆ a = (⁅d, e⁆ + ⁅d, f⁆) a
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d : Derivation R A A
⊢ ⁅d, d⁆ = 0

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d : Derivation R A A
a : A
⊢ ⁅d, d⁆ a = 0 a
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
d e f : Derivation R A A
a : A
⊢ ⁅d, ⁅e, f⁆⁆ a = (⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
r : R
d e : Derivation R A A
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a✝ : A
r : R
d e : Derivation R A A
a : A
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a
Module: Mathlib.RingTheory.Derivation.Lie

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

Tactic:
ext a

Goal state after:
case mp
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
hx : x ∈ couple R A A'
a : A
⊢ (⇑x.1 ∘ ⇑(Algebra.ofId A A')) a = (⇑(Algebra.ofId A A') ∘ ⇑x.2) a
Module: Mathlib.RingTheory.Derivation.Lie

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

Tactic:
ext a

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
x : Derivation R A' A' × Derivation R A A
hx : ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
a : A
⊢ ((compAlgebraMapL R A A' A') x.1) a = ((Algebra.ofId A A').toLinearMap.compDer x.2) a
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ ∀ (x y : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x⁆ =
        ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) x⁆ - ⁅x, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
      (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆ →
        (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, x + y⁆ =
          ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) (x + y)⁆ - ⁅x + y, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

Tactic:
· intros _ _ h1 h2
            simp [h1, h2]
            abel_nf

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

Goal state before:
pp: case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
· simp only [lie_of_of_ne L hij x y, hij, dite_false]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
⊢ (lift R).symm g₁ = (lift R).symm g₂

Tactic:
by simp [h]

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

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Cycle α
x✝ : α
h : Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hn : Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
⊢ False

Tactic:
simpa [Nat.succ_le_succ_iff] using length_nontrivial hn

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p.toList x)[n] = (p.toList x)[m] → n = m

Tactic:
getElem_toList,

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p ^ n) x = (p.toList x)[m] → n = m
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p ^ n) x = (p.toList x)[m] → n = m

Tactic:
getElem_toList,

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (p ^ n) x = (p ^ m) x → n = m
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p.toList x)[(k + 1) % (p.toList x).length] = p (p.toList x)[k]

Tactic:
getElem_toList,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = p (p.toList x)[k]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = p (p.toList x)[k]

Tactic:
getElem_toList,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
hy✝ : y ∈ p.toList x
hy : p.SameCycle x y ∧ x ∈ p.support
k : ℕ
hk : k < (p.cycleOf x).support.card
hk' : (p.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = p ((p ^ k) x)