mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ∀ (i j : ↥LieSubalgebra.root),
    ¬LinearIndependent K ![(rootSystem H).root i, (rootSystem H).root j] →
      (rootSystem H).root i = (rootSystem H).root j ∨ (rootSystem H).root i = -(rootSystem H).root j

Tactic:
intro ⟨α, hα⟩ ⟨β, hβ⟩ e

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α✝ β✝ α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
β : Weight K (↥H) L
hβ : β ∈ LieSubalgebra.root
e : ¬LinearIndependent K ![(rootSystem H).root ⟨α, hα⟩, (rootSystem H).root ⟨β, hβ⟩]
⊢ (rootSystem H).root ⟨α, hα⟩ = (rootSystem H).root ⟨β, hβ⟩ ∨ (rootSystem H).root ⟨α, hα⟩ = -(rootSystem H).root ⟨β, hβ⟩
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 : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
⊢ ∀ (k : ι), (P.coroot' k) t = 0

Tactic:
intro k

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 : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
htQ : t ∈ Q
k : ι
⊢ (P.coroot' k) t = 0
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✝ : P.IsIrreducible
B : P.InvariantForm
i j : ι
contra : ∀ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) → (B.form (P.root i)) (P.root k) = 0
this : span R (orbit (↥P.weylGroup) (P.root j)) ≤ (B.form (P.root i)).ker
⊢ B.form (P.root i) = 0

Tactic:
simpa [span_orbit_eq_top] using this

Goal state after:
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
P : RootPairing ι R M N
⊢ Injective ⇑(coweightHom P)

Tactic:
refine Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_
  have h : (MulOpposite.unop (coweightHom P g)).toLinearMap =
      (MulOpposite.unop (coweightHom P g')).toLinearMap := by
    simp_all
  rw [coweightHom_toLinearMap, coweightHom_toLinearMap] at h
  suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')
  apply Hom.coweightHom_injective P
  exact MulOpposite.unop_inj.mp h

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✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j * P.pairingIn ℤ j i = 0

Tactic:
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
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : P.pairingIn ℤ i j = 0
⊢ 0 * P.pairingIn ℤ j i = 0
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
i : ι
f : ι → ℤ
heq : P.root i = ∑ j ∈ b.support, f j • P.root j
j : ι
hj : j ∈ b.support
h : P.root i = ∑ j ∈ b.support, ⋯.choose j • P.root j
⊢ ⋯.choose j = f j

Tactic:
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
i : ι
f : ι → ℤ
heq : ∑ j ∈ b.support, ⋯.choose j • P.root j = ∑ j ∈ b.support, f j • P.root j
j : ι
hj : j ∈ b.support
h : P.root i = ∑ j ∈ b.support, ⋯.choose j • P.root j
⊢ ⋯.choose j = f j
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
l : ι → ℚ := fun i ↦ ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
contra :
  (2 / (P.RootForm (P.root i)) (P.root i)) • P.root i =
    (2 / (P.RootForm (P.root j)) (P.root j)) • P.root j + (2 / (P.RootForm (P.root k)) (P.root k)) • P.root k
l' : ι → R := fun i ↦ (P.RootForm (P.root i)) (P.root i)
hll' : ∀ (i : ι), ↑(l i) = l' i
⊢ P.root i = (l i / l j) • P.root j + (l i / l k) • P.root k

Tactic:
change (2 / l' i) • P.root i = (2 / l' j) • P.root j + (2 / l' k) • P.root k at contra

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
l : ι → ℚ := fun i ↦ ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
l' : ι → R := fun i ↦ (P.RootForm (P.root i)) (P.root i)
hll' : ∀ (i : ι), ↑(l i) = l' i
contra : (2 / l' i) • P.root i = (2 / l' j) • P.root j + (2 / l' k) • P.root k
⊢ P.root i = (l i / l j) • P.root j + (l i / l k) • P.root k
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : 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 : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainTopCoeff i j) - ↑(chainBotCoeff i j) = -P.pairingIn ℤ j i

Tactic:
← chainBotCoeff_sub_chainTopCoeff h,

Goal state after:
ι : 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 : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainTopCoeff i j) - ↑(chainBotCoeff i j) = -(↑(chainBotCoeff i j) - ↑(chainTopCoeff i 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 : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
⊢ p i

Tactic:
by
  let := P.indexNeg
  rcases IsPos.or_neg b i with hi | hi
  · exact hi.induction_on_add h₁ h₂
  · suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
    exact hi.induction_on_add h₁ h₂

Goal state after:
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
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j) i)
this : (P.reflection j) (P.root i) = P.root i - P.pairingIn ℤ i j • P.root j
⊢ b.height ((P.reflectionPerm j) i) < b.height i

Tactic:
rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this

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
inst✝ : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j) i)
this : P.root ((P.reflectionPerm j) i) = P.root i + -P.pairingIn ℤ i j • P.root j
⊢ b.height ((P.reflectionPerm j) i) < b.height i
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ { cauchy := ⟦f⟧ }.lt { cauchy := ⟦g⟧ } ↔ f < g

Tactic:
rw [lt_def]

Goal state after:
f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 ↦ x1 < x2) definition._proof_1✝) ↔
    f < g
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
h✝ : (g - f).LimZero ∨ (-(g - f)).Pos
h : (-(g - f)).Pos
⊢ g < f

Tactic:
by rwa [neg_sub] at h

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

Goal state before:
pp: x : ℝ
⊢ ∀ (a b c : ℝ), a ≤ c → b ≤ c → a ⊔ b ≤ c

Tactic:
intro a b c

Goal state after:
x a b c : ℝ
⊢ a ≤ c → b ≤ c → a ⊔ b ≤ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b c : ℝ), a ≤ b → a ≤ c → a ≤ b ⊓ c

Tactic:
intro a b c

Goal state after:
x a b c : ℝ
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (x y z : ℝ), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
intro a b c

Goal state after:
x a b c : ℝ
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
hf : ¬f.LimZero
hl : f.lim ≠ 0
h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero
⊢ (f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹)).LimZero

Tactic:
rw [← mul_assoc, mul_right_comm, const_inv hl]; exact h₁ _ _ _

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

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, ∑ x_1, B k x * A l x_1 * X.vec (x, x_1) = ∑ x, ∑ i, A l i * X i x * B k x

Tactic:
(hB ..).right_comm,

Goal state after:
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, ∑ x_1, B k x * A l x_1 * X.vec (x, x_1) = ∑ x, ∑ x_1, A l x_1 * B k x * X x_1 x
Module: Mathlib.LinearAlgebra.Matrix.ZPow

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

Tactic:
h,

Goal state after:
case pos
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : n = 0
⊢ 0 ^ 0 = 1
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A⁻¹ ^ (k + l) = A⁻¹ ^ k * A⁻¹ ^ l

Tactic:
h,

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ 0 ^ (k + l) = 0 ^ k * 0 ^ l
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A⁻¹ ^ (n + 1) = A⁻¹ ^ (n + 2) * A

Tactic:
h,

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ 0 ^ (n + 1) = 0 ^ (n + 2) * A
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A

Tactic:
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
    · apply zpow_add_one (isUnit_det_of_left_inverse h)
    · change A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A
      simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_mul]

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✝¹ : Finite n
inst✝ : StarOrderedRing R
a : n → R
⊢ (vecMulVec (star a) a).PosSemidef

Tactic:
simp [vecMulVec_eq Unit, ← conjTranspose_replicateRow, posSemidef_conjTranspose_mul_self]

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

Goal state before:
pp: case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ (X - 1).leadingCoeff ^ (descPochhammer R n).natDegree = 1

Tactic:
h,

Goal state after:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ 1 ^ (descPochhammer R n).natDegree = 1
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
sub_comp,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
| descPochhammer ℤ (n + 1) * (X.comp (X - 1) - (↑n).comp (X - 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
sub_comp,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (X.comp (X - 1) - (↑n).comp (X - 1)) * (descPochhammer ℤ n).comp (X - 1) =
    (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹¹ : Finite ι₁
inst✝¹⁰ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁹ : LieRing L₁
inst✝⁸ : LieRing L₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this✝ : Nontrivial L₂
this : I₁ = ⊤
⊢ prod eι b₁ b₂ = ⊤

Tactic:
have hI₁ : (I₁ : Set L₂) = p₂ '' p₁.ker :=
      congr_arg SetLike.coe <| p₁.ker.coe_map_of_surjective (surjective_snd_prod eι b₁ b₂)

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹¹ : Finite ι₁
inst✝¹⁰ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁹ : LieRing L₁
inst✝⁸ : LieRing L₂
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L₁
inst✝⁴ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝³ : LieAlgebra K L₂
inst✝² : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝¹ : IsSimple K L₁
inst✝ : IsSimple K L₂
L : LieSubalgebra K (L₁ × L₂) := prod eι b₁ b₂
p₁ : ↥L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
p₂ : ↥L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
disj : Disjoint p₁.ker p₂.ker
I₁ : LieIdeal K L₂ := LieIdeal.map p₂ p₁.ker
this✝ : Nontrivial L₂
this : I₁ = ⊤
hI₁ : ↑I₁ = ⇑p₂ '' ↑p₁.ker
⊢ prod eι b₁ b₂ = ⊤
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
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
⊢ (⇑derivative)^[k] ((interpolate s v) r) =
    ↑k.factorial *
      ∑ i ∈ s,
        C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (X - C (v a))

Tactic:
simp_rw [interpolate_eq_sum, iterate_derivative_sum, iterate_derivative_C_mul, mul_sum s,
    ← mul_assoc, mul_comm (k.factorial : F[X]), mul_assoc]
  congr! 2 with i hi
  have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
  calc
    derivative^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    derivative^[k] (∏ vj ∈ (s.erase i).image v, (X - C vj)) := by rw [Finset.prod_image hvs']
    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powersetCard (#s - (k + 1)),
          ∏ va ∈ t, (X - C va) := by
        grind [iterate_derivative_prod_X_sub_C]
    _ = k.factorial * ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)), ∏ a ∈ t, (X - C (v a)) := by
        rw [powersetCard_eq_filter, powerset_image, eq_comm]
        congrm k.factorial * ?_
        refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
        case hi => grind [card_image_of_injOn, hvs'.mono]
        case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)
        case i_surj => grind [card_image_of_injOn, hvs'.mono]
        case h => exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]

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

Goal state before:
pp: case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d ↦ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ⊆
    φ.support.biUnion fun d ↦ d.support.biUnion fun i ↦ (f i).vars

Tactic:
apply Finset.biUnion_mono

Goal state after:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ∀ a ∈ φ.support, (C (coeff a φ) * ∏ i ∈ a.support, f i ^ a i).vars ⊆ a.support.biUnion fun i ↦ (f i).vars
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (d.support.biUnion fun i ↦ (f i ^ d i).vars) ⊆ d.support.biUnion fun i ↦ (f i).vars

Tactic:
apply Finset.biUnion_mono

Goal state after:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ ∀ a ∈ d.support, (f a ^ d a).vars ⊆ (f a).vars
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
⊢ (derivative X - 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_X,

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 - 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
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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h✝ : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ False

Tactic:
h,

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
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h✝ : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * 0
h : P = 0
⊢ False
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
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j : ι
⊢ ∀ c ∈ DFinsupp.support ((decompose 𝒜) r), (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) c) * x) ∈ I

Tactic:
intro k

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 𝒜
I : Ideal A
r x : A
hx₁ : IsHomogeneousElem 𝒜 x
hx₂ : x ∈ I
j k : ι
⊢ k ∈ DFinsupp.support ((decompose 𝒜) r) → (GradedRing.proj 𝒜 j) (↑(((decompose 𝒜) r) k) * x) ∈ I
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.coeff.support
⊢ ↑((weight w) d) ≤ φ.support.sup fun s ↦ ↑((weight w) s)

Tactic:
apply Finset.le_sup hd

Goal state after: