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

Goal state before:
pp: 𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ ValuationRing 𝒪

Tactic:
suffices PreValuationRing 𝒪 from .mk

Goal state after:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ PreValuationRing 𝒪
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:
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.KrullDimension.Zero

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔ ∀ J ∈ comap (Quotient.mk I) '' minimalPrimes (R ⧸ I), J.IsMaximal

Tactic:
Set.forall_mem_image

Goal state after:
R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔
    ∀ ⦃x : Ideal (R ⧸ I)⦄, x ∈ minimalPrimes (R ⧸ I) → (comap (Quotient.mk I) x).IsMaximal
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) ϖ = 1

Tactic:
by
  simpa only [one_mul, eq_self_iff_true, Units.val_one, pow_one, forall_true_left, Nat.cast_one]
    using addVal_def ϖ 1 hϖ 1

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ 1 < v x ↔ v x⁻¹ < 1

Tactic:
simp [inv_lt_one₀ (v.pos_iff.2 h)]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
· simp only [← one_le_val_iff v h, le_total]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ Ideal.span {a} ≤ maximalIdeal R

Tactic:
rwa [Ideal.span_le, Set.singleton_subset_iff]

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

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x✝ : ∃ x, 1 < v x
x : K
hx1 : 1 < v x
⊢ v x ≠ 0 ∧ v x ≠ 1

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : (ofClass v) r ≠ 0
hs : (ofClass v) s ≠ 0
hr' : (ofClass w) r ≠ 0
hs' : (ofClass w) s ≠ 0
pf✝⁵ : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝⁴ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝³ : ∀ (d : { xy // (ofClass v) xy.1 ≠ 0 ∧ (ofClass v) xy.2 ≠ 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝² : ∀ (d : { xy // (ofClass v) xy.1 ≠ 0 ∧ (ofClass v) xy.2 ≠ 0 }), (ofClass v) (↑d).2 ≠ 0
H : ∃ d, ↑(valueGroup.mk (ofClass v) r s hr hs) = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑H.choose).1 ≠ 0
pf✝ : (ofClass w) (↑H.choose).2 ≠ 0
c_spec : ↑(valueGroup.mk (ofClass v) r s hr hs) = ↑(valueGroup.mk (ofClass v) (↑H.choose).1 (↑H.choose).2 ⋯ ⋯)
⊢ ↑(valueGroup.mk (ofClass w) (↑H.choose).1 (↑H.choose).2 pf✝¹ pf✝) = ↑(valueGroup.mk (ofClass w) r s hr' hs')

Tactic:
simp only [MonoidWithZeroHom.coe_ofClass, ne_eq, WithZero.coe_inj, valueGroup.mk_inj] at c_spec ⊢

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : (ofClass v) r ≠ 0
hs : (ofClass v) s ≠ 0
hr' : (ofClass w) r ≠ 0
hs' : (ofClass w) s ≠ 0
pf✝⁵ : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝⁴ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝³ : ∀ (d : { xy // (ofClass v) xy.1 ≠ 0 ∧ (ofClass v) xy.2 ≠ 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝² : ∀ (d : { xy // (ofClass v) xy.1 ≠ 0 ∧ (ofClass v) xy.2 ≠ 0 }), (ofClass v) (↑d).2 ≠ 0
H : ∃ d, ↑(valueGroup.mk (ofClass v) r s hr hs) = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝¹ : (ofClass w) (↑H.choose).1 ≠ 0
pf✝ : (ofClass w) (↑H.choose).2 ≠ 0
c_spec : v (r * (↑⋯.choose).2) = v ((↑⋯.choose).1 * s)
⊢ w ((↑⋯.choose).1 * s) = w (r * (↑⋯.choose).2)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: 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
⊢ P.jacobson = P

Tactic:
by_cases Pb : P = ⊥

Goal state after:
case pos
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

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
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates ↥R⁰
⊢ (associatesNonZeroDivisorsEquivIsPrincipal R).toFun (x✝¹ * x✝) =
    (associatesNonZeroDivisorsEquivIsPrincipal R).toFun x✝¹ * (associatesNonZeroDivisorsEquivIsPrincipal R).toFun x✝

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, Equiv.toFun_as_coe,
      associatesNonZeroDivisorsEquivIsPrincipal_mul]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates ↥R⁰
⊢ ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝¹) * ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝) =
    ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x✝¹ * (associatesNonZeroDivisorsEquivIsPrincipal R) x✝)
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case hf
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')))
⊢ (w'.comp (algebraMap R (S ⧸ Q'))).IsIntegral

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')))
⊢ w.toRingEquiv.toRingHom.IsIntegral

Tactic:
· apply RingHom.IsIntegral.trans
    · apply IH
      apply Polynomial.isMaximal_comap_C_of_isJacobsonRing
    · suffices w'.toRingHom = Ideal.quotientMap Q (Polynomial.C) le_rfl by
        rw [this]
        rw [isIntegral_quotientMap_iff _]
        apply Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
      rfl

Goal state after:
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')))
⊢ w.toRingEquiv.toRingHom.IsIntegral
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
x : R
hx : IsSquare x
⊢ IsSumSq x

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : MulOneClass R
⊢ IsSumSq 1

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSquare (x i)
⊢ IsSumSq (∑ i ∈ I, x i)

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
a : ι → R
⊢ IsSumSq (∑ i ∈ I, a i * a i)

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
a : ι → R
⊢ IsSumSq (∑ i ∈ I, a i ^ 2)

Tactic:
by aesop

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 : ι
contra : B.form (P.root i) = 0
⊢ (B.form (P.root i)) (P.root i) = 0

Tactic:
by simp [contra]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
L : Type u_8
inst✝⁶ : Field L
inst✝⁵ : Module L M
inst✝⁴ : Module L N
Q : RootPairing ι L M N
inst✝³ : Q.IsRootSystem
inst✝² : Finite ι
inst✝¹ : CharZero L
inst✝ : Q.IsCrystallographic
_i : Module ℚ M := compHom M (algebraMap ℚ L)
⊢ finrank ℤ ↥(Q.rootSpan ℤ) = finrank L M

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

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
L : Type u_8
inst✝⁶ : Field L
inst✝⁵ : Module L M
inst✝⁴ : Module L N
Q : RootPairing ι L M N
inst✝³ : Q.IsRootSystem
inst✝² : Finite ι
inst✝¹ : CharZero L
inst✝ : Q.IsCrystallographic
_i✝ : Module ℚ M := compHom M (algebraMap ℚ L)
_i : Module ℚ N := compHom N (algebraMap ℚ L)
⊢ finrank ℤ ↥(Q.rootSpan ℤ) = finrank L M
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 ι
j : ι
⊢ (P.RootForm (P.root j)) (P.root j) = ∑ i, P.pairing j i * P.pairing j i

Tactic:
by
  simp [rootForm_apply_apply]

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✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
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
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R N
this : IsTorsionFree S N
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.PolarizationIn S).range

Tactic:
have h_ne : ∏ i, (P.RootFormIn S (P.rootSpanMem S i) (P.rootSpanMem S i)) ≠ 0 := by
    refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_
    have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
    rw [algebraMap_rootFormIn] at this
    apply IsAnisotropic.rootForm_root_ne_zero i this

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✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
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
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R N
this : IsTorsionFree S N
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
⊢ finrank S ↥(P.corootSpan S) ≤ finrank S ↥(P.PolarizationIn S).range
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₁ P₂ : RootPairing ι R M N
inst✝¹ : P₁.IsRootSystem
inst✝ : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
⊢ P₁ = P₂

Tactic:
by
  suffices ∀ (P₁ P₂ : RootPairing ι R M N) [P₁.IsRootSystem] [P₂.IsRootSystem],
      P₁.toLinearMap = P₂.toLinearMap → P₁.root = P₂.root → range P₁.coroot ⊆ range P₂.coroot by
    have h₁ := this P₁ P₂ he hr
    have h₂ := this P₂ P₁ he.symm hr.symm
    exact RootPairing.ext he hr (le_antisymm h₁ h₂)
  clear! P₁ P₂
  rintro P₁ P₂ hP₁ hP₂ he hr - ⟨i, rfl⟩
  use i
  apply P₁.flip.toPerfPair.injective
  apply Dual.eq_of_preReflection_mapsTo (finite_range P₁.root) IsRootSystem.span_root_eq_top
  · exact hr ▸ he ▸ P₂.coroot_root_two i
  · change MapsTo (preReflection _ (P₁.toLinearMap.flip.toPerfPair _)) _ _
    simp_rw [hr, he]
    exact P₂.mapsTo_reflection_root i
  · exact P₁.coroot_root_two i
  · exact P₁.mapsTo_reflection_root i

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 : ι
c : R
hc : ∏ i, (P.RootForm (P.root i)) (P.root i) = (P.RootForm (P.root i)) (P.root i) * c
⊢ c • 2 • P.root i ∈ P.rootSpan R

Tactic:
by aesop

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
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 ι
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) (((P.posRootForm S).posForm x) y) = (P.RootForm ↑x) ↑y

Tactic:
simp [posRootForm]

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
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 ι
x : M
hx : x ∈ span S (range ⇑P.root)
⊢ (algebraMap S R) (((P.posRootForm S).posForm ⟨x, hx⟩) ⟨x, hx⟩) = (P.RootForm x) x

Tactic:
simp [posRootForm]

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
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 ι
x y : ↥(P.rootSpan S)
⊢ (algebraMap S R) (((P.posRootForm S).posForm x) y) = (algebraMap S R) (∑ i, (P.coroot'In S i) x * (P.coroot'In S i) y)

Tactic:
simp [posRootForm, rootForm_apply_apply]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case insert.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ↑s.card < ENat.card K → ⋃ i ∈ s, ↑(p i) ≠ univ
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
⊢ ⋃ i ∈ insert j s, ↑(p i) ≠ univ

Tactic:
specialize hj' (lt_trans ENat.natCast_lt_succ h₂)

Goal state after:
case insert.inr
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ⋃ i ∈ s, ↑(p i) ≠ univ
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
⊢ ⋃ i ∈ insert j s, ↑(p i) ≠ univ
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 i, P.root j]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4

Tactic:
rw [LinearIndependent.pair_symm_iff] at 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
⊢ P.coxeterWeight i j = 4
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
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
k : ι
hk : k ∈ s
t₁ t₂ : K
htne : x + t₁ • y ≠ x + t₂ • y
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
⊢ t₁ ≠ t₂

Tactic:
by aesop

Goal state after:
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
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
this : Injective fun t ↦ x + t • y
⊢ ENat.card K ≤ sxy.encard + 1

Tactic:
have aux : sxy = ((fun t : K ↦ x + t • y) '' {t | t ≠ 0}) := by ext; simp [sxy]

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
f : ↑sxy → ι
hf : ∀ (z : ↑sxy), ↑z ∈ ⋃ (_ : f z ∈ s), ↑(p (f z))
hf' : MapsTo f univ ↑s
this : Injective fun t ↦ x + t • y
aux : sxy = (fun t ↦ x + t • y) '' {t | t ≠ 0}
⊢ ENat.card K ≤ sxy.encard + 1
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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4

Tactic:
rw [pairing, pairing, h]

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✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsTorsionFree R N
h2 : IsSMulRegular R 2
this✝ : IsAddTorsionFree M
this : IsAddTorsionFree N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot j) = 1 ∧ (P.root' j) (2 • P.coroot j) = 4
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case a
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 α β ≤ chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β

Tactic:
← not_lt

Goal state after:
case a
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
⊢ ¬chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β < chainLength α β
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥

Tactic:
set k := chainTopCoeff α β - n with hk

Goal state after:
case mpr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ := ↑(chainTopCoeff (⇑α) β) - n
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ rootSpace H (n • ⇑α + ⇑β) ≠ ⊥