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

Goal state before:
pp: case hB
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ ∀ x ∈ range ⇑P.root,
    ∀ y ∈ range ⇑P.root, ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) x) y ∈ (Algebra.linearMap S R).range

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩

Goal state after:
case hB
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i✝ j✝ : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
i j : ι
⊢ ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) (P.root i)) (P.root j) ∈ (Algebra.linearMap S R).range
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
h' : w.IsEquiv u
⊢ h.orderMonoidIso.trans h'.orderMonoidIso = ⋯.orderMonoidIso

Tactic:
by
  ext x
  obtain (rfl | ⟨x, y, _, _, rfl⟩) := x.zero_or_exists_mk
  · simp
  · simp [orderMonoidIso, valueGroup₀Fun_spec h, valueGroup₀Fun_spec h',
      valueGroup₀Fun_spec (trans h h')]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
this : ↑(p j) ⊆ ⋃ i ∈ s, ↑(p i)
⊢ ⋃ i ∈ s, ↑(p i) = univ

Tactic:
by rwa [union_eq_right.mpr this] at hj'

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

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
S : Type u_5
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : FaithfulSMul S R
inst✝¹ : P.IsValuedIn S
inst✝ : P.IsReduced
h : i ≠ j
h' : P.root i ≠ -P.root j
⊢ LinearIndependent R ![P.root i, P.root j]

Tactic:
exact IsReduced.linearIndependent P h h'

Goal state after:
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
n : ℕ
hn : chainLength α β < n
e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), genWeightSpace_ne_bot' := e }
hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)
H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W
H₂ : (1 + n + chainTopCoeff (⇑(-α)) W) • ⇑α + ⇑(chainTop (⇑(-α)) W) = (chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β
this : rootSpace H (-((1 + n + chainTopCoeff (⇑(-α)) W) • ⇑(-α)) + ⇑(chainTop (⇑(-α)) W)) ≠ ⊥
⊢ False

Tactic:
rw [Weight.coe_neg, ← smul_neg, neg_neg, ← Weight.coe_neg, H₂] at this

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
n : ℕ
hn : chainLength α β < n
e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), genWeightSpace_ne_bot' := e }
hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)
H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W
H₂ : (1 + n + chainTopCoeff (⇑(-α)) W) • ⇑α + ⇑(chainTop (⇑(-α)) W) = (chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β
this : rootSpace H ((chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β) ≠ ⊥
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
p : Submodule K M
f : ι → Dual K M
h : ∀ (i : ι), ∃ x ∈ p, (f i) x ≠ 0
⊢ ∃ x ∈ p, ∀ (i : ι), (f i) x ≠ 0

Tactic:
by
  let f' (i : ι) : Dual K p := (f i).domRestrict p
  replace h (i : ι) : ∃ x : p, f' i x ≠ 0 := by obtain ⟨x, hxp, hx₀⟩ := h i; exact ⟨⟨x, hxp⟩, hx₀⟩
  obtain ⟨⟨x, hxp⟩, hx₀⟩ := exists_forall_ne_zero_of_forall_exists f' h
  exact ⟨x, hxp, hx₀⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.a
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α : ¬α.IsZero
⊢ ¬(chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (-⇑α) β

Tactic:
← Weight.coe_neg

Goal state after:
case neg.a
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α : ¬α.IsZero
⊢ ¬(chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.a
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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L (-((↑(chainLength α β) + 1) • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥

Tactic:
← @Nat.cast_one ℤ,

Goal state after:
case neg.a
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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L (-((↑(chainLength α β) + ↑1) • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ polar (⇑(Q₁.prod Q₂)) x y = polar (⇑Q₁) x.1 y.1 + polar (⇑Q₂) x.2 y.2

Tactic:
dsimp [polar]
  abel

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mp
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
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ n ≤ ↑(chainBotCoeff (-⇑α) β)

Tactic:
← Weight.coe_neg

Goal state after:
case mp
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
n : ℤ
hn : rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
⊢ n ≤ ↑(chainBotCoeff (⇑(-α)) β)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

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
inst✝ : Nontrivial M
⊢ IsSimpleOrder (Submodule R[↥P.weylGroup] P.weylGroupRootRep.asModule) ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤

Tactic:
← P.weylGroupRootRep.mapSubmodule.isSimpleOrder_iff

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
inst✝ : Nontrivial M
⊢ IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule ↔
    ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
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
inst✝⁷ : AddCommGroup M₂✝
inst✝⁶ : Module R M₂✝
inst✝⁵ : AddCommGroup N₂✝
inst✝⁴ : Module R N₂✝
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂✝ R M₂✝ N₂✝
ι₂ : 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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ Bijective ⇑(coweightEquiv P Q f).symm

Tactic:
exact LinearEquiv.bijective (coweightEquiv P Q f).symm

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
obtain ⟨si, hsi, hsi'⟩ := (P.posRootForm S).exists_pos_eq 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
inst✝⁸ : Finite ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
hsi' : (algebraMap S R) si = ((P.posRootForm S).form (P.root i)) (P.root i)
⊢ P.coxeterWeightIn S i j ≤ 4
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case h
ι : 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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
f : ↥b.support → ℤ
g : ↥b.support →₀ R := single ⟨i, h⟩ 1
hf :
  (linearCombination R fun k ↦ P.coroot ↑k) g =
    (linearCombination R fun k ↦ P.coroot ↑k) (t • (linearEquivFunOnFinite R R ↥b.support).symm fun x ↦ ↑(f x))
hg : P.coroot i = (linearCombination R fun k ↦ P.coroot ↑k) g
this : Injective ⇑(linearCombination R fun k ↦ P.coroot ↑k)
⊢ ↑(f ⟨i, h⟩) * t = 1

Tactic:
simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm

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]
⊢ {k | P.root j - k • P.root i ∈ range ⇑P.root} = Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j)

Tactic:
ext; rw [← root_sub_zsmul_mem_range_iff h, mem_ofPred_eq]

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

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✝ : CharZero R
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 i ≤ f i

Tactic:
change 0 ≤ f' ⟨i, hi⟩

Goal state after:
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✝ : CharZero R
f✝ : ι → ℤ
hf : ∑ j ∈ b.support, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ ↑b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun i ↦ f ↑i
c : ↑↑b.support → ℕ
hc : ∀ (i : ↥b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 ≤ f' ⟨i, hi⟩
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
f : ι → ℤ
hf : ∑ j ∈ b.support, f j • P.root j ∈ range ⇑P.root
hf₀ : Function.support f ⊆ ↑b.support
⊢ ¬f ≤ 0 ↔ 0 < f

Tactic:
by
  rw [Pi.lt_def]
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at hi⟩
  · rcases b.pos_or_neg_of_sum_smul_root_mem f hf hf₀ with h' | h'
    · exact le_of_lt h'
    · exfalso
      exact h (le_of_lt h')
  · contrapose! h; exact h

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 : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₁ : 0 < f ∨ f < 0
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ b.height i ≠ 0

Tactic:
height_eq_sum 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 : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₁ : 0 < f ∨ f < 0
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ∑ j ∈ b.support, f j ≠ 0
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₀ : 0 < b.height i
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₁ : 0 < f ∨ f < 0
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ¬f < 0

Tactic:
height_eq_sum 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
inst✝ : P.IsCrystallographic
i : ι
contra : ∀ j ∈ b.support, P.pairingIn ℤ j i ≤ 0
f : ι → ℤ
h₀ : 0 < ∑ j ∈ b.support, f j
hf₀ : Function.support f ⊆ ↑b.support
hf₁ : 0 < f ∨ f < 0
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
⊢ ¬f < 0
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 g : CauSeq β abv
⊢ f.lim + -g.lim = (f + -g).lim

Tactic:
← lim_neg,

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 g : CauSeq β abv
⊢ f.lim + (-g).lim = (f + -g).lim
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:
fromBlocks_conjTranspose,

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ᴴ Cᴴ Bᴴ Dᴴ = Matrix.fromBlocks A B C D
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

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

Tactic:
by
  refine ⟨fun h ↦ ?_, (·.neg)⟩
  rw [← neg_neg A]
  exact h.neg

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ (A * B).vec = kroneckerMap (fun x1 x2 ↦ x1 * x2) 1 A *ᵥ B.vec

Tactic:
kronecker_mulVec_vec_of_commute,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ (A * B).vec = (A * B * 1ᵀ).vec

case hB
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ ∀ (x : R) (i j : n), Commute x (1 i j)
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: case inr
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 : ∀ (j : n), (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
⊢ ((b.repr x) j * d j) • b j = μ • (b.repr x) j • b j

Tactic:
· rw [← hj.1, mul_comm, mul_smul]

Goal state after:
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.succ * ↑n.succ) = ((A ^ (m + 1))⁻¹ ^ (n + 1))⁻¹

Tactic:
← Int.natCast_mul,

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.succ * n.succ) = ((A ^ (m + 1))⁻¹ ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
h_mem : ⁅b.e i, b.f i⁆ ∈ H
h_eq : b.h' i = ⟨⁅b.e i, b.f i⁆, h_mem⟩
he : b.e i ∈ rootSpace H ⇑(b.baseSupp i)
x✝ : ↥H
z : L
hz : z ∈ H
⊢ (((toEnd K (↥H) L) ⟨z, hz⟩ - (-⇑(b.baseSupp i)) ⟨z, hz⟩ • 1) ^ 1) (b.f i) = 0

Tactic:
simp [← eq_neg_iff_add_eq_zero]

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

Goal state before:
pp: r : ℕ
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
by
    by_cases h : r = 0
    · simp only [h, zero_mul, zero_add]
    · simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * (-1) ^ 1 * (eval r (descPochhammer R k) * r - ↑k * eval r (descPochhammer R k))

Tactic:
pow_one,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ (-1) ^ k * (eval r (descPochhammer R k) * (-r + ↑k)) =
    (-1) ^ k * -1 * (eval r (descPochhammer R k) * r - ↑k * eval r (descPochhammer R k))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = ∑ j ∈ {x, y}, Lagrange.basis {x, y} id j

Tactic:
sum_insert (notMem_singleton.mpr hxy),

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = Lagrange.basis {x, y} id x + ∑ x_1 ∈ {y}, Lagrange.basis {x, y} id x_1