mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ 1 • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
⊢ (a * b) • c = a • b • c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
⊢ ∀ (x y : ⨁ (i : ιA), A i) (b : ⨁ (i : ιB), M i), (x * y) • b = x • y • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
⊢ ∀ (b : ⨁ (i : ιB), M i), 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
r s : ⨁ (i : ιA), A i
x : ⨁ (i : ιB), M i
⊢ (r + s) • x = r • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GSemiring A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ 0 • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ Module A (⨁ (i : ιM), ↥(𝓜 i))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J = I ⊓ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝¹ ⊔ x✝ ∣ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

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✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
h_minus_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
γ : Weight K (↥H) L :=
  { toFun := ⇑(Weight.toLinear K (↥H) L χ) - ⇑(Weight.toLinear K (↥H) L α), genWeightSpace_ne_bot' := h_minus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L (-α)
h_sum_in_range : S.root i + S.root j ∈ Set.range ⇑S.root
h_equiv : Weight.toLinear K (↥H) L χ ∈ ↑⟨q, ⋯⟩ ↔ S.root j ∈ ↑⟨q, ⋯⟩
⊢ S.root j ∈ ↑⟨q, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝¹ ⊔ x✝ ∣ x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ∀ {a b c : Ideal A}, a ∣ c → a ∣ b → a ∣ c ⊔ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ Associated ((x✝¹ ⊔ x✝) * (x✝¹ ⊓ x✝)) (x✝¹ * x✝)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : Ideal A
⊢ 0 ⊓ x✝ = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : Ideal A
⊢ x✝ ⊓ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
j : ιM
_hj : j ∈ DFinsupp.support ((decompose 𝓜) y)
⊢ (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ↑(((decompose 𝓜) y) j)) =
    ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) j)

Tactic:
show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
j : ιM
_hj : j ∈ DFinsupp.support ((decompose 𝓜) y)
⊢ (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ↑(((decompose 𝓜) y) j)) =
    ((Gmodule.smulAddMonoidHom (fun i ↦ ↥(𝓐 i)) fun i ↦ ↥(𝓜 i)) ((decompose 𝓐) ↑(((decompose 𝓐) x) i)))
      ((decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) j))
Module: Mathlib.Algebra.Lie.Weights.IsSimple

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✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
⊢ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
⊢ IsCoprime I J ↔ gcd I J = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : Ideal K[X]
hq : q ∈ Multiset.map (fun q ↦ span {q}) (factors p)
⊢ Prime q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: K : Type u_3
inst✝ : Field K
p : K[X]
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
⊢ spanSingleton A⁰ ((algebraMap A K) (↑I.den * ↑I.den * ↑J.den * ↑J.den)) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ιM), ↥(𝓜 i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
⊢ Module.Finite R ↥M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
a : Aˣ
⊢ (a • M).FG

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
a : Aˣ
x : V
⊢ x ∈ a • ⊤ ↔ x ∈ ⊤

Tactic:
refine ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
a : Aˣ
x : V
x✝ : x ∈ ⊤
⊢ x ∈ a • ⊤
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
a : Aˣ
x : V
x✝ : x ∈ ⊤
⊢ a⁻¹ • x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
a : Aˣ
⊢ span A ↑(a • M) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M N : Submodule R V
hle : M ≤ N
inst✝ : IsLattice A M
hfg : N.FG
⊢ ⊤ ≤ span A ↑M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := ↑s) K (⇑f ∘ Subtype.val)
hfin : Fintype ↑s
hcard : Fintype.card ↑s = finrank K N
⊢ (Set.range fun x ↦ f ↑x) ⊆ ↑f.range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
K : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Algebra R K
M N : Type u
inst✝⁸ : IsDomain R
inst✝⁷ : IsFractionRing R K
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module K N
inst✝¹ : IsScalarTower R K N
inst✝ : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
h : Module.rank K N ≤ Module.rank R M
⊢ span K ↑f.range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
⊢ (I ⊓ J) * (I ⊔ J) = I * J

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

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✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
h_minus_bot : genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α) = ⊥
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_eq : i = j
⊢ Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
⊢ LinearIndependent K fun i ↦ ↑(b i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ J ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
hli : LinearIndependent K fun i ↦ ↑(b i)
⊢ ⊤ ≤ span K (Set.range fun i ↦ (⇑M.subtype ∘ ⇑b) i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
k : κ
⊢ (Basis.extendOfIsLattice K b) k = ↑(b k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
V : Type u_3
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
inst✝⁴ : Module R V
inst✝³ : IsScalarTower R K V
inst✝² : IsDomain R
inst✝¹ : Module.Finite K V
inst✝ : IsFractionRing R K
M : Submodule R V
hfg : M.FG
hr : Module.rank K V ≤ Module.rank R ↥M
⊢ span K ↑M = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsTorsionFree R K
M : Submodule R V
inst✝ : IsLattice K M
⊢ Free R ↥M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsFractionRing R K
M : Submodule R V
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = Module.rank K V

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = ↑(Fintype.card ι)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
⊢ (M ⊓ N).FG

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
K : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
V : Type u_3
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Module R V
inst✝⁶ : IsScalarTower R K V
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Module.Finite K V
inst✝² : IsFractionRing R K
M N : Submodule R V
inst✝¹ : IsLattice K M
inst✝ : IsLattice K N
⊢ span K ↑(M ⊓ N) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hST : Codisjoint S T
hS : S.FG
this : Module.Finite R ↥S
⊢ Function.Surjective ⇑(T.mkQ.domRestrict S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ T.CoFG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ f.range.FG ↔ f.ker.CoFG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S ⊓ T).CoFG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
⊢ (sInf ↑s).CoFG

Tactic:
by

Goal state after: