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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
obtain ⟨x, h0, h1⟩ := hv.exists_lt_one
  use x⁻¹
  simp [one_lt_inv₀ (zero_lt_iff.mpr (by simp [h0] : v x ≠ 0)), h1]

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v v' : Valuation R Γ₀
h : v = v'
⊢ v.IsEquiv v'

Tactic:
subst h

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
property✝¹ : R ∙ x ∈ (Ideal R)⁰
y : R
property✝ : R ∙ y ∈ (Ideal R)⁰
⊢ ↑(⟨R ∙ x, property✝¹⟩ * ⟨R ∙ y, property✝⟩) = R ∙ x * y

Tactic:
simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ∀ {a b : ↥(Ideal R)⁰}, a ∈ {I | IsPrincipal ↑I} → b ∈ {I | IsPrincipal ↑I} → a * b ∈ {I | IsPrincipal ↑I}

Tactic:
by
    rintro ⟨_, _⟩ ⟨_, _⟩ ⟨x, rfl⟩ ⟨y, rfl⟩
    exact ⟨x * y, by
      simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]⟩

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
f : R[X]
n : ℕ
hf : ↑(((Ideal.Quotient.mk I).comp C).rangeRestrict (f.coeff n)) = ↑0
⊢ f.coeff n ∈ comap C I

Tactic:
mem_comap,

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
f : R[X]
n : ℕ
hf : ↑(((Ideal.Quotient.mk I).comp C).rangeRestrict (f.coeff n)) = ↑0
⊢ C (f.coeff n) ∈ I
Module: Mathlib.RingTheory.Jacobson.Ring

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

Tactic:
mem_comap,

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

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

Tactic:
mem_comap,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ f (C z) ∈ Ideal.map f P
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 : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    (P.PolarizationIn S) (P.rootSpanMem S i) +
      ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)

Tactic:
rw [PolarizationIn_apply]

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
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 : ι
hP :
  (P.PolarizationIn S) (P.rootSpanMem S i) =
    ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) j)
⊢ ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) • P.coroot i =
    ∑ i_1, (P.coroot'In S i_1) (P.rootSpanMem S i) • P.coroot i_1 +
      ∑ j, P.pairingIn S i ((P.reflectionPerm i) j) • P.coroot ((P.reflectionPerm i) 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✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
⊢ ∃ i ∈ Finset.univ, 0 < (P.coroot'In S i) x * (P.coroot'In S i) x

Tactic:
obtain ⟨i, hi⟩ := P.exists_coroot_ne S hx

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : P.IsValuedIn S
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
x : ↥(P.rootSpan S)
hx : x ≠ 0
this : P.IsAnisotropic
i : ι
hi : (P.coroot'In S i) x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (P.coroot'In S i) x * (P.coroot'In S i) x
Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: 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 := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo (⇑(preReflection (sα β) (p.flip.toPerfPair ((preReflection α' (p α)) β')))) (range ⇑root) (range ⇑root)

Tactic:
LinearMap.toLinearMap_toPerfPair,

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 := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo (⇑(preReflection (sα β) (p.flip ((preReflection α' (p α)) β')))) (range ⇑root) (range ⇑root)
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
inst✝² : CharZero R
inst✝¹ : IsAddTorsionFree M
inst✝ : P.IsReduced
i j : ι
h : P.root i - P.root j ∈ range ⇑P.root
⊢ LinearIndependent R ![P.root i, P.root j]

Tactic:
by
  suffices LinearIndependent R ![P.root i, P.root (P.reflectionPerm j j)] by simpa using this
  apply P.linearIndependent_of_add_mem_range_root
  simpa [sub_eq_add_neg] using h

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
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : ¬α.IsZero
x' : L := ⋯.choose
h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0
⊢ chainLength α β • x = ⁅coroot α, x⁆

Tactic:
obtain ⟨k, rfl⟩ : ∃ k : K, k • x' = x := by
    simpa using (finrank_eq_one_iff_of_nonzero' ⟨x', h.1⟩ (by simpa using h.2)).mp
      (finrank_rootSpace_eq_one _ (chainTop_isNonZero α β hα)) ⟨_, hx⟩

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
x' : L := ⋯.choose
h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0
k : K
hx : k • x' ∈ rootSpace H ⇑(chainTop (⇑α) β)
⊢ chainLength α β • k • x' = ⁅coroot α, k • x'⁆
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: case mp
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic

pp: case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic

Tactic:
· rintro ⟨⟨hle₁, hle₂⟩, ha⟩
    obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
    exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩

Goal state after:
case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic
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
a : R
p : Module.Dual R M × M
⊢ (a • p).1 (a • p).2 = (a * a) • p.1 p.2

Tactic:
Prod.smul_fst,

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
a : R
p : Module.Dual R M × M
⊢ (a • p.1) (a • p).2 = (a * a) • p.1 p.2
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
hα : α.IsZero
⊢ β = -α ∨ β = α

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β : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
hα : ¬α.IsZero
⊢ β = -α ∨ β = α

Tactic:
· rw [hα, smul_zero] at h; cases hβ h

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β : β.IsNonZero
k : K
h : ⇑β = k • ⇑α
hα : ¬α.IsZero
⊢ β = -α ∨ β = α
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: case refine_2
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
h : Nontrivial V
⊢ ↑⊥ ≠ ⊤

Tactic:
invtSubmodule.coe_bot

Goal state after:
case refine_2
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
h : Nontrivial 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 fun x ↦ Weight.toLinear K (↥H) L ↑x

Tactic:
intro α β h

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
α β : ↥LieSubalgebra.root
h : (fun x ↦ Weight.toLinear K (↥H) L ↑x) α = (fun x ↦ Weight.toLinear K (↥H) L ↑x) β
⊢ α = β
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₂✝
ι₂ : 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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this : (↑f).weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ (↑f).coweightMap
⊢ (((↑(weightEquiv P Q f).symm).dualMap ∘ₗ ↑P.flip.toPerfPair) ((coweightEquiv P Q f) ((coweightEquiv P Q f).symm n)))
      m =
    ((↑Q.flip.toPerfPair ∘ₗ ↑(coweightEquiv P Q f).symm) n) ((weightEquiv P Q f) ((weightEquiv P Q f).symm m))

Tactic:
rw [LinearMap.ext_iff₂] at this

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
inst✝⁷ : AddCommGroup M₂✝
inst✝⁶ : Module R M₂✝
inst✝⁵ : AddCommGroup N₂✝
inst✝⁴ : Module R N₂✝
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂✝ R M₂✝ N₂✝
ι₂ : 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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this :
  ∀ (m : N₂) (n : M),
    (((↑f).weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair) m) n = ((↑P.flip.toPerfPair ∘ₗ (↑f).coweightMap) m) n
⊢ (((↑(weightEquiv P Q f).symm).dualMap ∘ₗ ↑P.flip.toPerfPair) ((coweightEquiv P Q f) ((coweightEquiv P Q f).symm n)))
      m =
    ((↑Q.flip.toPerfPair ∘ₗ ↑(coweightEquiv P Q f).symm) n) ((weightEquiv P Q f) ((weightEquiv P Q f).symm m))
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: I : Set ℤ
h₀ : I.Nonempty
h₁ : BddBelow I
h₂ : BddAbove I
⊢ I = Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ x + 1

Tactic:
by
  simp [← h₀.ordConnected_iff_of_bdd h₁ h₂, ordConnected_iff_disjoint_Ioo_empty]

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 ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : si > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4

Tactic:
rw [hsi'] at hsi

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 ι
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : LinearOrder S
inst✝⁵ : IsStrictOrderedRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
i j : ι
this : Fintype ι
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, ⋯⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, ⋯⟩
li : S := (P.posRootForm S).rootLength i
lj : S := (P.posRootForm S).rootLength j
lij : S := ((P.posRootForm S).posForm ri) rj
si : S
hsi : li > 0
sj : S
hsj : sj > 0
hsi' : si = li
hsj' : sj = lj
⊢ P.coxeterWeightIn S i j ≤ 4
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)
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)

Tactic:
let := P.indexNeg

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
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)
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 : ι
⊢ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j)

Tactic:
let := P.indexNeg

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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) 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 : ι
⊢ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-j))

Tactic:
let := P.indexNeg

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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) = Icc (-↑(chainBotCoeff i (-j))) ↑(chainTopCoeff i (-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 : ι
⊢ chainTopCoeff ((P.reflectionPerm i) i) j = chainBotCoeff i j

Tactic:
let := P.indexNeg

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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainTopCoeff ((P.reflectionPerm i) i) j = chainBotCoeff i 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 : ι
⊢ chainBotCoeff ((P.reflectionPerm i) i) j = chainTopCoeff i j

Tactic:
let := P.indexNeg

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 : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ chainBotCoeff ((P.reflectionPerm i) i) j = chainTopCoeff i j