mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
·

Goal state after:
case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr.right
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z

Tactic:
·

Goal state after:
case mpr.right
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
⊢ ∃ y_1 ∈ N₁, ∃ z_1 ∈ N₂, y_1 + z_1 = y + z
Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s / t) (a / b)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Goal state after:
G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s * t⁻¹) (a * b⁻¹)
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

Tactic:
·

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • 0 = 0

pp: case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i

Tactic:
·

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • 0 = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i, i.maxPowDividing (span {a}) → x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a})

pp: case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a}) → x ∈ ⨅ i, i.maxPowDividing (span {a})

Tactic:
·

Goal state after:
case mp
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i, i.maxPowDividing (span {a}) → x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a})
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i

Tactic:
·

Goal state after:
case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a}) → x ∈ ⨅ i, i.maxPowDividing (span {a})

Tactic:
·

Goal state after:
case mpr
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a}) → x ∈ ⨅ i, i.maxPowDividing (span {a})
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ht S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
·

Goal state after:
case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ht S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
·

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
⊢ x ≤ mk g

pp: case refine_2
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
·

Goal state after:
case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
⊢ x ≤ mk g
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
·

Goal state after:
case refine_2
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Tactic:
·

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Tactic:
·

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

pp: case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Tactic:
·

Goal state after:
case refine_1
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
⊢ ↑(sSup ∅) = sSup (toReal '' ∅)

pp: case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
·

Goal state after:
case inl
⊢ ↑(sSup ∅) = sSup (toReal '' ∅)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case pos
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
a : A
ha : a ∈ A⁰
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : x ∈ ⨆ (_ : P ∈ S), torsionBySet A M ↑(P.maxPowDividing (span {a}))
hPS : P ∈ S
⊢ x ∈ primaryComponent M P.asIdeal

pp: case neg
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
a : A
ha : a ∈ A⁰
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : x ∈ ⨆ (_ : P ∈ S), torsionBySet A M ↑(P.maxPowDividing (span {a}))
hPS : P ∉ S
⊢ x ∈ primaryComponent M P.asIdeal

Tactic:
·

Goal state after:
case pos
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
a : A
ha : a ∈ A⁰
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : x ∈ ⨆ (_ : P ∈ S), torsionBySet A M ↑(P.maxPowDividing (span {a}))
hPS : P ∈ S
⊢ x ∈ primaryComponent M P.asIdeal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Tactic:
·

Goal state after:
case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

pp: case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
·

Goal state after:
case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨆ x, 0 = 0

pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨆ x, 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
·

Goal state after:
case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0

pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
⊢ sSup (-∅) = -sInf ∅

pp: case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s

Tactic:
·

Goal state after:
case inl
⊢ sSup (-∅) = -sInf ∅
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case pos
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
⊢ sSup (-s) = -sInf s

pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s

Tactic:
·

Goal state after:
case pos
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
⊢ sSup (-s) = -sInf s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s

Tactic:
·

Goal state after:
case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅

pp: case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
·

Goal state after:
case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
⊢ ↑(sInf ∅) = sInf (toReal '' ∅)

pp: case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
·

Goal state after:
case inl
⊢ ↑(sInf ∅) = sInf (toReal '' ∅)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
·

Goal state after:
case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
hs : ∀ x ∈ ∅, x ≤ 0
⊢ sInf ∅ ≤ 0

pp: case inr
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Tactic:
·

Goal state after:
case inl
hs : ∀ x ∈ ∅, x ≤ 0
⊢ sInf ∅ ≤ 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Tactic:
·

Goal state after:
case inr
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

pp: case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
·

Goal state after:
case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
·

Goal state after:
case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False

pp: case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False

Tactic:
·

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ ∏ v ∈ Finite.toFinset h✝, v.maxPowDividing I ≠ 0

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ ∏ v ∈ Finite.toFinset h✝, v.maxPowDividing I ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
by
  rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False

Tactic:
·

Goal state after:
case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

pp: case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
·

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
toNNReal_eq_zero.mpr hx,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = 0⁻¹
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Tactic:
·

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Tactic:
·

Goal state after:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

pp: case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s

Tactic:
·

Goal state after:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s