mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ¬f ≤ 0 ↔ 0 < f

Tactic:
Pi.lt_def

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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ i, 0 i < f i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i✝ j✝ : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i✝ + P.root j✝ ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
i j k : ι
hk : P.root k = P.root i + P.root j
hi : P.root i ∈ q
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ P.root j ∈ q

Tactic:
suffices P.root k ∈ q from (q.add_mem_iff_right hi).mp <| hk ▸ this

Goal state after:
case inl
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
i✝ j✝ : ι
K : Type u_5
inst✝³ : Field K
inst✝² : NeZero 2
inst✝¹ : Module K M
inst✝ : Module K N
P : RootPairing ι K M N
hij : P.root i✝ + P.root j✝ ∈ range ⇑P.root
q : Submodule K M
hq✝ : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
i j k : ι
hk : P.root k = P.root i + P.root j
hi : P.root i ∈ q
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ P.root k ∈ q
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 : ι
⊢ b.height i ≠ 0

Tactic:
obtain ⟨f, hf₀, hf₁, hf₂⟩ := b.exists_root_eq_sum_int i
  rw [height_eq_sum hf₂]
  rcases hf₁ with pos | neg
  · refine (Finset.sum_pos' (fun i _ ↦ pos.le i) ?_).ne'
    by_contra! contra
    replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (contra j (hf₀ hj)) (pos.le j)
      · simpa using hj
    exact P.ne_zero i <| by simp [hf₂, contra]
  · refine (Finset.sum_neg' (fun i _ ↦ neg.le i) ?_).ne
    by_contra! contra
    replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (neg.le j) (contra j (hf₀ hj))
      · simpa using hj
    exact P.ne_zero i <| by simp [hf₂, contra]

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
i : ι
h : i ∈ b.support
⊢ b.IsPos i

Tactic:
by
  rw [isPos_iff, height_one_of_mem_support h]
  exact Int.one_pos

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
⊢ P.pairingIn ℤ i i ≤ 0

Tactic:
have : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i :=
    algebraMap_injective ℤ R <| by
      simp_rw [algebraMap_pairingIn, map_sum, ← root_coroot_eq_pairing, hf₂, map_sum, map_zsmul,
        LinearMap.coe_sum, Finset.sum_apply, LinearMap.smul_apply, root_coroot_eq_pairing,
        zsmul_eq_mul, algebraMap_pairingIn]

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✝ : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
hf₁ : 0 < f
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
⊢ P.pairingIn ℤ i i ≤ 0
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)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
q : ℚ
hq : q > 0
hq' : P.root j = q • P.root i
⊢ ¬LinearIndependent R ![P.root i, P.root j]

Tactic:
LinearIndependent.pair_iff,

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)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
q : ℚ
hq : q > 0
hq' : P.root j = q • P.root i
⊢ ¬∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
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 : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε / F * F
⊢ abv (↑(f * g) j) < ε

Tactic:
div_mul_cancel₀ _ (ne_of_gt F0),

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 : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε
⊢ abv (↑(f * g) 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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)

Tactic:
let g : Dual ℚ N := f ∘ₗ (P.PolarizationEquiv.symm.restrictScalars ℚ).toLinearMap

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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
aux : ∀ (i : ι), ∃ q, 0 < q ∧ ↑q = 2 / (P.RootForm (P.root i)) (P.root i)
g : Dual ℚ N := f ∘ₗ ↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm)
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)
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
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv f.lim
⊢ f.LimZero

Tactic:
rw [h] at hf

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.lim = 0
hf : f ≈ const abv 0
⊢ f.LimZero
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ ↑a j ≤ ↑b j

Tactic:
← sub_nonneg

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(b - a) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑b j - ↑a j
Module: Mathlib.LinearAlgebra.Matrix.DotProduct

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0

Tactic:
by
  simpa only [← Matrix.replicateRow_vecMul, replicateRow_eq_zero] using
    mul_conjTranspose_mul_self_eq_zero A (replicateRow (Fin 1) v)

Goal state after:
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
hc : a ≈ c
hb : c ≤ b
⊢ a ≤ b ⊓ c

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

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroClass α
v w : n → α
⊢ diagonal v ⊙ diagonal w = diagonal (v * w)

Tactic:
by simp [diagonal_hadamard]

Goal state after:
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:
← inv_pow',

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
⊢ A⁻¹ ^ (k + l) = A⁻¹ ^ k * A⁻¹ ^ 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:
← inv_pow',

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
⊢ A⁻¹ ^ (n + 1) = A⁻¹ ^ (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
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A ^ (m + 1))⁻¹ ^ n

Tactic:
← inv_pow',

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A⁻¹ ^ (m + 1)) ^ n
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
u : Mˣ
k : ℕ
⊢ ↑u⁻¹ ^ (k + 1) = (↑u ^ (k + 1))⁻¹

Tactic:
← inv_pow',

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑u⁻¹ ^ (k + 1) = (↑u)⁻¹ ^ (k + 1)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (star ∘ (fun v ↦ v ᵥ* B) ∘ star)
⊢ (B * A * Bᴴ).PosDef

Tactic:
Function.comp_def,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective fun x ↦ star (star x ᵥ* B)
⊢ (B * A * Bᴴ).PosDef
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ { toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ⋯ } ∈ root

Tactic:
simpa [Weight.IsNonZero, Weight.IsZero] using b.linearIndependent_baseSupp.ne_zero i

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
⊢ p j

Tactic:
by
  let q : Submodule R M := span R (P.root ∘ (↑) '' {i | p i})
  have hq₀ : q ≠ ⊥ := q.ne_bot_iff.mpr ⟨P.root i, subset_span <| by simpa, P.ne_zero i⟩
  have hq_mem (k : b.support) : P.root k ∈ q ↔ p k := by
    refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩
    contrapose hk
    exact b.linearIndepOn_root.linearIndependent.notMem_span_image hk
  have hq_notMem (k : b.support) (hk : P.root k ∉ q) : q ≤ LinearMap.ker (P.coroot' k) := by
    refine fun x hx ↦ LinearMap.mem_ker.mpr ?_
    contrapose! hk
    rw [hq_mem]
    induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨l, hl, rfl⟩ : ∃ l : b.support, p l ∧ P.root l = x := by simp_all
      replace hk : b.cartanMatrix k l ≠ 0 := by
        rwa [ne_eq, cartanMatrix_apply_eq_zero_iff_symm, cartanMatrix_apply_eq_zero_iff_pairing]
      tauto
    | zero => simp_all
    | add x y hx hy hx' hy' =>
      replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
      tauto
    | smul a x hx hx' => simp_all
  have hq : ∀ k, q ∈ invtSubmodule (P.reflection k) := by
    rw [← b.forall_mem_support_invtSubmodule_iff]
    refine fun k hkb ↦ (mem_invtSubmodule _).mpr fun x hx ↦ ?_
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply]
    apply q.sub_mem hx
    by_cases hk : P.root k ∈ q
    · exact q.smul_mem _ hk
    · replace hk : P.coroot' k x = 0 := hq_notMem ⟨k, hkb⟩ hk hx
      simp [hk]
  simp [← hq_mem, IsIrreducible.eq_top_of_invtSubmodule_reflection q hq hq₀]

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

Goal state before:
pp: S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑(r ! * (r + 1).ascFactorial n) = ↑(r + n)!

Tactic:
Nat.factorial_mul_ascFactorial

Goal state after:
S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑(r + n)! = ↑(r + n)!
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
| succ b =>

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R (k + 1)) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
by
    rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ rectVandermonde v w (n + 1) i j = Pi.single (last n) (v i ^ n) j

Tactic:
rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ ↑j.rev ≠ 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
← sub_nonneg

Goal state after:
case succ
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
n : ℕ
ih : ↑n - 1 ≤ s → (s - ↑n + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - ↑n
⊢ (s - ↑(n + 1) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 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₂
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₂
h₁ :
  ↑(LieSubalgebra.map (prod eι b₁ b₂).incl (prodCartan eι b₁ b₂)) =
    ↑(lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})
h₂ :
  (lieSpan R (L₁ × L₂) {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}).toSubmodule = span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}
h₃ : Submodule.map (LinearMap.fst R L₁ L₂) (span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x}) = span R (Set.range b₁.h)
h₄ : (lieSpan R L₁ (Set.range b₁.h)).toSubmodule = span R (Set.range b₁.h)
⊢ ↑H₁ = ↑(lieSpan R L₁ (Set.range b₁.h))

Tactic:
by simp [b₁.cartan_eq_lieSpan]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (-1) ^ ↑0 * W 0 0 * (W.submatrix succ (succAbove 0)).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
succAbove_zero,

Goal state after:
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  of fun i ↦
    Fin.cons (projVandermonde v w i 0) fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq : W.submatrix succ succ = of fun i j ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (-1) ^ ↑0 * W 0 0 * (W.submatrix succ succ).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ (vandermonde fun i ↦ ↑↑i).det = ↑(n.succ.factorial * n.superFactorial)

Tactic:
det_vandermonde,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > i, (↑↑j - ↑↑i) = ↑(n.succ.factorial * n.superFactorial)
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
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)), ∏ va ∈ t, (X - C va) =
    ↑k.factorial * ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (X - C (v a))

Tactic:
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: