mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ Associates.mk (p ^ fx.card) = Associates.mk x

Tactic:
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
p : R
hp : Irreducible p
x : R
hx : x ≠ 0
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.replicate fx.card (Associates.mk p)).prod = (Multiset.map Associates.mk fx).prod
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
m n : ℕ
hle : m ≤ n
⊢ Submodule.factorPow I N hle ∘ₗ extend ha f n = extend ha f m

Tactic:
ext
  simp [extend, ← factorPow_comp_eq_of_factorPow_comp_succ_eq ha f hf hle]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ Associates.mk x = Associates.mk (ϖ ^ fx.card)

Tactic:
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.map Associates.mk fx).prod = (Multiset.replicate fx.card (Associates.mk ϖ)).prod
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (x + -y) = v x

Tactic:
map_add_eq_of_lt_left

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v x = v x

case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v y < v x
⊢ v (-y) < v x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ m = n

Tactic:
by
  have key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod := by
    rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]
    refine ⟨u * v⁻¹, ?_⟩
    simp only [Units.val_mul]
    rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]
  have := by
    refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)
    all_goals
      intro x hx
      obtain rfl := Multiset.eq_of_mem_replicate hx
      assumption
  simpa only [Multiset.card_replicate]

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
h : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) ≠ ⊤
m : R
hm : m ∈ ↑(maximalIdeal R)
k : R
hk : k * a = b * m
hk' : x * (algebraMap R K) m = (algebraMap R K) k
⊢ x * (algebraMap R K) m ∈ M

Tactic:
exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates ↥R⁰
⊢ ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) =
    ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x) * ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) y)

Tactic:
by
  simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_mul, Submonoid.coe_mul,
    associatesEquivIsPrincipal_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
⊢ x ≠ 0

Tactic:
by rwa [Ne, ← IsPrincipal.eq_bot_iff_generator_eq_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ (Ideal.Quotient.mk P') z = 0

Tactic:
rwa [Quotient.eq_zero_iff_mem, mem_comap, hPJ, mem_comap, coe_mapRingHom, map_C]

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ Flat R M ↔ torsion R M = ⊥

Tactic:
refine ⟨fun _ ↦ torsion_eq_bot, ?_⟩
  -- now assume R is a Bezout domain and M is a torsionfree R-module
  intro htors
  -- we need to show that if I is an ideal of R then the natural map I ⊗ M → M is injective
  rw [iff_lift_lsmul_comp_subtype_injective]
  rintro I hFG
  -- If I = 0 this is obvious because I ⊗ M is a subsingleton (i.e. has ≤1 element)
  obtain (rfl | h) := eq_or_ne I ⊥
  · rintro x y -
    apply Subsingleton.elim
  · -- If I ≠ 0 then I ≅ R because R is Bezout and I is finitely generated
    have hprinc : I.IsPrincipal := IsBezout.isPrincipal_of_FG I hFG
    have : IsPrincipal.generator I ≠ 0 := by
      rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
    apply Function.Injective.of_comp_right _
      (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective
    rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp, LinearEquiv.coe_rTensor, rTensor,
      lift_comp_map, LinearMap.compl₂_id, LinearMap.comp_assoc,
      Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul,
      LinearMap.coe_comp]
    rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at htors
    refine Function.Injective.comp (LinearMap.lsmul_injective this) ?_
    rw [← Equiv.injective_comp (TensorProduct.lid R M).symm.toEquiv]
    convert! Function.injective_id
    ext
    simp

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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i : ι
⊢ (((span K (range ⇑P.root)).subtype.restrictScalarsRange₂ (span K (range ⇑P.coroot)).subtype (Algebra.linearMap K L) ⋯
          P.toLinearMap ⋯)
        ({ toFun := fun i ↦ ⟨P.root i, ⋯⟩, inj' := ⋯ } i))
      ({ toFun := fun i ↦ ⟨P.coroot i, ⋯⟩, inj' := ⋯ } i) =
    2

Tactic:
by
    have : algebraMap K L 2 = 2 := by
      rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
    exact FaithfulSMul.algebraMap_injective K L <| by simp [this]

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

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
B : P.InvariantForm
i j : ι
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

Tactic:
by
  calc B.form (P.root i) (P.root j) = 0
      ↔ 2 * B.form (P.root i) (P.root j) = 0 := by simp [two_ne_zero]
    _ ↔ P.pairing i j * B.form (P.root j) (P.root j) = 0 := by rw [B.two_mul_apply_root_root i j]
    _ ↔ P.pairing i j = 0 := by simp [B.ne_zero j]

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

Goal state before:
pp: ι : 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
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⋯
rj : ↥(span S (range ⇑P.root)) := ⋯
⊢ (algebraMap S R) (2 * (B.posForm ri) rj) = (algebraMap S R) (P.pairingIn S i j * (B.posForm rj) rj)

Tactic:
simpa [map_ofNat] using B.toInvariantForm.two_mul_apply_root_root i j

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
this : IsTorsionFree S N
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.PolarizationIn S).range

Tactic:
refine LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S)
    (LinearMap.range (M₂ := N) (P.PolarizationIn S))
    (smul_right_injective N h_ne) ?_

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
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
⊢ ∀ x ∈ P.corootSpan S,
    (∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) • x ∈ (P.PolarizationIn S).range
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
this : IsTorsionFree S N
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan S
c : ι → S
hc : ∑ i, c i • P.coroot i = x✝
⊢ ∑ x, (∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) • c x • P.coroot x ∈ (P.PolarizationIn S).range

Tactic:
simp_rw [smul_smul, mul_comm, ← smul_smul]

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
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan S
c : ι → S
hc : ∑ i, c i • P.coroot i = x✝
⊢ ∑ x, c x • (∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) • P.coroot x ∈ (P.PolarizationIn S).range
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
⊢ ¬chainLength α β < chainTopCoeff (⇑α) β

Tactic:
← Nat.succ_le_iff

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
⊢ ¬(chainLength α β).succ ≤ chainTopCoeff (⇑α) β
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
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β
⊢ False

Tactic:
apply genWeightSpace_nsmul_add_ne_bot_of_le α β
    (Nat.sub_le (chainTopCoeff α β) (chainLength α β).succ)

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
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α) β
⊢ genWeightSpace L ((chainTopCoeff (⇑α) β - (chainLength α β).succ) • ⇑α + ⇑β) = ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

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

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
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 : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ x = y

Tactic:
simp_rw [hx, hy, neg_smul, Finset.sum_neg_distrib, ← add_eq_zero_iff_eq_neg]

Goal state after:
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), 0 < f (v i)
hn : Pairwise fun i j ↦ (B (v i)) (v j) ≤ 0
s : Finset ι
c : ι → R
hc : ∑ i ∈ s, c i • v i = 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∑ i ∈ s with 0 < c i, c i • v i + ∑ x ∈ s with 0 < -c x, c x • v x = 0
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
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ chainLength α β' = chainLength α β

Tactic:
by
  by_cases hα : α.IsZero
  · rw [chainLength_of_isZero _ _ hα, chainLength_of_isZero _ _ hα]
  · 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: 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
⊢ chainLength α 0 = 2

Tactic:
by
  rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α hα]

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

Goal state before:
pp: case inr.inr.refine_1
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
⊢ ↑n ≤ ↑(chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β)

Tactic:
chainBotCoeff_add_chainTopCoeff,

Goal state after:
case inr.inr.refine_1
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = 2 * n + 1
H : k * 2 / 2 = ↑(↑(2 * n + 1) - 2 * ↑(chainTopCoeff (⇑α) β)) / 2
hk : k = ↑n + 2⁻¹ - ↑(chainTopCoeff (⇑α) β)
⊢ ↑n ≤ ↑(chainLength α β)
Module: Mathlib.RepresentationTheory.Basic

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
r : k
x : V
⊢ ρ.asModuleEquiv.symm (r • x) = (algebraMap k k[G]) r • ρ.asModuleEquiv.symm x

Tactic:
rw [LinearEquiv.symm_apply_eq]
  simp

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

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
g : G
x : V
⊢ ρ.asModuleEquiv.symm ((ρ g) x) = (of k G) g • ρ.asModuleEquiv.symm x

Tactic:
rw [LinearEquiv.symm_apply_eq]
  simp

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

Goal state before:
pp: case coweightMap
ι : 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 : (coweightHom P) f = (coweightHom P) g
x : N
⊢ f.coweightMap x = g.coweightMap x

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 : (coweightHom P) f = (coweightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
· dsimp [coweightHom] at hfg
    simp_all

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 : (coweightHom P) f = (coweightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : Semiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
g h : G
hgh : ↑g = ↑h
⊢ ρ g = ρ h

Tactic:
by
  ext x
  apply (ρ.apply_bijective g⁻¹).1
  simpa [← Module.End.mul_apply, ← map_mul, -isTrivial_def] using
    (congr($(isTrivial_def (ρ.comp S.subtype) ⟨g⁻¹ * h, QuotientGroup.eq.1 hgh⟩) x)).symm

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✝ : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
⊢ P.root i ≠ -P.root j

Tactic:
intro contra
  have := linearIndepOn_iff'.mp b.linearIndepOn_root ({i, j} : Finset ι) 1
    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
  simp_all

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
⊢ Injective fun z ↦ Exists.choose ⋯

Tactic:
intro ⟨z, hz⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
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
z : ℤ
hz : z ∈ S
⊢ ∀ ⦃a₂ : ↑S⦄, (fun z ↦ Exists.choose ⋯) ⟨z, hz⟩ = (fun z ↦ Exists.choose ⋯) a₂ → ⟨z, hz⟩ = a₂