mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f (-1) * f x = f x

Tactic:
map_neg_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ 1 * f x = f x
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ Order.krullDim (Submodule R (M ⧸ N)) = Order.krullDim ↑(Set.Ici N)

Tactic:
Order.krullDim_eq_of_orderIso (Submodule.comapMkQRelIso N)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ Order.krullDim ↑(Set.Ici N) = Order.krullDim ↑(Set.Ici N)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
⊢ ∀ (c : O) {x : O}, x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1 → c • x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1

Tactic:
intro c x

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
c x : O
⊢ x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1 → c • x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Tactic:
simp only [hm, one_mul, pow_zero] at h ⊢

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
h : p ∣ b
⊢ p ∣ 1 ∨ p ∣ b
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 ↔ ringKrullDim R ≤ 0 ∧ 0 ≤ ringKrullDim R

Tactic:
iff_self_and

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ringKrullDim R ≤ 0 → 0 ≤ ringKrullDim R
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : KrullDimLE 0 R
inst✝ : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ IsLocalRing.maximalIdeal R ∈ {J | I ≤ J ∧ J.IsPrime}

Tactic:
exact ⟨IsLocalRing.le_maximalIdeal hI, inferInstance⟩

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
⊢ (addVal R) x = (addVal R) y → Associated x y

Tactic:
intro h
    by_cases hx : x = 0
    · simp_all only [AddValuation.map_zero]
      rw [addVal_eq_top_iff.mp h.symm]
    by_cases hy : y = 0
    · simp_all only [AddValuation.map_zero, associated_zero_iff_eq_zero]
      exact hx (addVal_eq_top_iff.mp h)
    obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
    obtain ⟨m, α, hx'⟩ := eq_unit_mul_pow_irreducible hx hϖ
    obtain ⟨n, β, hy'⟩ := eq_unit_mul_pow_irreducible hy hϖ
    simp only [hx', AddValuation.map_mul, addVal_eq_zero_of_unit, AddValuation.map_pow,
      nsmul_eq_mul, zero_add, hy', associated_unit_mul_right_iff,
      associated_unit_mul_left_iff] at h ⊢
    simp only [addVal_uniformizer hϖ, mul_one, ENat.natCast_inj] at h
    rw [h]
    exact Associates.mk_eq_mk_iff_associated.mp rfl

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

Goal state before:
pp: case h
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
h : v.IsEquiv v'
x : R
hx : v x ≠ 0 ∧ v x ≠ 1
⊢ v' x ≠ 0 ∧ v' x ≠ 1

Tactic:
simpa [← Valuation.IsEquiv.eq_one_iff_eq_one h, ← Valuation.IsEquiv.eq_zero h]

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
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))

Tactic:
simp_rw [mk_mul_mk, associatesEquivIsPrincipal_apply, span_singleton_mul_span_singleton]

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 j k : ι
⊢ P.pairing j ((P.reflectionPerm i) k) = P.pairing ((P.reflectionPerm i) j) k

Tactic:
exact pairing_reflectionPerm P i j k

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✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ IsCompl (P.rootSpan R) (Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator)

Tactic:
simpa only [ker_rootForm_eq_dualAnnihilator] using! P.isCompl_rootSpan_ker_rootForm

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

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ p.flip.toPerfPair (coroot k) = p.flip.toPerfPair ((preReflection α' (p α)) β')

Tactic:
apply Dual.eq_of_preReflection_mapsTo (finite_range root) hsp (hp k) (hs k)

Goal state after:
case hg₁
ι : 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 : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ (p.flip.toPerfPair ((preReflection α' (p α)) β')) (root k) = 2

case hg₂
ι : 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 : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
α : M := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo (⇑(preReflection (root k) (p.flip.toPerfPair ((preReflection α' (p α)) β')))) (range ⇑root) (range ⇑root)
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
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✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : P.root i + P.root j ∈ range ⇑P.root
hij : P.root i = -P.root j
⊢ 0 ∈ range ⇑P.root

Tactic:
rwa [hij, neg_add_cancel] at h

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✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
⊢ LinearIndepOn R (⇑P.coroot) s

Tactic:
obtain ⟨f, hf⟩ : ∃ f : s → Rˣ, ∀ i : s, P.coroot i = f i • P.PolarizationEquiv (P.root i) :=
    ⟨fun i ↦ Units.mk0 (2 / P.RootForm (P.root i) (P.root i))
      (by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]),
     fun i ↦ by simp [coroot_eq_polarizationEquiv_apply_root]⟩

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✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
f : ↑s → Rˣ
hf : ∀ (i : ↑s), P.coroot ↑i = f i • P.PolarizationEquiv (P.root ↑i)
⊢ LinearIndepOn R (⇑P.coroot) s
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup) ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
| inv_mem w' hw' =>

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

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
⊢ range (MulOpposite.op ∘ P.coreflection) ⊆ ↑((Equiv.coweightHom P).domRestrict P.weylGroup).range

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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
· rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, mem_image,
      SetLike.mem_coe]
    use Equiv.reflection P i
    refine ⟨reflection_mem_weylGroup P i, by simp⟩

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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup) ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
| inv_mem w' hw' =>

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

Goal state before:
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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
· rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.coweightHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.coweightHom_apply,
        Equiv.reflection_coweightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.domRestrict_apply, Equiv.coweightHom_apply,
        Equiv.reflection_coweightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using! Subgroup.mul_mem _ h₁ h₂

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

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
⊢ P.weylGroupToPerm ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
| inv_mem w' hw' =>

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
⊢ ⇑(g.weightMap ∘ₗ f.weightMap) ∘ ⇑P.root = ⇑P₂.root ∘ ⇑(f.indexEquiv.trans g.indexEquiv)

Tactic:
ext i
    simp only [LinearMap.coe_comp, Equiv.coe_trans]
    rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]

Goal state after:
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
⊢ genWeightSpace L (-↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) ≠ ⊥

Tactic:
← Int.cast_neg,

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
⊢ genWeightSpace L (↑(-(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))) • ⇑α + ⇑β) ≠ ⊥
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
y : k[G]
r : k
x : k[G]
hx : ((ofMulAction k G G).asAlgebraHom x) y = x * y
⊢ ((ofMulAction k G G).asAlgebraHom (r • x)) y = r • x * y

Tactic:
simp [← hx]

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

Goal state before:
pp: case h.left
ι : 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₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ LeftInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap

Tactic:
refine leftInverse_iff_comp.mpr ?_
        simp only [← @LinearMap.coe_comp]
        rw [← Hom.coweightMap_mul, f.val_inv, Hom.coweightMap_one, LinearMap.id_coe]

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤

Tactic:
replace b : P.root '' Φ ⊆ q := by
      simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using! b

Goal state after:
case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
b : ⇑P.root '' Φ ⊆ ↑q
⊢ q = ⊤
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
hij : P.root i ≠ P.root j
hij' : P.root i ≠ -P.root j
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
by
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
  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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainTopCoeff i j = ⋯.choose.toNat
⊢ ↑n ∈ S ↔ n ≤ chainTopCoeff i j

Tactic:
obtain ⟨hp, h₂ : S = _⟩ :=
    (P.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose_spec

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 : LinearIndependent R ![P.root i, P.root j]
n : ℕ
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}
aux : chainTopCoeff i j = ⋯.choose.toNat
hp : ⋯.choose ≥ 0
h₂ : S = Icc ⋯.choose ⋯.choose
⊢ ↑n ∈ S ↔ n ≤ chainTopCoeff i j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ f i • P.root i + f j • P.root j = P.root i - P.root j

Tactic:
simp [f, hij, sub_eq_add_neg]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
l : ι → ℚ := fun i ↦ ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ l i / l j > 0

Tactic:
simp [hl]

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]
this :
  ∀ (i j : ι),
    LinearIndependent R ![P.root i, P.root j] → ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) ≤ P.pairingIn ℤ j i
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) = P.pairingIn ℤ j i

Tactic:
refine le_antisymm (this i j h) ?_
    specialize this (P.reflectionPerm i i) j (by simpa)
    simp only [chainBotCoeff_reflectionPerm_left, chainTopCoeff_reflectionPerm_left,
      pairingIn_reflectionPerm_self_right] at this
    lia

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
l : ι → ℚ := fun i ↦ ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)
hl : ∀ (i : ι), 0 < l i
⊢ l i / l k > 0

Tactic:
simp [hl]

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₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
pos : 0 < f
contra : ∀ (j : ι), f j = 0
⊢ P.root i = 0

Tactic:
by simp [hf₂, contra]

Goal state after: