mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_2
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J

Tactic:
]

Goal state after:
case refine_2.refine_2
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
⊢ (↑J).FG

Tactic:
]

Goal state after:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
⊢ (↑J).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_3
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y✝ : K
hy✝¹ : y✝ ∈ I
x y : K
hx✝ : x ∈ Submodule.span A (f '' ↑s)
hy✝ : y ∈ Submodule.span A (f '' ↑s)
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * x + a * y ∈ ↑J

Tactic:
]

Goal state after:
case refine_2.refine_3
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y✝ : K
hy✝¹ : y✝ ∈ I
x y : K
hx✝ : x ∈ Submodule.span A (f '' ↑s)
hy✝ : y ∈ Submodule.span A (f '' ↑s)
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * x + a * y ∈ ↑J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_4
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx✝ : x ∈ Submodule.span A (f '' ↑s)
hx : a * x ∈ ↑J
⊢ b • (a * x) ∈ ↑J

Tactic:
]

Goal state after:
case refine_2.refine_4
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : ∀ i ∈ s, a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx✝ : x ∈ Submodule.span A (f '' ↑s)
hx : a * x ∈ ↑J
⊢ b • (a * x) ∈ ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
J : FractionalIdeal R₁⁰ K
hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I
s : Finset K
hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))
⊢ ↑J = ↑J

Tactic:
]

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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J * I⁻¹ < I⁻¹

Tactic:
]

Goal state after:
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J * I⁻¹ < I⁻¹
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < ↑⊤

Tactic:
]

Goal state after:
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
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < ↑⊤
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hx : x ∈ I
r' : R
hr' : (algebraMap R K) r' = r • x
⊢ (algebraMap S L) (f r') = (algebraMap S L) (f r')

Tactic:
]

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

Goal state before:
pp: case neg
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ I * iInf ?m.119 ≤ I * ⨅ i, J i

pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ Sort ?u.69

pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
⊢ ?m.117 → Ideal A

pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ?m.117
⊢ K ≤ ?m.119 i

Tactic:
]

Goal state after:
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ι
⊢ K ≤ J i
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ι
⊢ ⨅ i, I * J i ≤ I * J i

pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ι
⊢ 0 < I

Tactic:
]

Goal state after:
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ι
⊢ ⨅ i, I * J i ≤ I * J i

A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal A
ι : Type u_4
inst✝ : Nonempty ι
J : ι → Ideal A
hI : ¬I = 0
H : ⨅ i, I * J i ≤ I
K : Ideal A
hK : ⨅ i, I * J i = I * K
i : ι
⊢ 0 < I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J K : Ideal A
⊢ (⨅ i, I * bif i then J else K) = ⨅ b, bif b then I * J else I * K

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J K : Ideal A
⊢ (⨅ i, I * bif i then J else K) = ⨅ b, bif b then I * J else I * K
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)
⊢ ?m.51 = I ⊔ J

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := ⋯
⊢ Ideal A

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ ?m.51

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ ?m.51 ∣ gcd I J

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ I ⊔ J ∣ gcd I J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
x : K
⊢ ∀ (x_1 : L),
    x_1 ∈ ⟨Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (R ∙ x), ⋯⟩ ↔
      x_1 ∈ spanSingleton S⁰ ((IsLocalization.map L ↑f ⋯) x)

Tactic:
]

Goal state after:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
x : K
⊢ ∀ (x_1 : L),
    x_1 ∈ ⟨Submodule.map (↑(semilinearEquivOfRingEquiv K L f)) (R ∙ x), ⋯⟩ ↔
      x_1 ∈ spanSingleton S⁰ ((IsLocalization.map L ↑f ⋯) x)
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)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J
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)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J
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
⊢ ?m.129 = I ⊓ J

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := ⋯
hgcd : gcd I J = I ⊔ J
⊢ Ideal A

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 ∣ ?m.129

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
⊢ ?m.129 ∣ lcm I J

Tactic:
]

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

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
⊢ I ⊓ J ∣ lcm I J
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
i : ιB
xi : M i
⊢ ((smulAddMonoidHom A M) ((of A 0) GOne.one)) ((of M i) xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)

Tactic:
]

Goal state after:
ι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
i : ιB
xi : M i
⊢ ((smulAddMonoidHom A M) ((of A 0) GOne.one)) ((of M i) xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
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
i : ιB
xi : M i
⊢ (of M (0 +ᵥ i)) (GSMul.smul GOne.one xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)

Tactic:
]

Goal state after:
ι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
i : ιB
xi : M i
⊢ (of M (0 +ᵥ i)) (GSMul.smul GOne.one xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
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
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J

Tactic:
]

Goal state after:
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
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J
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
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ (of M ((ai + bi) +ᵥ ci)) (GSMul.smul (GMul.mul ax bx) cx) = (of M (ai +ᵥ bi +ᵥ ci)) (GSMul.smul ax (GSMul.smul bx cx))

Tactic:
]

Goal state after:
ι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
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ (of M ((ai + bi) +ᵥ ci)) (GSMul.smul (GMul.mul ax bx) cx) = (of M (ai +ᵥ bi +ᵥ ci)) (GSMul.smul ax (GSMul.smul bx cx))
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, ⋯⟩
⊢ -Weight.toLinear K (↥H) L α = -Weight.toLinear K (↥H) L α

Tactic:
]

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
⊢ I ∣ lcm I J ∧ J ∣ lcm I J

Tactic:
]

Goal state after:
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
⊢ I ∣ lcm I J ∧ J ∣ lcm I J
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
⊢ ∑ x_1 ∈ DFinsupp.support ((decompose 𝓐) x), (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) x_1) • y) =
    ∑ i ∈ DFinsupp.support ((decompose 𝓐) x), (RingHom.id A) ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) y

Tactic:
]

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
⊢ ∑ x_1 ∈ DFinsupp.support ((decompose 𝓐) x), (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) x_1) • y) =
    ∑ i ∈ DFinsupp.support ((decompose 𝓐) x), (RingHom.id A) ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) y
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
hlcm : lcm I J = I ⊓ J
⊢ I * J = I * J

Tactic:
]

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✝¹ * x✝

Tactic:
]

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)
⊢ ∑ x_1 ∈ DFinsupp.support ((decompose 𝓜) y),
      (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ↑(((decompose 𝓜) y) x_1)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) x_1)

Tactic:
]

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)
⊢ ∑ x_1 ∈ DFinsupp.support ((decompose 𝓜) y),
      (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ↑(((decompose 𝓜) y) x_1)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓐) x) i) • (decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) x_1)