mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
⊢ 0 = 0

Tactic:
rw [← h1, 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✝
⊢ 0 = 0
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ᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : Qᵀ * P = Pᵀ * Q
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
replace con2 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0 := by
    apply_fun reindex s s at con2
    rw [reindex_apply, reindex_apply, ← hf, ← hf, f_mul, f_mul Pᵀ, heq, hf,
      ← transpose_submatrix, ← hf Q, ← (f Q).fromBlocks_toBlocks, hf (_)ᵀ, hf
      ((fromBlocks 1 0 0 0).submatrix _ _)] at con2
    simp [fromBlocks_transpose, fromBlocks_multiply] at con2; tauto

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ᵀ)
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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: 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} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
⊢ z ∈ engel K ↑v → z ∈ engel K x

Tactic:
hz

Goal state after:
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} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
⊢ z ∈ engel K x
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: case refine_1
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 : Derivation R A A
x y : A ⊗[R] L
x✝ : A
l : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝ ⊗ₜ[R] l, y⁆ =
    ⁅x✝ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l)⁆

Tactic:
refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)

Goal state after:
case refine_1.refine_1
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 : Derivation R A A
x y : A ⊗[R] L
x✝¹ : A
l : L
x✝ : A
l' : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ ⊗ₜ[R] l, x✝ ⊗ₜ[R] l'⁆ =
    ⁅x✝¹ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l')⁆ - ⁅x✝ ⊗ₜ[R] l', (LinearMap.rTensor L ↑d) (x✝¹ ⊗ₜ[R] l)⁆

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 : Derivation R A A
x y : A ⊗[R] L
x✝² : A
l : L
x✝¹ x✝ : A ⊗[R] L
h1 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝¹⁆ - ⁅x✝¹, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
h2 :
  (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) x✝⁆ - ⁅x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝² ⊗ₜ[R] l, x✝¹ + x✝⁆ =
    ⁅x✝² ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆ - ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) (x✝² ⊗ₜ[R] l)⁆
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 B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
⊢ f.mapMatrix (Aᵀ * C) = f.mapMatrix Cᵀ * f.mapMatrix A

Tactic:
(fromBlocks_mem_iff.1 hA).1,

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : IsLocalRing R
hA : fromBlocks A B C D ∈ symplecticGroup l R
k : Type u_2 := IsLocalRing.ResidueField R
f : R →+* IsLocalRing.ResidueField R := IsLocalRing.residue R
A' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix A
C' : Matrix l l (IsLocalRing.ResidueField R) := f.mapMatrix C
F' : Matrix (l ⊕ l) (l ⊕ l) (IsLocalRing.ResidueField R) := fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
F'_def : F' = fromBlocks A' (f.mapMatrix B) C' (f.mapMatrix D)
hF' : IsUnit F'
hker : ∀ (x : l → k), A' *ᵥ x = 0 → C' *ᵥ x = 0 → x = 0
⊢ f.mapMatrix (Cᵀ * A) = f.mapMatrix Cᵀ * f.mapMatrix A
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
        ((fun F ↦ ⇑F ∘ of R) F))
      (Quot.mk (Rel R X) a) =
    F (Quot.mk (Rel R X) a)

Tactic:
let F' := F.toNonUnitalAlgHom.comp (mk R)

Goal state after:
case mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
F' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  F.toNonUnitalAlgHom.comp (mk R)
⊢ ((fun f ↦ { toFun := fun c ↦ Quot.liftOn c ⇑(liftAux R f) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ })
        ((fun F ↦ ⇑F ∘ of R) F))
      (Quot.mk (Rel R X) a) =
    F (Quot.mk (Rel R X) a)
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby✝ : single m b + y ∈ gradeBy R (⇑f) i
hmby : ↑((Finsupp.single m b).support ∪ y.coeff.support) ⊆ ⇑f ⁻¹' {i}
this : Disjoint (Finsupp.single m b).support y.coeff.support
⊢ (decomposeAux f) ↑⟨single m b + y, hmby✝⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby✝⟩

Tactic:
Finset.coe_union,

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
ih : ∀ (hx : y ∈ gradeBy R (⇑f) i), (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩
hmby✝ : single m b + y ∈ gradeBy R (⇑f) i
hmby : ↑(Finsupp.single m b).support ∪ ↑y.coeff.support ⊆ ⇑f ⁻¹' {i}
this : Disjoint (Finsupp.single m b).support y.coeff.support
⊢ (decomposeAux f) ↑⟨single m b + y, hmby✝⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hmby✝⟩
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : 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
c : ↥(twoCocycle R L M)
r : R
x y : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm x).1, ((ofProd c).symm (r • y)).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (r • y)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (r • y)).2⁆ -
          ⁅((ofProd c).symm (r • y)).1, ((ofProd c).symm x).2⁆) =
    r •
      (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
            ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆)

Tactic:
exact Equiv.congr_arg (by simp [← smul_add, smul_sub])

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
⊢ E.toKer.symm ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    E.toKer.symm ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ +
      E.toKer.symm ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆

Tactic:
have aux (z : E.proj.ker) : ⁅⁅h.choose x, h.choose y⁆, z⁆ = ⁅h.choose ⁅x, y⁆, z⁆ := by
      rw [← sub_eq_zero, ← sub_lie]
      exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ z

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
aux : ∀ (z : ↥E.proj.ker), ⁅⁅Exists.choose h x, Exists.choose h y⁆, z⁆ = ⁅Exists.choose h ⁅x, y⁆, z⁆
⊢ E.toKer.symm ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    E.toKer.symm ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ +
      E.toKer.symm ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
⊢ LieModule R L M

Tactic:
by
  let := E.ringModuleOf
  set h := E.proj_surjective.hasRightInverse
  exact
    { smul_lie r x m := by
        rw [ringModuleOf_bracket, ringModuleOf_bracket, ← map_smul, ← smul_lie,
          EquivLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie]
        exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)
      lie_smul r x m := by simp }

Goal state after:
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 ^ k) x = y
⊢ (p.toList x).next y hy✝ = p y

Tactic:
← getElem_toList p x k (by simpa using hk)

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.toList x).next y hy✝ = p y
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case tmul.tmul
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
y v : L
x : AddMonoidAlgebra R A
hx : x ∈ AddMonoidAlgebra.grade R i
u : AddMonoidAlgebra R A
hu : u ∈ AddMonoidAlgebra.grade R j
⊢ ⁅↑⟨x, hx⟩ ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (⟨u, hu⟩ ⊗ₜ[R] v)⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
use ⟨x * u, SetLike.mul_mem_graded hx hu⟩ ⊗ₜ ⁅y, v⁆

Goal state after:
case h
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
y v : L
x : AddMonoidAlgebra R A
hx : x ∈ AddMonoidAlgebra.grade R i
u : AddMonoidAlgebra R A
hu : u ∈ AddMonoidAlgebra.grade R j
⊢ (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) (⟨x * u, ⋯⟩ ⊗ₜ[R] ⁅y, v⁆) =
    ⁅↑⟨x, hx⟩ ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) (⟨u, hu⟩ ⊗ₜ[R] v)⁆
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
this :
  ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) + (⁅s z, ⁅s x, s y⁆⁆ - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - s ⁅z, ⁅x, y⁆⁆)) -
      (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - s ⁅z, ⁅y, x⁆⁆)) =
    0
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
u : L
v : ↥E.proj.ker
⊢ ⁅Exists.choose h u, v⁆ = ⁅s u, v⁆

Tactic:
← E.lie_apply_proj_of_leftInverse_eq hs,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
this :
  ⁅s x, ⁅s y, s z⁆⁆ - ⁅s x, s ⁅y, z⁆⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) + (⁅s z, ⁅s x, s y⁆⁆ - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, ⁅y, z⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - s ⁅z, ⁅x, y⁆⁆)) -
      (⁅s ⁅y, z⁆, s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - s ⁅z, ⁅y, x⁆⁆)) =
    0
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
u : L
v : ↥E.proj.ker
⊢ ⁅s (E.proj (Exists.choose h u)), v⁆ = ⁅s u, v⁆
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case tmul.add
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
u' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hu' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) u' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆
v' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hv' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) v' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ +
      ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
use u' + v'

Goal state after:
case h
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
x : ↥(AddMonoidAlgebra.grade R i)
y : L
u v : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
u' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hu' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) u' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆
v' : ↥(AddMonoidAlgebra.grade R (i + j)) ⊗[R] L
hv' :
  (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) v' =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆
⊢ (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype) (u' + v') =
    ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) u⁆ +
      ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) v⁆
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✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
hu₃ : (F (x + y)).support ⊆ u
⊢ ∑ x_1 ∈ u, x_1 • (Φ ((F f) (-x_1))) ((F (x + y)) x_1) =
    ∑ x_1 ∈ u, x_1 • (Φ ((F f) (-x_1))) ((F x) x_1) + (F y).sum fun a v ↦ a • (Φ ((F f) (-a))) v

Tactic:
sum_of_support_subset _ hu₂ _ (by simp)

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✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A := (F x).support ∪ (F y).support
hu₁ : (F x).support ⊆ u
hu₂ : (F y).support ⊆ u
hu₃ : (F (x + y)).support ⊆ u
⊢ ∑ x_1 ∈ u, x_1 • (Φ ((F f) (-x_1))) ((F (x + y)) x_1) =
    ∑ x_1 ∈ u, x_1 • (Φ ((F f) (-x_1))) ((F x) x_1) + ∑ x ∈ u, x • (Φ ((F f) (-x))) ((F y) x)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ ((-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α) * A i j + ∑ k > i, (Spec.stepEntry A)^[p] A i k * A k j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)

Tactic:
hEq1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
hEq1 : Eq1 A p
⊢ ((-1) ^ (p + 1) * ∑ α ∈ S (p + 1) i, pminor A α) * A i j +
      ∑ x > i, Matrix.of (fun i j ↦ (-1) ^ p * ∑ α ∈ S p i, bminor A i j α) i x * A x j =
    (-1) ^ (p + 1) * (∑ α ∈ S (p + 1) i, pminor A α * A i j - ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j)
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
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : δ ∈ I.rootSet
⊢ (S.reflectionPerm γ) δ ∈ I.rootSet

Tactic:
simp only [mem_rootSet] at hδ ⊢

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
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
⊢ p = c 1

Tactic:
by
  rcases n with - | n
  · contradiction
  obtain ⟨i, rfl⟩ := h₂.1 (dvd_trans hp' hr)
  refine congr_arg c (eq_of_le_of_not_lt' ?_ fun hi => ?_)
  · rw [Fin.le_iff_val_le_val, Fin.val_one, Nat.succ_le_iff, ← Fin.val_zero (n.succ + 1), ←
      Fin.lt_def, Fin.pos_iff_ne_zero]
    rintro rfl
    exact hp.not_isUnit (first_of_chain_isUnit h₁ @h₂)
  obtain rfl | ⟨j, rfl⟩ := i.eq_zero_or_eq_succ
  · cases hi
  refine
    not_irreducible_of_not_isUnit_of_dvdNotUnit
      (DvdNotUnit.not_isUnit
        (Associates.dvdNotUnit_iff_lt.2 (h₁ (show (0 : Fin (n + 2)) < j.castSucc from ?_))))
      ?_ hp.irreducible
  · simpa using Fin.lt_def.mp hi
  · refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)
    simpa only [Fin.coe_eq_castSucc] using Fin.castSucc_lt_succ

Goal state after: