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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ (1 - derivative (C (v i))) * nodal t v + (X - C (v i)) * ∑ i ∈ t, nodal (t.erase i) v =
    ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v

Tactic:
derivative_C,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v
⊢ (1 - 0) * nodal t v + (X - C (v i)) * ∑ i ∈ t, nodal (t.erase i) v =
    ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (algEquivMatrix (chooseBasis R M)) ((aeval f) f.charpoly) = 0

Tactic:
← AlgEquiv.coe_toAlgHom,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(algEquivMatrix (chooseBasis R M)) ((aeval f) f.charpoly) = 0
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly

Tactic:
← charpoly_toMatrix (f₁.prodMap f₂) b,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ ((toMatrix b b) (f₁.prodMap f₂)).charpoly = ((toMatrix b₁ b₁) f₁).charpoly * ((toMatrix b₂ b₂) f₂).charpoly
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
⊢ ∀ {s : HomogeneousSubmodule 𝒜 ℳ} (r : A) {m : M}, m ∈ s → r • m ∈ s

Tactic:
intro x r m hm
    exact Submodule.smul_mem x.toSubmodule r hm

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 𝒜
I : Ideal A
x✝ : A
h : x✝ ∈ Subtype.val '' Subtype.val ⁻¹' ↑I
⊢ IsHomogeneousElem 𝒜 x✝

Tactic:
by
      have := Subtype.image_preimage_coe (Set.ofPred (SetLike.IsHomogeneousElem 𝒜)) (I : Set A)
      exact (cast congr(_ ∈ $this) h).1

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
h : charpoly φ = X ^ finrank R M
m : M
⊢ (φ ^ finrank R M) m = 0

Tactic:
suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
h : charpoly φ = X ^ finrank R M
m : M
⊢ φ ^ finrank R M = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case neg
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
hd : coeff d (((finSuccEquiv R N) F).coeff n) ≠ 0
i : Fin N
hi : i ∉ d.support
⊢ d i = 0

Tactic:
· simpa using hi

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 φ
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Tactic:
← e.symm.charpoly_conj φ,

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 := φ.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 φ
⊢ finrank K ↥V = (charpoly (e.symm.conj φ)).natTrailingDegree
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

Tactic:
apply LieEquiv.ofSubalgebras _ _ e.lieConj
  ext f
  simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
  exact (LinearMap.isPairSelfAdjoint_equiv (B := -B) (F := B) e f).symm

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

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval fun i ↦ (b.repr y) i * (aeval r) X + (b.repr x) i)) ((↑φ).polyCharpoly b) =
    charpoly (φ (r • y) + φ x)

Tactic:
aeval_X,

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval fun i ↦ (b.repr y) i * r + (b.repr x) i)) ((↑φ).polyCharpoly b) =
    charpoly (φ (r • y) + φ x)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
f : oneCochain R L M
x y : L
⊢ (((d₁₂ R L M) f) x) y = -f ⁅x, y⁆

Tactic:
simp [trivial_lie_zero]

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

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

Tactic:
hmy

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
i : ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
⊢ b ≠ 0 →
    (∀ (hx : y ∈ gradeBy R (⇑f) i),
        (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨y, hx⟩) →
      ∀ (hx : single m b + y ∈ gradeBy R (⇑f) i),
        (decomposeAux f) ↑⟨single m b + y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) i) ⟨single m b + y, hx⟩
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' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
i : ℕ
hi : i ≠ 0
⊢ ∃ j < i, Submodule.map (T χ w) (U' i) ≤ U' j

Tactic:
obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hi

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 :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
U : LieSubmodule R A V :=
  let __Submodule := ⨆ k, U' k;
  { toSubmodule := __Submodule, lie_mem := ⋯ }
hzU : ∀ x ∈ U, ((toEnd R L V) z) x ∈ U
trace_za_zero : (LinearMap.trace R ↥U) ((toEnd R A ↥U) ⁅z, a⁆) = 0
w : A
j : ℕ
hi : j.succ ≠ 0
⊢ ∃ j_1 < j.succ, Submodule.map (T χ w) (U' j.succ) ≤ U' j_1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ n + 1 = m + 1

Tactic:
← Nat.mod_eq_of_lt hn,

Goal state after:
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ (n + 1) % orderOf (p.cycleOf x) = m + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ (f.toCycle hf).Nodup

Tactic:
simpa [toCycle_eq_toList f hf x hx] using nodup_toList _ _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j =
    ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j

Tactic:
Finset.sum_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ y ∈ S p i, ∑ x > i, bminor A i x y * A x j =
    ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
⊢ (Matrix.ofArray A hA).det = birdDet n A

Tactic:
birdDet_eq_birdDetSpec,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
⊢ (Matrix.ofArray A hA).det = Spec.birdDet (Matrix.ofArray A ?hA)

case hA
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
⊢ A.size = n * n
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
by
  let imL := (toEnd k L V).range
  let toEndo : L →ₗ[k] imL := LinearMap.codRestrict imL.toSubmodule (toEnd k L V)
      (fun x ↦ LinearMap.mem_range.mpr ⟨x, rfl⟩ : ∀ x : L, (toEnd k L V) x ∈ imL)
  have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL
  use χ.comp toEndo
  obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)
  refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
  · rw [mem_weightSpace] at hv ⊢
    intro x
    apply hv (toEndo x)
  · simpa using hv0

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : n < E.order
⊢ u n = init ⟨n, h'⟩

Tactic:
exact mod_cast heq ⟨n, h'⟩

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

Goal state before:
pp: i : Fin 6
⊢ E₆ i i = 2

Tactic:
fin_cases i

Goal state after:
case «0»
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i : Fin 7
⊢ E₇ i i = 2

Tactic:
fin_cases i

Goal state after:
case «0»
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

case «6»
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i : Fin 8
⊢ E₈ i i = 2

Tactic:
fin_cases i

Goal state after:
case «0»
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

case «6»
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

case «7»
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i : Fin 4
⊢ F₄ i i = 2

Tactic:
fin_cases i

Goal state after:
case «0»
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i : Fin 2
⊢ G₂ i i = 2

Tactic:
fin_cases i

Goal state after:
case «0»
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 6
h : i ≠ j
⊢ E₆ i j ≤ 0

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 6
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 6
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 6
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 6
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 6
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 6
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
⊢ E.charPoly.Monic

Tactic:
nontriviality R
  rw [Monic, leadingCoeff, natDegree_eq_of_degree_eq_some <| charPoly_degree_eq_order _, charPoly,
    coeff_sub, coeff_monomial_same, finsetSum_coeff, sub_eq_self]
  refine sum_eq_zero fun _ _ ↦ coeff_eq_zero_of_degree_lt ?_
  grw [degree_monomial_le]
  simp

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

Goal state before:
pp: i j : Fin 7
h : i ≠ j
⊢ E₇ i j ≤ 0

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 7
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 7
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 7
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 7
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 7
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 7
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

case «6»
j : Fin 7
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 8
h : i ≠ j
⊢ E₈ i j ≤ 0

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 8
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 8
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 8
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 8
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 8
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 8
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

case «6»
j : Fin 8
h : (fun i ↦ i) ⟨6, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) j ≤ 0

case «7»
j : Fin 8
h : (fun i ↦ i) ⟨7, ⋯⟩ ≠ j
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) j ≤ 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)

Tactic:
rw [one_smul]

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S 0

Tactic:
convert! ((0 : Ideal R) : FractionalIdeal S P).isFractional

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
x✝ : IsFractional S I
⊢ 0 = ↑↑0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 4
h : i ≠ j
⊢ F₄ i j ≤ 0

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 4
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 4
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 4
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 4
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 2
h : i ≠ j
⊢ G₂ i j ≤ 0

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁷ : Field K
R₁ : Type u_4
inst✝⁶ : CommRing R₁
inst✝⁵ : IsDomain R₁
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) I⁻¹ = (map (↑h) I)⁻¹

Tactic:
inv_eq,

Goal state after:
K : Type u_3
inst✝⁷ : Field K
R₁ : Type u_4
inst✝⁶ : CommRing R₁
inst✝⁵ : IsDomain R₁
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (1 / I) = (map (↑h) I)⁻¹