mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
i : ↑w
j : ↑v
⊢ (bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b) i j ∈ (algebraMap K L).fieldRange

Tactic:
simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
      Basis.dualBasis_repr]

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
i : ↑w
j : ↑v
⊢ (p.toPerfPair (b j)) (bN i) ∈ (algebraMap K L).fieldRange
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : ↑s), IsSimpleModule R ↥↑x
⊢ IsNoetherian R ↥(⨆ i, ↑i) ∧ IsArtinian R ↥(⨆ i, ↑i)

Tactic:
have := fin.to_subtype

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : ↑s), IsSimpleModule R ↥↑x
this : Finite ↑s
⊢ IsNoetherian R ↥(⨆ i, ↑i) ∧ IsArtinian R ↥(⨆ i, ↑i)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝¹ : Field F
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ ¬IsUnit x ↔ ¬1 ≤ v ↑x

Tactic:
not_iff_not,

Goal state after:
F : Type u
Γ₀ : Type v
inst✝¹ : Field F
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ IsUnit x ↔ 1 ≤ v ↑x
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 : ℕ
⊢ I ^ n • ⊤ ≤ (eval I M n).ker

Tactic:
simp only [smul_le, mem_top, LinearMap.mem_ker, map_smul, coe_eval, forall_const]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ r ∈ I ^ n, ∀ (n_1 : AdicCompletion I M), r • ↑n_1 n = 0
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P

Tactic:
jacobson,

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ sInf {J | I ≤ J ∧ J.IsMaximal}
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P.jacobson

Tactic:
jacobson,

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ sInf {J | P ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
this : y ∉ (under R J).jacobson.toAddSubmonoid
⊢ (under R J).IsMaximal

Tactic:
jacobson,

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : (under R J).IsPrime ∧ Disjoint ↑(powers y) ↑(under R J)
this : y ∉ (sInf {J_1 | under R J ≤ J_1 ∧ J_1.IsMaximal}).toAddSubmonoid
⊢ (under R J).IsMaximal
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
⊢ v (∑ i ∈ s, f i) = v (f j)

Tactic:
rcases eq_or_ne (v (f j)) 0 with h0 | h0

Goal state after:
case inl
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) = 0
⊢ v (∑ i ∈ s, f i) = v (f j)

case inr
R : Type u_3
Γ₀ : Type u_4
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
h0 : v (f j) ≠ 0
⊢ v (∑ i ∈ s, f i) = v (f j)
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
⊢ minimalPrimes R = {I | I.IsPrime}

Tactic:
by
  ext
  exact Ideal.mem_minimalPrimes_iff_isPrime

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

Goal state before:
pp: R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
I : Ideal R
⊢ (fun n ↦ ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) (OrderDual.ofDual n))
      ((fun I ↦ OrderDual.toDual ((addVal R) (generator I))) I) =
    I

Tactic:
by
    let x := generator I
    suffices (addVal R x).recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) = span {x} by
      rwa [Ideal.span_singleton_generator] at this
    by_cases hx0 : x = 0
    · simp [hx0]
    · obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
      obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx0 hϖ
      rw [hu, addVal_def' u hϖ, span_singleton_mul_left_unit u.isUnit,
        ENat.recTopCoe_natCast, hϖ.maximalIdeal_eq, span_singleton_pow]

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

Goal state before:
pp: case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ embedding (v.restrict x) = embedding (v.restrict a) * embedding ↑γ

Tactic:
embedding_restrict,

Goal state after:
case right
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
ha0 : v.restrict a ≠ 0
⊢ v x = embedding (v.restrict a) * embedding ↑γ
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
n : ℕ
IH : ∀ (P : Ideal (MvPolynomial (Fin n) R)), P.IsMaximal → (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral
P : Ideal (MvPolynomial (Fin (n + 1)) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin (n + 1)) R ⧸ P)).IsIntegral

Tactic:
| succ n IH =>

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

Goal state before:
pp: case mem
ι : 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✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x✝ : M
i : ι
x : M
hx : x ∈ range ⇑P.root
⊢ (P.coroot' i) x ∈ ↑(Algebra.linearMap S R).range

Tactic:
obtain ⟨k, rfl⟩ := hx

Goal state after:
case mem
ι : 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✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
i k : ι
⊢ (P.coroot' i) (P.root k) ∈ ↑(Algebra.linearMap S R).range
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: case hB
ι : 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
x✝¹ x✝ : ↥(span S (range ⇑P.root))
x : M
hx : x ∈ span S (range ⇑P.root)
y : M
hy : y ∈ span S (range ⇑P.root)
⊢ ∀ x ∈ range ⇑P.root,
    ∀ y ∈ range ⇑P.root, ((LinearMap.restrictScalarsₗ S R M R S ∘ₗ ↑S B.form) x) y ∈ (Algebra.linearMap S R).range

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
      simpa using B.exists_eq i j

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
p : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ root ⋯.choose = root j

Tactic:
(exist_eq_reflection_of_mapsTo p root coroot i _ h).choose_spec,

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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ (preReflection (root i) (p.flip (coroot i))) (root ⋯.choose) = root j
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
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
this : 2 • 2 • P.root i = 2 • P.root j
⊢ P.root j = 2 • P.root i

Tactic:
exact smul_right_injective M two_ne_zero this.symm

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
S : Type u_5
i j : ι
inst✝⁸ : Finite ι
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : FaithfulSMul S R
inst✝¹ : P.IsValuedIn S
inst✝ : IsTorsionFree R N
⊢ P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = -2 • P.root i

Tactic:
rw [← P.pairing_neg_one_neg_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S,
    ← map_one (algebraMap S R), ← map_ofNat (algebraMap S R), ← map_neg, ← map_neg,
    (algebraMap_injective S R).eq_iff, (algebraMap_injective S R).eq_iff]

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

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

Tactic:
← Nat.succ_add,

Goal state after:
case a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
e : chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
⊢ rootSpace H (-(((chainBotCoeff (⇑α) β).succ + chainTopCoeff (⇑α) β) • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Q (m i) = ∑ i_1, (Pi.single i Q i_1) (m i_1)

Tactic:
Fintype.sum_eq_single i (fun j hij => ?_),

Goal state after:
ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
⊢ Q (m i) = (Pi.single i Q i) (m i)

ι : Type u_1
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
P : Type u_7
Mᵢ : ι → Type u_8
Nᵢ : ι → Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)
inst✝⁵ : AddCommMonoid P
inst✝⁴ : (i : ι) → Module R (Mᵢ i)
inst✝³ : (i : ι) → Module R (Nᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
Q : QuadraticMap R (Mᵢ i) P
m : (i : ι) → Mᵢ i
j : ι
hij : j ≠ i
⊢ (Pi.single i Q j) (m j) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ p.1 p.2 + p.1 q.2 + (q.1 p.2 + q.1 q.2) = p.1 p.2 + q.1 q.2 + (q.1 p.2 + p.1 q.2)

Tactic:
add_right_comm _ (q.1 q.2),

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
p q : Module.Dual R M × M
⊢ p.1 p.2 + p.1 q.2 + (q.1 p.2 + q.1 q.2) = p.1 p.2 + (q.1 p.2 + p.1 q.2) + q.1 q.2
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case h₁
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
e : chainTopCoeff (⇑α) 0 = 0
⊢ False

Tactic:
exact α.2 (by simpa [e] using!
      genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα)

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
hα : α.IsNonZero
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
by
  cases subsingleton_or_nontrivial L
  · exact IsEmpty.elim inferInstance α
  simpa [chainTopCoeff_zero_right α hα] using
    genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα

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
hα : α.IsNonZero
h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥
W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, genWeightSpace_ne_bot' := h }
hW : 2 • ⇑W = ⇑α
this : rootSpace H (2 • ⇑W) = ⊥
⊢ genWeightSpace L ⇑α = ⊥

Tactic:
hW

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥
W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, genWeightSpace_ne_bot' := h }
hW : 2 • ⇑W = ⇑α
this : rootSpace H ⇑α = ⊥
⊢ genWeightSpace L ⇑α = ⊥
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
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ (ρ.asAlgebraHom x) v ∈ p

Tactic:
apply x.induction_on

Goal state after:
case of
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
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (m : G), (ρ.asAlgebraHom ((MonoidAlgebra.of k G) m)) v ∈ p

case add
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (x y : k[G]), (ρ.asAlgebraHom x) v ∈ p → (ρ.asAlgebraHom y) v ∈ p → (ρ.asAlgebraHom (x + y)) v ∈ p

case smul
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
p : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p
v : V
hv : v ∈ p
x : k[G]
⊢ ∀ (r : k) (x : k[G]), (ρ.asAlgebraHom x) v ∈ p → (ρ.asAlgebraHom (r • x)) v ∈ p
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
x : k[G]
v : ρ.asModule
⊢ ∀ (t : k), (t • x) • v = t • x • v

Tactic:
apply x.induction_on

Goal state after:
case of
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (m : G) (t : k), (t • (of k G) m) • v = t • (of k G) m • v

case add
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (x y : k[G]),
    (∀ (t : k), (t • x) • v = t • x • v) →
      (∀ (t : k), (t • y) • v = t • y • v) → ∀ (t : k), (t • (x + y)) • v = t • (x + y) • v

case smul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : k[G]
v : ρ.asModule
⊢ ∀ (r : k) (x : k[G]), (∀ (t : k), (t • x) • v = t • x • v) → ∀ (t : k), (t • r • x) • v = t • (r • x) • v
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
⊢ Function.Injective (coroot ∘ Subtype.val)

Tactic:
rintro ⟨α, hα⟩ ⟨β, hβ⟩ h; simpa using h

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

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1
⊢ B.rootLength i ≤ B.rootLength j

Tactic:
hij'.1,

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h' : P.pairingIn ℤ j i * B.rootLength i = 1 * B.rootLength j
hi : 0 < B.rootLength i
hij' : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1
⊢ B.rootLength i ≤ B.rootLength j