mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl.inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inl.inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inl.inr.inr.inr.inr.inr
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inl.inr.inr.inr.inr.inr
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inr.inr.inr.inr.inl
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case inr.inr.inr.inr.inr.inr
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i

Tactic:
rw [hji, hij'] at aux₂

Goal state after:
case inr.inr.inr.inr.inr.inr
ι : 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength 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 : ι
inst✝ : P.IsReduced
h : P.root i - P.root j ∈ range ⇑P.root
⊢ 1 ≤ chainBotCoeff i j

Tactic:
have h' := P.linearIndependent_of_sub_mem_range_root' 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 : ι
inst✝ : P.IsReduced
h : P.root i - P.root j ∈ range ⇑P.root
h' : LinearIndependent R ![P.root i, P.root j]
⊢ 1 ≤ chainBotCoeff i j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
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
h : ¬f ≤ 0
⊢ ∃ i, 0 i < f i

Tactic:
contrapose! h; exact h

Goal state after:
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
⊢ (P.reflection i) (P.root (chainBotIdx i j)) ∈ range ⇑P.root

Tactic:
rw [← root_reflectionPerm]

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
⊢ P.root ((P.reflectionPerm i) (chainBotIdx i j)) ∈ range ⇑P.root
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
this : P.pairingIn ℤ i i = ∑ j ∈ b.support, f j • P.pairingIn ℤ j i
⊢ ∑ j ∈ b.support, f j • P.pairingIn ℤ j i ≤ 0

Tactic:
refine Finset.sum_nonpos fun j _ ↦ ?_

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
j : ι
x✝ : j ∈ b.support
⊢ f j • P.pairingIn ℤ j i ≤ 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
⊢ ∀ (n : ℕ) (x : CauSeq β abv), ↑(n • x) = n • ↑x

Tactic:
intros

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℕ
x✝ : CauSeq β abv
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
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
⊢ ∀ (n : ℤ) (x : CauSeq β abv), ↑(n • x) = n • ↑x

Tactic:
intros

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℤ
x✝ : CauSeq β abv
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
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
⊢ ∀ (n : ℕ), ↑↑n = ↑n

Tactic:
intros

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝
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
⊢ ∀ (n : ℤ), ↑↑n = ↑n

Tactic:
intros

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝
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:
simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)

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 : ℕ → β
g : CauSeq β abv
h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (f j - f i) < ε

Tactic:
obtain ⟨h₁, h₂⟩ := hi _ le_rfl; rw [abv_sub abv] at h₁
      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
      have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij))
      rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this

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
G : Type u_3
inst✝¹ : SMul G β
inst✝ : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2

Tactic:
by
  simpa [const_smul, smul_one_mul _ _] using
    mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf

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✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ g * (1 - f * f.inv hf) = g * (1 - f.inv hf * f)

Tactic:
mul_comm f

Goal state after:
α : 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
g f : CauSeq β abv
hf : ¬f.LimZero
h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g
h₃ : f * f.inv hf * g = f * f.inv hf * g
h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g
h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)
⊢ g * (1 - f.inv hf * f) = g * (1 - f.inv hf * f)
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case inl
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ ↑n).PosSemidef

pp: case inr
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ (-↑n)).PosSemidef

Tactic:
· simpa using hM.pow n

Goal state after:
case inr
n✝ : Type u_2
R' : Type u_4
inst✝⁵ : CommRing R'
inst✝⁴ : PartialOrder R'
inst✝³ : StarRing R'
inst✝² : Fintype n✝
inst✝¹ : StarOrderedRing R'
inst✝ : DecidableEq n✝
M : Matrix n✝ n✝ R'
hM : M.PosSemidef
n : ℕ
⊢ (M ^ (-↑n)).PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case mpr
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 ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ x

Tactic:
← Sum.elim_comp_inl_inr x,

Goal state after:
case mpr
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.inl ⊕ᵥ x ∘ Sum.inr) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ∘ Sum.inl ⊕ᵥ x ∘ Sum.inr)
Module: Mathlib.LinearAlgebra.Matrix.ZMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
⊢ μ * (d i * |v i| ^ 2) ≤ (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i

Tactic:
have h₀ : 0 ≤ ρ - μ := by grind [diag_pos_of_mul_diagonal_posDef A d hA hD hρ.nonempty.some]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
h₀ : 0 ≤ ρ - μ
⊢ μ * (d i * |v i| ^ 2) ≤ (|v| ᵥ* diagonal d) i * (N *ᵥ |v|) i
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case pos
ι : 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
hq_notMem : ∀ (k : ↥b.support), P.root ↑k ∉ q → q ≤ LinearMap.ker (P.coroot' ↑k)
k : ι
hkb : k ∈ b.support
x : M
hx : x ∈ q
hk : P.root k ∈ q
⊢ (P.coroot' k) x • P.root k ∈ q

Tactic:
exact q.smul_mem _ hk

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
n✝ : ℕ
⊢ eval 0 (descPochhammer R (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0

Tactic:
· simp [X_mul, descPochhammer_succ_left]

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

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

Tactic:
← descPochhammer_succ_left,

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