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

Goal state before:
pp: case lie
ι : 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
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hu : u ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
⊢ ⁅u, v⁆ ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))

Tactic:
let s : Set (H → R) := {χ | ∃ n : ι → ℕ, n ≠ 0 ∧ χ = ∑ i, n i • b.baseSupp i}
    have hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s := by
      rintro - ⟨n₁, hn₁, rfl⟩ - ⟨n₂, hn₂, rfl⟩
      refine ⟨n₁ + n₂, by simp [hn₁], ?_⟩
      ext; simp [add_smul, Finset.sum_add_distrib]
    let e : {n : ι → ℕ | n ≠ 0} ≃ s :=
      .ofBijective (fun n ↦ ⟨∑ i, n.val i • b.baseSupp i, n.val, n.property, by ext; simp⟩) <| by
      refine ⟨fun n₁ n₂ h ↦ ?_, fun χ ↦ ?_⟩
      · ext i
        have := b.linearIndependent_baseSupp.restrict_scalars' ℕ
        refine Fintype.linearIndependent_iffₛ.mp this n₁ n₂ ?_ i
        ext v
        rw [Subtype.mk.injEq] at h
        simpa using congr_fun h v
      · use ⟨χ.property.choose, χ.property.choose_spec.1⟩
        ext i
        simpa using congr_fun χ.property.choose_spec.2.symm i
    replace hu : u ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace H χ := by
      convert! hu; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    replace hv : v ∈ ⨆ χ, ⨆ (_ : χ ∈ s), rootSpace H χ := by
      convert! hv; rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl
    convert! mem_biSup_genWeightSpace_of hs hu hv
    rw [iSup_subtype', iSup_subtype', ← e.iSup_comp]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
x : R[X]
hx : x ∈ (fun m ↦ derivative (T R ↑m)) '' Set.Icc 0 (n - k)
⊢ x ∈ ↑(Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1))))

Tactic:
obtain ⟨m, hm, rfl⟩ := hx

Goal state after:
R : Type u_1
inst✝ : CommRing R
n k : ℕ
ih : (⇑derivative)^[k] (T R ↑n) ∈ Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - k))
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
⊢ (fun m ↦ derivative (T R ↑m)) m ∈ ↑(Submodule.span ℕ ((fun m ↦ T R ↑m) '' Set.Icc 0 (n - (k + 1))))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
⊢ (2 * ↑k + 3) * eval 1 ((⇑derivative)^[k + 1] (U R n)) =
    ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 1 ((⇑derivative)^[k] (U R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 1
  rw [one_pow, sub_self, zero_mul, mul_one] at h
  exact sub_eq_zero.mp h.symm

Goal state after:
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
⊢ IsFiniteLength R N

Tactic:
have := e.symm.toEquiv.subsingleton

Goal state after:
case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
a b : { N // N.FG }
⊢ DvdNotUnit (f a) (f b) ↔ b < a

Tactic:
rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // J.FG } → R
hf : ∀ (I : { J // J.FG }), ↑I = Ideal.span {f I}
a b : { N // N.FG }
⊢ ↑b < ↑a ↔ b < a
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : Ring R
ι : Type u_5
inst✝² : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∑ i, length R (M (some i)) + length R (M none) = ∑ i, length R (M i)

Tactic:
Fintype.sum_option,

Goal state after:
case h_option
R : Type u_1
inst✝³ : Ring R
ι : Type u_5
inst✝² : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    length R ((i : ι) → M i) = ∑ i, length R (M i)
M : Option ι → Type u_6
inst✝¹ : (i : Option ι) → AddCommGroup (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∑ i, length R (M (some i)) + length R (M none) = length R (M none) + ∑ i, length R (M (some i))
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
by
  cases finite_or_infinite ι
  · cases nonempty_fintype ι
    simp
  nontriviality M
  rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ← top_le_iff]
  refine le_trans ?_ (Module.length_le_of_injective Finsupp.lcoeFun DFunLike.coe_injective)
  simp [ENat.top_mul length_pos.ne']

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case neg.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b✝ : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
left✝ : IsNoetherian R R
right✝ : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ ENat.card (Free.ChooseBasisIndex R M) * length R R =
    Cardinal.toENat (Cardinal.mk (Free.ChooseBasisIndex R M)) * length R R

Tactic:
ENat.card

Goal state after:
case neg.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
b✝ : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
a✝¹ : Nontrivial R
a✝ : Nontrivial M
left✝ : IsNoetherian R R
right✝ : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ Cardinal.toENat (Cardinal.mk (Free.ChooseBasisIndex R M)) * length R R =
    Cardinal.toENat (Cardinal.mk (Free.ChooseBasisIndex R M)) * length R R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ (MulAction.orbitRel Aˣ K) 0⁻¹ 0

Tactic:
rw [inv_zero]

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

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r : ↥v.integer
x : R
h : x ∈ (v.leAddSubgroup γ).carrier
⊢ r • x ∈ (v.leAddSubgroup γ).carrier

Tactic:
by
    simpa [Subring.smul_def] using mul_le_of_le_one_of_le r.prop h

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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ (span {p}).IsPrime

pp: case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}

Tactic:
· rwa [Ideal.span_singleton_prime hp.ne_zero, ← UniqueFactorizationMonoid.irreducible_iff_prime]

Goal state after:
case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = span {p}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
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)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
⊢ under R J = I

Tactic:
have hI_p : (I.map (algebraMap R S)).IsPrime := by
        refine isPrime_of_isPrime_disjoint (powers y) _ I hIm.isPrime ?_
        rwa [disjoint_powers_iff_notMem_of_isPrime]

Goal state after:
case neg
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)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2✝ : CommRing.toCommSemiring.toSemiring = inst✝³.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
hI_p : (Ideal.map (algebraMap R S) I).IsPrime
⊢ under R J = I
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 : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x : M
⊢ (AdicCompletion.eval I N (a n))
      ((of I N) ((LinearEquiv.ofBijective (of I N) ⋯).symm ((AdicCompletion.lift I (extend ha f) ⋯) x))) =
    (f n) x

Tactic:
simp [extend_eq ha f hf]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
⊢ ∃ n, I = maximalIdeal R ^ n

Tactic:
by_cases h : IsField R

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : IsField R
⊢ ∃ n, I = maximalIdeal R ^ n

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
⊢ ∃ n, I = maximalIdeal R ^ n
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ sInf (comap (algebraMap S Sₘ) '' {J | ⊥ ≤ J ∧ J.IsMaximal})

Tactic:
exact sInf_le_sInf fun j hj => ⟨bot_le,
      let ⟨J, hJ⟩ := hj
      hJ.2 ▸ this J hJ.1.2⟩

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
inst✝ : Small.{v, u} R
⊢ Flat R M ↔
    ∀ ⦃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 → Function.Injective ⇑(rTensor M f)

Tactic:
iff_rTensor_preserves_injective_linearMap'

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v, u} R
⊢ (∀ ⦃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 → Function.Injective ⇑(rTensor M f)) ↔
    ∀ ⦃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 → Function.Injective ⇑(rTensor M f)
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
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : TensorProduct R (↥J) M
hx : (rTensor M (Submodule.subtype I ∘ₗ Submodule.inclusion hle)) y = 0
⊢ (rTensor M (Submodule.inclusion hle)) y = 0

Tactic:
rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]

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

Goal state before:
pp: case hg
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ Function.Surjective ⇑w.toRingEquiv.toRingHom

Tactic:
exact w.surjective

Goal state after:
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
x s : R
hx : IsSquare x
hs : IsSumSq s
⊢ IsSumSq (x + s)

Tactic:
by rcases hx with ⟨_, rfl⟩; exact sq_add _ hs

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

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
B : P.InvariantForm
i j : ι
inst✝¹ : IsDomain R
inst✝ : NeZero 2
⊢ 2 * (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j * (B.form (P.root j)) (P.root j) = 0

Tactic:
rw [B.two_mul_apply_root_root i j]

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

Goal state before:
pp: case neg.mp.inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, v x < 1 ↔ v' x < 1
x : K
hx : ¬x = 0
hh : v x = 1
h_1 : ¬v' x = 1
h_2 : 1 < v' x
⊢ False

Tactic:
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
          exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))

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
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
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
hk : root k = (preReflection (root i) (p.flip (coroot i))) (root j)
⊢ coroot k = (preReflection (coroot i) (p (root i))) (coroot j)

Tactic:
set α := root i
  set β := root j
  set α' := coroot i
  set β' := coroot j
  set sα := preReflection α (p.flip α')
  set sβ := preReflection β (p.flip β')
  let sα' := preReflection α' (p α)
  have hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα := by
    ext
    have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
    simp [α, β, α', β', sα, sβ, sα', ← preReflection_preReflection β (p.flip β') hpi,
      preReflection_apply]
  obtain ⟨l, hl⟩ := hc i (mem_range_self j)
  rw [← hl]
  have hkl : (p.flip (coroot l)) (root k) = 2 := by
    simp only [hl, preReflection_apply, map_sub, map_smul, hk, LinearMap.flip_apply,
      LinearMap.sub_apply, hp j, LinearMap.smul_apply, smul_eq_mul, hp i, mul_two,
      sub_add_cancel_right, mul_neg, sub_neg_eq_add, sα, α, α', β]
    rw [mul_comm (p (root i) (coroot j))]
    abel
  suffices p.flip (coroot k) = p.flip (coroot l) from p.flip.toPerfPair.injective this
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  have := injOn_dualMap_subtype_span_range_range (finite_range root)
    (c := p.flip ∘ coroot) hp hr
  apply this (mem_range_self k) (mem_range_self l)
  refine Dual.eq_of_preReflection_mapsTo' (finite_range root)
    (Submodule.subset_span <| mem_range_self k) (hp k) (hr k) hkl ?_
  rw [comp_apply, hl, hk, hij]
  exact (hr i).comp <| (hr j).comp (hr i)

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

Goal state before:
pp: case 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
i j : ι
inst✝¹ : Nontrivial R
inst✝ : P.IsReduced
h : i ≠ j → P.root i = -P.root j
h' : i ≠ j
⊢ ∃ s t, s • -P.root j + t • P.root j = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
exact ⟨1, 1, by simp⟩

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
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4

Tactic:
have h₂ := P.pairing_smul_root_eq_of_not_linearIndependent h

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
this : IsAddTorsionFree M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j = 4
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
hα : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) • x - (chainTop (⇑α) β) (coroot α) • x = 0
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
← sub_smul,

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
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : (↑(chainLength α β) - (chainTop (⇑α) β) (coroot α)) • x = 0
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ⅟2 • (pi Q).polarBilin = ∑ i, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)

Tactic:
polarBilin_pi,

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ⅟2 • ∑ i, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i) =
    ∑ i, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Ring k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
n : ℕ
h : (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x
x✝ : Fin (n + 1)
⊢ Fin.init (fun j ↦ (ρ (g ^ ↑j)) x) x✝ = (ρ (g ^ ↑x✝)) x

Tactic:
simp [Fin.init]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
ι₂✝ : Type u_5
M₂✝ : Type u_6
N₂✝ : Type u_7
inst✝¹¹ : AddCommGroup M₂✝
inst✝¹⁰ : Module R M₂✝
inst✝⁹ : AddCommGroup N₂✝
inst✝⁸ : Module R N₂✝
P✝ : RootPairing ι R M N
Q : RootPairing ι₂✝ R M₂✝ N₂✝
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective (⇑(↑f).coweightMap ∘ ⇑(↑g).coweightMap)

Tactic:
exact Bijective.comp f.bijective_coweightMap g.bijective_coweightMap

Goal state after: