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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ ↑(RelSeries.smash t' s' ⋯).length = ↑t.length + ↑s.length

Tactic:
RelSeries.smash_length,

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ ↑(t'.length + s'.length) = ↑t.length + ↑s.length
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
h✝ : Infinite ι
a✝ : Nontrivial M
m : ℕ
⊢ ↑m ≤ length R (ι →₀ M)

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq ι m

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_5
h✝ : Infinite ι
a✝ : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
⊢ ↑m ≤ length R (ι →₀ M)
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
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ length R M = ↑(finrank R M) * length R R

Tactic:
length_of_free,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Cardinal.toENat (Module.rank R M) * length R R = ↑(finrank R M) * length R R
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inl
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
x : F
h : v x ≤ 1
a : O
ha : (algebraMap O F) a = x
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

pp: case inr
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
x : F
h : v x⁻¹ ≤ 1
a : O
ha : (algebraMap O F) a = x⁻¹
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Tactic:
exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]

Goal state after:
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
⊢ ∀ (a b : ValueGroup A K), a ≤ b → b ≤ a → a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨e, rfl⟩ ⟨f, hf⟩
    by_cases hb : b = 0; · simp [hb]
    have : IsUnit e := by
      apply isUnit_of_dvd_one
      use f
      rw [mul_comm]
      rw [← mul_smul, Algebra.smul_def] at hf
      nth_rw 2 [← one_mul b] at hf
      rw [← (algebraMap A K).map_one] at hf
      exact IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm
    apply Quotient.sound'
    exact ⟨this.unit, rfl⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : Submodule.comap (⨅ n, I ^ n • ⊤).mkQ (Submodule.map (⨅ n, I ^ n • ⊤).mkQ (I ^ n • ⊤)) = I ^ n • ⊤
⊢ (⨅ n, I ^ n • ⊤).mkQ x ∈ I ^ n • ⊤

Tactic:
← SModEq.zero

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : Submodule.comap (⨅ n, I ^ n • ⊤).mkQ (Submodule.map (⨅ n, I ^ n • ⊤).mkQ (I ^ n • ⊤)) = I ^ n • ⊤
⊢ (⨅ n, I ^ n • ⊤).mkQ x ≡ 0 [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Tactic:
have : IsDomain 𝒪 := hinj.isDomain

Goal state after:
𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this : IsDomain 𝒪
⊢ IsFractionRing 𝒪 K
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Surjective ⇑(of I M) → IsPrecomplete I M

pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsPrecomplete I M → Function.Surjective ⇑(of I M)

Tactic:
· refine fun h ↦ ⟨fun f hmn ↦ ?_⟩
    let u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), fun c ↦ (hmn c).symm⟩
    obtain ⟨x, hx⟩ := h u
    refine ⟨x, fun n ↦ ?_⟩
    simp only [SModEq]
    rw [← mkQ_apply _ x, ← eval_of, hx]
    simp [u]

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsPrecomplete I M → Function.Surjective ⇑(of I M)
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 : ℕ
r : R
r_in : r ∈ I ^ n
x : AdicCompletion I M
⊢ r • out (↑x n) ∈ I ^ n • ⊤

Tactic:
exact smul_mem_smul r_in mem_top

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R

Tactic:
by
  classical
  constructor
  intro I
  by_cases I0 : I = ⊥
  · rw [I0]
    use 0
    simp only [Set.singleton_zero, Submodule.span_zero]
  obtain ⟨x, hxI, hx0⟩ : ∃ x ∈ I, x ≠ (0 : R) := I.ne_bot_iff.mp I0
  obtain ⟨p, _, H⟩ := HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible h₁ h₂
  have ex : ∃ n : ℕ, p ^ n ∈ I := by
    obtain ⟨n, u, rfl⟩ := H hx0
    refine ⟨n, ?_⟩
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hxI
  constructor
  use p ^ Nat.find ex
  change I = Ideal.span _
  apply le_antisymm
  · intro r hr
    by_cases hr0 : r = 0
    · simp only [hr0, Submodule.zero_mem]
    obtain ⟨n, u, rfl⟩ := H hr0
    simp only [mem_span_singleton, Units.isUnit, IsUnit.dvd_mul_right]
    apply pow_dvd_pow
    apply Nat.find_min'
    simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hr
  · rw [span_singleton_le_iff_mem]
    exact Nat.find_spec ex

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
x y : R
hy : y ∈ nonZeroDivisors R
hx : (algebraMap R K) x / (algebraMap R K) y ≠ 0
⊢ x ≠ 0

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit ((algebraMap A (FractionRing A)) ↑⟨y, hy⟩)

Tactic:
exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
⊢ v₁ x < v₁ y ↔ v₂ x < v₂ y

Tactic:
rw [← le_iff_le_iff_lt_iff_lt, h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝ : R
⊢ (fun I ↦ Associates.mk (IsPrincipal.generator ↑I)) (Quotient.lift (fun x ↦ ⟨span {x}, ⋯⟩) ⋯ ⟦x✝⟧) = ⟦x✝⟧

Tactic:
by simpa [Quotient.eq] using!
    Ideal.span_singleton_eq_span_singleton.mp (@Ideal.span_singleton_generator _ _ _ ⟨_, rfl⟩)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
m : M
r : R
hr : r ∈ R⁰
h : ⟨r, hr⟩ • m = 0
⊢ (fun x ↦ r • x) m = (fun x ↦ r • x) 0

Tactic:
by simpa using h

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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.root i, ⋯⟩) i = (fun i ↦ ⟨P.root i, ⋯⟩) j
⊢ i = j

Tactic:
by simpa using h

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

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.coroot i, ⋯⟩) i = (fun i ↦ ⟨P.coroot i, ⋯⟩) j
⊢ i = j

Tactic:
by simpa using h

Goal state after:
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✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint (P.rootSpan R) (LinearMap.ker P.RootForm)

Tactic:
rw [← P.ker_polarization_eq_ker_rootForm]

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✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ Disjoint (P.rootSpan R) P.Polarization.ker
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 := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ (p.flip.toPerfPair ((preReflection α' (p α)) β')) (root k) = 2

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

Tactic:
· simp [map_sub, α, β, α', β', sα, hk, preReflection_apply, hp i, hp j,
      mul_comm (p α β')]
    ring

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 := ⋯
β : M := ⋯
α' : N := ⋯
β' : N := ⋯
sα : End R M := ⋯
hk : root k = sα β
sβ : End R M := ⋯
sα' : End R N := ⋯
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo (⇑(preReflection (root k) (p.flip.toPerfPair ((preReflection α' (p α)) β')))) (range ⇑root) (range ⇑root)
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
inst✝ : Fintype ι
i✝ j i : ι
⊢ ∃ s > 0, (algebraMap S R) s = (P.RootForm (P.root i)) (P.root i)

Tactic:
refine ⟨∑ k, P.pairingIn S i k ^ 2, ?_, by simp [sq, rootForm_apply_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✝⁷ : 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
inst✝ : Fintype ι
i✝ j i : ι
⊢ ∑ k, P.pairingIn S i k ^ 2 > 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✝⁴ : Field R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
i : ι
⊢ P.coroot i = (2 / (P.RootForm (P.root i)) (P.root i)) • P.PolarizationEquiv (P.root i)

Tactic:
have h₀ := IsAnisotropic.rootForm_root_ne_zero (P := P) i
  rw [polarizationEquiv_apply, ← (smul_right_injective N h₀).eq_iff, P.rootForm_self_smul_coroot i,
    smul_smul, mul_div_cancel₀ _ h₀]
  norm_cast

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
hα : ¬α.IsZero
⊢ chainTopCoeff (⇑α) β ≤ chainLength α β

Tactic:
rw [← not_lt, ← Nat.succ_le_iff]

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
⊢ ¬(chainLength α β).succ ≤ chainTopCoeff (⇑α) β
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
n : ℤ
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ≤ ↑(chainTopCoeff (⇑α) β) ∧ -n ≤ ↑(chainBotCoeff (⇑α) β)

Tactic:
by
  constructor
  · refine (fun hn ↦ ⟨?_, le_chainBotCoeff_of_rootSpace_ne_top α β hα _ (by rwa [neg_neg])⟩)
    rw [← chainBotCoeff_neg, ← Weight.coe_neg]
    apply le_chainBotCoeff_of_rootSpace_ne_top _ _ hα.neg
    rwa [neg_smul, Weight.coe_neg, smul_neg, neg_neg]
  · 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.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.mem
ι : 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 w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
⊢ P.weylGroupToPerm ⟨w', ⋯⟩ ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
y : G
z : Gᵐᵒᵖ
hz : z ∈ S.op
w : V
⊢ ↑(y * MulOpposite.unop z) = ↑y

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedLinear

Goal state before:
pp: α : Type u_1
I : Set α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
h' : I.OrdConnected
x : α
hx : x ∈ I
y : α
hy : y ∈ I
hxy : Ioo x y ⊆ Iᶜ
z : α
hz : x < z
this : z ∉ Ioo x y
⊢ y ≤ z

Tactic:
by simp_all

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
i j : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ 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
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : P.coxeterWeightIn ℤ i j ≤ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
i j : ↥b.support
hij : i ≠ j
this : {↑j, ↑i} ⊆ ↑b.support
⊢ Injective ![P.root ↑i, P.root ↑j]

Tactic:
by simp_all

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i : Module ℚ M := compHom M (algebraMap ℚ R)
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)

Tactic:
let _i : Module ℚ N := Module.compHom N (algebraMap ℚ R)

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)
⊢ LinearIndepOn R (⇑P.root) (baseOf (⇑P.root) f)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rw [← neg_mem_range_root_iff, neg_sub]

Goal state after:
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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝¹ : Module.IsReflexive R M
this✝ : Module.IsReflexive R N
this : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
h₁ : P.pairing j i = 1
⊢ P.root j - P.root i ∈ range ⇑P.root
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
this : InvolutiveNeg ι := P.indexNeg
hf : ∀ i ∈ baseOf (⇑P.root) f, f (P.root i) = 1
i : ι
⊢ f (P.root i) ≠ 0

Tactic:
by simp_all

Goal state after: