mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (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
⊢ f Vᵀ * Y * f V * C.submatrix ⇑s.symm ⇑s.symm =
    Vᵀ.submatrix ⇑s.symm ⇑s.symm * Y * V.submatrix ⇑s.symm ⇑s.symm * C.submatrix ⇑s.symm ⇑s.symm

Tactic:
rfl

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
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑d), map_add' := ⋯, map_smul' := ⋯ } ⁅x, y⁆ =
    ⁅x, { toFun := ⇑(LinearMap.lTensor A ↑d), map_add' := ⋯, map_smul' := ⋯ } y⁆ -
      ⁅y, { toFun := ⇑(LinearMap.lTensor A ↑d), map_add' := ⋯, map_smul' := ⋯ } x⁆

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk]
        refine x.induction_on (by simp) ?_ ?_
        · intros _ _
          refine y.induction_on (by simp) ?_ ?_
          · intros _ _
            simp [LieAlgebra.ExtendScalars.bracket_tmul, tmul_sub, mul_comm]
          · intros _ _ h1 h2
            simp [h1, h2]
            abel_nf
        · intros _ _ h1 h2
          simp [h1, h2]
          abel_nf

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 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)
⊢ F'.det = (fromBlocks (A.map ⇑f) (B.map ⇑f) (C.map ⇑f) (D.map ⇑f)).det

Tactic:
rfl

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
inst✝ : IsLocalRing R
M : Matrix (l ⊕ l) (l ⊕ l) R
hM : M ∈ symplecticGroup l R
A : Matrix l l R := M.toBlocks₁₁
B : Matrix l l R := M.toBlocks₁₂
C : Matrix l l R := M.toBlocks₂₁
D : Matrix l l R := M.toBlocks₂₂
X : Matrix l l R
hX_symm : X.IsSymm
hA_isUnit : IsUnit (M.toBlocks₁₁ + X * M.toBlocks₂₁).det
⊢ fromBlocks (M.toBlocks₁₁ + X * M.toBlocks₂₁) (M.toBlocks₁₂ + X * M.toBlocks₂₂) M.toBlocks₂₁ M.toBlocks₂₂ =
    fromBlocks (A + X * C) (B + X * D) C D

Tactic:
rfl

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
F : UniversalEnvelopingAlgebra R L →ₐ[R] A
x✝ : L
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl

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

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (Quot.mk (Rel R X) a + Quot.mk (Rel R X) b) ⇑(liftAux R f) ⋯ = (liftAux R f) (a + b)

Tactic:
rfl

Goal state after:
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 : X → L
t : R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn (t • Quot.mk (Rel R X) a) ⇑(liftAux R f) ⋯ = (liftAux R f) ((RingHom.id R) t • a)

Tactic:
rfl

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

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ =
    ⁅(Quot.mk (Rel R X) a).liftOn ⇑(liftAux R f) ⋯, (Quot.mk (Rel R X) b).liftOn ⇑(liftAux R f) ⋯⁆

Tactic:
rw [← liftAux_map_mul]

Goal state after:
case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ = (liftAux R f) (a * b)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.liftOn ⁅Quot.mk (Rel R X) a, Quot.mk (Rel R X) b⁆ ⇑(liftAux R f) ⋯ = (liftAux R f) (a * b)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : M → ι
i : ι
a : R[M]
⊢ a ∈ gradeBy R f i ↔ ↑a.coeff.support ⊆ f ⁻¹' {i}

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ ↑a.coeff.support ⊆ {m}

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ a ∈ grade R m ↔ a ∈ (lsingle m).range

Tactic:
rw [mem_grade_iff, Finsupp.support_subset_singleton']

Goal state after:
M : Type u_1
R : Type u_3
inst✝ : CommSemiring R
m : M
a : R[M]
⊢ (∃ b, a.coeff = Finsupp.single m b) ↔ a ∈ (lsingle m).range
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
r : R
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m)) r = ↑(GradedMonoid.mk (f m) ⟨single m r, ⋯⟩).snd

Tactic:
rfl

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

Goal state before:
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:
ext : 1
    rw [← LinearMap.cancel_right ((ℳ _).toBaseChange_surjective S)]
    ext : 3
    simp

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

Goal state before:
pp: ι : 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
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (rTensor N (ℳ i).subtype) x = ↑((decomposeTensorEquiv ℳ N i) x)

Tactic:
rfl

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
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (decomposeTensorEquiv ℳ N i) x = ⟨(rTensor N (ℳ i).subtype) x, ⋯⟩

Tactic:
rfl

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
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ ↑((decomposeTensorEquiv ℳ N i) x) = (rTensor N (ℳ i).subtype) x

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
n : ℕ
⊢ Submodule.span R ((fun a ↦ ⁅z, a⁆) '' {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}) ≤
    Submodule.span R {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}

Tactic:
apply Submodule.span_mono

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V := ⋯
n : ℕ
⊢ (fun a ↦ ⁅z, a⁆) '' {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x} ⊆ {x | ∃ i < n + 1, ((toEnd R L V) z ^ i) v = x}
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case refine_2
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 : (toEnd k L M) x ∈ k ∙ LinearMap.id
y : L
⊢ ⁅y, x⁆ = 0

Tactic:
obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx

Goal state after:
case refine_2
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 : (toEnd k L M) x ∈ k ∙ LinearMap.id
y : L
t : k
ht : t • LinearMap.id = (toEnd k L M) x
⊢ ⁅y, x⁆ = 0
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: 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
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id
x : L
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
hx : (toEnd k L M) x ∈ k ∙ LinearMap.id
⊢ x = 0

Tactic:
obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx

Goal state after:
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
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ k ∙ LinearMap.id
x : L
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
hx : (toEnd k L M) x ∈ k ∙ LinearMap.id
t : k
ht : t • LinearMap.id = (toEnd k L M) x
⊢ x = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), l.formPerm x = x ∨ l'.formPerm x = x

Tactic:
intro h x

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
⊢ l.formPerm x = x ∨ l'.formPerm x = x
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: case mp
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
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : LieAlgebra.ofTwoCocycle c
n : M
h : ↑{ toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } n = x
⊢ ↑{ toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } n ∈
    LieIdeal.toLieSubalgebra R (LieAlgebra.ofTwoCocycle c)
      { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }.ker

Tactic:
rfl

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
E : Extension R M L
x✝ : M
⊢ (LinearEquiv.ofEq (↑E.proj).ker (↑E.incl).range ⋯) ⟨E.incl x✝, ⋯⟩ = ⟨E.incl x✝, ⋯⟩

Tactic:
rfl

Goal state after:
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
E : Extension R M L
x : M
y : E.L
⊢ ⁅y, ↑(E.toKer x)⁆ = ⁅y, E.incl x⁆

Tactic:
rfl

Goal state after:
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
a : A
ha : (F x) a + (F y) a ≠ 0
⊢ a ∈ u

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : f y = y
⊢ s = s

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : ¬f y = y
⊢ ↑(f.toList y) = ↑(f.toList y)

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : f y = y
⊢ ↑(f.toList x) = ↑(f.toList x)

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)

Tactic:
rfl

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)
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
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - -⁅s (-⁅z, y⁆), s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, -⁅z, y⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (⁅s ⁅x, z⁆, s y⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, -⁅z, y⁆⁆ - ⁅y, ⁅x, z⁆⁆))) -
      (⁅s (-⁅z, y⁆), s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, ⁅x, z⁆⁆ - ⁅x, -⁅z, y⁆⁆))) =
    0

Tactic:
← lie_skew (s ⁅x, 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
s : L →ₗ[R] E.L
hs : LeftInverse ⇑E.proj ⇑s
x y z : L
hjac : ⁅s z, ⁅s x, s y⁆⁆ = -(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆)
hja : s ⁅z, ⁅x, y⁆⁆ = -s (⁅x, ⁅y, z⁆⁆ - ⁅y, ⁅x, z⁆⁆)
hj : s ⁅z, ⁅y, x⁆⁆ = -s (⁅y, ⁅x, z⁆⁆ - ⁅x, ⁅y, z⁆⁆)
⊢ ⁅s x, ⁅s y, s z⁆⁆ - -⁅s (-⁅z, y⁆), s x⁆ - (⁅s y, ⁅s x, s z⁆⁆ - ⁅s y, s ⁅x, z⁆⁆) +
            (-(⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆) - ⁅s z, s ⁅x, y⁆⁆) -
          (⁅s ⁅x, y⁆, s z⁆ - (s ⁅x, -⁅z, y⁆⁆ - s ⁅y, ⁅x, z⁆⁆)) +
        (-⁅s y, s ⁅x, z⁆⁆ - (s ⁅x, ⁅z, y⁆⁆ - -s (⁅x, -⁅z, y⁆⁆ - ⁅y, ⁅x, z⁆⁆))) -
      (⁅s (-⁅z, y⁆), s x⁆ - (s ⁅y, ⁅z, x⁆⁆ - -s (⁅y, ⁅x, z⁆⁆ - ⁅x, -⁅z, y⁆⁆))) =
    0
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
⊢ a + b = -c

Tactic:
grind

Goal state after:
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
⊢ a + c = -b

Tactic:
grind

Goal state after:
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 + c = -a

Tactic:
grind

Goal state after:
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
⊢ b = -(a + c)

Tactic:
grind

Goal state after:
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
⊢ -b ≠ a + c

Tactic:
grind

Goal state after:
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
⊢ -c ≠ a + b

Tactic:
grind

Goal state after:
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
⊢ -a ≠ b + c

Tactic:
grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
i j : ℕ
⊢ BirdDet.get n A i j = A.getD (n * i + j) 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
F : ℕ → ℕ → R
i j : ℕ
⊢ stepEntry n A F i j =
    (-BirdDet.sumFrom n (i + 1) fun k ↦ F k k) * BirdDet.get n A i j +
      BirdDet.sumFrom n (i + 1) fun k ↦ F i k * BirdDet.get n A k j

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A : Array R
⊢ birdDet 0 A = 1

Tactic:
rfl

Goal state after: