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

Goal state before:
pp: 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})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
⊢ ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : 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, (1 - (S i).indicator 1 a)) • f a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
inst✝ : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a - ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a =
    ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a = ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.biUnion S)) = ∑ t, (-1) ^ (#↑t + 1) * ↑(#((↑t).inf' ⋯ S))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a, f a - ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ t.inf S, f a +
      ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i ↦ (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |(fun i ↦ ↑(f i)) j - (fun i ↦ ↑(f i)) i| < ε

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs fun i ↦ ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun i ↦ ↑(f i)) j - (fun i ↦ ↑(f i)) i| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}

Tactic:
by

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

Goal state before:
pp: 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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(↑(f n) / ↑n) ≤ y

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)

Tactic:
by

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

Goal state before:
pp: 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)
ε : ℚ
ε0 : ε > 0
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
⊢ ∃ i, ∀ j ≥ i, |(fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) i| < ε

Tactic:
by

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

Goal state before:
pp: 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)
⊢ IsCauSeq abs fun n ↦ ↑(f n) / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ v.maxPowDividing I = v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) v = (fun v ↦ ⟨(↑v).asIdeal, ⋯⟩) w
⊢ ((fun a ↦ ↑a) v).asIdeal = ((fun a ↦ ↑a) w).asIdeal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.asIdeal ∣ I}.Finite

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
hne : s.Nonempty
hbdd : BddAbove s
⊢ ∃ x, IsLUB s x

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
⊢ ∃ x, IsGLB s x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ x • ↑y

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ
s✝ : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: p q : ℝ≥0
h1p : 0 < p
h2p : p ≤ q
⊢ q⁻¹ ≤ p⁻¹

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ
s✝ : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = NNReal.mk r hr

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Zero ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ One ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Add ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Sub ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Mul ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inv ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Div ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ LE ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Bot ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inhabited ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Nontrivial ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = 0 ↔ r = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = 1 ↔ r = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommSemiring ℝ≥0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ v.maxPowDividing I = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r✝ r₁ r₂ : ℝ≥0
x✝ y : ℝ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : A
⊢ ((algebraMap ℝ A).comp toRealHom) r * x = x * ((algebraMap ℝ A).comp toRealHom) r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r✝ r₁ r₂ : ℝ≥0
x✝ y : ℝ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : A
⊢ r • x = ((algebraMap ℝ A).comp toRealHom) r * x

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ Algebra ℝ≥0 ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ DistribMulAction ℝ≥0ˣ ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ MonoidWithZero ℝ≥0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.maxPowDividing I ≠ 1} ⊆ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommMonoidWithZero ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommGroupWithZero ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrder ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ 1 ≤ ↑r ↔ 1 ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ 1 < ↑r ↔ 1 < r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r ≤ 1 ↔ r ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r < 1 ↔ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNNReal = ↑↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ OrderBot ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ PartialOrder ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ AddCommMonoid ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ IsOrderedAddMonoid ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DistribLattice ℝ≥0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeInf ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeSup ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ Semiring ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ CommMonoid ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrderedCommMonoidWithZero ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DenselyOrdered ℝ≥0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ NoMaxOrder ℝ≥0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ sSup (Subtype.val '' s) ∈ Set.Ici 0

Tactic:
by

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

Goal state before:
pp: ⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
by

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

Goal state before:
pp: ⊢ sInf Set.univ = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨆ i, f i = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
by

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

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨅ i, f i = 0

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨅ x, 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
⊢ sSup (-s) = -sInf s

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
⊢ sInf (-s) = -sSup s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
⊢ sSup s ≤ a

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
⊢ a ≤ sInf s

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(⨆ i, s i) = ⨆ i, ↑(s i)

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
hs : s.Nonempty
⊢ sInf (Subtype.val '' s) ∈ Set.Ici 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
by

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

Goal state before:
pp: s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(⨅ i, s i) = ⨅ i, ↑(s i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
h : ↑a < ↑b
q : ℚ
haq : ↑a < ↑q
hqb : ↑q < ↑b
this : 0 ≤ ↑q
⊢ a < (↑q).toNNReal ∧ (↑q).toNNReal < b

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ 0 < r.toNNReal ↔ 0 < r

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
by

Goal state after: