mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ (monomial (single a b + f)) r ∈ homogeneousSubmodule σ R 1 ^ degree (single a b + f)

Tactic:
| single_add a b f _ _ 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
w : σ → M
m : M
motive : (p : MvPolynomial σ R) → IsWeightedHomogeneous w p m → Prop
zero : motive 0 ⋯
add :
  ∀ (p q : MvPolynomial σ R) (hp : IsWeightedHomogeneous w p m) (hq : IsWeightedHomogeneous w q m),
    motive p hp → motive q hq → motive (p + q) ⋯
monomial : ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ motive p hp

Tactic:
by
  suffices h : ∀ a, motive (C a * p) (.C_mul hp _) by simpa using h 1
  let A : Submodule R (MvPolynomial σ R) :=
    { carrier := { p | ∃ hp, ∀ a, motive (C a * p) (.C_mul hp _) }
      add_mem' := fun ⟨_, hx⟩ ⟨_, hy⟩ ↦
        ⟨.add ‹_› ‹_›, fun a ↦ by simp [mul_add, add _ _ _ _ (hx a) (hy a)]⟩
      zero_mem' := ⟨isWeightedHomogeneous_zero R w m, by simp [zero]⟩
      smul_mem' := fun a x ⟨_, hx⟩ ↦ ⟨by simp [Algebra.smul_def, C_mul ‹_› a], fun a ↦ by
        simp_rw [Algebra.smul_def, algebraMap_eq, ← mul_assoc, ← map_mul]
        apply hx⟩ }
  rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
    AddMonoidAlgebra.supported_eq_span_single] at hp
  refine (Submodule.span_le (p := A) |>.mpr ?_ hp).2
  rw [Set.image_subset_iff]
  intro d hd
  simp only [MvPolynomial, Submodule.coe_set_mk, AddSubmonoid.coe_set_mk,
    AddSubsemigroup.coe_set_mk, preimage_ofPred_eq, mem_ofPred_eq, A]
  refine ⟨isWeightedHomogeneous_monomial w d 1 hd, fun a ↦ ?_⟩
  simpa only [single_eq_monomial, ← MvPolynomial.C_mul_monomial] using monomial _ (a * 1) hd

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

Tactic:
h,

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) 0)) 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (n * m)

Tactic:
rw [← zero_add (n * m)]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (0 + n * m)
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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ eval 0 (minpoly K φ) * eval 0 F = 0

Tactic:
h,

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
F : K[X]
hF : charpoly φ = minpoly K φ * F
h : eval 0 (minpoly K φ) = 0
⊢ 0 * eval 0 F = 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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
h : ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).charpoly.coeff 0 = 0
⊢ (-1) ^ Fintype.card (ChooseBasisIndex K M) * ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).charpoly.coeff 0 = 0

Tactic:
h,

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
tfae_1_iff_2 : φ.HasEigenvalue 0 ↔ (minpoly K φ).IsRoot 0
tfae_2_to_3 : (minpoly K φ).IsRoot 0 → constantCoeff (charpoly φ) = 0
h : ((toMatrix (chooseBasis K M) (chooseBasis K M)) φ).charpoly.coeff 0 = 0
⊢ (-1) ^ Fintype.card (ChooseBasisIndex K M) * 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case succ
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
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by
      linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀]

Goal state after:
case succ
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
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ ∃ r, (eval r) F ≠ 0
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:
by
  rw [← polyCharpolyAux_map_eval (tensorProduct R A M M ∘ₗ baseChange A φ) _ (basis A bₘ),
    polyCharpolyAux_baseChange, Polynomial.map_map]
  congr
  exact DFunLike.ext _ _ fun f ↦ (MvPolynomial.eval_map (algebraMap R A) x f).symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ = ∑ d ∈ φ.support with degree d = n, (monomial d) (coeff d φ)

Tactic:
by
  simp_rw [degree_eq_weight_one]
  convert! weightedHomogeneousComponent_apply n φ

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
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h : ∀ (T S : Module.End R (n → R)), f (T ∘ₗ S) = f T * f S
⊢ f (T ∘ₗ S) - f (S ∘ₗ T) = f T * f S - f S * f T

Tactic:
h,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h : ∀ (T S : Module.End R (n → R)), f (T ∘ₗ S) = f T * f S
⊢ f T * f S - f (S ∘ₗ T) = f T * f S - f S * f T
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case hf
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ ∀ (i : ChooseBasisIndex R L), (C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i)).natDegree ≤ 1

Tactic:
intro k

Goal state after:
case hf
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr y) k) * X + C (((chooseBasis R L).repr x) k)).natDegree ≤ 1
Module: Mathlib.LinearAlgebra.Matrix.Diagonal

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })

Tactic:
have B₁ := iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) hIJ (Set.toFinite _)

Goal state after:
m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
B₁ : ⨆ i ∈ {i | w i ≠ 0}, (single K (fun x ↦ K) i).range = ⨅ i ∈ {i | w i = 0}, (proj i).ker
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
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
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Tactic:
h,

Goal state after:
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)
⊢ fromBlocks 1 1 1 (-1) * PD l R = 2 • S l R
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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
have f_unit {x} : IsUnit x → IsUnit (f x) := (isUnit_submatrix_equiv ..).2

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)
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).eRank = A.eRank

Tactic:
simpa [-lift_cRank_submatrix] using! congr_arg Cardinal.toENat <| A.lift_cRank_submatrix em en

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✝¹ : 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
hB : B * A.submatrix Subtype.val id = A
⊢ A.rank = (B * A.submatrix Subtype.val id).rank

Tactic:
by rw [hB]

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

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

Tactic:
have hs : s.card = M.rank := by
    simp [← rank_mul_eq_right_of_isUnit_det V M hVdet, ← rank_mul_eq_left_of_isUnit_det U (V * M)
      hUdet, hM, rank_diagonal]

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

Goal state before:
pp: case mpr
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
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ A *ᵥ x = 0

Tactic:
h,

Goal state after:
case mpr
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
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ 0 = 0
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: 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 y : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
⊢ ∀ (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)⁆

Tactic:
intro i y
        rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
        simp only [map_neg, neg_inj, ← LieAlgebra.ad_apply R]
        rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
        congr; clear x; ext j x; exact this j i x y

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l[(k + 1) % l.length]

Tactic:
formPerm_apply_getElem _ hl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l[(k + 1) % l.length] = l[(k + 1) % l.length]
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

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

Tactic:
mem_support,

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

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

Tactic:
mem_support,

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

Goal state before:
pp: case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
⊢ n + 1 = m + 1

Tactic:
← hc.support_pow_eq_iff

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

Goal state before:
pp: case neg.succ.succ.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
k : ℕ
hy : (p.cycleOf x ^ k) x ∈ (p.cycleOf x).support
⊢ (p.cycleOf x ^ k) ((p.cycleOf x ^ (n + 1)) x) = (p.cycleOf x ^ (m + 1)) ((p.cycleOf x ^ k) x)

Tactic:
h,

Goal state after:
case neg.succ.succ.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
k : ℕ
hy : (p.cycleOf x ^ k) x ∈ (p.cycleOf x).support
⊢ (p.cycleOf x ^ k) ((p.cycleOf x ^ (m + 1)) x) = (p.cycleOf x ^ (m + 1)) ((p.cycleOf x ^ k) x)
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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ s

Tactic:
Finset.mem_union

Goal state after:
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Φ : Φ.IsSymm
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
s : Finset A := (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs : s = (F f).support ∪ Finset.image (⇑(Equiv.neg A)) (F f).support
hs' : (F f).support ⊆ s
x : A
hx : x ∈ Finset.map (Equiv.toEmbedding (Equiv.neg A)) s
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support