mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
⊢ -⇑α = (chainTopCoeff (⇑α) 0 + 1) • -⇑α + chainTopCoeff (⇑α) 0 • ⇑α

Tactic:
succ_nsmul',

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
inst✝ : Nontrivial L
hα : α.IsNonZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
⊢ -⇑α = -⇑α + chainTopCoeff (⇑α) 0 • -⇑α + chainTopCoeff (⇑α) 0 • ⇑α
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
φ : N₂
x : M
⊢ (((f.weightMap.dualMap ∘ₗ g.weightMap.dualMap) ∘ₗ ↑P₂.flip.toPerfPair) φ) x =
    ((↑P.flip.toPerfPair ∘ₗ f.coweightMap ∘ₗ g.coweightMap) φ) x

Tactic:
← LinearMap.comp_assoc _ f.coweightMap,

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
φ : N₂
x : M
⊢ (((f.weightMap.dualMap ∘ₗ g.weightMap.dualMap) ∘ₗ ↑P₂.flip.toPerfPair) φ) x =
    (((↑P.flip.toPerfPair ∘ₗ f.coweightMap) ∘ₗ g.coweightMap) φ) x
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: 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
p q : ↥ρ.invtSubmodule
h : p ≤ q
x : ρ.asModule
hx :
  x ∈
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      p
⊢ x ∈
    {
        toFun := fun p ↦
          let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
        invFun := fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩,
        left_inv := ⋯, right_inv := ⋯ }
      q

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: case refine_1
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
⊢ Ioo x y = ∅

pp: case refine_2
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ I

Tactic:
· suffices ∀ z, x < z → y ≤ z by ext z; simpa using this z
    intro z hz
    suffices z ∉ Ioo x y by simp_all
    exact fun contra ↦ hxy contra <| h'.out hx hy <| mem_Icc_of_Ioo contra

Goal state after:
case refine_2
α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : ∀ x ∈ I, ∀ y ∈ I, Ioo x y ⊆ Iᶜ → Ioo x y = ∅
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : x < y
z : α
hz : z ∈ Ioo x y
⊢ z ∈ 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 l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hk : P.root k + P.root i = P.root j + (r + 1) • P.root i
⊢ r + 1 ∈ Ioo r s

Tactic:
by simp [contra]

Goal state after:
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
f' : Dual S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB : (LinearMap.BilinMap.toQuadraticMap B.posForm).PosDef
hp : ∀ (i : ↑(baseOf ⇑P.root ↑f)), 0 < f' (v i)
i : ι
hi : i ∈ baseOf ⇑P.root ↑f
j : ι
hj : j ∈ baseOf ⇑P.root ↑f
hij : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ i ≠ j

Tactic:
by aesop

Goal state after:
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)
i : ι
⊢ P.root i ∈ ↑(span ℤ (range fun x ↦ P.root ↑x))

Tactic:
rcases hsp i with hi | hi <;>
      simpa [SetLike.mem_coe, ← Submodule.mem_toAddSubgroup, span_int_eq_addSubgroupClosure,
        ← image_eq_range] using AddSubgroup.le_closure_toAddSubmonoid (P.root '' s) hi

Goal state after:
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
x : ↥(P.rootSpan ℚ)
i : x ∈ range v
⊢ x ∈ range (P.rootSpanMem ℚ)

Tactic:
by aesop

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 : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ ∀ x ∈ b.support, x ∉ {i, j} → f x • P.root x = 0

Tactic:
by aesop

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 : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ Function.support f ⊆ ↑b.support

Tactic:
by aesop

Goal state after:
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
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)
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
i : ι
⊢ ∀ i ∈ s, 0 < f (P.root i)

Tactic:
by aesop

Goal state after:
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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
f : M →+ ℚ
hf : ∀ i ∈ s, f (P.root i) = 1
_i : InvolutiveNeg ι := P.indexNeg
h_card : (baseOf (⇑P.root) f).ncard = s.ncard
hsp : ∀ (i : ι), ∃ z, f (P.root i) = ↑z
i : ι
hi : i ∈ s
⊢ i ∈ {i | 0 < f (P.root i)}

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
h : i ∈ b.support
⊢ b.IsPos i

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

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

Goal state before:
pp: case 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
b : P.Base
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j i
⊢ ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0

Tactic:
exact ⟨j, hj, hj₀.ne'⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos (-i)
j : ι
hj : j ∈ b.support
hj₀ : 0 < P.pairingIn ℤ j (-i)
⊢ P.pairingIn ℤ j i ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: case pred
ι : 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
⊢ p i

Tactic:
rw [isPos_iff] at h₀

Goal state after:
case pred
ι : 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₀ : 0 < b.height i
hN : b.height i = -↑n - 1
⊢ p 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
inst✝ : P.IsReduced
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
g : N →+ ℚ
hg : ∀ (i : ι), g (P.coroot i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
⊢ ∀ (i : ι), 0 < g (P.flip.root i) ↔ 0 < f (P.flip.coroot i)

Tactic:
by aesop

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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j) i)
⊢ b.height ((P.reflectionPerm j) i) < b.height i

Tactic:
have := P.reflection_apply_root' ℤ (i := j) (j := i)

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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι}, b.IsPos i → (b.height i).natAbs = m → p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j) i)
this : (P.reflection j) (P.root i) = P.root i - P.pairingIn ℤ i j • P.root j
⊢ b.height ((P.reflectionPerm j) i) < b.height i
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:
sub_neg_eq_add,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
a : α
h : -f < const a
⊢ (f + const a).Pos
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (-f - -const abv f.lim).LimZero

Tactic:
sub_neg_eq_add,

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (-f + const abv f.lim).LimZero
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f g : Cauchy abs
⊢ { cauchy := f / g } = { cauchy := f } / { cauchy := g }

Tactic:
simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ Matrix.fromBlocks A B C Dᴴ = Matrix.fromBlocks A B C D

Tactic:
hD

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ Matrix.fromBlocks A B C D = Matrix.fromBlocks A B C D
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case succ
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:
exact DivInvMonoid.zpow_neg' _ _

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
this : P.pairingIn ℤ ↑i ↑j ≠ -4
⊢ P.pairingIn ℤ ↑i ↑j ∈ {-3, -2, -1, 0}

Tactic:
by aesop

Goal state after:
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
hq₁ : Q ≤ q
⊢ False

Tactic:
← not_lt

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
hq₁ : ¬q < Q
⊢ 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
d : ↥b.support → ℤ
hd : ∀ (i : ↥b.support), 0 < d i
hdS : (Matrix.diagonal d * b.cartanMatrix).PosDef
aux : ∀ (i j : ↥b.support), b.cartanMatrix i j ≤ if i = j then 2 else 0
⊢ ¬HasEigenvalue (toLin' b.cartanMatrix) 4

Tactic:
have := b.cartanMatrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen d hdS hd 2 4 aux

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
d : ↥b.support → ℤ
hd : ∀ (i : ↥b.support), 0 < d i
hdS : (Matrix.diagonal d * b.cartanMatrix).PosDef
aux : ∀ (i j : ↥b.support), b.cartanMatrix i j ≤ if i = j then 2 else 0
this : HasEigenvalue (toLin' b.cartanMatrix) 4 → 4 < 2 * 2
⊢ ¬HasEigenvalue (toLin' b.cartanMatrix) 4
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ (minpoly R f).IsRoot μ

Tactic:
refine Or.resolve_right (smul_eq_zero.1 ?_) ne0

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ : R
h : f.HasEigenvalue μ
w : M
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ eval μ (minpoly R f) • w = 0
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
⊢ (b₁.h i, b₂.h (eι i)) ∈
    {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪ {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x}

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
i : ι₁
⊢ (b₁.e i, b₂.e (eι i)) ∈
    {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} ∪ {x | ∃ i, (b₁.e i, b₂.e (eι i)) = x} ∪ {x | ∃ i, (b₁.f i, b₂.f (eι i)) = x}

Tactic:
by aesop

Goal state after: