mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹⁴ : CommRing R
inst✝¹³ : Module R M
inst✝¹² : Module R N
P : RootPairing ι R M N
inst✝¹¹ : IsDomain R
S : Type u_6
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), f (P.root i) ≠ 0
this✝ : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range ⇑P.root)
v : ↑(baseOf ⇑P.root ↑f) → ↥M₀ := fun i ↦ P.rootSpanMem S ↑i
⊢ LinearIndepOn S (⇑P.root) (baseOf ⇑P.root ↑f)

Tactic:
change LinearIndependent S (M₀.subtype ∘ v)

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✝¹⁴ : CommRing R
inst✝¹³ : Module R M
inst✝¹² : Module R N
P : RootPairing ι R M N
inst✝¹¹ : IsDomain R
S : Type u_6
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), f (P.root i) ≠ 0
this✝ : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range ⇑P.root)
v : ↑(baseOf ⇑P.root ↑f) → ↥M₀ := fun i ↦ P.rootSpanMem S ↑i
⊢ LinearIndependent (ι := ↑(baseOf ⇑P.root ↑f)) S (⇑M₀.subtype ∘ v)
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 : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ P.pairing k i = (algebraMap ℤ R) (P.pairingIn ℤ j i) + (algebraMap ℤ R) (r * 2)

Tactic:
map_mul,

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 : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ P.pairing k i = (algebraMap ℤ R) (P.pairingIn ℤ j i) + (algebraMap ℤ R) r * (algebraMap ℤ R) 2
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 : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ P.pairing l i = (algebraMap ℤ R) (P.pairingIn ℤ j i) + (algebraMap ℤ R) (s * 2)

Tactic:
map_mul,

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 : ∀ (s t : ℤ), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
S : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S_def : S = {z | P.root j + z • P.root i ∈ range ⇑P.root}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hli_notMem : P.root l - P.root i ∉ range ⇑P.root
hli_ne : P.root l ≠ P.root i
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ P.pairing l i = (algebraMap ℤ R) (P.pairingIn ℤ j i) + (algebraMap ℤ R) s * (algebraMap ℤ R) 2
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✝⁴ : CommRing R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : Nontrivial R
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)
⊢ range ⇑P.root ⊆ ↑(span R (range fun x ↦ P.root ↑x))

Tactic:
← span_span_of_tower (R := ℤ)

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✝⁴ : CommRing R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : Nontrivial R
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)
⊢ range ⇑P.root ⊆ ↑(span R ↑(span ℤ (range fun x ↦ P.root ↑x)))
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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
this : span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ))
⊢ map (P.rootSpan ℚ).subtype ⊤ ≤ span ℚ (⇑(P.rootSpan ℚ).subtype '' P.rootSpanMem ℚ '' univ)

Tactic:
← image_comp

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
this : span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ))
⊢ map (P.rootSpan ℚ).subtype ⊤ ≤ span ℚ (⇑(P.rootSpan ℚ).subtype ∘ P.rootSpanMem ℚ '' univ)
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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
i : ι
this : ↑(P.rootSpanMem ℚ i) ∈ span ℚ (⇑P.root '' baseOf (⇑P.root) f)
⊢ (P.rootSpan ℚ).subtype (P.rootSpanMem ℚ i) ∈ span ℚ (⇑(P.rootSpan ℚ).subtype '' v '' univ)

Tactic:
← image_comp

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
i : ι
this : ↑(P.rootSpanMem ℚ i) ∈ span ℚ (⇑P.root '' baseOf (⇑P.root) f)
⊢ (P.rootSpan ℚ).subtype (P.rootSpanMem ℚ i) ∈ span ℚ (⇑(P.rootSpan ℚ).subtype ∘ v '' univ)
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: case pos
ι : 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
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root (-i), P.root j]
z : ℤ
⊢ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j) ↔ P.root j + z • -P.root i ∈ range ⇑P.root

Tactic:
smul_neg,

Goal state after:
case pos
ι : 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
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root (-i), P.root j]
z : ℤ
⊢ -↑(chainTopCoeff i j) ≤ z ∧ z ≤ ↑(chainBotCoeff i j) ↔ P.root j + -(z • P.root i) ∈ range ⇑P.root
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]
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) = P.pairingIn ℤ j i

Tactic:
suffices ∀ i j, LinearIndependent R ![P.root i, P.root j] →
      P.chainBotCoeff i j - P.chainTopCoeff i j ≤ P.pairingIn ℤ j i by
    refine le_antisymm (this i j h) ?_
    specialize this (P.reflectionPerm i i) j (by simpa)
    simp only [chainBotCoeff_reflectionPerm_left, chainTopCoeff_reflectionPerm_left,
      pairingIn_reflectionPerm_self_right] at this
    lia

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]
⊢ ∀ (i j : ι),
    LinearIndependent R ![P.root i, P.root j] → ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) ≤ P.pairingIn ℤ j i
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✝]
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
h₁ : (P.reflection i) (P.root (chainBotIdx i j)) = P.root j + (↑(chainBotCoeff i j) - P.pairingIn ℤ j i) • P.root i
h₂ : (P.reflection i) (P.root (chainBotIdx i j)) ∈ range ⇑P.root
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) ≤ P.pairingIn ℤ j i

Tactic:
rw [h₁, root_add_zsmul_mem_range_iff h, mem_Icc] at 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✝]
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
h₁ : (P.reflection i) (P.root (chainBotIdx i j)) = P.root j + (↑(chainBotCoeff i j) - P.pairingIn ℤ j i) • P.root i
h₂ :
  -↑(chainBotCoeff i j) ≤ ↑(chainBotCoeff i j) - P.pairingIn ℤ j i ∧
    ↑(chainBotCoeff i j) - P.pairingIn ℤ j i ≤ ↑(chainTopCoeff i j)
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) ≤ P.pairingIn ℤ j i
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 : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε

Tactic:
← add_halves ε

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2
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
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 - g1 ≈ f2 - g2

Tactic:
by simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)

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
i : ι
hi : b.IsPos i
⊢ ∃ n f, range f ⊆ ↑b.support ∧ P.root i = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
by
  apply hi.induction_on_add (fun j hj ↦ ⟨1, ![j], by simpa⟩)
  intro j k l h₁ ⟨n, f, h₂, h₃, h₄⟩ h₅
  refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
  · simpa using insert_subset h₅ h₂
  · simp [Fin.sum_univ_castSucc, h₁, h₃]
  · by_cases hm : m < n
    · have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
      rw [this, Fin.sum_Iic_castSucc]
      simp only [Fin.snoc_castSucc, h₄]
    · replace hm : m = n := by lia
      replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
      simp [hm, Fin.sum_univ_castSucc, ← h₃, ← h₁]

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

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

Tactic:
rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]

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

Goal state before:
pp: α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace

Tactic:
rw [← sum_hadamard_eq, Finset.sum_comm]

Goal state after:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y, ∑ x, ((diagonal v * A) ⊙ (B * diagonal w)) x y
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✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M ^ (k + 2)).PosSemidef

Tactic:
rw [pow_succ, pow_succ']
    simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

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

Goal state before:
pp: n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
a b : n → K
ha : M *ᵥ a = M *ᵥ b ∧ a ≠ b
⊢ ∃ a, a ≠ 0 ∧ M *ᵥ a = 0

Tactic:
exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩

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

Goal state before:
pp: case hbc
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this : Fintype n
h : (D - Bᴴ * A⁻¹ * B).PosSemidef
x : m ⊕ n → R'
⊢ 0 ≤ star (x ∘ Sum.inr) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x ∘ Sum.inr

Tactic:
rw [← dotProduct_mulVec (star (x ∘ Sum.inr))]
      apply (posSemidef_iff_dotProduct_mulVec.mp h).2

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

Goal state before:
pp: case refine_3
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
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) (X * (X ^ n * C a))) x = eval μ (X * (X ^ n * C a)) • x

Tactic:
map_mul,

Goal state after:
case refine_3
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
n : ℕ
a : R
hna : ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x
⊢ ((aeval f) X * (aeval f) (X ^ n * C a)) x = eval μ (X * (X ^ n * C a)) • x
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R A).Finite

Tactic:
rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ P.pairing i k = ∑ x ∈ b.support, (algebraMap ℤ R) (f x * P.pairingIn ℤ x k)

Tactic:
map_mul,

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ P.pairing i k = ∑ x ∈ b.support, (algebraMap ℤ R) (f x) * (algebraMap ℤ R) (P.pairingIn ℤ x k)
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
k : ι
⊢ P.pairing j k = ∑ x ∈ b.support, (algebraMap ℤ R) (g x * P.pairingIn ℤ x k)

Tactic:
map_mul,

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
k : ι
⊢ P.pairing j k = ∑ x ∈ b.support, (algebraMap ℤ R) (g x) * (algebraMap ℤ R) (P.pairingIn ℤ x k)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
⊢ descPochhammer ℤ (n + 1) * (X - 1 - ↑n) = descPochhammer ℤ (n + 1) * (X - ↑(n + 1))