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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : ∀ (q : Submodule K M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : Submodule K N
stab : ∀ (i : ι), q ∈ invtSubmodule ↑(P.coreflection i)
ne_bot : q ≠ ⊥
⊢ q = ⊤

Tactic:
specialize h (q.dualAnnihilator.map P.toPerfPair.symm)
      fun i ↦ invtSubmodule_reflection_of_invtSubmodule_coreflection P i q (stab i)

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
q : Submodule K N
h : Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator ≠ ⊥ → Submodule.map (↑P.toPerfPair.symm) q.dualAnnihilator = ⊤
stab : ∀ (i : ι), q ∈ invtSubmodule ↑(P.coreflection i)
ne_bot : q ≠ ⊥
⊢ q = ⊤
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: I : Set ℤ
h₀ : I.Nonempty
h₁ : BddBelow I
h₂ : BddAbove I
⊢ I = Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ x + 1

Tactic:
simp [← h₀.ordConnected_iff_of_bdd h₁ h₂, ordConnected_iff_disjoint_Ioo_empty]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
⊢ q = ⊤

Tactic:
obtain ⟨Φ, b, c⟩ := P.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule q h₁

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
⊢ { val := ↑(f * g), inv := ↑(symm P P (f * g)), val_inv := ⋯, inv_val := ⋯ } =
    { val := ↑f, inv := ↑(symm P P f), val_inv := ⋯, inv_val := ⋯ } *
      { val := ↑g, inv := ↑(symm P P g), val_inv := ⋯, inv_val := ⋯ }

Tactic:
simp only [Equiv.mul_eq_comp, Equiv.toHom_comp]
    ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: ι : 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
P : RootPairing ι R M N
inst✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
sj : S
hsj : sj > 0
hsj' : (algebraMap S R) sj = ((P.posRootForm S).form (P.root j)) (P.root j)
hsi' : si = li
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
replace hsj' : sj = lj := algebraMap_injective S R <| by simpa [lj] using hsj'

Goal state after:
ι : 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
P : RootPairing ι R M N
inst✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inl
ι : 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
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 2
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rw [P.pairingIn_two_two_iff] at hij
      contradiction

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
ε : α
ε0 : ε > 0
j : ℕ
x✝ : j ≥ 0
⊢ abv ((fun x_1 ↦ x) j - (fun x_1 ↦ x) 0) < ε

Tactic:
simpa [abv_zero] using ε0

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε / G * G
⊢ abv (↑(f * g) j) < ε

Tactic:
div_mul_cancel₀ _ (ne_of_gt G0),

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε
⊢ abv (↑(f * g) j) < ε
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : 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
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
⊢ (∃ n f,
      range f ⊆ ↑b.support ∧ P.root j = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root) →
    k ∈ b.support →
      ∃ n f,
        range f ⊆ ↑b.support ∧ P.root l = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
⟨n, f, h₂, h₃, h₄⟩

Goal state after:
ι : 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
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
⊢ k ∈ b.support →
    ∃ n f, range f ⊆ ↑b.support ∧ P.root l = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j

Tactic:
abs_of_nonneg

Goal state after:
case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ ↑f j
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ K ≤ ↑f j

case inr.refine_1
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h✝ : ¬f.LimZero
K : α
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ |↑f j|
i : ℕ
hi : ∀ j ≥ i, K ≤ |↑f j| ∧ ∀ k ≥ j, |↑f k - ↑f j| < K
h : 0 ≤ ↑f i
j : ℕ
ij : j ≥ i
this : K ≤ |↑f j|
h₁ : K ≤ |↑f i|
h₂ : ∀ k ≥ i, |↑f k - ↑f i| < K
⊢ 0 ≤ ↑f j
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
this : mk f = 0 ↔ (f - 0).LimZero
⊢ mk f = 0 ↔ f.LimZero

Tactic:
sub_zero

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
this : mk f = 0 ↔ f.LimZero
⊢ mk f = 0 ↔ f.LimZero
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ a ≤ b ⊓ c

Tactic:
refine le_of_eq_of_le hb (Or.inr ?_)

Goal state after:
case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : a ≈ b
hc : b ≤ c
⊢ b ≈ b ⊓ c
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero R
i : m
j : n
r : R
⊢ (single i j r).vec = Pi.single (j, i) r

Tactic:
rw [single_eq_of_single_single, vec_of, Function.uncurry_flip, Pi.uncurry_single_single]
  exact Pi.single_comp_equiv (Equiv.prodComm _ _) _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f).IsHermitian ↔ A.IsHermitian

Tactic:
by
  rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
⊢ x ∈ eigenspace ((toLin b b) (diagonal d)) μ

Tactic:
obtain ⟨k, hk⟩ := (mem_maxGenEigenspace _ _ _).mp hx

Goal state after:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
⊢ x ∈ eigenspace ((toLin b b) (diagonal d)) μ
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ ↑n).PosSemidef

Tactic:
simpa using hM.pow n

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M.PosDef ↔ M.IsHermitian ∧ ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
have (x : n →₀ R) : x = 0 ↔ Finsupp.equivFunOnFinite x = 0 :=
    ⟨fun h1 ↦ Finsupp.coe_eq_zero.mpr h1,fun h2 ↦ Finsupp.coe_eq_zero.mp h2⟩

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : Fintype n
M : Matrix n n R
this : ∀ (x : n →₀ R), x = 0 ↔ Finsupp.equivFunOnFinite x = 0
⊢ M.PosDef ↔ M.IsHermitian ∧ ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M *ᵥ x
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
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
h₀ : 0 ≤ ρ - μ
h₁ : μ ≤ ρ - μ
h₂ : 0 ≤ d i
h₃ : (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i
⊢ (N *ᵥ |v|) i * (diagonal d *ᵥ |v|) i = (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i

Tactic:
by simp [mulVec_eq_sum, vecMul_eq_sum, mul_comm]

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ((aeval f) p) x = eval μ p • x

Tactic:
by
  refine p.induction_on ?_ ?_ ?_
  · intro a; simp [Module.algebraMap_end_apply]
  · intro p q hp hq; simp [hp, hq, add_smul]
  · intro n a hna
    rw [mul_comm, pow_succ', mul_assoc, map_mul, Module.End.mul_apply, mul_comm, hna]
    simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X,
      map_smulₛₗ, RingHom.id_apply, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
n : ℕ
hn : (ascPochhammer S n).Monic
this : (X + 1).leadingCoeff = 1
⊢ (ascPochhammer S (n + 1)).Monic

Tactic:
rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * (ascPochhammer S (m + 1)).comp (X + ↑n) = ascPochhammer S (n + (m + 1))

Tactic:
| succ m ih =>

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Finite ι
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Module K M
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
p : Submodule K (ι → K) := span K (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
f : ι ⊕ ↑{(i, j) | i ≠ j} → Module.Dual K (ι → K) :=
  LinearMap.proj ⊕ᵥ fun x ↦ LinearMap.proj (↑x).1 - LinearMap.proj (↑x).2
d : ι → K
hp : d ∈ p
hf : ∀ (i : ι ⊕ ↑{(i, j) | i ≠ j}), (f i) d ≠ 0
i j : ι
h : i ≠ j
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on d) i j

Tactic:
simpa [f, sub_eq_zero] using hf (Sum.inr ⟨⟨i, j⟩, h⟩)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R n * (descPochhammer R (m + 1)).comp (X - ↑n) = descPochhammer R (n + (m + 1))

Tactic:
| succ m ih =>

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
⊢ vandermonde (Fin.cons v0 v) = Fin.cons (fun j ↦ v0 ^ ↑j) fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j

Tactic:
by
  ext i j
  refine Fin.cases (by simp) (fun i => ?_) i
  refine Fin.cases (by simp) (fun j => ?_) j
  simp [pow_succ']

Goal state after:
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:
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.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:
by
  simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_iff]
  exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)

Tactic:
interpolate_empty,

Goal state after:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ degree 0 < ↑(#∅)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ of (fun i j ↦ eval (v i) (p j)) i j = (vandermonde v * of fun i j ↦ (p j).coeff ↑i) i j

Tactic:
simp_rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂_eq_sum]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a ↦ (RingHom.id R) a * v i ^ e) = ∑ j_1, vandermonde v i j_1 * (p j).coeff ↑j_1
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 ∈ N
⊢ ⁅x, n⁆ ∈ H

Tactic:
rw [mem_normalizer_iff] at hn

Goal state after:
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 : ∀ y ∈ H, ⁅n, y⁆ ∈ H
⊢ ⁅x, n⁆ ∈ H
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ (aeval (id ∘ f)) p = (aeval f) p

Tactic:
Function.id_comp

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ (aeval f) p = (aeval f) p
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ (nodal s v).degree = ↑(#s)

Tactic:
simp_rw [degree_eq_natDegree nodal_ne_zero, natDegree_nodal]

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
⊢ (P * A * Q).charpoly = A.charpoly

Tactic:
let φ₂ := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ (P * A * Q).charpoly = A.charpoly
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
a✝ : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
A : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ (φ₁ P * φ₂ A * φ₃ Q).charpoly = A.charpoly

Tactic:
rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ Polynomial.map (MvPolynomial.map f) (univ R n) = univ S n

Tactic:
by
  rw [MvPolynomial.map_eq_eval₂Hom_C_comp, univ_map_eval₂Hom]; rfl

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✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ (⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal

Tactic:
simp_rw [toIdeal_iSup]

Goal state after: