mathlib-initiative/mathlib-tactics huggingface dataset:
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) ≤ 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) ≤ 1 + if y = 1 then 0 else 1
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬a₁ = 0

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬a₁ = 0
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: 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 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ r • p (-x) = r • p x

Tactic:
map_neg_eq_map p

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : ¬a = 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : ¬a = 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬a = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: 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 f g : NonarchAddGroupNorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f; cases g; congr

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ x ∈ s ↔ x ∈ s

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ x ∉ s ↔ x ∉ s

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
⊢ [[y, x]] ⊆ s ↔ [[y, x]] ⊆ s

Tactic:
]

Goal state after:
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
⊢ ↑y ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ s.ordT5Nhd t ⊓ t.ordT5Nhd s ⊆ ⊥

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ s.ordT5Nhd t ⊓ t.ordT5Nhd s ⊆ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ x ∈ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
H :
  ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄,
    ∀ a ∈ s,
      [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ →
        ∀ b ∈ t, [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ → a ≤ b → x ∈ ⊥
hab : ¬a ≤ b
⊢ x ∈ ⊥

pp: α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
⊢ x ∈ ⊥

Tactic:
· exact H b hbt hb a has ha (le_of_not_ge hab)

Goal state after:
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
⊢ x ∈ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
]

Goal state after:
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ s.ordSeparatingSet t
⊢ x ∈ ⊥

Tactic:
lift x to ordSeparatingSet s t using h'

Goal state after:
case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ ↑x ∈ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ ¬y < a ∧ ¬b < y

Tactic:
]

Goal state after:
case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ ¬y < a ∧ ¬b < y
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ a ∈ (closure[inst✝¹] t)ᶜ

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ a ∈ (closure[inst✝¹] t)ᶜ
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : a < a + b
⊢ a < a + b

Tactic:
]

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : a < a + b
⊢ a < a + b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x : ℝ≥0∞
⊢ x = ∞ ↔ x = ∞

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
h : a * b ≠ ∞
ha : a ≠ 0
⊢ a * b ≠ ∞

Tactic:
]

Goal state after:
a b : ℝ≥0∞
h : a * b ≠ ∞
ha : a ≠ 0
⊢ a * b ≠ ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mp
a b : ℝ≥0∞
h : a * b < ∞
⊢ ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞

Tactic:
]

Goal state after:
case mp
a b : ℝ≥0∞
h : a * b < ∞
⊢ ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
⊢ a = 0 → a < ∞

Tactic:
]

Goal state after:
a : ℝ≥0∞
⊢ a = 0 → a < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: m n : ℕ
⊢ ↑m - ↑n = ↑m - ↑n

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ x✝¹ - x✝ = x✝¹ - x✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a ≠ ∞

Tactic:
]

Goal state after:
case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a ≠ ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal p = ENNReal.ofReal p

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b - x✝ = b - x✝

pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b ≤ a

Tactic:
]

Goal state after:
case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b ≤ a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
iInf_of_empty,

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : IsEmpty ι
⊢ ∞.toNNReal = ⨅ i, (f i).toNNReal
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iInf f).toReal = ⨅ i, (f i).toReal

Tactic:
by
  simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]

Goal state after:
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ Icc x y

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ Icc x y
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⊥

Tactic:
]

Goal state after:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⊥
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ [[y, x]]

Tactic:
by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i

Tactic:
]

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬J = 0

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬J = 0
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
x : X
hx : x ∈ s
⊢ x ∈ (closure[inst✝¹] t)ᶜ

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
x : X
hx : x ∈ s
⊢ x ∈ (closure[inst✝¹] t)ᶜ
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c

Tactic:
]

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b

Tactic:
]

Goal state after:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬choose ⋯ = 0

Tactic:
]

Goal state after:
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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬choose ⋯ = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ ⨅ i ∈ s, a + i = ⨅ b ∈ s, a + b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulMono 𝕜 G
h : a < 0
⊢ a • b₂ ≤ b₁ ↔ a • b₂ ≤ b₁

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulMono 𝕜 G
h : a < 0
⊢ b₂ ≤ a • b₁ ↔ b₂ ≤ a • b₁

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ a • b₂ < b₁ ↔ a • b₂ < b₁

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ b₂ < a • b₁ ↔ b₂ < a • b₁

Tactic:
]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ iSup f = ⨆ i, f i

Tactic:
]

Goal state after: