mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
h_deg_le : f.degree ≤ ↑(#s)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g

Tactic:
by
  rcases eq_or_ne f 0 with rfl | hf
  · rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
  · exact eq_of_degree_sub_lt_of_eval_index_eq s hvs
      (lt_of_lt_of_le (degree_sub_lt_left h_deg_eq hf hlc) h_deg_le)
      h_eval

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
⊢ (b₁.f i, b₂.f (eι i)) ∈
    {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪ {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x}

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i : ι
⊢ Lagrange.basis {i} v i = 1

Tactic:
Lagrange.basis,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i : ι
⊢ ∏ j ∈ {i}.erase i, basisDivisor (v i) (v j) = 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ Lagrange.basis s v i ≠ 0

Tactic:
Lagrange.basis,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (Lagrange.basis s v i) = 1

Tactic:
Lagrange.basis,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (∏ j ∈ s.erase i, basisDivisor (v i) (v j)) = 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ eval (v j) (Lagrange.basis s v i) = 0

Tactic:
Lagrange.basis,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ eval (v j) (∏ j ∈ s.erase i, basisDivisor (v i) (v j)) = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
let u (b : Bool) (i : Fin n) := (algebraMap (MvPolynomial (Fin n × Bool) ℤ)
    (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X ⟨i, b⟩)
  have hdet := det_projVandermonde_of_field (u true) (u false)
  simp only [u] at hdet
  norm_cast at hdet
  rw [projVandermonde_map, ← RingHom.map_det, IsFractionRing.coe_inj] at hdet
  apply_fun MvPolynomial.eval₂Hom (Int.castRingHom R) (fun x ↦ (if x.2 then v else w) x.1) at hdet
  rw [RingHom.map_det] at hdet
  convert! hdet <;>
  simp [← Matrix.ext_iff, projVandermonde_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| f

Tactic:
rw [eq_interpolate hvs hf]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
f : F[X]
hf : f.degree < ↑(#s)
| (interpolate s v) fun i ↦ eval (v i) f
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial

Tactic:
rw [det_vandermonde] at hn

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : ∏ i, ∏ j > i, (↑↑j - ↑↑i) = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
this : s = 0
⊢ _root_.IsNilpotent (φ x)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
x : ↥H₁ × ↥H₂
⊢ (↑x.1, ↑x.2) ∈ prod eι b₁ b₂

Tactic:
by simp [contra]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (insert i (s \ {i, j})) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {i, j})) v) r * basisDivisor (v j) (v i) =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s

Tactic:
sdiff_insert_insert_of_mem_of_notMem hi (notMem_singleton.mpr hij),

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate (s \ {j}) v) r * basisDivisor (v i) (v j) +
      (interpolate (insert j (s \ {i, j})) v) r * basisDivisor (v j) (v i) =
    (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)

F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i j : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ {i, j} ⊆ s
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this✝¹ : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
this✝ : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
this : Nontrivial ↥(s.eigenspace ν)
hν : ν ∈ E
⊢ ∀ (a b : Dual ℚ ↥E), a = b

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsArtinian R L
H : LieSubalgebra R L
x : L
h : engel R x ≤ H
N : LieSubalgebra R L := H.normalizer
n : L
hn : ⁅n, x⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H

Tactic:
rwa [← lie_skew, neg_mem_iff (G := L)]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ ∏ i ∈ s, (X - C (v i)) = (X - C (v i)) * ∏ i ∈ s.erase i, (X - C (v i))

Tactic:
Finset.mul_prod_erase _ (fun x => X - C (v x)) hi

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type u_6} (f : MvPolynomial (α → β) R) (x : MvPolynomial α R),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
by aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ Lagrange.basis s v i = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))

Tactic:
Lagrange.basis,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, basisDivisor (v i) (v j) = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
⊢ ∀ (i j : I), μ i = μ j → fμ i = fμ j

Tactic:
by aesop

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

Goal state before:
pp: ι : 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 𝒜
x : A
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
⊢ 0 ≠ i

Tactic:
by aesop

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

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

Tactic:
by aesop

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
m : Type w₁
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
x y : Matrix n n R
v : n → R
⊢ x *ᵥ y *ᵥ v = ⁅x, y⁆ *ᵥ v + y *ᵥ x *ᵥ v

Tactic:
by simp only [Ring.lie_def, mulVec_mulVec, sub_mulVec, sub_add_cancel]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ∃ x, φ.IsNilRegular x

Tactic:
apply exists_isNilRegular_of_finrank_le_card

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ↑(finrank R M) ≤ Cardinal.mk R
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ∃ x, φ.IsNilRegular x

Tactic:
by
  apply exists_isNilRegular_of_finrank_le_card
  exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

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
x : Fin (Fintype.card l - C.rank) → R
hx : (f Q).toBlocks₂₂ *ᵥ x = 0
⊢ f Q • Sum.elim 0 x = 0

Tactic:
← (f Q).fromBlocks_toBlocks

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
x : Fin (Fintype.card l - C.rank) → R
hx : (f Q).toBlocks₂₂ *ᵥ x = 0
⊢ fromBlocks (f Q).toBlocks₁₁ (f Q).toBlocks₁₂ (f Q).toBlocks₂₁ (f Q).toBlocks₂₂ • Sum.elim 0 x = 0
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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det

Tactic:
set C' := f.mapMatrix C

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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C).det
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 B C D).map ⇑f).det

Tactic:
Matrix.fromBlocks_map

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

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, y⁆) =
    ⁅(↑(f i)).toAddMonoidHom x, (↑(f i)).toAddMonoidHom y⁆
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
⊢ r •
      {
          toFun := fun m ↦
            (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd m)))
              ⟨single (Multiplicative.toAdd m) 1, ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯ }
        (Multiplicative.ofAdd m) =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m r, ⋯⟩

Tactic:
refine (DirectSum.of_smul R _ _ _).symm.trans ?_

Goal state after:
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
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f (Multiplicative.toAdd (Multiplicative.ofAdd m))))
      (r • ⟨single (Multiplicative.toAdd (Multiplicative.ofAdd m)) 1, ⋯⟩) =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m r, ⋯⟩
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: case hadd.hadd.e_a
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) -
      -↑((-(φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆)) j) =
    0

Tactic:
sub_neg_eq_add,

Goal state after:
case hadd.hadd.e_a
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f✝ : ⨁ (i : ι), ↥(ℒ i)
a✝³ : f✝ i = 0
a✝² : a ≠ 0
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ ↑((φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆) j) +
      ↑((-(φ i • ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun x ↦ ↥(ℒ x)) k) b⁆)) j) =
    0
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:
simp_rw [length_toList]

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.cycleOf x).support.card)) x = (p ^ (k + 1)) x