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

Goal state before:
pp: 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
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
inst✝¹³ : CharZero R
inst✝¹² : IsDomain R
inst✝¹¹ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R M₂
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : Module R N₂
P : RootPairing ι R M N
inst✝⁶ : P.IsRootSystem
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝³ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
m : M
h : m ∈ range ⇑P.root
⊢ f m ∈ range ⇑P₂.root

Tactic:
exact apply_mem_range_root_of_cartanMatrixEq b b₂ e f (by simp [f, Module.Basis.equiv]) m h he

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v f g : ι → F
⊢ ∑ i ∈ s, C ((f + g) i) * Lagrange.basis s v i =
    ∑ i ∈ s, C (f i) * Lagrange.basis s v i + ∑ i ∈ s, C (g i) * Lagrange.basis s v i

Tactic:
by
    simp_rw [← Finset.sum_add_distrib]
    have h : (fun x => C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) =
    (fun x => C ((f + g) x) * Lagrange.basis s v x) := by
      simp_rw [← add_mul, ← C_add, Pi.add_apply]
    rw [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Tactic:
simp only [Ne, forall_exists_index, and_imp]
    refine fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)
    rw [vandermonde_apply, vandermonde_apply, h₁]

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
⊢ v = 0

Tactic:
apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf

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), ∑ i, f j ^ ↑i * v i = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case e_f
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ (fun i_1 ↦ (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1) = fun j_1 ↦
    of (fun i j ↦ v i ^ ↑j) i j_1 * (p j).coeff ↑j_1

Tactic:
ext k

Goal state after:
case e_f
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
⊢ (RingHom.id R) ((p j).coeff ↑k) * v i ^ ↑k = of (fun i j ↦ v i ^ ↑j) i k * (p j).coeff ↑k
Module: Mathlib.LinearAlgebra.Lagrange

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

Tactic:
degree_pow,

Goal state after:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ↑(Fintype.card ↑↑G) = Fintype.card ↥G • X.degree
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 : ι
hi : i ∈ s
⊢ nodalWeight s v i = (eval (v i) (derivative (nodal s v)))⁻¹

Tactic:
rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]

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✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
⊢ (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ I

Tactic:
have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) :=
    GradedMul.mul_mem (SetLike.coe_mem _) hi

Goal state after:
ι : 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
r x : A
hx₂ : x ∈ I
j k : ι
a✝ : k ∈ DFinsupp.support ((decompose 𝒜) r)
i : ι
hi : x ∈ 𝒜 i
mem₁ : ↑(((decompose 𝒜) r) k) * x ∈ 𝒜 (k + i)
⊢ (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ 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✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal

Tactic:
rw [iSup, toIdeal_sSup, iSup_range]

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
⊢ (p.coeff i).IsHomogeneous j

Tactic:
let e' := e.optionCongr.trans (_root_.finSuccEquiv _).symm

Goal state after:
σ : 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
⊢ (p.coeff i).IsHomogeneous j
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) = ((finSuccEquiv R k) ((rename ⇑e') ((optionEquivLeft R σ).symm p))).coeff i

Tactic:
rw [finSuccEquiv_rename_finSuccEquiv, AlgEquiv.apply_symm_apply]

Goal state after:
σ : 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
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case e_f.hX
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
ij : ιM × ιM
⊢ (bind₁ (toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ)))
      (toMvPolynomial (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij) =
    toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ) ij

Tactic:
suffices toMvPolynomial (M₂ := (Module.End A (TensorProduct R A M)))
        (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij = X ij by
      rw [this, bind₁_X_right]

Goal state after:
case e_f.hX
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
ij : ιM × ιM
⊢ toMvPolynomial (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij = X ij
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
inst✝¹ : Module.Finite A (A ⊗[R] M)
inst✝ : Free A (A ⊗[R] M)
x : ι → A
⊢ Polynomial.map (aeval x).toRingHom (φ.polyCharpolyAux b bₘ) =
    ((tensorProduct R A M M ∘ₗ baseChange A φ) ((basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly

Tactic:
← polyCharpolyAux_map_eval (tensorProduct R A M M ∘ₗ baseChange A φ) _ (basis A bₘ),

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
inst✝¹ : Module.Finite A (A ⊗[R] M)
inst✝ : Free A (A ⊗[R] M)
x : ι → A
⊢ Polynomial.map (aeval x).toRingHom (φ.polyCharpolyAux b bₘ) =
    Polynomial.map (eval x) ((tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (basis A bₘ))
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: case refine_1
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
h : c ≤ f.rank
⊢ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndepOn K (⇑f) s

Tactic:
rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩

Goal state after:
case refine_1
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #↑s ≤ f.rank
⊢ ∃ s_1, lift.{v', v} #↑s_1 = lift.{v, v'} #↑s ∧ LinearIndepOn K (⇑f) s_1
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.inl
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} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r = finrank K L
⊢ (engel K x).toSubmodule = ⊤.toSubmodule

Tactic:
apply Submodule.eq_top_of_finrank_eq hr

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
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * b * J l R * bᵀ * aᵀ = J l R

Tactic:
a.mul_assoc,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * (b * J l R) * bᵀ * aᵀ = J l R
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
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * (b * J l R) * bᵀ * aᵀ = J l R

Tactic:
a.mul_assoc,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * (b * J l R * bᵀ) * aᵀ = J l R
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
s : Finset m
hz : ∀ x ∉ ↑s, A.row x = 0
B : Matrix m (↥s) R := of fun i a ↦ if ↑a = i then 1 else 0
hBdef : B = of fun i a ↦ if ↑a = i then 1 else 0
i : m
j : n
hi : i ∈ s
a : ↥s
ha : a ≠ ⟨i, hi⟩
⊢ (if ↑a = i then 1 else 0) * A (↑a) j = 0

Tactic:
by rw [if_neg fun he => ha (Subtype.ext he), zero_mul]

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᴴ * A).mulVecLin.range + finrank R ↥(Aᴴ * A).mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
simp only [LinearMap.finrank_range_add_finrank_ker]

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

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
⊢ finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
simp only [LinearMap.finrank_range_add_finrank_ker]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: 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
x✝¹ x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝¹, x✝⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
      { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆

Tactic:
by
    ext z
    refine z.induction_on (by simp) (by simp [sub_tmul]) (fun _ _ hx hy ↦ ?_)
    simp_all
    abel

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

Goal state before:
pp: ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
⊢ ⁅(of L i) x, (of L j) y⁆ = 0

Tactic:
ext k

Goal state after:
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅(of L i) x, (of L j) y⁆ k = 0 k
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
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
⊢ M.det = 1

Tactic:
set A := M.toBlocks₁₁; set B := M.toBlocks₁₂
  set C := M.toBlocks₂₁; set D := M.toBlocks₂₂
  obtain ⟨X, hX_symm, hA_isUnit⟩ := exists_symmetric_X_isUnit_det_add_mul_of_symplectic <|
    M.fromBlocks_toBlocks ▸ hM
  -- `fromBlocks 1 X 0 1` turns the upper-left block of `M` into an invertible matrix, here `X`
  -- is obtained via previous result.
  have Lx_mul : (fromBlocks 1 X 0 1) * M = fromBlocks (A + X * C) (B + X * D) C D := by
    rw [← M.fromBlocks_toBlocks, fromBlocks_multiply]
    simp only [one_mul, zero_mul, zero_add]; rfl
  have h_fromBlocks_in : fromBlocks (A + X * C) (B + X * D) C D ∈ symplecticGroup l R := by
    rw [← Lx_mul]
    refine (symplecticGroup l R).mul_mem ?_ hM
    simp [mem_iff, fromBlocks_transpose, hX_symm.eq, J, fromBlocks_multiply]
  have _ : Invertible (A + X * C) := (A + X * C).invertibleOfIsUnitDet hA_isUnit
  -- And we know that a symmetric matrix with invertible upper-left block has determinant 1.
  have h_main : ((fromBlocks 1 X 0 1) * M).det = 1 := by
    rw [Lx_mul, det_one_if_fromBlocks_invertible h_fromBlocks_in]
  rwa [det_mul, det_fromBlocks_zero₂₁, det_one, one_mul, one_mul] at h_main

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
⊢ engel K x ≤ engel K y

Tactic:
suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
⊢ IsBot Ex
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ Inhabited (FreeLieAlgebra R X)

Tactic:
FreeLieAlgebra

Goal state after:
R : Type u
X : Type v
inst✝ : CommRing R
⊢ Inhabited (Quot (FreeLieAlgebra.Rel R X))
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ ((lift R) f) (of R x) = f x

Tactic:
← @Function.comp_apply _ _ _ (lift R f) (of R) x,

Goal state after:
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ (⇑((lift R) f) ∘ of R) x = f x
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case refine_1
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
aux : radical k L = center k L
x : L
hx : x ∈ center k L
⊢ (toEnd k L M) x ∈ k ∙ LinearMap.id

Tactic:
← aux

Goal state after:
case refine_1
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k M ⇑χ
hχ : ∀ (x : L) (hx : x ∈ radical k L), (toEnd k L M) x = χ ⟨x, hx⟩ • LinearMap.id
aux : radical k L = center k L
x : L
hx : x ∈ radical k L
⊢ (toEnd k L M) x ∈ k ∙ LinearMap.id
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
this : b • (Φ ⁅x, z⁆) y = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

Tactic:
by
        simpa only [show a + b = -c by grind, show a + c = -b by grind, show b + c = -a by grind,
          Finsupp.single_eq_same]

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.toLieSubalgebra R) L₁' = (fun L' ↦ L'.toLieSubalgebra R) L₂'
⊢ L₁' = L₂'

Tactic:
rw [SetLike.ext'_iff] at h
  rw [← coe_set_eq]
  exact h

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p

Tactic:
by
  suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm
  simp [TensorProduct.Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ x_1, E.coeffs x_1 * (x * y x_1) = ∑ i, x * (E.coeffs i * y i)

Tactic:
exact sum_congr rfl fun x _ ↦ by ac_rfl

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1 - ∑ i, (monomial ↑i) (E.coeffs i)).degree = ↑E.order

Tactic:
degree_sub_eq_left_of_degree_lt

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ Associated (p * b) p

Tactic:
conv_rhs => rw [h]

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

Goal state before:
pp: case mpr.inr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij✝ : i ≠ j
hij : j < i
⊢ A i j = 0 ∨ A i j = -1

Tactic:
· exact h hij

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0

Tactic:
eq_spanSingleton_of_principal I,

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ spanSingleton R₁⁰ (generator ↑I) = 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
⊢ map (↑g.symm) (map (↑g) I) = I

Tactic:
by
  rw [← map_comp, g.symm_comp, map_id]

Goal state after: