mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk f = 1
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (f.inv ⋯) = mk (g.inv ⋯)

Tactic:
rw [mk_eq.2 fg, ← Ig] at If

Goal state after:
case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (f.inv ⋯) = mk (g.inv ⋯)
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
i : ι
⊢ 0 < A i i

Tactic:
rw [← mul_pos_iff_of_pos_left (hD i)]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
i : ι
⊢ 0 < d i * A i i
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
⊢ False

Tactic:
obtain ⟨v, hv, hv₀⟩ : ∃ v, N *ᵥ v = (μ - ρ) • v ∧ v ≠ 0 := by
    replace hρ : HasEigenvalue (toLin' N) (μ - ρ) := by simpa [N_def, hasEigenvalue_sub'_iff]
    simpa [hasEigenvector_iff, mulVec_transpose] using hρ.exists_hasEigenvector

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
⊢ False
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

Goal state before:
pp: n : ℕ
⊢ (sf n) * ((n + 1) * n !) = sf n + 1

Tactic:
superFactorial,

Goal state after:
n : ℕ
⊢ (sf n) * ((n + 1) * n !) = n.succ ! * sf n
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))

Tactic:
simp_rw [add_succ, Nat.add_one_sub_one]

Goal state after:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝²² : CommRing R
inst✝²¹ : AddCommGroup M
inst✝²⁰ : Module R M
inst✝¹⁹ : AddCommGroup N
inst✝¹⁸ : Module R N
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
inst✝¹³ : CharZero R
inst✝¹² : IsDomain R
inst✝¹¹ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R M₂
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : Module R N₂
P : RootPairing ι R M N
inst✝⁶ : P.IsRootSystem
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝³ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
m : M
h : m ∈ range ⇑P.root
⊢ f m ∈ range ⇑P₂.root

Tactic:
· exact apply_mem_range_root_of_cartanMatrixEq b b₂ e f (by simp [f, Module.Basis.equiv]) m h he

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
wlog h0 : w 0 ≠ 0 generalizing v w with aux

Goal state after:
case succ.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
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
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬basisDivisor (v i) (v j) = 0

Tactic:
rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]

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 : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬i = j
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ eval (v i) (Lagrange.basis s v j) = 0

Tactic:
eval_basis_of_ne hij hi

Goal state after:
case refine_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right✝ : j ∈ s
⊢ 0 = 0
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
s : Finset ι
v : ι → F
c : F
f : ι → F
⊢ ∑ i ∈ s, C ((c • f) i) * Lagrange.basis s v i = (RingHom.id F) c • ∑ i ∈ s, C (f i) * Lagrange.basis s v i

Tactic:
Finset.smul_sum,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s✝ t : Finset ι
i j : ι
v✝ r r' : ι → F
s : Finset ι
v : ι → F
c : F
f : ι → F
⊢ ∑ i ∈ s, C ((c • f) i) * Lagrange.basis s v i = ∑ x ∈ s, (RingHom.id F) c • (C (f x) * Lagrange.basis s v x)
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: case inl
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij ∈ Finset.antidiagonal (m + n)
h : m ≤ ij.1
⊢ (m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0

Tactic:
simp [Module.End.pow_map_zero_of_le h, hm, hn]

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

Goal state before:
pp: case inr
R : Type u_1
L : Type u_2
M : Type u_3
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
x y z : L
m : ℕ
hm : ((ad R L) x ^ m) y = 0
n : ℕ
hn : ((ad R L) x ^ n) z = 0
ij : ℕ × ℕ
hij : ij ∈ Finset.antidiagonal (m + n)
h : n ≤ ij.2
⊢ (m + n).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, ((ad R L) x ^ ij.2) z⁆ = 0

Tactic:
simp [Module.End.pow_map_zero_of_le h, hm, hn]

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
⊢ nodal s v = (X - C (v i)) * nodal (s.erase i) v

Tactic:
simp_rw [nodal, Finset.mul_prod_erase _ (fun x => X - C (v x)) hi]

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 r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v) r) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Tactic:
rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
    eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : IsEmpty σ
w : σ → M
f : MvPolynomial σ R
⊢ IsWeightedHomogeneous w f 0

Tactic:
rw [eq_C_of_isEmpty f]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : IsEmpty σ
w : σ → M
f : MvPolynomial σ R
⊢ IsWeightedHomogeneous w (C (coeff 0 f)) 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)

Tactic:
exact h j (Finset.mem_insert_of_mem hjs)

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✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ↑(((decompose 𝒜) (s.sum fun i a ↦ a • ↑i)) i) ∈ span s✝

Tactic:
Finsupp.sum,

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
⊢ ↑(((decompose 𝒜) (∑ a ∈ s.support, s a • ↑a)) i) ∈ span s✝
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
f : MvPolynomial σ R
⊢ f.IsHomogeneous 0

Tactic:
rw [eq_C_of_isEmpty f]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
f : MvPolynomial σ R
⊢ (C (coeff 0 f)).IsHomogeneous 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ (n * i.sum fun i c ↦ c * 1 i) = n * ∑ i_1 ∈ i.support, i i_1

Tactic:
Finsupp.sum,

Goal state after:
case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ n * ∑ x ∈ i.support, i x * 1 x = n * ∑ i_1 ∈ i.support, i i_1
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (d.sum fun x e ↦ e) ≤ n

Tactic:
Finsupp.sum,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x ∈ d.support, d x ≤ n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x ∈ d.support, d x ≤ d.sum fun i c ↦ c

Tactic:
Finsupp.sum,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x ∈ d.support, d x ≤ ∑ x ∈ d.support, d x
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (m.sum fun i c ↦ c • w i) = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
Finsupp.sum,

Goal state after:
M : Type u_2
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ ∑ a ∈ m.support, m a • w a = 0 ↔ ∀ (x : σ), m x = 0
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
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
hF₀ : ∀ (i : ℕ), ((finSuccEquiv R N) F).coeff i = 0
⊢ ∀ (n : ℕ), ((finSuccEquiv R N) F).coeff n = ((finSuccEquiv R N) 0).coeff n

Tactic:
simpa using! hF₀

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
⊢ G.charpoly.natTrailingDegree = 0

Tactic:
apply Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := ⋯
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⋯
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := ⋯
G : ↥W →ₗ[K] ↥W := ⋯
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := ⋯
e : (↥V × ↥W) ≃ₗ[K] M := ⋯
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := ⋯
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := ⋯
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := ⋯
hψ : ψ = e.symm.conj φ
⊢ constantCoeff G.charpoly ≠ 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ φ.polyCharpoly b ≠ 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case mpr
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
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree ≠ 0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Goal state after:
case mpr
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
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ charpoly (φ x) ≠ 0
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((LieEquiv.ofEq (skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i))
          (so (p ⊕ q) R) ⋯)
        ((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)) A)) =
    (Pso p q R i)⁻¹ * ↑A * Pso p q R i

Tactic:
LieEquiv.ofEq_apply

Goal state after:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)) A) =
    (Pso p q R i)⁻¹ * ↑A * Pso p q R i
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1

Tactic:
rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]

Goal state after:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * 1 + 0 * 0) (1 * 0 + 0 * ⅟(PD l R)) (0 * 1 + PD l R * 0) (0 * 0 + 1) = 1
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ᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : f Q • x = 0
heq2 : f P • x = 0
⊢ x = 0

Tactic:
refine (f_unit hU).smul_left_cancel.1 ?_

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ᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : f Q • x = 0
heq2 : f P • x = 0
⊢ f U • x = f U • 0
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✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
key : B * A * A.adjugate = A.det • B
⊢ (A.det • B).rank = (B * A * A.adjugate).rank

Tactic:
rw [key]

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range ((A.submatrix r id)ᵀ.submatrix c id).row)) ≤
    finrank R ↥(span R (range (A.submatrix r id).col))

Tactic:
← Matrix.transpose_submatrix,

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range ((A.submatrix r id).submatrix id c)ᵀ.row)) ≤
    finrank R ↥(span R (range (A.submatrix r id).col))
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
hn✝ : 2 ≤ l.length
x : { x // x ∈ l }
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup

Tactic:
by rwa [← nodup_attach] at hl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Subsingleton
⊢ s.formPerm ⋯ = 1

Tactic:
obtain ⟨s⟩ := s

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
s✝ : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) ⋯ = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).support = s.toFinset

Tactic:
obtain ⟨s⟩ := s

Goal state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s✝ : Cycle α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) h).support = toFinset (Quot.mk (⇑(IsRotated.setoid α)) s)