mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ * spanSingleton R⁰ ((algebraMap R K) a) = ↑J * spanSingleton R⁰ ((algebraMap R K) 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:
← coeIdeal_span_singleton,

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 * spanSingleton R⁰ ((algebraMap R K) 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.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 * spanSingleton R⁰ ((algebraMap R K) 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:
← coeIdeal_span_singleton,

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.Data.EReal.Basic

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊤

Tactic:
rcases lt_trichotomy x 0 with (hx | rfl | hx)
    exacts [neg_top x hx, zero_top, pos_top x hx]

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ (⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
⊢ P ⊤ ↑y

Tactic:
by
    rcases lt_trichotomy y 0 with (hy | rfl | hy)
    exacts [top_neg y hy, top_zero, top_pos y hy]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal

pp: case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
· simp only [h', bot_le]

Goal state after:
case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ⊥ ↑y = Iic y

Tactic:
by
  rw [← Ioi_inter_Iic]
  simp

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
y : ℝ≥0∞
⊢ ↑(∞ + y) = ↑∞ + ↑y

Tactic:
cases y

Goal state after:
case top.top
⊢ ↑(∞ + ∞) = ↑∞ + ↑∞

case top.coe
x✝ : ℝ≥0
⊢ ↑(∞ + ↑x✝) = ↑∞ + ↑↑x✝
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
y : ℝ≥0∞
x✝ : ℝ≥0
⊢ ↑(↑x✝ + y) = ↑↑x✝ + ↑y

Tactic:
cases y

Goal state after:
case coe.top
x✝ : ℝ≥0
⊢ ↑(↑x✝ + ∞) = ↑↑x✝ + ↑∞

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ↑(↑x✝¹ + ↑x✝) = ↑↑x✝¹ + ↑↑x✝
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
toENNReal_ne_zero_iff

Goal state after:
x : EReal
⊢ 0 < x ↔ 0 < x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ENNReal.ofReal x.toReal = x

pp: x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬↑x = ⊤

Tactic:
ENNReal.ofReal_toReal_eq_iff

Goal state after:
case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ x ≠ ∞

x : ℝ≥0∞
h_top : ¬x = ∞
⊢ ¬↑x = ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x / y ≤ z ↔ x ≤ z * y

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ (2 ^ n)⁻¹ < (↑n)⁻¹

Tactic:
ENNReal.inv_lt_inv

Goal state after:
a : ℝ≥0∞
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ↑n < 2 ^ n
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
convert! finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2

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
I : FractionalIdeal R⁰ K
hI : ¬I = 0
x✝ : HeightOneSpectrum R
⊢ count K x✝ I =
    ↑((Associates.mk x✝.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk x✝.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ (ball x ε ∪ sphere x ε) \ sphere x ε = ball x ε

Tactic:
Set.union_sdiff_cancel_right sphere_disjoint_ball.symm.le_bot

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε = ball x ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ Bornology.IsBounded univ ↔ ∃ C, ∀ (a b : α), dist a b ≤ C

Tactic:
Metric.isBounded_iff

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ univ → ∀ ⦃y : α⦄, y ∈ univ → dist x y ≤ C) ↔ ∃ C, ∀ (a b : α), dist a b ≤ C
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s

Tactic:
rcases hf ε₀ with ⟨i, hi, H⟩

Goal state after:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p | dist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
this : ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤
⊢ ∃ a, J * I ⊔ Ideal.span {a} = J

Tactic:
obtain ⟨a, K, e, e'⟩ := this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ ∃ a, J * I ⊔ Ideal.span {a} = J
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case pos
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
exact ((OrderIso.smulRight ha').map_csInf' hs h).symm

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

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h

Tactic:
mul_iInf

Goal state after:
ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ i, g * h i
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range f) ↔ ∀ r > 0, ∃ y, dist x (f y) < r

Tactic:
by simp only [mem_closure_iff, exists_range_iff]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ioc a b) = Ioo a b

Tactic:
by
  rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
by
  obtain hr | rfl | hr := lt_trichotomy r 0
  · simp [hr]
  · rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]
    let := h.resolve_left (lt_irrefl _)
    inhabit β
    refine subset_iUnion_of_subset default ?_
    intro x hx
    replace hx := hx.le
    rw [dist_pi_le_iff le_rfl] at hx
    exact le_antisymm (hx default) dist_nonneg
  · ext
    simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
simpa using! hs.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

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

Goal state before:
pp: X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
      (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)

Goal state after:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝²] (s.domRestrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : s.domRestrict f b = s.domRestrict g b
⊢ ∃ x ∈ s, f x = g x
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : PreconnectedSpace α
x y : α
hxy : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
by
    suffices (Iio y ∩ Ioi x).Nonempty by grind [Set.inter_nonempty_iff_exists_left]
    exact nonempty_inter (isOpen_Iio' y) (isOpen_Ioi' x) (Set.Iio_union_Ioi_of_lt hxy)
      ⟨x, Set.mem_Iio.mpr hxy⟩ ⟨y, Set.mem_Ioi.mpr hxy⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
by_cases hyK : y ∈ K

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∈ K
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

case neg
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∉ K
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ (↑I).subtype.range ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J

Tactic:
Submodule.range_subtype

Goal state after:
case refine_3
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖u⁻¹ * u * v‖

Tactic:
inv_mul_cancel,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖1 * v‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

Tactic:
mul_min_of_nonneg _ _ (by positivity)

Goal state after:
E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
⊢ Icc a b ⊆ s

Tactic:
obtain ⟨⟨t₁a, t₁b⟩, ht₁⟩ : t₁ ∈ A := by
    refine ⟨t₁_mem, fun t ht ↦ ?_⟩
    rcases ht.2.eq_or_lt with rfl | h
    · have : closure A ⊆ s ∩ Icc a b := by
        apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)
        have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
        exact ht.2 this
      apply this.trans inter_subset_left
      exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A
    · obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
      apply cA.2
      exact ⟨ht.1, tc.le⟩

Goal state after:
case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
⊢ Icc a b ⊆ s
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = ∅ ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
· exact ⟨fun i ↦ ∅, monotone_const, by simp_all⟩

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Ioi (e.symm a))

Tactic:
apply isOpen_lt'

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ BddAbove (range f)

Tactic:
have : Nonempty β := ⟨b⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (range f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥

Tactic:
by
  constructor <;> intro h
  · rintro rfl
    rw [add_bot] at h
    exact bot_ne_top h
  · cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h

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

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
hx : ¬↑a✝ = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬↑a✝ = ⊤ ∧ ¬y = ⊤

Tactic:
cases y

Goal state after:
case coe.bot
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊥ = ⊥
⊢ ¬↑a✝ + ⊥ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊥ = ⊤

case coe.coe
a✝¹ : ℝ
hx : ¬↑a✝¹ = ⊥
a✝ : ℝ
hy : ¬↑a✝ = ⊥
⊢ ¬↑a✝¹ + ↑a✝ = ⊤ → ¬↑a✝¹ = ⊤ ∧ ¬↑a✝ = ⊤

case coe.top
a✝ : ℝ
hx : ¬↑a✝ = ⊥
hy : ¬⊤ = ⊥
⊢ ¬↑a✝ + ⊤ = ⊤ → ¬↑a✝ = ⊤ ∧ ¬⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
h_top : ⊥ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥

Tactic:
cases y

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊥ - ↑a✝ ↔ ↑a✝ ≤ ⊥

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊤ ↔ ⊤ ≤ ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ↑a✝ - y ↔ y ≤ ↑a✝

Tactic:
cases y

Goal state after:
case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ↑a✝¹ - ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊤ ↔ ⊤ ≤ ↑a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
h_top : ⊤ ≠ ⊤ ∨ y ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤

Tactic:
cases y

Goal state after:
case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊥ ↔ ⊥ ≤ ⊤

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊤ - ↑a✝ ↔ ↑a✝ ≤ ⊤

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊤ ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y

Tactic:
cases y

Goal state after:
case bot.bot
⊢ ⊥ - ⊥ ≤ 0 ↔ ⊥ ≤ ⊥

case bot.coe
a✝ : ℝ
⊢ ⊥ - ↑a✝ ≤ 0 ↔ ⊥ ≤ ↑a✝

case bot.top
⊢ ⊥ - ⊤ ≤ 0 ↔ ⊥ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ - y ≤ 0 ↔ ↑a✝ ≤ y

Tactic:
cases y

Goal state after:
case coe.bot
a✝ : ℝ
⊢ ↑a✝ - ⊥ ≤ 0 ↔ ↑a✝ ≤ ⊥

case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ - ↑a✝ ≤ 0 ↔ ↑a✝¹ ≤ ↑a✝

case coe.top
a✝ : ℝ
⊢ ↑a✝ - ⊤ ≤ 0 ↔ ↑a✝ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y

Tactic:
cases y

Goal state after:
case top.bot
⊢ ⊤ - ⊥ ≤ 0 ↔ ⊤ ≤ ⊥

case top.coe
a✝ : ℝ
⊢ ⊤ - ↑a✝ ≤ 0 ↔ ⊤ ≤ ↑a✝

case top.top
⊢ ⊤ - ⊤ ≤ 0 ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
⊢ 0 < ⊥ - y ↔ y < ⊥

Tactic:
cases y

Goal state after:
case bot.bot
⊢ 0 < ⊥ - ⊥ ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
⊢ 0 < ⊥ - ↑a✝ ↔ ↑a✝ < ⊥

case bot.top
⊢ 0 < ⊥ - ⊤ ↔ ⊤ < ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
⊢ 0 < ↑a✝ - y ↔ y < ↑a✝

Tactic:
cases y

Goal state after:
case coe.bot
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊥ ↔ ⊥ < ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
⊢ 0 < ↑a✝¹ - ↑a✝ ↔ ↑a✝ < ↑a✝¹

case coe.top
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊤ ↔ ⊤ < ↑a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
⊢ 0 < ⊤ - y ↔ y < ⊤

Tactic:
cases y

Goal state after:
case top.bot
⊢ 0 < ⊤ - ⊥ ↔ ⊥ < ⊤

case top.coe
a✝ : ℝ
⊢ 0 < ⊤ - ↑a✝ ↔ ↑a✝ < ⊤

case top.top
⊢ 0 < ⊤ - ⊤ ↔ ⊤ < ⊤