mathlib-initiative/mathlib-tactics huggingface dataset:
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 : σ → τ
h : φ.IsHomogeneous n
⊢ ((rename f) φ).IsHomogeneous n

Tactic:
by
  rw [← φ.support_sum_monomial_coeff, map_sum]; simp_rw [rename_monomial]
  apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _
  intro d hd
  apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans
  convert! h (mem_support_iff.mp hd)
  simp only [weight_apply, AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one]

Goal state after:
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
x : L
i✝ j✝ : ιM
⊢ (eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ (i✝, j✝)) = (toMatrix bₘ bₘ) (φ x) i✝ j✝

Tactic:
toMvPolynomial_eval_eq_apply,

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
x : L
i✝ j✝ : ιM
⊢ (bₘ.end.repr (φ (b.repr.symm (b.repr x)))) (i✝, j✝) = (toMatrix bₘ bₘ) (φ x) i✝ j✝
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
hF₀ : F ≠ 0
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
j : ℕ
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hF : F.IsHomogeneous ((finSuccEquiv R N) F).natDegree
hnR : ↑((finSuccEquiv R N) F).natDegree ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < ((finSuccEquiv R N) F).natDegree + 1
hin✝ : i ≤ ((finSuccEquiv R N) F).natDegree
hFn : ((finSuccEquiv R N) F).coeff ((finSuccEquiv R N) F).natDegree = 0
hin : i < ((finSuccEquiv R N) F).natDegree
hj : i + (j + 1) = ((finSuccEquiv R N) F).natDegree
⊢ False

Tactic:
refine leadingCoeff_ne_zero.mpr ?_ hFn

Goal state after:
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
hF₀ : F ≠ 0
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
j : ℕ
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hF : F.IsHomogeneous ((finSuccEquiv R N) F).natDegree
hnR : ↑((finSuccEquiv R N) F).natDegree ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < ((finSuccEquiv R N) F).natDegree + 1
hin✝ : i ≤ ((finSuccEquiv R N) F).natDegree
hFn : ((finSuccEquiv R N) F).coeff ((finSuccEquiv R N) F).natDegree = 0
hin : i < ((finSuccEquiv R N) F).natDegree
hj : i + (j + 1) = ((finSuccEquiv R N) F).natDegree
⊢ (finSuccEquiv R N) F ≠ 0
Module: Mathlib.Algebra.Lie.Matrix

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ toEnd R (Matrix n n R) (n → R) = lieEquivMatrix'.symm.toLieHom

Tactic:
ext; 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 ∈ symplecticGroup l R
⊢ IsUnit A.det

Tactic:
by
  rw [isUnit_iff_exists_inv]
  use A.det
  refine (isUnit_det_J l R).mul_left_cancel ?_
  rw [mul_one]
  rw [mem_iff] at hA
  apply_fun det at hA
  simp only [det_mul, det_transpose] at hA
  rw [mul_comm A.det, mul_assoc] at hA
  exact hA

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ᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R

Tactic:
by simpa using transpose_mem hA

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✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).eRank ≤ A.eRank

Tactic:
by
  simpa using! OrderHom.mono (β := ℕ∞) Cardinal.toENat <| lift_cRank_submatrix_le A r c

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

Goal state before:
pp: case neg
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
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j

Tactic:
have h0 : A i = 0 := hz i hi

Goal state after:
case neg
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
h0 : A i = 0
⊢ ∑ j_1, (if ↑j_1 = i then 1 else 0) * A (↑j_1) j = A i j
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case neg
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
i✝ j✝ : m
h1 : i✝ = j✝
h2 : ¬D i✝ = 0
⊢ (D i✝)⁻¹ * D i✝ = 1

Tactic:
inv_mul_cancel₀ h2

Goal state after:
case neg
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
i✝ j✝ : m
h1 : i✝ = j✝
h2 : ¬D i✝ = 0
⊢ 1 = 1
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.mulVecLin.ker =
    finrank R ↥A.mulVecLin.range + finrank R ↥A.mulVecLin.ker

Tactic:
trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }

Goal state after:
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.mulVecLin.ker =
    finrank R ↥(Aᵀ * A).mulVecLin.range + finrank R ↥(Aᵀ * A).mulVecLin.ker

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
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:
ext; simp

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✝¹ : R
x✝ : Derivation R A A
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_2
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ᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
heq' : f (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹
⊢ IsUnit (f Vᵀ * (f Q + Y * f P)) ∧ IsUnit (f U⁻¹)

Tactic:
IsUnit.mul_iff

Goal state after:
case refine_2
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ᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
con3 : IsUnit (f Q).toBlocks₂₂
Y : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
Y_def : Y = fromBlocks (1 - (f Q).toBlocks₁₁) 0 0 0
hY_symm : Y.IsSymm
X : Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R := f Vᵀ * Y * f V
X_def : X = f Vᵀ * Y * f V
heq' : f (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹
⊢ (IsUnit (f Vᵀ) ∧ IsUnit (f Q + Y * f P)) ∧ IsUnit (f U⁻¹)
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
⊢ (toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x =
    (LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x) ∘ₗ toModule R ι L' fun i ↦ ↑(f i)

Tactic:
ext i y

Goal state after:
R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
x : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i : ι) (y : L i),
    (toModule R ι L' f') ⁅x, (of L i) y⁆ = ⁅(toModule R ι L' f') x, (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
⊢ (((toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) x) ∘ₗ lof R ι L i) y =
    (((LieAlgebra.ad R L') ((toModule R ι L' fun i ↦ ↑(f i)) x) ∘ₗ toModule R ι L' fun i ↦ ↑(f i)) ∘ₗ lof R ι L i) y
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
⊢ ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))).comp
      ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)) =
    AlgHom.id R (FreeAlgebra R X)

Tactic:
ext; simp

Goal state after:
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
⊢ ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)).comp
      ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))) =
    AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (single 0 1).coeff.support
⊢ f m = 0

Tactic:
obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h

Goal state after:
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
h : 0 ∈ (single 0 1).coeff.support
⊢ f 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
      (lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
          ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)) =
    LinearMap.id

pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (((lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
          ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) ∘ₗ
      coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) =
    LinearMap.id

Tactic:
· simp_rw [← comp_assoc]
    rw [← LinearEquiv.eq_comp_toLinearMap_symm]
    ext
    simp

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (((lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
        ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
          ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) ∘ₗ
      coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) =
    LinearMap.id
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
⊢ rTensor N (component R ι (fun i ↦ ↥(ℳ i)) i ∘ₗ ↑(decomposeLinearEquiv ℳ)) ∘ₗ rTensor N (ℳ i).subtype = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ℳ : ι → Submodule R M
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
⊢ ↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = lof R ι (fun i ↦ ↥(ℳ i)) i

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : Perm α
hf : f.IsCycle
⊢ ∀ (a a' : α) (m : Multiset α) (b : Cycle α),
    (if f a = a then if f a' = a' then b else ↑(f.toList a') else ↑(f.toList a)) ≍
      if f a' = a' then if f a = a then b else ↑(f.toList a) else ↑(f.toList a')

Tactic:
intro x y _ s

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if f x = x then if f y = y then s else ↑(f.toList y) else ↑(f.toList x)) ≍
    if f y = y then if f x = x then s else ↑(f.toList x) else ↑(f.toList y)
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ + x✝)) ⋯ =
    Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯ + Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : R
x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ • x✝)) ⋯ =
    (RingHom.id R) x✝¹ • Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
⊢ { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
      (x✝¹ • x✝) =
    (AlgHom.id R A₁) x✝¹ •
      { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝ : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : a ∈ corootSpace ⇑α
hx : H.toLieSubmodule.incl a ∈ corootSubmodule α
⊢ H.toLieSubmodule.incl a ∈ LieSubmodule.restr I H

Tactic:
have : (⟨a.val, a.property⟩ : H) ∈ corootSpace α := ha

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝ : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
a : ↥H.toLieSubmodule
ha : a ∈ corootSpace ⇑α
hx : H.toLieSubmodule.incl a ∈ corootSubmodule α
this : ⟨↑a, ⋯⟩ ∈ corootSpace ⇑α
⊢ H.toLieSubmodule.incl a ∈ LieSubmodule.restr I H
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
⊢ ↑α (coroot ↑β) = 0

Tactic:
by
  have h_ker : coroot (α : Weight K H L) ∈ (β : Weight K H L).ker :=
    I.root_apply_eq_zero_of_notMem_rootSet
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule _)) hβ
  change coroot (β : Weight K H L) ∈ (α : Weight K H L).ker
  rw [← orthogonal_span_coroot_eq_ker,
    LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LinearMap.mem_ker]
  exact traceForm_eq_zero_of_mem_ker_of_mem_span_coroot h_ker (Submodule.mem_span_singleton_self _)

Goal state after: