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

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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ (Subgroup.closure (range (Equiv.reflection P))).toSubmonoid = Submonoid.closure (range (Equiv.reflection P))

Tactic:
Subgroup.closure_toSubmonoid,

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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ Submonoid.closure (range (Equiv.reflection P) ∪ (range (Equiv.reflection P))⁻¹) =
    Submonoid.closure (range (Equiv.reflection P))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
⊢ rootSpace H✝ (⇑β + 0) ≠ ⊥

Tactic:
add_zero

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑(↑n - ↑(chainTopCoeff (⇑α) β))
⊢ rootSpace H✝ ⇑β ≠ ⊥
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup) ⟨1, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
| one =>

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

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup) ⟨1, ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
| one =>

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

Goal state before:
pp: case refine_2.one
ι : 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
w : P.Aut
⊢ P.weylGroupToPerm ⟨1, ⋯⟩ ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
| one =>

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

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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflectionPerm)

Tactic:
rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.domRestrict_apply, Equiv.indexHom_apply,
        Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using! Subgroup.mul_mem _ h₁ h₂

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

Goal state before:
pp: case one
ι : 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.InvariantForm
g : P.Aut
⊢ ∀ (x y : M), (B.form (⟨1, ⋯⟩ • x)) (⟨1, ⋯⟩ • y) = (B.form x) y

Tactic:
| one =>

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ (t • s • y) • v = t • (s • y) • v

Tactic:
rw [← smul_assoc, smul_eq_mul, hy (t * s), ← smul_eq_mul, smul_assoc]

Goal state after:
case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ t • s • y • v = t • (s • y) • v
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ Submodule.span K (Set.range ⇑{ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ }) = ⊤

Tactic:
by convert! span_weight_isNonZero_eq_top K L H; ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s + 0 ∈ S

Tactic:
add_zero

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ T
hv : s + t ∈ Q
this : t = 0
⊢ s ∈ S
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
y✝ x y : k[G]
hx : ((ofMulAction k G G).asAlgebraHom x) y✝ = x * y✝
hy : ((ofMulAction k G G).asAlgebraHom y) y✝ = y * y✝
⊢ ((ofMulAction k G G).asAlgebraHom (x + y)) y✝ = (x + y) * y✝

Tactic:
| add x y hx hy =>

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommSemiring k
inst✝¹ : Group G
inst✝ : Fintype G
i : G
⊢ ((leftRegular k G).norm ∘ₗ MonoidAlgebra.lsingle i) 1 =
    (((lsmul k k[G]).flip ((leftRegular k G).norm (MonoidAlgebra.single 1 1)) ∘ₗ
          (linearCombination k fun x ↦ 1) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle i)
      1

Tactic:
simpa [Representation.norm] using Finset.sum_bijective _
    (Group.mulRight_bijective i) (by simp) (by simp)

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

Goal state before:
pp: case refine_1.one
ι : 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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
g : P.Aut
⊢ q ∈ invtSubmodule (P.weylGroupRootRep ⟨1, ⋯⟩)

Tactic:
| one =>

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

Goal state before:
pp: case h.left
ι : 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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.weightMap ⇑(↑f).weightMap

Tactic:
refine leftInverse_iff_comp.mpr ?_
        simp only [← @LinearMap.coe_comp]
        rw [← Hom.weightMap_mul, f.inv_val, Hom.weightMap_one, LinearMap.id_coe]

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✝¹ : Nonempty ι
inst✝ : NeZero 2
⊢ b.support.Nonempty

Tactic:
by_contra! contra
  inhabit ι
  simpa [P.ne_zero default, contra] using b.root_mem_or_neg_mem default

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✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
ht : ↑z • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * ↑z = 1
this✝ : ↑z * ↑w = 1
this : z = 1 ∨ z = -1
⊢ t = 1 ∨ t = -1

Tactic:
rcases this with rfl | rfl
    · left; simpa using hz
    · right; simpa [neg_eq_iff_eq_neg] using hz

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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ ↑(chainTopCoeff ↑i ↑j) = -P.pairingIn ℤ ↑j ↑i

Tactic:
by
  rw [← chainTopCoeff_sub_chainBotCoeff (b.linearIndependent_pair_of_ne hij)]
  simp

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 j k : ι
hk : P.root k = P.root i + P.root 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
⊢ P.root k = ∑ x ∈ b.support, f x • P.root x + ∑ x ∈ b.support, g x • P.root x

Tactic:
← hf,

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
i j k : ι
hk : P.root k = P.root i + P.root 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
⊢ P.root k = P.root i + ∑ x ∈ b.support, g x • P.root x
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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
x✝ : ℤ
⊢ P.root (chainTopIdx i j) + x✝ • P.root i ∈ range ⇑P.root ↔
    x✝ ∈ Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))

Tactic:
root_add_zsmul_mem_range_iff 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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
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}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
x✝ : ℤ
⊢ x✝ ∈ Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j)) ↔
    x✝ ∈ Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i 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
i j k : ι
z : ℤ
hk : P.root k = P.root i + z • P.root 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
⊢ P.root k = ∑ x ∈ b.support, f x • P.root x + z • ∑ x ∈ b.support, g x • P.root x

Tactic:
← hf,

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
i j k : ι
z : ℤ
hk : P.root k = P.root i + z • P.root 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
⊢ P.root k = P.root i + z • ∑ x ∈ b.support, g x • P.root 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
ε 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₂ + abv a₁ * abv (a₂ - b₂) < ε

Tactic:
h₂.le,

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 * abv b₂ + abv a₁ * (ε / 2 / M) < ε
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
⊢ ∃ r, ∀ (i : ℕ), abv (f i) < r

Tactic:
obtain ⟨i, h⟩ := hf _ zero_lt_one
  set R : ℕ → α := @Nat.rec (fun _ => α) (abv (f 0)) fun i c => max c (abv (f i.succ)) with hR
  have : ∀ i, ∀ j ≤ i, abv (f j) ≤ R i := by
    refine Nat.rec (by simp [hR]) ?_
    rintro i hi j (rfl | hj)
    · simp [R]
    · exact (hi j hj).trans (le_max_left _ _)
  refine ⟨R i + 1, fun j ↦ ?_⟩
  obtain hji | hij := le_total j i
  · exact (this i _ hji).trans_lt (lt_add_one _)
  · simpa using (abv_add abv _ _).trans_lt <| add_lt_add_of_le_of_lt (this i _ le_rfl) (h _ hij)

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
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f * g) j) < ε

Tactic:
have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
      rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this

Goal state after:
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 : m → R
⊢ (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mulVec_eq_zero Aᴴ _

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

Goal state before:
pp: x : ℝ
q : ℚ≥0
⊢ { cauchy := ↑q.num } / { cauchy := ↑q.den } = ↑q.num / ↑q.den

Tactic:
ofCauchy_natCast,

Goal state after:
x : ℝ
q : ℚ≥0
⊢ ↑q.num / { cauchy := ↑q.den } = ↑q.num / ↑q.den
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
q : ℚ
⊢ { cauchy := ↑q.num } / { cauchy := ↑q.den } = ↑q.num / ↑q.den

Tactic:
ofCauchy_natCast,

Goal state after:
x : ℝ
q : ℚ
⊢ { cauchy := ↑q.num } / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← neg_neg A]

Goal state after:
α : Type u_1
n : Type u_4
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
A : Matrix n n α
h : (-A).IsHermitian
⊢ (- -A).IsHermitian
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
n : ℕ
⊢ 1 ^ -[n+1] = 1

Tactic:
zpow_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ (1 ^ (n + 1))⁻¹ = 1
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
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹

Tactic:
zpow_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A⁻¹ ^ (n + 1))⁻¹ = (A ^ -[n+1])⁻¹
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
n : ℕ
⊢ (A⁻¹ ^ (n + 1))⁻¹ = (A ^ -[n+1])⁻¹

Tactic:
zpow_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A⁻¹ ^ (n + 1))⁻¹ = (A ^ (n + 1))⁻¹⁻¹
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
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹

Tactic:
zpow_negSucc,

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
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ (n + 1))⁻¹⁻¹
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])

Tactic:
zpow_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ (n + 1))⁻¹ (Y ^ -[n+1])
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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ (n + 1))⁻¹ (Y ^ -[n+1])

Tactic:
zpow_negSucc,

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ SemiconjBy A (X ^ (n + 1))⁻¹ (Y ^ (n + 1))⁻¹
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
⊢ spectrum R (diagonal d) = Set.range d

Tactic:
ext μ

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
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 * -[n+1]) = (A ^ m) ^ -[n+1]

Tactic:
zpow_negSucc,

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 * -[n+1]) = ((A ^ m) ^ (n + 1))⁻¹
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:
zpow_negSucc,

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

Tactic:
zpow_negSucc,

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+1]) = ((A ^ -[m+1]) ^ (n + 1))⁻¹
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+1]) = ((A ^ -[m+1]) ^ (n + 1))⁻¹

Tactic:
zpow_negSucc,

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+1]) = ((A ^ (m + 1))⁻¹ ^ (n + 1))⁻¹
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:
zpow_negSucc,

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.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:
zpow_negSucc,

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))⁻¹