mathlib-initiative/mathlib-tactics huggingface dataset:
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:
uIcc_of_ge (hx.2.trans this).le

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 inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
obtain rfl | ha := eq_or_ne a ∞

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

case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Goal state after:
case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ∞ + ⨆ i, f i = ⨆ i, ∞ + f i

case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

pp: case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
· simp [hy_top]

Goal state after:
case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal
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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ ↑1 - ↑((Associates.mk v.asIdeal).count 0) = 1

Tactic:
Associates.count_zero hv_irred,

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ ↑1 - ↑0 = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0 ∨ ∞ ≠ ∞
hb : a ≠ ∞ ∨ ∞ ≠ 0
⊢ (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹

Tactic:
simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
      mul_top, inv_top, mul_zero]

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

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ a = b

Tactic:
by rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]

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

Goal state before:
pp: case pos
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = 0

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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0

Tactic:
· rw [count_mul' K v, if_pos h, hI, hI', add_zero]

Goal state after:
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
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]
  exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

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

Goal state before:
pp: case mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ 0 < x ∧ x < ∞ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
rintro ⟨hx, h'x⟩

Goal state after:
case mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
hx : 0 < x
h'x : x < ∞
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
· refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
        simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)

Goal state after:
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' closedEBall a r = closedEBall (↑a) r ∩ {a | p a}

Tactic:
rw [← preimage_closedEBall, image_preimage_eq_inter_range, range_val_subtype]

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

Goal state before:
pp: case neg.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Goal state after:
case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨆ i, f i = ⨆ i, ∞ * f i

case neg.inr.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Goal state after:
case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨅ i, f i = ⨅ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

Tactic:
obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)

Goal state after:
case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i

case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∞ * ⨅ i, f i = ⨅ i, ∞ * f i
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y ≤ ↑c ↔ nndist x y ≤ c

Tactic:
by
  rw [edist_nndist, ENNReal.coe_le_coe]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε

Tactic:
by
    simp only [true_and, mem_ball, mem_Ici]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
by
  rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
  exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ
hC : 0 ≤ C
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s → ∀ ⦃x_1 : (x : β) → X x⦄, x_1 ∈ s → ↑(nndist (Function.eval i x) (Function.eval i x_1)) ≤ C) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C

Tactic:
lift C to ℝ≥0 using hC

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s → ∀ ⦃x_1 : (x : β) → X x⦄, x_1 ∈ s → ↑(nndist (Function.eval i x) (Function.eval i x_1)) ≤ ↑C) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ ↑C
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
x : K
e : b⁻¹ * a + FractionalIdeal.spanSingleton R⁰ x * 1 = b⁻¹ * c
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
use x

Goal state after:
case h
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
x : K
e : b⁻¹ * a + FractionalIdeal.spanSingleton R⁰ x * 1 = b⁻¹ * c
⊢ a + FractionalIdeal.spanSingleton R⁰ x * b = c
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

pp: R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
hb' : b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
· obtain ⟨x, e⟩ := this (a := b⁻¹ * a) (b := 1) (c := b⁻¹ * c) (by gcongr) (by simp [ha, hb])
      one_ne_zero rfl
    use x
    simpa [hb, ← mul_assoc, mul_add, mul_comm b (.spanSingleton _ _)] using congr(b * $e)

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✝
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
hb' : b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
by simp [hd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
by simp [hd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
by simp [hd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
by simp [hd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
by simp [hd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
by simp [hd]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
v : ℕ → β
hu : StrictMono (f ∘ v)
huxf : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
hux : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖

Tactic:
rw [dist_eq_norm_inv_mul', div_eq_inv_mul]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ p.asIdeal ^ Multiset.count p.asIdeal (normalizedFactors I) = p.asIdeal ^ multiplicity p.asIdeal I

Tactic:
count_normalizedFactors_eq_multiplicity hI

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ p.asIdeal ^ multiplicity p.asIdeal I = p.asIdeal ^ multiplicity p.asIdeal I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I

Tactic:
count_normalizedFactors_eq_multiplicity hI

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ multiplicity p.asIdeal I = multiplicity p.asIdeal I
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z

Tactic:
by
    simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

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

Goal state before:
pp: x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y

Tactic:
by
  simpa [add_comm] using add_lt_add_right_coe h z

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

Goal state before:
pp: a : EReal
⊢ 0 ≤ -a ↔ a ≤ 0

Tactic:
by rw [EReal.le_neg, neg_zero]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ b ≤ x

Tactic:
have hbx : ∃ᶠ _ in f, b ≤ x := by
    contrapose! h
    exact hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
a b : EReal
h : a ≤ b + ⊥
⊢ a - ⊥ ≤ b

Tactic:
rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]

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

Goal state before:
pp: x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x - t < y - z

Tactic:
refine sub_lt_of_lt_add' ?_

Goal state after:
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x < t + (y - z)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inr.refine_2
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
⊢ ⨆ i, u i v < b

Tactic:
apply lt_of_le_of_lt (iSup_le fun n ↦ ?_) hb''b.2

Goal state after:
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
⊢ u n v ≤ b''
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
⊢ x * -y = -(x * y)

Tactic:
rw [x.mul_comm, x.mul_comm]
    exact y.neg_mul x

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
⊢ (conditional β).support = univ

Tactic:
by
  simpa [eq_univ_iff_forall, support, -eventually_and]
    using! fun x ↦ prod_mem_prod (eventually_le_atBot x) (eventually_ge_atTop x)

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
h'd : c < d
e : R
he : e ∈ {a | ∀ᶠ (n : R) in F, n ≤ a}
fe_eq_d : f e = d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∏ i ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) i = ∏ b ∈ ⋯.toFinset, f b

Tactic:
exact Finset.prod_congr rfl (by simp_all)

Goal state after: