mathlib-initiative/mathlib-tactics huggingface dataset:
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]
⊢ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]

Tactic:
P.root_chainTopIdx,

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]
⊢ LinearIndependent R ![P.root i, P.root j + chainTopCoeff i j • P.root i]
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case zero
ι : 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
j : ι
hj : j ∈ b.support
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + 0 • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ b.IsPos k

Tactic:
| zero =>

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
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ + a₂ - (b₁ + b₂)) < ε

Tactic:
add_sub_add_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ - b₁ + (a₂ - b₂)) < ε
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
i j : ι
hi : b.IsPos i
hj : j ∈ b.support
hij : i ≠ j
⊢ P.root ((P.reflectionPerm j) i) = P.root i + -P.pairingIn ℤ i j • P.root j

Tactic:
rw [root_reflectionPerm, neg_smul, reflection_apply_root' ℤ, sub_eq_add_neg]

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

Goal state before:
pp: case zero
ι : 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
p : ι → Prop
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
i : ι
h₀ : b.IsPos i
hN : b.height i = 0
⊢ p i

Tactic:
| zero =>

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 : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_2 ≥ x_1), abv (↑f x_2) < x
⊢ ∃ i, ∀ j ≥ i, abv (↑f j) < ε

Tactic:
obtain ⟨i, hi⟩ := f.cauchy₃ (half_pos ε0)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
nk : ∀ x > 0, ∀ (x_1 : ℕ), ∃ x_2, ∃ (_ : x_2 ≥ x_1), abv (↑f x_2) < x
i : ℕ
hi : ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2
⊢ ∃ i, ∀ j ≥ i, abv (↑f j) < ε
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 : CauSeq β abv
hf : f1 ≈ f2
⊢ f1 ^ 0 ≈ f2 ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: a b : Cauchy abs
⊢ { cauchy := a } = { cauchy := b } ↔ { cauchy := a }.cauchy = { cauchy := b }.cauchy

Tactic:
by rw [ofCauchy.injEq]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h

Tactic:
by
  have := pos_add_limZero gh (neg_limZero fg)
  rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (if h : f.LimZero then 0 else f.inv h) = f.inv hf

Tactic:
dif_neg

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ f.inv ?hnc = f.inv hf

case hnc
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ ¬f.LimZero
Module: Mathlib.Data.Real.Basic

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

Tactic:
intro a

Goal state after:
x a : ℝ
⊢ ∀ (b : ℝ), a ≤ a ⊔ b
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b < c

Tactic:
obtain ⟨⟨εa, εa0, ia, ha⟩, ⟨εb, εb0, ib, hb⟩⟩ := ha, hb

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
⊢ a ⊔ b < c
Module: Mathlib.Data.Real.Basic

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

Tactic:
intro a

Goal state after:
x a : ℝ
⊢ ∀ (b : ℝ), b ≤ a ⊔ b
Module: Mathlib.Data.Real.Basic

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

Tactic:
intro a

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 : ℝ), a ⊓ b ≤ a

Tactic:
intro a

Goal state after:
x a : ℝ
⊢ ∀ (b : ℝ), a ⊓ b ≤ a
Module: Mathlib.Data.Real.Basic

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

Tactic:
intro a

Goal state after:
x a : ℝ
⊢ ∀ (b : ℝ), a ⊓ b ≤ b
Module: Mathlib.Data.Real.Basic

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

Tactic:
intro a

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

Goal state after:
x a : ℝ
⊢ ∀ (y z : ℝ), (a ⊔ y) ⊓ (a ⊔ z) ≤ a ⊔ y ⊓ z
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
⊢ ∀ (a b : ℝ), a ≤ b ∨ b ≤ a

Tactic:
intro a

Goal state after:
x a : ℝ
⊢ ∀ (b : ℝ), a ≤ b ∨ b ≤ a
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case inr.zero
a : ℝ
ha' : 0 < a
⊢ a * ↑0 + 1 ≤ (a + 1) ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

Tactic:
obtain hb | hb := hb

Goal state after:
case inl.inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c

case inl.inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c
Module: Mathlib.Algebra.Order.CauSeq.Basic

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

Tactic:
obtain hb | hb := hb

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a < b
⊢ a ≤ b ⊓ c

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hc : a ≤ c
hb : a ≈ b
⊢ a ≤ b ⊓ c
Module: Mathlib.Algebra.Order.CauSeq.Basic

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

Tactic:
replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
      refine le_of_eq_of_le hc (Or.inr ?_)
      exact Setoid.symm (CauSeq.inf_eq_right hb)

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A⁻¹ ^ 0 = (A ^ 0)⁻¹

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m : ℕ
⊢ A⁻¹ ^ m * A ^ 0 = A ^ 0 * A⁻¹ ^ m

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (A ^ 0).det ↔ IsUnit A.det ∨ 0 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0

Tactic:
| zero =>

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
inst✝ : DecidableEq n
U x : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosSemidef
⊢ x.PosSemidef

Tactic:
lift U to (Matrix n n R)ˣ using hU

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosSemidef
⊢ x.PosSemidef
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
inst✝ : DecidableEq n
x U : Matrix n n R
hU : IsUnit U
h : (star U * x * U).PosDef
⊢ x.PosDef

Tactic:
lift U to (Matrix n n R)ˣ using hU

Goal state after:
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : Matrix n n R
U : (Matrix n n R)ˣ
h : (star ↑U * x * ↑U).PosDef
⊢ x.PosDef
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: case refine_1
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
⊢ ∀ (a : R), ((aeval f) (C a)) x = eval μ (C a) • x

Tactic:
intro a

Goal state after:
case refine_1
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
a : R
⊢ ((aeval f) (C a)) x = eval μ (C a) • x
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case zero
ι : 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 ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
k : ↥b.support
x : M
hk : (P.coroot' ↑k) 0 ≠ 0
⊢ p k

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: n : ℕ
⊢ (n + 1)! = ∏ i ∈ range (n + 1), (i + 1)

Tactic:
factorial,

Goal state after:
n : ℕ
⊢ n.succ * n ! = ∏ i ∈ range (n + 1), (i + 1)
Module: Mathlib.Data.Nat.Factorial.SuperFactorial

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

Tactic:
factorial,

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

Goal state before:
pp: case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S 0).Monic

Tactic:
| zero =>

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

Goal state before:
pp: case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (ascPochhammer S 0) = ascPochhammer T 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
S : Type u
inst✝ : Semiring S
⊢ ascPochhammer ℕ (0 + 1) = ascPochhammer ℕ 0 * (X + ↑0)

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: n t : ℕ
⊢ n.ascFactorial t * (n + ↑t) = n.ascFactorial (t + 1)

Tactic:
Nat.cast_id,

Goal state after:
n t : ℕ
⊢ n.ascFactorial t * (n + t) = n.ascFactorial (t + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
⊢ (ascPochhammer S 0).natDegree = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
⊢ 0 < eval s (ascPochhammer S 0)

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R 0).Monic

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
⊢ map f (descPochhammer R 0) = descPochhammer T 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
⊢ descPochhammer ℤ (0 + 1) = descPochhammer ℤ 0 * (X - ↑0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (descPochhammer R 0).natDegree = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ descPochhammer ℤ 0 = (ascPochhammer ℤ 0).comp (X - ↑0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
r : R
⊢ eval r (descPochhammer R 0) = eval (r - ↑0 + 1) (ascPochhammer R 0)

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
n : ℕ
⊢ eval (↑n) (descPochhammer R 0) = ↑(n.descFactorial 0)

Tactic:
| zero =>

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
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j = Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) i j

Tactic:
refine Fin.cases (by simp) (fun i => ?_) i

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j =
    Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) i.succ j
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
k : ℕ
h : k < 0
⊢ eval (-↑k) (ascPochhammer R 0) = 0

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1.zero
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
zero' : eval r (ascPochhammer R 0) = 0
⊢ ∃ k < 0, ↑k = -r

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
r : R
⊢ eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - ↑j)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : ↑0 - 1 ≤ s
⊢ (s - ↑0 + 1) ^ 0 ≤ eval s (descPochhammer S 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
⊢ MonotoneOn (fun x ↦ eval x (descPochhammer S 0)) (Set.Ici (↑0 - 1))

Tactic:
| zero =>

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

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
⊢ MonotoneOn (fun x ↦ eval x (descPochhammer S (n + 1))) (Set.Ici (↑(n + 1) - 1))

Tactic:
intro a

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (fun x ↦ eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
a : S
⊢ a ∈ Set.Ici (↑(n + 1) - 1) →
    ∀ ⦃b : S⦄,
      b ∈ Set.Ici (↑(n + 1) - 1) →
        a ≤ b → (fun x ↦ eval x (descPochhammer S (n + 1))) a ≤ (fun x ↦ eval x (descPochhammer S (n + 1))) b
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = #s - 1

Tactic:
rw [← card_erase_of_mem hi, card_eq_sum_ones]

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = ∑ x ∈ s.erase i, 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ (Lagrange.basis s v i).natDegree = #s - 1

Tactic:
by
  have H : ∀ j, j ∈ s.erase i → basisDivisor (v i) (v j) ≠ 0 := by
    simp_rw [Ne, mem_erase, basisDivisor_eq_zero_iff]
    exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)
  rw [← card_erase_of_mem hi, card_eq_sum_ones]
  convert! natDegree_prod _ _ H using 1
  refine sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).symm
  rw [Ne, ← basisDivisor_eq_zero_iff]
  exact H _ hj

Goal state after:
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₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodH eι b₁ b₂ i ∈ ↑(lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))

Tactic:
rw [hef]

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₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ ∈
    ↑(lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: case zero
ι₁ : 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₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
y : ↥(prod eι b₁ b₂)
x : ↥H₁
this : IsLieAbelian ↥H₁
⊢ ⁅(↑0).1, ↑x⁆ = 0

Tactic:
| zero =>

Goal state after:
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✝ : Nontrivial L₂
this : Fintype ι₁
⊢ prod eι b₁ b₂ < ⊤

Tactic:
have := Fintype.ofFinite ι₂

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✝ : Nontrivial L₂
this✝ : Fintype ι₁
this : Fintype ι₂
⊢ prod eι b₁ b₂ < ⊤
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
⊢ (vandermonde fun i ↦ ↑↑i).det = ↑(Nat.superFactorial 0)

Tactic:
| zero =>

Goal state after: