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, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
have _ : Invertible U := hU.invertible

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

Goal state before:
pp: m : Type um
R : Type u_1
inst✝³ : CommRing R
inst✝² : Nontrivial R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
hA : A.det ∈ nonZeroDivisors R
⊢ A.rank = Fintype.card m

Tactic:
by
  rw [rank, LinearMap.finrank_range_of_inj (mulVec_injective_of_det_mem_nonZeroDivisors hA),
    Module.finrank_eq_card_basis (Pi.basisFun R m)]

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

Goal state before:
pp: m : Type um
n : Type un
inst✝³ : Fintype n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ (A * B).rank = B.rank

Tactic:
rw [rank, rank, mulVecLin_mul, LinearMap.range_comp,
    ← (Submodule.equivMapOfInjective A.mulVecLin
      (mulVec_injective_of_det_mem_nonZeroDivisors hA) _).finrank_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_1
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
⊢ X.IsSymm

Tactic:
[

Goal state after:
case refine_1
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
⊢ X.IsSymm
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ ∀ (a : m), diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a

Tactic:
[

Goal state after:
m : Type um
R : Type uR
inst✝¹ : Field R
inst✝ : DecidableEq m
w : m → R
w' : { i // w i ≠ 0 } → m → R := fun i ↦ diagonal w ↑i
h : LinearIndependent R w'
⊢ ∀ (a : m), diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a
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
hz : z ∈ engel K ↑v
⊢ z ∈ engel K x

Tactic:
change z ∈ E

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 ∈ E
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 (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹

Tactic:
[

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
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 (A + X.submatrix ⇑s ⇑s * C) = f Vᵀ * (f Q + Y * f P) * f U⁻¹
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)⁆

pp: case 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 x✝¹ x✝ : A ⊗[R] L
h1 : (LinearMap.rTensor L ↑d) ⁅x✝¹, y⁆ = ⁅x✝¹, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝¹⁆
h2 : (LinearMap.rTensor L ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ + x✝, y⁆ =
    ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆

Tactic:
· refine y.induction_on (by simp) (fun _ l' ↦ ?_) (fun _ _ h1 h2 ↦ ?_)
          · simp [← lie_skew l' l, -lie_skew, add_tmul, tmul_neg]
          · simp [h1, h2, sub_add_sub_comm]

Goal state after:
case 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 x✝¹ x✝ : A ⊗[R] L
h1 : (LinearMap.rTensor L ↑d) ⁅x✝¹, y⁆ = ⁅x✝¹, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝¹⁆
h2 : (LinearMap.rTensor L ↑d) ⁅x✝, y⁆ = ⁅x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) x✝⁆
⊢ (LinearMap.rTensor L ↑d) ⁅x✝¹ + x✝, y⁆ =
    ⁅x✝¹ + x✝, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) (x✝¹ + x✝)⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inl
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)
i : ι
y x : L i
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L i) x, (of L i) y⁆ =
    ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆

Tactic:
[

Goal state after:
case inl
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)
i : ι
y x : L i
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L i) x, (of L i) y⁆ =
    ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
Module: Mathlib.Algebra.Lie.DirectSum

Goal state before:
pp: case inr
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)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L j) x, (of L i) y⁆ =
    ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆

Tactic:
[

Goal state after:
case inr
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)
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ (toAddMonoid fun i ↦ (↑(f i)).toAddMonoidHom) ⁅(of L j) x, (of L i) y⁆ =
    ⁅(↑(f j)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
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)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((a + b) * c) = Quot.mk (Rel R X) (a * c + b * c)

Tactic:
[

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
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)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((a + b) * c) = Quot.mk (Rel R X) (a * c + b * c)
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
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)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) (a * (b + c)) = Quot.mk (Rel R X) (a * b + a * c)

Tactic:
[

Goal state after:
case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
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)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) (a * (b + c)) = Quot.mk (Rel R X) (a * b + a * c)
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

Tactic:
[

Goal state after:
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
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
s✝ : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ s.formPerm = 1

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
s✝ : Cycle α
s : List α
h : s.length ≤ 1
⊢ s.formPerm = 1
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)
⊢ ⁅Exists.choose h x + Exists.choose h y - Exists.choose h (x + y), E.toKer m⁆ = 0

Tactic:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)

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
inst✝ : IsLieAbelian M
E : Extension R M L
this : LieRingModule L M := E.ringModuleOf
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
r : R
x : L
m : M
⊢ ⁅Exists.choose ⋯ (r • x) - r • Exists.choose ⋯ x, E.toKer m⁆ = 0

Tactic:
exact trivial_lie_zero E.proj.ker _ ⟨_, by simp [h.choose_spec _]⟩ (E.toKer m)

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.toList x)[k] = y
⊢ (p.toList x).next y hy✝ = p y

Tactic:
[

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.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.toList x)[k] = y
⊢ (p ^ ((k + 1) % (p.toList x).length)) x = (p ^ (k + 1)) x

Tactic:
[

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 ^ ((k + 1) % (p.toList x).length)) x = (p ^ (k + 1)) x
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
⊢ ⁅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

Tactic:
have hjac := lie_lie (s x) (s y) (s 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 x, s y⁆, s z⁆ = ⁅s x, ⁅s y, s z⁆⁆ - ⁅s y, ⁅s x, s z⁆⁆
⊢ ⁅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
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case inl
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
h : -x ∈ (F f).support
⊢ x ∈ (F f).support ∨ x ∈ Finset.image (⇑(Equiv.neg A)) (F f).support

Tactic:
exact Or.inr <| Finset.mem_image.mpr ⟨-x, by simp [h]⟩

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

Goal state before:
pp: case stop
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : ¬lo < n
⊢ 0 = ∑ k ∈ ∅, f k

Tactic:
Finset.sum_empty

Goal state after:
case stop
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : ¬lo < n
⊢ 0 = 0