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 : ∀ (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
⊢ P.root k + P.root i = P.root j + (r + 1) • P.root i

Tactic:
rw [hk]

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
⊢ P.root j + r • P.root i + P.root i = P.root j + (r + 1) • P.root 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 : ∀ (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
⊢ P.root k ≠ -P.root i

Tactic:
rw [hk]

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
⊢ P.root j + r • P.root i ≠ -P.root i
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 : ι
⊢ ↑(P.rootSpanMem ℚ i) ∈ span ℚ (⇑P.root '' baseOf (⇑P.root) f)

Tactic:
← span_span_of_tower ℤ,

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 : ι
⊢ ↑(P.rootSpanMem ℚ i) ∈ span ℚ ↑(span ℤ (⇑P.root '' baseOf (⇑P.root) f))
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]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
z : ℤ
⊢ P.root k - z • P.root i = P.root j - (z - 1) • P.root i

Tactic:
rw [hk]

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]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
z : ℤ
⊢ P.root j + P.root i - z • P.root i = P.root j - (z - 1) • P.root i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = ∑ j ∈ b.support, f j • P.root j
contra : f = 0
⊢ P.root i = 0

Tactic:
simp [hf', contra]

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 k : ι
hk : P.root k = P.root j + P.root i
h : LinearIndependent R ![P.root i, P.root k]
⊢ P.root j = P.root k - P.root i

Tactic:
rw [hk]

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 k : ι
hk : P.root k = P.root j + P.root i
h : LinearIndependent R ![P.root i, P.root k]
⊢ P.root j = P.root j + P.root i - P.root i
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i = -∑ j ∈ b.support, f j • P.root j
contra : f = 0
⊢ P.root i = 0

Tactic:
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
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + ↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (↑w + 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root k = P.root i + (w + 1) • P.root j

Tactic:
rw [hk]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + ↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (↑w + 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root i + (↑w + 1) • P.root j = P.root i + (w + 1) • P.root j
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
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ ε / 2 / M * abv b₂ + M * (ε / 2 / M) ≤ ε

Tactic:
hb₂,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K₁ K₂ : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
M : α := max 1 (max K₁ K₂)
K0 : 0 < M
εK : 0 < ε / 2 / M
h₁ : abv (a₁ - b₁) < ε / 2 / M
h₂ : abv (a₂ - b₂) < ε / 2 / M
ha₁ : abv a₁ < M
hb₂ : abv b₂ < M
⊢ ε / 2 / M * M + M * (ε / 2 / M) ≤ ε
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
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (-↑w - 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root k = P.root i - (w + 1) • P.root j

Tactic:
rw [hk]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : CharZero R
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
j : ι
hj : j ∈ b.support
w : ℕ
hw :
  ∀ {i k : ι}, b.IsPos i → P.root k = P.root i + -↑w • P.root j → LinearIndependent R ![P.root j, P.root i] → b.IsPos k
i k : ι
hi : b.IsPos i
hk : P.root k = P.root i + (-↑w - 1) • P.root j
hij : LinearIndependent R ![P.root j, P.root i]
⊢ P.root i + (-↑w - 1) • P.root j = P.root i - (w + 1) • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
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
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = ↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = ↑n + 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
hkn : b.height k = ↑n
hkpos : b.IsPos k
⊢ P.root i = P.root k + P.root j

Tactic:
rw [hk]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
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
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = ↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = ↑n + 1
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
hkn : b.height k = ↑n
hkpos : b.IsPos k
⊢ P.root i = P.root i - P.root j + P.root j
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i

Tactic:
rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), |↑f i| < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk y✝ → mk y✝ ≤ c → mk y✝¹ ≤ c

Tactic:
induction c using Real.ind_mk

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝¹ → mk y✝¹ ≤ mk y✝ → mk y✝² ≤ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ c → mk y✝ ≤ c → mk y✝¹ ⊔ mk y✝ ≤ c

Tactic:
induction c using Real.ind_mk

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝ → mk y✝¹ ≤ mk y✝ → mk y✝² ⊔ mk y✝¹ ≤ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk y✝ → mk y✝¹ ≤ c → mk y✝¹ ≤ mk y✝ ⊓ c

Tactic:
induction c using Real.ind_mk

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝² ≤ mk y✝¹ → mk y✝² ≤ mk y✝ → mk y✝² ≤ mk y✝¹ ⊓ mk y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x c : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ (mk y✝¹ ⊔ mk y✝) ⊓ (mk y✝¹ ⊔ c) ≤ mk y✝¹ ⊔ mk y✝ ⊓ c

Tactic:
induction c using Real.ind_mk

Goal state after:
case h.h.h
x : ℝ
y✝² y✝¹ y✝ : CauSeq ℚ abs
⊢ (mk y✝² ⊔ mk y✝¹) ⊓ (mk y✝² ⊔ mk y✝) ≤ mk y✝² ⊔ mk y✝¹ ⊓ mk y✝
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≈ b
⊢ b ⊔ b ≈ b

Tactic:
CauSeq.sup_idem

Goal state after:
case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : CauSeq α abs
h : a ≈ b
⊢ b ≈ b
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, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |min (↑a j) (↑b j) - ↑b j| < ε✝

Tactic:
← min_sub_sub_right

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace

Tactic:
by
  simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : CommMonoid α
inst✝ : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A ⊙ B)ᴴ = A ⊙ B

Tactic:
conjTranspose_hadamard,

Goal state after:
α : Type u_1
n : Type u_4
inst✝¹ : CommMonoid α
inst✝ : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ Bᴴ ⊙ Aᴴ = A ⊙ B
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
⊢ (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal (d - μ • 1))

Tactic:
Pi.sub_def,

Goal state after:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
⊢ (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal fun i ↦ d i - (μ • 1) i)
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 B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)

Tactic:
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)

Goal state after:
case inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)

case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
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
⊢ False

Tactic:
obtain ⟨a, ha, ha2⟩ : ∃ a ≠ 0, M *ᵥ a = 0 := by
    obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩

Goal state after:
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 : n → K
ha : a ≠ 0
ha2 : M *ᵥ a = 0
⊢ False
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✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬(toLin' b.cartanMatrix - 4 • 1).ker ≠ ⊥

Tactic:
← eigenspace_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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ ¬eigenspace (toLin' b.cartanMatrix) 4 ≠ ⊥
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
← add_assoc,

Goal state after:
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S (n + m) * (X + ↑n + ↑m) = ascPochhammer S (n + m + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

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

Tactic:
← add_assoc,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
n m : ℕ
ih : descPochhammer R n * (descPochhammer R m).comp (X - ↑n) = descPochhammer R (n + m)
⊢ descPochhammer R (n + m) * (X - ↑n - ↑m) = descPochhammer R (n + m + 1)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ * (X - C y) = 0
⊢ x = y

Tactic:
mul_eq_zero,

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : C (x - y)⁻¹ = 0 ∨ X - C y = 0
⊢ x = y
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
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ (-1) ^ ↑j.succ * W 0 j.succ * (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
mul_eq_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
j : Fin n
a✝ : j.succ ∈ univ
hj0 : j.succ ≠ 0
⊢ (-1) ^ ↑j.succ * W 0 j.succ = 0 ∨ (W.submatrix succ j.succ.succAbove).det = 0
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : ↑(#s) = P.degree + 1
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
lift P.degree to ℕ using (by contrapose! hP; simp [hP]) with deg hdeg

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
deg : ℕ
hdeg : ↑deg = P.degree
hP : ↑(#s) = ↑deg + 1
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
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
⊢ nodalWeight s v i ≠ 0

Tactic:
rw [nodalWeight, prod_ne_zero_iff]

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
⊢ ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ n * m = n * ∑ i_1 ∈ i.support, i i_1

Tactic:
← hφ hi,

Goal state after:
case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ.coeff i ≠ 0
⊢ n * (weight 1) i = n * ∑ i_1 ∈ i.support, i i_1