mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α β)
⊢ rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥

Tactic:
simp only [← smul_neg, ne_eq, LieSubmodule.eq_bot_iff, not_forall]

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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α β)
⊢ ∃ x, ∃ (_ : x ∈ rootSpace H (n • -⇑α + ⇑(chainTop (⇑α) β))), ¬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
⊢ β (coroot α) = ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))

Tactic:
rw [apply_coroot_eq_cast', ← chainTopCoeff_add_chainBotCoeff]

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
⊢ ↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) =
    ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ Q₁ (x.1 + y.1) + Q₂ (x.2 + y.2) - (Q₁ x.1 + Q₂ x.2) - (Q₁ y.1 + Q₂ y.2) =
    Q₁ (x.1 + y.1) - Q₁ x.1 - Q₁ y.1 + (Q₂ (x.2 + y.2) - Q₂ x.2 - Q₂ y.2)

Tactic:
abel

Goal state after:
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₂⟩
    set k := chainTopCoeff α β - n with hk; clear_value k
    lift k to ℕ using (by rw [hk, le_sub_iff_add_le, zero_add]; exact h₁)
    rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hk
    subst hk
    simp only [neg_sub, tsub_le_iff_right, ← Nat.cast_add, Nat.cast_le,
      chainBotCoeff_add_chainTopCoeff] at h₂
    have := rootSpace_neg_nsmul_add_chainTop_of_le α β h₂
    rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] at this

Goal state after:
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
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : chainLength α 0 = 2 * chainTopCoeff (⇑α) 0
⊢ chainTopCoeff (⇑α) 0 + 1 < chainTopCoeff (⇑α) 0 + chainTopCoeff (⇑α) 0

Tactic:
add_lt_add_iff_left

Goal state after:
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
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) 0)
x_ne0 : x ≠ 0
e✝ f : L
he : e✝ ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
isSl2 : IsSl2Triple (↑(coroot α)) e✝ f
prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α 0)
k : K
hk : 0 = ((toEnd K L L) f ^ (chainTopCoeff (⇑α) 0 + 1 + 1)) x
e : 1 < chainTopCoeff (⇑α) 0
this : chainLength α 0 = 2 * chainTopCoeff (⇑α) 0
⊢ 1 < chainTopCoeff (⇑α) 0
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

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

Tactic:
change ((Equiv.coweightHom P).domRestrict P.weylGroup) 1 ∈ _

Goal state after:
case refine_2.one
ι : 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 : P.Aut
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup) 1 ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : 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 : ↥P.invtRootSubmodule
h : q = ⊥
⊢ ∀ (i : ι), P.root i ∉ ↑q

Tactic:
simp [h, P.ne_zero]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
g : G
x : H
r : k
⊢ ((ofMulAction k G H) g) (MonoidAlgebra.single x r) = MonoidAlgebra.single (g • x) r

Tactic:
simp [ofMulAction_def]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective fun x ↦ g • x

Tactic:
intro h₁

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Group G
H : Type u_4
inst✝ : MulAction G H
g : G
f : k[H]
h : H
h' : H := g⁻¹ • h
h₁ : H
⊢ ∀ ⦃a₂ : H⦄, (fun x ↦ g • x) h₁ = (fun x ↦ g • x) a₂ → h₁ = a₂
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ TensorProduct.map (ρV (g * h)) (ρW (g * h)) = TensorProduct.map (ρV g) (ρW g) * TensorProduct.map (ρV h) (ρW h)

Tactic:
simp only [map_mul, TensorProduct.map_mul]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : V →ₗ[k] W
⊢ ρW g ∘ₗ (f₁ + f₂) ∘ₗ ρV g⁻¹ = ρW g ∘ₗ f₁ ∘ₗ ρV g⁻¹ + ρW g ∘ₗ f₂ ∘ₗ ρV g⁻¹

Tactic:
simp_rw [add_comp, comp_add]

Goal state after:
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ ↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) = ↑(b.leastOfBdd Hb Hinh)

Tactic:
convert! (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : NeZero 2
inst✝ : P.IsIrreducible
B : P.InvariantForm
i j : ι
⊢ ∃ k, (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j) ∧ (B.form (P.root i)) (P.root k) ≠ 0

Tactic:
by
  by_contra! contra
  suffices span R (orbit P.weylGroup (P.root j)) ≤ ker (B.form (P.root i)) from
    B.apply_root_ne_zero i <| by simpa [span_orbit_eq_top] using this
  refine span_le.mpr fun v hv ↦ ?_
  obtain ⟨g, rfl⟩ := mem_orbit_iff.mp hv
  simp only [P.weylGroup_apply_root, SetLike.mem_coe, LinearMap.mem_ker]
  apply contra
  simp [← Subgroup.smul_def g]

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

pp: case h.right
ι : 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ˣ
⊢ RightInverse ⇑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:
case h.right
ι : 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ˣ
⊢ RightInverse ⇑f.inv.coweightMap ⇑(↑f).coweightMap
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
i : ι
⊢ Bijective ⇑↑(P.reflection i)

Tactic:
simp only [LinearEquiv.coe_coe]
    exact LinearEquiv.bijective (P.reflection i)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1
h :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4
⊢ B.rootLength i ≤ B.rootLength j

Tactic:
have h' := B.pairingIn_mul_eq_pairingIn_mul_swap i j

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
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 ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
        P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
              P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -4
h' : P.pairingIn ℤ j i * B.rootLength i = P.pairingIn ℤ i j * B.rootLength j
⊢ B.rootLength i ≤ B.rootLength j
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
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
⊢ False

Tactic:
have hki_ne : P.root k ≠ -P.root i := by
    rw [hk]
    contrapose! h
    replace h : r • P.root i = - P.root j - P.root i := by rw [← sub_eq_of_eq_add h.symm]; module
    exact ⟨r + 1, 1, by simp [add_smul, h], by lia⟩

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
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
x✝¹ : r ∈ S
s : ℤ
x✝ : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk : P.root k = P.root j + r • P.root i
l : ι
hl : P.root l = P.root j + s • P.root i
contra : r + 1 < s
hki_notMem : P.root k + P.root i ∉ range ⇑P.root
hki_ne : P.root k ≠ -P.root i
⊢ False
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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
h_span : span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)) = ⊤
⊢ Fintype.card ↑(baseOf (⇑P.root) f) = finrank R ↥⊤

Tactic:
finrank_top,

Goal state after:
ι : 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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
h_span : span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)) = ⊤
⊢ Fintype.card ↑(baseOf (⇑P.root) f) = finrank R M
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 k : ι
hk : P.root k = P.root j + P.root i
h : LinearIndependent R ![P.root i, P.root k]
⊢ P.root j = P.root j + P.root i - P.root i

Tactic:
abel

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
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
⊢ i = j

Tactic:
obtain ⟨a, ha⟩ : ∃ c : P.root '' s → ℕ, ∑ x, c x • (x : M) = P.root j := hjk hj

Goal state after:
ι : 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
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
⊢ i = j
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
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
this : ∀ (x : ↑(⇑P.root '' s)), x ≠ ri → a x = 0
x : ↑(⇑P.root '' s)
hx : a x • ↑x ≠ 0
⊢ x ∈ {ri}

Tactic:
rw [Finset.mem_singleton]

Goal state after:
ι : 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
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
this : ∀ (x : ↑(⇑P.root '' s)), x ≠ ri → a x = 0
x : ↑(⇑P.root '' s)
hx : a x • ↑x ≠ 0
⊢ x = ri
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
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
⊢ ∃ q > 0, P.root j = q • P.root i

Tactic:
by
    suffices P.root j = (a ri : ℚ) • P.root i by
      refine ⟨a ri, ?_, this⟩
      by_contra contra
      replace contra : a ri = 0 := by simpa using contra
      simp [contra, P.ne_zero j] at this
    have (x : P.root '' s) (hx : x ≠ ri) : a x = 0 := by
      replace huv : u * ↑(a x) + v * ↑(b x) = 0 := by simpa [hx] using congr($huv x)
      suffices u * (a x) = 0 by simpa [hu.ne'] using this
      have : 0 ≤ u * (a x) := by positivity
      have : 0 ≤ v * (b x) := by positivity
      grind
    replace this (x : P.root '' s) (hx : a x • (x : M) ≠ 0) :  x ∈ ({ri} : Finset _) := by
      rw [Finset.mem_singleton]
      by_contra! contra
      simp [this x contra] at hx
    simp [← ha, ← Fintype.sum_subset this, ri, Nat.cast_smul_eq_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f * g) j) < ε

Tactic:
have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε