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

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) -
      φ' ((algebraMap (R ⧸ P') Rₘ) ((Ideal.Quotient.mk P') (p.coeff 0))) =
    0

Tactic:
sub_eq_zero,

Goal state after:
case refine_1.inr
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = C (p.coeff 0)
⊢ ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P)) (C (p.coeff 0)) =
    φ' ((algebraMap (R ⧸ P') Rₘ) ((Ideal.Quotient.mk P') (p.coeff 0)))
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ IsDedekindDomain Aₘ

Tactic:
by
  have h : ∀ y : M, IsUnit (algebraMap A (FractionRing A) y) := by
    rintro ⟨y, hy⟩
    exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
  let : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (IsLocalization.lift h)
  have : IsScalarTower A Aₘ (FractionRing A) :=
    IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
  have : IsFractionRing Aₘ (FractionRing A) :=
    IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
  refine (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨?_, ?_, ?_, ?_⟩
  · infer_instance
  · exact IsLocalization.isNoetherianRing M _ inferInstance
  · exact Ring.DimensionLEOne.localization Aₘ hM
  · intro x hx
    obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
    obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegralClosure hy
    refine ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
    rw [hz, ← Algebra.smul_def]
    rfl

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
S : Type u_6
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i : ι
⊢ (algebraMap S R) (P.pairingIn S i i) = (algebraMap S R) 2

Tactic:
by simp [map_ofNat]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
⊢ f.Finite

Tactic:
algebraize [f]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite
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
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i j k l : ι
x y : S
h : P.root k = x • P.root i + y • P.root l
⊢ P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j

Tactic:
by
  apply FaithfulSMul.algebraMap_injective S R
  replace h : P.root k = (algebraMap S R x) • P.root i + (algebraMap S R y) • P.root l := by simpa
  simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using
    pairing_eq_add_of_root_eq_smul_add_smul h

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

Goal state before:
pp: case h
ι : 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 : ι
⊢ (algebraMap S R) ((algebraMap T S) (P.pairingIn T i j)) = P.pairing i j

Tactic:
simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]

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

Goal state before:
pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Ring R
v : Valuation R Γ₀
h : v.IsEquiv v
x y : R
w✝¹ : (ofClass v) x ≠ 0
w✝ : (ofClass v) y ≠ 0
⊢ h.orderMonoidIso ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝) =
    (OrderMonoidIso.refl (ofClass v).ValueGroup₀) ↑(valueGroup.mk (ofClass v) x y w✝¹ w✝)

Tactic:
simp [orderMonoidIso, valueGroup₀Fun_spec h]

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

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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
j : ι
hj : ↑n = 1
⊢ False

Tactic:
have : 2 ≤ n := Nat.AtLeastTwo.prop

Goal state after:
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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
j : ι
hj : ↑n = 1
this : 2 ≤ n
⊢ False
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : α.IsZero
⊢ 0 = ⁅0, x⁆

Tactic:
zero_lie

Goal state after:
case pos
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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : α.IsZero
⊢ 0 = 0
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 α β) - (chainTop (⇑α) β) (coroot α) = 0
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
sub_eq_zero,

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 α β) = (chainTop (⇑α) β) (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x✝ : P.pairing i j = 2 ∧ P.pairing j i = 2
h₁ : P.pairing i j = 2
h₂ : P.pairing j i = 2
this : P.pairing j i • P.root i = 2 • P.root j
⊢ i = j

Tactic:
exact P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ this)

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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
ι : 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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
x✝ : P.pairing i j = 1 ∧ P.pairing j i = 4
h₁ : P.pairing i j = 1
h₂ : P.pairing j i = 4
⊢ P.root j = 2 • P.root i

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
i j : ι
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.root j = 2 • P.root i
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x : M × M
⊢ ⅟2 (2 * (Q x.1 - Q x.2)) = Q x.1 - Q x.2

Tactic:
← Module.End.smul_def

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x : M × M
⊢ ⅟2 • (2 * (Q x.1 - Q x.2)) = Q x.1 - Q x.2
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
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
hα : ¬α.IsZero
⊢ chainLength α β' = chainLength α β

Tactic:
· apply Nat.cast_injective (R := ℤ)
    rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]

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

Goal state before:
pp: case neg.inl
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α : ¬α.IsZero
h : ⇑β = -1 • ⇑α
⊢ β = -α ∨ β = α

pp: case neg.inr.inl
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α : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α

pp: case neg.inr.inr
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α : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
· exact .inl (by ext; rw [h, neg_one_smul]; rfl)

Goal state after:
case neg.inr.inl
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α : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β = -α ∨ β = α

case neg.inr.inr
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α : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α
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
q : Submodule k[G] ρ.asModule
⊢ (fun p ↦
        let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
      ((fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩) q) =
    q

Tactic:
ext; aesop

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

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y)
⊢ y = g.indexEquiv x

Tactic:
coroot_coweightMap_apply,

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : P.coroot (f.indexEquiv.symm y) = g.coweightMap (P.coroot y)
⊢ y = g.indexEquiv x
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : P.coroot (f.indexEquiv.symm y) = g.coweightMap (P.coroot y)
⊢ y = g.indexEquiv x

Tactic:
coroot_coweightMap_apply,

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : P.coroot (f.indexEquiv.symm y) = P.coroot (g.indexEquiv.symm y)
⊢ y = g.indexEquiv x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case pred
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : ∀ (a : G), (((leftRegular k G) g) x).coeff a = x.coeff a
n : ℕ
h : x.coeff ((fun x ↦ g ^ x) (-↑n)) = x.coeff g
⊢ x.coeff ((fun x ↦ g ^ x) (-↑n - 1)) = x.coeff g

Tactic:
simpa [zpow_sub, ← h, ← mul_inv_rev, ← pow_mul_comm'] using hx (g ^ (-n : ℤ))

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✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : k[G]
x : V
y : W
⊢ (r.coeff.sum fun i d ↦ d • x ⊗ₜ[k] (ρW i) y) = x ⊗ₜ[k] r.coeff.sum fun i d ↦ d • (ρW i) y

Tactic:
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]

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 : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
this : ∀ (g : ↥P.weylGroup), q ∈ invtSubmodule (P.weylGroupRootRep g)
⊢ q = ⊤

Tactic:
let q' : P.weylGroupRootRep.invtSubmodule :=
        ⟨q, (Representation.mem_invtSubmodule P.weylGroupRootRep).mpr this⟩

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
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
this : ∀ (g : ↥P.weylGroup), q ∈ invtSubmodule (P.weylGroupRootRep g)
q' : ↥P.weylGroupRootRep.invtSubmodule := ⟨q, ⋯⟩
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_1
ι : 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✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i j : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ∈ invtSubmodule ↑(P.reflection j)

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
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ≠ ⊥

Tactic:
· let g : P.weylGroup := ⟨Equiv.reflection P j, P.reflection_mem_weylGroup j⟩
    exact Module.End.span_orbit_mem_invtSubmodule R (P.root i) g

Goal state after:
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
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
i : ι
⊢ span R (orbit (↥P.weylGroup) (P.root i)) ≠ ⊥
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 : si > 0
hsi' : (algebraMap S R) si = ((P.posRootForm S).form (P.root i)) (P.root i)
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
obtain ⟨sj, hsj, hsj'⟩ := (P.posRootForm S).exists_pos_eq j

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)
sj : S
hsj : sj > 0
hsj' : (algebraMap S R) sj = ((P.posRootForm S).form (P.root j)) (P.root j)
⊢ P.coxeterWeightIn S i j ≤ 4
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
i j : ↥b.support
hij : i ≠ j
⊢ {↑j, ↑i} ⊆ ↑b.support

Tactic:
simp [pair_subset_iff]

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 ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

Tactic:
have : Nonempty ι := ⟨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 ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)