mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case hf.hf
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ Q'.IsMaximal

Tactic:
apply Polynomial.isMaximal_comap_C_of_isJacobsonRing

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P))

Tactic:
apply Function.Surjective.comp Quotient.mk_surjective

Goal state after:
case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R))
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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_6
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
T : Type u_7
inst✝⁴ : CommRing T
inst✝³ : Algebra T S
inst✝² : Algebra T R
inst✝¹ : IsScalarTower T S R
inst✝ : P.IsValuedIn T
i j : ι
⊢ ∃ s, (algebraMap S R) s = P.pairing i j

Tactic:
by
    use algebraMap T S (P.pairingIn T i j)
    simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ P.rootSpan R ∈ End.invtSubmodule ↑(P.reflection i)

Tactic:
rw [Module.End.mem_invtSubmodule, rootSpan]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ span R (range ⇑P.root) ≤ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
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
x y : R
w✝¹ : (ofClass v) x ≠ 0
w✝ : (ofClass v) y ≠ 0
⊢ (h.orderMonoidIso.trans h'.orderMonoidIso) ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝) =
    ⋯.orderMonoidIso ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝)

Tactic:
· simp [orderMonoidIso, valueGroup₀Fun_spec h, valueGroup₀Fun_spec h',
      valueGroup₀Fun_spec (trans h h')]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
⊢ v.IsEquiv v'

Tactic:
intro x y
  obtain rfl | hy := eq_or_ne y 0
  · simp
  · rw [← div_le_one₀, ← v.map_div, h, v'.map_div, div_le_one₀] <;>
      rwa [zero_lt_iff, ne_zero_iff]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.PolarizationIn S).range

Tactic:
have : Module.IsTorsionFree S N := .trans_faithfulSMul S R N

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R N
this : IsTorsionFree S N
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.PolarizationIn S).range
Module: Mathlib.LinearAlgebra.RootSystem.Basic

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ P₂.coroot i = P₁.coroot i

Tactic:
apply P₁.flip.toPerfPair.injective

Goal state after:
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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
hP₁ : P₁.IsRootSystem
hP₂ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
i : ι
⊢ P₁.flip.toPerfPair (P₂.coroot i) = P₁.flip.toPerfPair (P₁.coroot i)
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : OrzechProperty R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
spans : (Finsupp.linearCombination R b).range = ⊤
card_le : Fintype.card ι ≤ finrank R M
⊢ LinearIndependent R b

Tactic:
LinearMap.range_eq_top

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : OrzechProperty R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
spans : Function.Surjective ⇑(Finsupp.linearCombination R b)
card_le : Fintype.card ι ≤ finrank R M
⊢ LinearIndependent R b
Module: Mathlib.LinearAlgebra.Dimension.OrzechProperty

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(map (span R (Set.range b)).subtype (span R (Set.range fun i ↦ ⟨b i, ⋯⟩)))

Tactic:
← span_image,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : OrzechProperty R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
ι : Type u_3
inst✝ : Fintype ι
b : ι → M
hc : Fintype.card ι = Set.finrank R (Set.range b)
x✝¹ : ↥(span R (Set.range b))
val✝ : M
property✝ : val✝ ∈ span R (Set.range b)
x✝ : ⟨val✝, property✝⟩ ∈ ⊤
⊢ (span R (Set.range b)).subtype ⟨val✝, property✝⟩ ∈
    ↑(span R (⇑(span R (Set.range b)).subtype '' Set.range fun i ↦ ⟨b i, ⋯⟩))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
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
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = (↑(chainTopCoeff (⇑α) β) * ⇑α + ⇑β) (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
Pi.natCast_def,

Goal state after:
case neg
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
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = ((fun x ↦ ↑(chainTopCoeff (⇑α) β)) * ⇑α + ⇑β) (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
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:
← smul_neg,

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 ((1 + n + chainTopCoeff (-⇑α) W) • - -⇑α + ⇑(chainTop (-⇑α) W)) ≠ ⊥
⊢ False
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case 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 : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H (-(↑(chainBotCoeff (⇑α) β).succ • ⇑α) + ⇑β) = ⊥

Tactic:
← smul_neg,

Goal state after:
case 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 : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H (↑(chainBotCoeff (⇑α) β).succ • -⇑α + ⇑β) = ⊥
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
⊢ rootSpace H (2⁻¹ • ⇑α) = ⊥

Tactic:
by_contra h

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
h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥
⊢ False
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: case refine_1
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
h : Nontrivial ↥ρ.invtSubmodule
⊢ Nontrivial V

pp: case refine_2
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
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule

Tactic:
· contrapose! h
    infer_instance

Goal state after:
case refine_2
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
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case add
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
⊢ ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v

Tactic:
intro y z hy hz
      simp [add_smul, hy, hz]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ (ρV (g * h)).prodMap (ρW (g * h)) = (ρV g).prodMap (ρW g) * (ρV h).prodMap (ρW h)

Tactic:
simp [prodMap_mul]

Goal state after:
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
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
this : ↑q = ⊤
⊢ q = ⊥ ∨ q = ⊤

Tactic:
by right; simpa using this

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: x✝ : Set ℤ
hn : x✝.Nonempty
hb : BddAbove x✝
⊢ IsLUB x✝ (if h : x✝.Nonempty ∧ BddAbove x✝ then ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) else 0)

Tactic:
by
    rw [dif_pos ⟨hn, hb⟩]
    exact (isGreatest_coe_greatestOfBdd ..).isLUB

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
si : S
hsi : li > 0
sj : S
hsj : lj > 0
hsi' : si = li
hsj' : sj = lj
cs : 4 * lij ^ 2 ≤ 4 * (li * lj)
key : 4 * lij ^ 2 = P.coxeterWeightIn S i j * (li * lj)
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rwa [key, mul_le_mul_iff_left₀ (by positivity)] at cs

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 : ∀ (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 : ι
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
hl : P.root l - P.root i = P.root j + (s - 1) • P.root i
⊢ s - 1 ∈ Ioo r s

Tactic:
simp [lt_sub_right_of_add_lt contra]

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

pp: case neg
ι : 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⟩
      simp [← hc]

Goal state after:
case neg
ι : 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
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
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
pos : 0 < f
⊢ False

Tactic:
simpa [hij, f] using le_of_lt pos j

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
⊢ ⊤ ≤ span ℤ (range fun i ↦ P.rootSpanMem ℤ ↑i)

Tactic:
have : (fun i : b.support ↦ P.rootSpanMem ℤ i) = P.rootSpanMem ℤ ∘ ((↑) : b.support → ι) := rfl

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
this : (fun i ↦ P.rootSpanMem ℤ ↑i) = P.rootSpanMem ℤ ∘ Subtype.val
⊢ ⊤ ≤ span ℤ (range fun i ↦ P.rootSpanMem ℤ ↑i)
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
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
neg : f < 0
⊢ ∑ j ∈ b.support, f j ≠ 0

Tactic:
· refine (Finset.sum_neg' (fun i _ ↦ neg.le i) ?_).ne
    by_contra! contra
    replace contra (j : ι) : f j = 0 := by
      by_cases hj : j ∈ f.support
      · exact le_antisymm (neg.le j) (contra j (hf₀ hj))
      · simpa using hj
    exact P.ne_zero i <| by simp [hf₂, contra]

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

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

Tactic:
rw [mk_le]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Completion

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

Tactic:
rw [coe_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 g : CauSeq β abv
⊢ ↑(const abv (f.lim * g.lim) - f * g) = ↑((const abv f.lim - f) * g) + ↑(const abv f.lim * (const abv g.lim - g))
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
f : n ≃ m
⊢ (A.submatrix ⇑f.symm ⇑f.symm).IsHermitian

Tactic:
apply submatrix h

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ ((Matrix.fromBlocks A B Bᴴ D).submatrix Sum.swap Sum.swap).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
fromBlocks_submatrix_sum_swap_sum_swap

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
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
⊢ IsUnit M

Tactic:
by_contra h

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
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ ((fromBlocks A B Bᴴ D).submatrix Sum.swap Sum.swap).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

Tactic:
fromBlocks_submatrix_sum_swap_sum_swap

Goal state after:
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype n
inst✝³ : StarOrderedRing R'
inst✝² : Finite m
inst✝¹ : DecidableEq n
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hD : D.PosDef
inst✝ : Invertible D
⊢ (fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
i j : ↥b.support
h : i ≠ j
⊢ |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j

Tactic:
simpa [h] using b.cartanMatrix_le_zero_of_ne i j h

Goal state after: