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

Goal state before:
pp: case ha
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0

pp: case hb
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk I ≠ 0

pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
        p.count (Associates.mk I).factors

Tactic:
·

Goal state after:
case ha
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q ↦ f ↑↑q)

pp: case refine_2.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

pp: case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑?refine_2.refine_2 ≤ f ↑q

Tactic:
·

Goal state after:
case refine_2.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ BddBelow (range fun q ↦ f ↑↑q)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
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 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
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hb
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk I ≠ 0

pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ (p : Associates (Ideal R)),
    Irreducible p →
      p.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
        p.count (Associates.mk I).factors

Tactic:
·

Goal state after:
case hb
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk I ≠ 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

pp: case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑?refine_2.refine_2 ≤ f ↑q

Tactic:
·

Goal state after:
case refine_2.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑⟨y, hxy⟩ ≤ f ↑q

Tactic:
·

Goal state after:
case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑⟨y, hxy⟩ ≤ f ↑q
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬BddAbove (range fun x ↦ ↑x)

Tactic:
dsimp only [BddAbove, upperBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_gt _

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
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i, i.maxPowDividing I → x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I → x ∈ ⨅ i, i.maxPowDividing I

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i, i.maxPowDividing I → x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I → x ∈ ⨅ i, i.maxPowDividing I

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I → x ∈ ⨅ i, i.maxPowDividing I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
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 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
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < 1

pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ f ↑g⁻¹ < 1

Tactic:
·

Goal state after:
case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ f ↑g⁻¹ < 1

Tactic:
·

Goal state after:
case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ f ↑g⁻¹ < 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
·

Goal state after:
case inl
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
·

Goal state after:
case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
have : Nonempty s := hs.to_subtype
            refine ciSup_le fun p ↦ (map_mul_le_add p.1 x y).trans ?_
            gcongr
            all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
·

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ (fun P ↦ primaryComponent M₂ P.asIdeal) P

pp: case refine_2
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j

Tactic:
·

Goal state after:
case refine_1
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ (fun P ↦ primaryComponent M₂ P.asIdeal) P
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
·

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inl
b : ℝ≥0∞
h : ∞ ≤ b
ht : b = ∞ → ∞ = ∞
⊢ ∞.toReal ≤ b.toReal

pp: case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal

Tactic:
·

Goal state after:
case inl
b : ℝ≥0∞
h : ∞ ≤ b
ht : b = ∞ → ∞ = ∞
⊢ ∞.toReal ≤ b.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal

Tactic:
·

Goal state after:
case inr
a b : ℝ≥0∞
h : a ≤ b
ht : b = ∞ → a = ∞
ha : a ≠ ∞
⊢ a.toReal ≤ b.toReal
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j

Tactic:
·

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
·

Goal state after:
case inl
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
·

Goal state after:
case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ∞ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ∞ ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

pp: case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
·

Goal state after:
case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ∞ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ∞ ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∧ ∞ = 0 ∨
    p = 0 ∧ ∞ = ∞ ∨
      p = 0 ∧ 0 < ∞.toReal ∨ p = ∞ ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ 0 < ∞.toReal ∧ p.toReal ≤ ∞.toReal

pp: case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
·

Goal state after:
case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∧ ∞ = 0 ∨
    p = 0 ∧ ∞ = ∞ ∨
      p = 0 ∧ 0 < ∞.toReal ∨ p = ∞ ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ 0 < ∞.toReal ∧ p.toReal ≤ ∞.toReal
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

Tactic:
·

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

Tactic:
·

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
·

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
·

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[↑x, ↑y]] ⊆ s

pp: case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[↑x, ↑y]] ⊆ s
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y