mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
n : ι → ℕ
hn : n ≠ 0
hg : -⇑(∑ i, n i • b.baseSupp i) ∈ sU
contra : -⇑(∑ i, n i • b.baseSupp i) = 0
⊢ False

Tactic:
neg_eq_zero,

Goal state after:
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
inst✝³ : Fintype ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
n : ι → ℕ
hn : n ≠ 0
hg : -⇑(∑ i, n i • b.baseSupp i) ∈ sU
contra : ⇑(∑ i, n i • b.baseSupp i) = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ derivative (T R n) = ↑n * U R (n - 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one =>
    simp
  | add_two n ih1 ih2 =>
    have h₁ := congr_arg derivative (T_add_two R n)
    have h₂ := U_sub_one R n
    have h₃ := T_eq_U_sub_X_mul_U R (n + 1)
    simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
    linear_combination (norm := (push_cast; ring_nf))
      h₁ - ih2 + 2 * (X : R[X]) * ih1 + 2 * h₃ - n * h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := congr_arg derivative (T_sub_one R (-n))
    have h₂ := U_sub_two R (-n)
    have h₃ := T_eq_U_sub_X_mul_U R (-n)
    simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
    linear_combination (norm := (push_cast; ring_nf))
      -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))

Tactic:
have h₁ := C_add_two R (m + (-k - 1))

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : C R m * C R (-↑k) = C R (m + -↑k) + C R (m - -↑k)
ih2 : C R m * C R (-↑k + 1) = C R (m + (-↑k + 1)) + C R (m - (-↑k + 1))
h₁ : C R (m + (-↑k - 1) + 2) = X * C R (m + (-↑k - 1) + 1) - C R (m + (-↑k - 1))
⊢ C R m * C R (-↑k - 1) = C R (m + (-↑k - 1)) + C R (m - (-↑k - 1))
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ StrictMono ⇑withZeroUnitsEquiv

Tactic:
intro a b
  cases a <;> cases b <;>
  simp

Goal state after:
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE

Tactic:
by
  tfae_have 1 → 2
  | _ => inferInstance
  tfae_have 2 → 3
  | _ => inferInstance
  tfae_have 3 → 4
  | _ => inferInstance
  tfae_have 4 → 1
  | ⟨h⟩ => by
    rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
    refine ⟨RelEmbedding.wellFounded ?_ h⟩
    have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
      fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1
    choose f hf using this
    exact
      { toFun := f
        inj' := fun x y e => by ext1; rw [hf, hf, e]
        map_rel_iff' := by
          dsimp
          intro a b
          rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
          rfl }
  tfae_finish

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

Goal state before:
pp: case mp.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
y : Γ₀
hy : ∃ x_1, x ∣ x_1 ∧ v ((algebraMap O F) x_1) = y
⊢ y ≤ (⇑v ∘ ⇑(algebraMap O F)) x

Tactic:
obtain ⟨y, hy, rfl⟩ := hy

Goal state after:
case mp.refine_2
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
y : O
hy : x ∣ y
⊢ v ((algebraMap O F) y) ≤ (⇑v ∘ ⇑(algebraMap O F)) x
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_1
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

pp: case refine_2
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Tactic:
· obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
    exacts [⟨a, .inl e.symm⟩, ⟨a, .inr e.symm⟩]

Goal state after:
case refine_2
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K
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 : ¬∀ ⦃I : Ideal R⦄, I ∈ {J_1 | under R J ≤ J_1 ∧ J_1.IsMaximal} → y ∈ I
⊢ (under R J).IsMaximal

Tactic:
push Not at this

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 : ∃ I ∈ {J_1 | under R J ≤ J_1 ∧ J_1.IsMaximal}, y ∉ I
⊢ (under R J).IsMaximal
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case mpr
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
⊢ (under R J).IsMaximal ∧ y ∉ under R J → J.IsMaximal

Tactic:
simp only [Ideal.mem_comap, and_imp]

Goal state after:
case mpr
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
⊢ (under R J).IsMaximal → (algebraMap R S) y ∉ J → 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 Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 - x) = 1

Tactic:
rw [sub_eq_add_neg 1 x]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ r s, 0 < v r ∧ 0 < v s ∧ v.restrict r / v.restrict s = ↑γ

Tactic:
set u := WithZero.unzero (Units.ne_zero γ) with hu_def
  obtain ⟨a, ⟨ha, x, hax⟩⟩ := (mem_valueGroup_iff_of_comm _).mp u.2
  have hx : 0 < v x := by
    rw [← restrict_pos_iff, restrict_def, WithZero.pos_iff_ne_zero, ne_eq, restrict₀_eq_zero_iff]
    aesop
  use x, a, hx, zero_lt_iff.mpr ha
  have ha0 : v.restrict a ≠ 0 := by simpa using ha
  rw [div_eq_iff ha0, mul_comm, ← embedding_strictMono.injective.eq_iff, map_mul,
    embedding_restrict, embedding_restrict]
  rw [← MonoidWithZeroHom.coe_ofClass, ← hax]
  congr
  rw [← WithZero.coe_unzero (Units.ne_zero γ)]
  exact Eq.refl ..

Goal state after:
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X), h (f x) = g x) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f → ∀ (b : N →ₗ[R] CharacterModule M), ∃ a, (lcomp R (CharacterModule M) f) a = b

Tactic:
DFunLike.ext_iff

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y),
      Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X) (x_1 : M), (h (f x)) x_1 = (g x) x_1) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f →
        ∀ (b : N →ₗ[R] CharacterModule M),
          ∃ a, ∀ (x : N) (x_1 : M), (((lcomp R (CharacterModule M) f) a) x) x_1 = (b x) x_1
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.jacobson = P

Tactic:
rw [jacobson_eq_iff_jacobson_quotient_eq_bot]
    let P' := P.comap (C : R →+* R[X])
    have : P'.IsPrime := comap_isPrime C P
    have hR' : IsJacobsonRing (R ⧸ P') := by infer_instance
    obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP
    let x := (Polynomial.map (Ideal.Quotient.mk P') p).leadingCoeff
    have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero]
    let φ : R ⧸ P' →+* R[X] ⧸ P := Ideal.quotientMap P (C : R →+* R[X]) le_rfl
    let hφ : Function.Injective ↑φ := quotientMap_injective
    let Rₘ := Localization.Away x
    let Sₘ := (Localization ((Submonoid.powers x).map φ : Submonoid (R[X] ⧸ P)))
    refine jacobson_bot_of_integral_localization (S := R[X] ⧸ P) (R := R ⧸ P') Rₘ Sₘ _ hφ _ hx ?_
    exact isIntegral_isLocalization_polynomial_quotient P p pP

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ¬KrullDimLE 0 R

Tactic:
by
  simp [krullDimLE_iff, ringKrullDim_eq_one R]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsRootSystem
⊢ span R (range P.root') = ⊤

Tactic:
simp [← rootSpan_map_toPerfPair]

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
inst✝ : Fintype ι
m : M
⊢ (P.flip.toLinearMap ∘ₗ P.Polarization) m = 0 → P.Polarization m = 0

Tactic:
rintro (h : P.flip.toPerfPair (P.Polarization m) = 0)

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✝ : Fintype ι
m : M
h : P.flip.toPerfPair (P.Polarization m) = 0
⊢ P.Polarization m = 0
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
inst✝² : P.IsAnisotropic
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
i j k : ι
m n : R
hk : m • P.root i + n • P.root j = P.root k
⊢ (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i) • P.coroot k =
    m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j

Tactic:
let B := P.toInvariantForm
  let lsq (i) : R := B.form (P.root i) (P.root i)
  have hlsq (i : ι) : lsq i = P.RootForm (P.root i) (P.root i) := rfl
  have h₁ : lsq k • P.coroot k = (m • lsq i) • P.coroot i + (n • lsq j) • P.coroot j := by
    simp only [hlsq, smul_assoc, P.rootForm_self_smul_coroot, smul_comm _ 2]
    rw [← map_smul _ m, ← map_smul _ n, ← nsmul_add, ← map_add, hk]
  have h₂ :
      lsq k = (m * m) * lsq i + (m * n) * (2 * B.form (P.root i) (P.root j)) + (n * n) * lsq j := by
    have aux : P.RootForm (P.root j) (P.root i) = B.form (P.root i) (P.root j) :=
      P.rootForm_symmetric.eq (P.root j) (P.root i)
    simp [hlsq, ← hk, aux, B]
    ring
  have h₃ : 2 * B.form (P.root i) (P.root j) = P.pairing i j * lsq j :=
    B.two_mul_apply_root_root i j
  have h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j := B.pairing_mul_eq_pairing_mul_swap i j
  replace h₁ :
      (m * m * (P.pairing j i * lsq i)) • P.coroot k +
      (m * n * (P.pairing j i * P.pairing i j * lsq j)) • P.coroot k +
      (n * n * (P.pairing j i * lsq j)) • P.coroot k =
        (m * (P.pairing j i * lsq i)) • P.coroot i +
        (n * (P.pairing j i * lsq j)) • P.coroot j := by
    rw [h₂, h₃] at h₁
    replace h₁ := congr_arg (fun n ↦ P.pairing j i • n) h₁
    simp only [add_smul, smul_add, ← mul_smul, smul_eq_mul] at h₁
    convert! h₁ using 1
    · module
    · ring_nf
  simp only [h₄] at h₁
  apply smul_right_injective _ (r := lsq j) (RootPairing.IsAnisotropic.rootForm_root_ne_zero j)
  simp only
  convert! h₁ using 1
  · module
  · module

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
inst✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ (P.RootForm (P.root i)) (P.root i) * P.pairing j i * ((P.RootForm (P.root j)) (P.root j) * P.pairing i j) =
    P.coxeterWeight i j * ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
coxeterWeight

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✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ (P.RootForm (P.root i)) (P.root i) * P.pairing j i * ((P.RootForm (P.root j)) (P.root j) * P.pairing i j) =
    P.pairing i j * P.pairing j i * ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ P.pairing i j * P.pairing j i = P.coxeterWeight i j

Tactic:
coxeterWeight

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
i j : ι
inst✝¹ : NeZero 2
inst✝ : IsAddTorsionFree M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ P.pairing i j * P.pairing j i = P.pairing i j * P.pairing j i
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✝⁷ : 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 : ι
inst✝ : Finite ι
⊢ P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0

Tactic:
simpa using P.zero_lt_pairingIn_iff' S (i := i) (j := P.reflectionPerm j j)

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

Goal state before:
pp: case inr.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
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 : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i = 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

pp: case inr.inr
ι : 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✝¹⁰ : 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 : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
· rw [hji, P.pairingIn_eq_zero_iff.mp hji]

Goal state after:
case inr.inr
ι : 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✝¹⁰ : 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 : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j

Tactic:
simp only [← neg_eq_iff_eq_neg]

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ -P.pairing i j = 2 ∧ -P.pairing j i = 2 ↔ -P.root i = P.root j
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
f : ι → Dual K M
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
x : M
hx : ∀ (i : ι), x ∉ p i
⊢ ∀ (i : ι), (f i) x ≠ 0

Tactic:
simpa [p] using hx

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α : ¬α.IsZero
h : ⇑β = 0 • ⇑α
⊢ β.IsZero

Tactic:
zero_smul

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α : ¬α.IsZero
h : ⇑β = 0
⊢ β.IsZero
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: 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
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ ((t * s) • y) • v = t • (s • y) • v

Tactic:
hy (t * s),

Goal state after:
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
s : k
y : k[G]
hy : ∀ (t : k), (t • y) • v = t • y • v
t : k
⊢ (t * s) • y • v = t • (s • y) • v
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
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
this : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = univ
⊢ span K (⇑P.root '' ({i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q})) = ⊤

Tactic:
rw [this, Set.image_univ]

Goal state after:
ι : 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
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
this : {i | P.root i ∈ Q} ∪ {i | P.root i ∉ Q} = univ
⊢ span K (range ⇑P.root) = ⊤