mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
⊢ ⊥.IsMaximal

Tactic:
have hp0 : a ≠ 0 := fun hp0' =>
    hm' <| map_injective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))
      ((injective_iff_map_eq_zero (Ideal.Quotient.mk (P.comap (C : R →+* R[X]) : Ideal R))).2
        fun x hx => by
          rwa [Quotient.eq_zero_iff_mem, (by rwa [eq_bot_iff] : (P.comap C : Ideal R) = ⊥)] at hx)
        (by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0')

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
⊢ ⊥.IsMaximal
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : Nontrivial R
inst✝¹ : P.IsCrystallographic
inst✝ : Algebra ℚ R
i j : ι
⊢ P.pairingIn ℚ i j = ↑(P.pairingIn ℤ i j)

Tactic:
by
  simp [← P.algebraMap_pairingIn' ℚ ℤ]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ⨅ i, LinearMap.ker (P.root' i) = (span R (range P.root')).dualCoannihilator

Tactic:
rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_root']

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.rootSpan S)

Tactic:
by
  rw [← finrank_range_polarization_eq_finrank_span_coroot]
  exact LinearMap.finrank_range_le (P.PolarizationIn S)

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

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
P : RootPairing ι R M N
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i = P.root j ∨ P.root i = -P.root j

Tactic:
· rcases eq_or_ne i j with rfl | h'
    · tauto
    · exact Or.inr (h i j h' hLin)

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

Goal state before:
pp: case refine_1
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ (range fun n ↦ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j)) ⊆ range ⇑P.root

Tactic:
rw [range_subset_iff]

Goal state after:
case refine_1
ι : 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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ ∀ (y : ℕ), (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[y] (P.root j) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_1
ι : 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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝¹ : IsAddTorsionFree M
this✝ : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : 4 • P.root i = 2 • P.root j
⊢ P.root j = 2 • P.root i

Tactic:
show (4 : R) = 2 * 2 by norm_num,

Goal state after:
case refine_1
ι : 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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝¹ : IsAddTorsionFree M
this✝ : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
this : (2 * 2) • P.root i = 2 • P.root j
⊢ P.root j = 2 • P.root i
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective (⇑↑e.symm ∘ ⇑(dualProd R M)) ↔ Function.Injective ⇑(Module.Dual.eval R M)

Tactic:
← coe_comp

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) := ↑e.symm ∘ₗ dualProd R M
⊢ Function.Injective ⇑(↑e.symm ∘ₗ dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := fun g hg ↦ pred g ⋯
⊢ x ∈ Submonoid.closure (range (Equiv.reflection P))

Tactic:
rwa [← weylGroup_toSubmonoid]

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

Goal state before:
pp: case mul
ι : 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.InvariantForm
g g₁ g₂ : P.Aut
hg₁ : g₁ ∈ P.weylGroup
hg₂ : g₂ ∈ P.weylGroup
hg₁' : ∀ (x y : M), (B.form (⟨g₁, hg₁⟩ • x)) (⟨g₁, hg₁⟩ • y) = (B.form x) y
hg₂' : ∀ (x y : M), (B.form (⟨g₂, hg₂⟩ • x)) (⟨g₂, hg₂⟩ • y) = (B.form x) y
⊢ ∀ (x y : M), (B.form (⟨g₁ * g₂, ⋯⟩ • x)) (⟨g₁ * g₂, ⋯⟩ • y) = (B.form x) y

Tactic:
intro x y
    rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : k[G]
x : V
y : W
⊢ (r •
      have this := x ⊗ₜ[k] y;
      this) =
    (r •
        have this := x;
        this) ⊗ₜ[k]
      y

Tactic:
by
  change asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _
  simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
    LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, Module.End.one_apply]
  simp only [Finsupp.sum, TensorProduct.sum_tmul]
  rfl

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

Goal state before:
pp: case refine_1.one
ι : 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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
g : P.Aut
⊢ q ∈ invtSubmodule (P.weylGroupRootRep ⟨1, ⋯⟩)

Tactic:
simp [← Submonoid.one_def]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

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

Tactic:
by
  simp [← h₀.ordConnected_iff_of_bdd (OrderBot.bddBelow I) h₂, ordConnected_iff_disjoint_Ioo_empty]

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

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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
i : ι
hi : i ∉ {i | ¬Disjoint q (R ∙ P.root i)}
⊢ q ≤ ker (P.coroot' i)

Tactic:
simp only [mem_ofPred_eq, not_not] at hi

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✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
q : Submodule R M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
i : ι
hi : Disjoint q (R ∙ P.root i)
⊢ q ≤ ker (P.coroot' i)
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this✝ : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ z ∈ Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j)
⊢ chainTopCoeff i j ≤ chainBotCoeff ((P.reflectionPerm i) i) j

Tactic:
· simpa using this (-P.chainTopCoeff i j)

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this✝ : InvolutiveNeg ι := P.indexNeg
this :
  ∀ (z : ℤ),
    z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ z ∈ Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))
⊢ chainTopCoeff i j ≤ chainBotCoeff i ((P.reflectionPerm j) j)

Tactic:
· simpa using this (-P.chainTopCoeff i j)

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

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

Tactic:
refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_
    rw [CauSeq.inf_idem]

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: b : ℕ
hb : ∀ {a : ℝ}, 0 < a → a * ↑b + 1 ≤ (a + 1) ^ b
a : ℝ
ha' : 0 < a
⊢ a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * ↑b + 1)

Tactic:
simp [mul_add, add_assoc, add_left_comm]

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

Goal state before:
pp: case neg
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
· rw [zero_zpow _ h]

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✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n →₀ R
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * diagonal d i j * xj

Tactic:
by
    -- TODO: positivity
    refine Finsupp.sum_nonneg fun i _ ↦ Finsupp.sum_nonneg fun j _ ↦ ?_
    simp +contextual [diagonal, apply_ite, star_left_conjugate_nonneg (h _)]

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

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁷ : Fintype n
R : Type u_5
M : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : TrivialStar R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq n
b : Module.Basis n R M
B : LinearMap.BilinForm R M
hB_symm : B.IsSymm
aux : ∀ (i j : n) (s t : R), t * (B (b i)) (b j) * s = t * (s * (B (b j)) (b i))
h : ((LinearMap.BilinForm.toMatrix b) B).PosDef
v : M
hv : v ≠ 0
⊢ 0 < (LinearMap.BilinMap.toQuadraticMap B) v

Tactic:
· rw [B.toQuadraticMap_apply, ← b.linearCombination_repr (x := v)]
    simpa [Finsupp.linearCombination_apply, map_finsuppSum, Finsupp.mul_sum, aux]
      using h.2 (b.repr.map_ne_zero_iff.mpr hv)

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

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
k : ↥b.support
hk : P.root ↑k ∈ q
⊢ p k

Tactic:
contrapose hk

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
k : ↥b.support
hk : ¬p k
⊢ P.root ↑k ∉ q
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
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
⊢ False

Tactic:
have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : (minpoly R f).degree ≤ q.degree
⊢ False
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
induction m with
  | zero => simp
  | succ m ih =>
    rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

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

Goal state before:
pp: case e_g
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (⇑(map g) ∘ X) x✝ = X x✝

Tactic:
simp only [Function.comp_apply, map_X]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp C = f

Tactic:
ext1 r
  exact eval₂_C f g r

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
M : n × n → S
⊢ Polynomial.map (eval₂Hom f M) (univ R n) = (of (Function.curry M)).charpoly

Tactic:
univ,

Goal state after:
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
M : n × n → S
⊢ Polynomial.map (eval₂Hom f M) (mvPolynomialX n n R).charpoly = (of (Function.curry M)).charpoly
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)
hφ : φ.IsHomogeneous n
⊢ (F (p.coeff i)).IsHomogeneous j

Tactic:
convert! hφ.finSuccEquiv_coeff_isHomogeneous i j h using 1

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hσ : Finite σ
p : Polynomial (MvPolynomial σ R)
hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n
i j : ℕ
h : i + j = n
k : ℕ
e : σ ≃ Fin k
e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm
F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e
F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'
φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)
hφ : φ.IsHomogeneous n
⊢ F (p.coeff i) = ((finSuccEquiv R k) φ).coeff i
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case pos
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
this : ∑ x ∈ d.support, d x = 0
⊢ d i = 0

Tactic:
rw [Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ zero_le)] at this

Goal state after:
case pos
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
this : ∀ i ∈ d.support, d i = 0
⊢ d i = 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
ιM : Type u_7
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✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x : L
i : ℕ
⊢ (eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i

Tactic:
by
  nontriviality R
  rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]

Goal state after:
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 : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ Aᵀ ∈ symplecticGroup l R

Tactic:
rw [mem_iff] at hA ⊢

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R
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 : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
mem_iff'

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case mpr
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
⊢ Aᵀ *ᵥ 0 = 0

Tactic:
mulVec_zero

Goal state after:
case mpr
m : Type um
n : Type un
R : Type uR
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
A : Matrix m n R
x : n → R
h : A *ᵥ x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Lie.Free

Goal state before:
pp: case add_right
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
a b a✝¹ b✝ c' : lib R X
a✝ : Rel R X a✝¹ b✝
h₂ : (liftAux R f) a✝¹ = (liftAux R f) b✝
⊢ (liftAux R f) (a✝¹ + c') = (liftAux R f) (b✝ + c')

Tactic:
simp only [liftAux_map_add, h₂]

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F : FreeLieAlgebra R X →ₗ⁅R⁆ L
⊢ (lift R) ((lift R).symm F) = F

Tactic:
exact (lift R).apply_symm_apply F

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (rTensor N (ℳ i).subtype) x ∈ decomposeTensor ℳ N i

Tactic:
convert (decomposeTensorEquiv ℳ N i x).property

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i) ⊗[R] N
⊢ (rTensor N (ℳ i).subtype) x = ↑((decomposeTensorEquiv ℳ N i) x)
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ (projr ψ).range = ⊤

Tactic:
simp [LieHom.range_eq_top]

Goal state after: