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

Goal state before:
pp: case pos.refine_1
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
hx : ∀ y ∈ M, x * y ∈ M
⊢ M ≠ ⊥

pp: case pos.refine_2
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
hx : ∀ y ∈ M, x * y ∈ M
⊢ M.FG

Tactic:
· rw [Submodule.ne_bot_iff]; refine ⟨_, ⟨a, ha₁, rfl⟩, ?_⟩
      exact (IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂

Goal state after:
case pos.refine_2
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
hx : ∀ y ∈ M, x * y ∈ M
⊢ M.FG
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
⊢ ⊥.jacobson = ⊥

Tactic:
have hR' : IsJacobsonRing (R ⧸ P') := by infer_instance

Goal state after:
case neg
R : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst✝ : P.IsPrime
hP : ∀ (x : R), C x ∈ P → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap C P
this : P'.IsPrime
hR' : IsJacobsonRing (R ⧸ P')
⊢ ⊥.jacobson = ⊥
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:
simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_mul, Submonoid.coe_mul,
    associatesEquivIsPrincipal_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson = I

Tactic:
refine le_antisymm ?_ le_jacobson

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson ≤ I
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
h : ringKrullDim R < 1
⊢ False

Tactic:
· have : KrullDimLE 0 R := krullDimLE_iff.mpr (ENat.WithBot.lt_add_one_iff.mp h)
    exact IsDiscreteValuationRing.not_isField R KrullDimLE.isField_of_isDomain

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

Goal state before:
pp: 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
⊢ (algebraMap R (T ⧸ P)).IsIntegral

Tactic:
let Q := P.comap v.toAlgHom.toRingHom

Goal state after:
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] := comap (↑v).toRingHom P
⊢ (algebraMap R (T ⧸ P)).IsIntegral
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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✝ : Fintype ι
i : ι
x y : M
⊢ ∑ x_1, (P.coroot' ((P.reflectionPerm i) x_1)) x * (P.coroot' ((P.reflectionPerm i) x_1)) y =
    ∑ i, (P.coroot' i) x * (P.coroot' i) y

Tactic:
exact Fintype.sum_equiv (P.reflectionPerm i)
    (fun j ↦ (P.coroot' (P.reflectionPerm i j) x) * (P.coroot' (P.reflectionPerm i j) y))
    (fun j ↦ P.coroot' j x * P.coroot' j y) (congrFun rfl)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower S R M
inst✝³ : Module S N
inst✝² : IsScalarTower S R N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
i : ι
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i = 2 • (P.PolarizationIn S) (P.rootSpanMem S i)

Tactic:
by
  have hP : P.PolarizationIn S (P.rootSpanMem S i) =
      ∑ j : ι, P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j) := by
    simp_rw [PolarizationIn_apply, coroot'In_rootSpanMem_eq_pairingIn]
    exact (Fintype.sum_equiv (P.reflectionPerm i)
          (fun j ↦ P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j))
          (fun j ↦ P.pairingIn S i j • P.coroot j) (congrFun rfl)).symm
  rw [two_nsmul]
  nth_rw 2 [hP]
  rw [PolarizationIn_apply]
  simp only [coroot'In_rootSpanMem_eq_pairingIn, pairingIn_reflectionPerm,
    pairingIn_reflectionPerm_self_left, ← reflectionPerm_coroot, neg_smul,
    smul_sub, sub_neg_eq_add]
  rw [Finset.sum_add_distrib, ← add_assoc, ← sub_eq_iff_eq_add, RootFormIn]
  simp only [LinearMap.coe_sum, LinearMap.coe_smulRight, Finset.sum_apply,
    coroot'In_rootSpanMem_eq_pairingIn, LinearMap.smul_apply, smul_eq_mul, Finset.sum_smul,
    root_coroot_eq_pairing, Finset.sum_neg_distrib, add_neg_cancel, sub_eq_zero]
  refine Finset.sum_congr rfl ?_
  intro j hj
  rw [← P.algebraMap_pairingIn S, IsScalarTower.algebraMap_smul, ← mul_smul]

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

Goal state before:
pp: case neg.mp.inr
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
x : K
hx : ¬x = 0
hh : (v x)⁻¹ = 1
h_1 : ¬v' x = 1
h_2 : 1 < v' x
⊢ False

Tactic:
← map_inv₀

Goal state after:
case neg.mp.inr
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
x : K
hx : ¬x = 0
hh : v x⁻¹ = 1
h_1 : ¬v' x = 1
h_2 : 1 < v' x
⊢ False
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg.mpr.inr
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
x : K
hx : ¬x = 0
hh : (v' x)⁻¹ = 1
h_1 : ¬v x = 1
h_2 : 1 < v x
⊢ False

Tactic:
← map_inv₀

Goal state after:
case neg.mpr.inr
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
x : K
hx : ¬x = 0
hh : v' x⁻¹ = 1
h_1 : ¬v x = 1
h_2 : 1 < v x
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

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
h : ∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j
i j : ι
hij : i ≠ j
hLin : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i = -P.root 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
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i = P.root j ∨ P.root i = -P.root j

Tactic:
· specialize h i j hLin
    simp_all

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
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root i = P.root j ∨ P.root i = -P.root j
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
⊢ ↑(((P.flip ∘ₗ P.Polarization).linearEquivOfInjective ⋯ ⋯).trans P.flip.toPerfPair.symm) = P.Polarization

Tactic:
ext m

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
m : M
⊢ ↑(((P.flip ∘ₗ P.Polarization).linearEquivOfInjective ⋯ ⋯).trans P.flip.toPerfPair.symm) m = P.Polarization m
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
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥

Tactic:
by
  by_contra e
  let W : Weight K H L := ⟨_, e⟩
  have hW : (W : H → K) = -(n • α) + chainTop α β := rfl
  have H₁ : 1 + n + chainTopCoeff (-α) W ≤ chainLength (-α) W := by
    have := apply_coroot_eq_cast' (-α) W
    simp only [coroot_neg, map_neg, hW, nsmul_eq_mul, Pi.natCast_def, coe_chainTop, zsmul_eq_mul,
      Int.cast_natCast, Pi.add_apply, Pi.neg_apply, Pi.mul_apply, root_apply_coroot hα, mul_two,
      apply_coroot_eq_cast' α β, Int.cast_sub, Int.cast_mul, Int.cast_ofNat, mul_comm (2 : K),
      add_sub_cancel, add_sub, Nat.cast_inj, eq_sub_iff_add_eq, ← Nat.cast_add, ← sub_eq_neg_add,
      sub_eq_iff_eq_add] at this
    lia
  have H₂ : ((1 + n + chainTopCoeff (-α) W) • α + chainTop (-α) W : H → K) =
      (chainTopCoeff α β + 1) • α + β := by
    simp only [Weight.coe_neg, ← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_add, Nat.cast_one, coe_chainTop,
      smul_neg, ← neg_smul, hW, ← add_assoc, ← add_smul, ← sub_eq_add_neg]
    congr 2
    ring
  have := rootSpace_neg_nsmul_add_chainTop_of_le (-α) W H₁
  rw [Weight.coe_neg, ← smul_neg, neg_neg, ← Weight.coe_neg, H₂] at this
  exact this (genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα)

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

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

Tactic:
obtain ⟨⟨x, hxp⟩, hx₀⟩ := exists_forall_ne_zero_of_forall_exists f' h

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
p : Submodule K M
f : ι → Dual K M
f' : ι → Dual K ↥p := fun i ↦ LinearMap.domRestrict (f i) p
h : ∀ (i : ι), ∃ x, (f' i) x ≠ 0
x : M
hxp : x ∈ p
hx₀ : ∀ (i : ι), (f' i) ⟨x, hxp⟩ ≠ 0
⊢ ∃ x ∈ p, ∀ (i : ι), (f i) x ≠ 0
Module: Mathlib.Algebra.Module.Submodule.Union

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

Tactic:
by
  refine Dual.exists_forall_ne_zero_of_forall_exists (fun i ↦ Dual.eval K M (v i)) fun i ↦ ?_
  by_contra! contra
  simp_rw [Dual.eval_apply, forall_dual_apply_eq_zero_iff] at contra
  exact hv i contra

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

Goal state before:
pp: case neg.a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L ((↑(chainLength α β) - ↑(chainTopCoeff (⇑α) β) + 1) • ⇑(-α) + ⇑β) = ⊥

Tactic:
LieModule.Weight.coe_neg,

Goal state after:
case neg.a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L ((↑(chainLength α β) - ↑(chainTopCoeff (⇑α) β) + 1) • -⇑α + ⇑β) = ⊥
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 : ℤ
⊢ -n ≤ ↑(chainBotCoeff (⇑α) β) ∧ n ≤ ↑(chainTopCoeff (⇑α) β) ↔
    -↑(chainBotCoeff (⇑α) β) ≤ n ∧ n ≤ ↑(chainTopCoeff (⇑α) β)

Tactic:
neg_le

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 : ℤ
⊢ -↑(chainBotCoeff (⇑α) β) ≤ n ∧ n ≤ ↑(chainTopCoeff (⇑α) β) ↔
    -↑(chainBotCoeff (⇑α) β) ≤ n ∧ n ≤ ↑(chainTopCoeff (⇑α) β)
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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✝ : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
i : ι
this : Equiv.reflection P i ^ 2 = 1
⊢ pred 1 ⋯

Tactic:
simpa [sq, ← this] using mul _ _ _ _ (mem i) (mem i)

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mp
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
g : G
x y : V
⊢ (ρ g⁻¹) x = y → x = (ρ g) y

Tactic:
rintro rfl

Goal state after:
case mp
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
g : G
x : V
⊢ x = (ρ g) ((ρ g⁻¹) x)
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case mpr
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
g : G
x y : V
⊢ x = (ρ g) y → (ρ g⁻¹) x = y

Tactic:
rintro rfl

Goal state after:
case mpr
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
g : G
y : V
⊢ (ρ g⁻¹) ((ρ g) y) = y
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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.InvariantForm
g : P.Aut
hg : g ∈ P.weylGroup
⊢ ∀ (x y : M), (B.form (⟨g, hg⟩ • x)) (⟨g, hg⟩ • y) = (B.form x) y

Tactic:
induction hg using weylGroup.induction with

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₁
i : ι
⊢ ((⇑g.weightMap ∘ ⇑f.weightMap) ∘ ⇑P.root) i = (⇑P₂.root ∘ ⇑g.indexEquiv ∘ ⇑f.indexEquiv) i

Tactic:
comp_assoc,

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
ι₁ : 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₁
i : ι
⊢ (⇑g.weightMap ∘ ⇑f.weightMap ∘ ⇑P.root) i = (⇑P₂.root ∘ ⇑g.indexEquiv ∘ ⇑f.indexEquiv) i
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₁
i : ι₂
⊢ ((⇑f.coweightMap ∘ ⇑g.coweightMap) ∘ ⇑P₂.coroot) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i

Tactic:
comp_assoc,

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
ι₁ : 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₁
i : ι₂
⊢ (⇑f.coweightMap ∘ ⇑g.coweightMap ∘ ⇑P₂.coroot) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i
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
⊢ ⊥ ≠ ⊤

Tactic:
rw [ne_eq, Subtype.ext_iff]; exact bot_ne_top

Goal state after:
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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
g : P.Aut
hg : g ∈ P.weylGroup
⊢ q ∈ invtSubmodule (P.weylGroupRootRep ⟨g, hg⟩)

Tactic:
induction hg using weylGroup.induction with

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
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
e : P.Equiv P
⊢ symm P P e * e = 1

Tactic:
ext m

Goal state after:
case weightMap
ι : 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
e : P.Equiv P
m : M
⊢ (↑(symm P P e * e)).weightMap m = (↑1).weightMap m

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
ι₂ : 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
e : P.Equiv P
m : N
⊢ (↑(symm P P e * e)).coweightMap m = (↑1).coweightMap m

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
ι₂ : 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
e : P.Equiv P
m : ι
⊢ (↑(symm P P e * e)).indexEquiv m = (↑1).indexEquiv m