mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : p ≤ under R w
⊢ p = v

Tactic:
← Ideal.over_def w v

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : p ≤ v
⊢ p = v
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ * f (g s) ∈ f.range

Tactic:
rw [this, IsLocalization.mk'_spec_mk]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : ∀ (x : A ⊗[R] S), f (g x) = (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ (algebraMap (A ⊗[R] S) (Localization.AtPrime q)) x ∈ f.range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial.monomial
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
m : ι →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((m.prod fun x1 x2 ↦ Q.val x1 ^ x2) * n.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r

Tactic:
mul_comm (m.prod _) (n.prod _)

Goal state after:
case monomial.monomial
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
m : ι →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
⊢ Ω[Q.Ring⁄R] →ₗ[Q.Ring] T ⊗[S] P.CotangentSpace

Tactic:
refine LinearMap.liftBaseChange _ ?_ ∘ₗ
        (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm.toLinearMap
      exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ
        (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
q : Ideal S
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.IsTorsionFree R S
inst✝ : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp
  exact ramificationIdx'_eq_ramificationIdx' p q hpS

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
p : Ideal R
inst✝⁶ : p.IsPrime
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : Module.Finite R S
inst✝¹ : Module.Flat R S
inst✝ : Fintype ↑(p.primesOver S)
⊢ Module.finrank p.ResidueField (p.Fiber S) = Module.finrank R S

Tactic:
finrank_fiber_eq_finrank

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
p : Ideal R
inst✝⁶ : p.IsPrime
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : Module.Finite R S
inst✝¹ : Module.Flat R S
inst✝ : Fintype ↑(p.primesOver S)
⊢ Module.finrank R S = Module.finrank R S
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Countable R
inst✝ : Module.Finite R M
⊢ Countable M

Tactic:
by
  obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)
  rw [← Set.countable_univ_iff]
  have : Countable (Submodule.span R (Set.range s)) := inferInstance
  rwa [h] at this

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

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

Tactic:
sSup_inv

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

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

Tactic:
by
  rw [le_iff_forall_pos_lt_add]
  refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
  · exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))
  · rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
    exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

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

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False

Tactic:
rcases h with ⟨ε, ε0, i, ih⟩
    refine (csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))
    refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
    rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
    exact ih _ ij

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

Goal state before:
pp: case inl
r : ℝ
hr : 0 ≤ r
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
rw [← neg_neg r]
    lift (_ : ℝ) to ℝ≥0 using hr with r
    aesop

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

Goal state before:
pp: case inr
r : ℝ
hr : 0 ≤ -r
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
rw [← neg_neg r]
    lift (_ : ℝ) to ℝ≥0 using hr with r
    aesop

Goal state after:
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ p 1 + q (1 / 1) < r

Tactic:
div_one,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ p 1 + q 1 < r
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:
wlog hab : a ≤ b with H

Goal state after:
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 ∈ ⊥

α✝ : 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.Data.ENNReal.Operations

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

pp: case inr
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
· rw [top_add, lt_top_iff_ne_top]
    exact fun _ => h.resolve_right (Classical.not_not.2 rfl)

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

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

Tactic:
sInf_eq_iInf,

Goal state after:
a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: p : EReal → Prop
⊢ (∃ r, p r) → p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
rintro ⟨r, hr⟩; cases r <;> aesop

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

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b

Tactic:
· simp [← mul_assoc, ENNReal.inv_mul_cancel, *]

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

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ x ≠ ⊤ ∧ x ≠ ⊥

pp: x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩

Tactic:
· simpa [not_or, and_comm] using hx

Goal state after:
x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inl
α✝ : 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
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
hs : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ ∅ ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

pp: case 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
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
· rwa [empty_union]

Goal state after:
case 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
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1

Tactic:
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using! h

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

Goal state before:
pp: n : ℤ
hn : n ≤ 0
x : ℝ≥0∞
hx : 1 ≤ x
⊢ x ^ n ≤ 1

Tactic:
obtain ⟨m, rfl⟩ := neg_surjective n

Goal state after:
x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ x ^ (-m) ≤ 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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

Tactic:
conv_rhs => rw [← finprod_heightOneSpectrum_factorization hI h]

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
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I =
    ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

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

Tactic:
· rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩

Goal state after:
case mpr
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
⊢ ∀ (x : α), edist x x = 0

Tactic:
by simp [edist_dist]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ edist x z ≤ edist x y + edist y z

Tactic:
simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
by
  rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
  exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

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

Goal state before:
pp: ι : Sort u_4
f : ι → ℕ
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
by
  obtain hι | hι := isEmpty_or_nonempty ι
  · simp [iInf_empty]
  apply eq_of_forall_le_iff
  simp [le_ciInf_iff, ← Nat.ceil_le]

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

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
⊢ ⨆ s, f ↑s = ⨆ i, f i

Tactic:
rw [← sSup_range, ← sSup_range]
  obtain (_ | _) := isEmpty_or_nonempty γ
  · simp [Set.range_eq_empty]
  refine ((isLUB_csSup (range_nonempty f) h).unique ?_).symm
  refine (isLUB_congr (hS.upperBounds_image hf)).mp (isLUB_ciSup_set ?_ hS.nonempty)
  exact h.mono (by grind)

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ioc a b) ↔ b ≤ a

Tactic:
by
  refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this
  exact this hab.le

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {x} ⊔ Ideal.span {y} = Ideal.span {x, y_1}

Tactic:
simp_rw [← Ideal.span_union, Set.union_singleton, Set.pair_comm x]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {y, x} = Ideal.span {y_1, x}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
h : x < y
⊢ ∃ u v,
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
h : x < y
u : ℕ → α
hu_anti : StrictAnti u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ u v,
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
⊢ ∀ {a b : αᵒᵈ}, IsCompact (Icc a b)

Tactic:
by
    intro a b
    convert! isCompact_Icc (α := α) (a := b) (b := a) using 1
    exact Icc_toDual (α := α)

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

Goal state before:
pp: α : 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✝ : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
⊢ t ∈ s

Tactic:
have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩

Goal state after:
α : 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✝ : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
this : t ∈ Icc a t
⊢ t ∈ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
· rw [inter_comm s t]
        rw [union_comm s t] at hab
        exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s → BddBelow s ∧ BddAbove s

Tactic:
Metric.isBounded_iff_subset_closedBall x

Goal state after:
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ (∃ r, s ⊆ closedBall x r) → BddBelow s ∧ BddAbove s
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: α : Type u_1
m n : ℤ
⊢ dist m n = ‖↑(-m + n)‖

Tactic:
simp only [dist_eq, norm, cast_add, cast_neg]

Goal state after:
α : Type u_1
m n : ℤ
⊢ |↑m - ↑n| = |-↑m + ↑n|
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
simpa using diam_union xs xt

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:

Tactic:
x ≤ a ^ (n + 1) := hxn
    _ ≤ a ^ (m + 1) := by grw [hnm]; exact h₀.le
    _ = a ^ m * a := pow_succ _ _
    _ < y * a := by gcongr

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

Goal state before:
pp: r₁ r₂ : ℚ
⊢ dist r₁ r₂ = ‖↑(-r₁ + r₂)‖

Tactic:
simp only [dist_eq, norm, cast_add, cast_neg]

Goal state after:
r₁ r₂ : ℚ
⊢ |↑r₁ - ↑r₂| = |-↑r₁ + ↑r₂|
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t

Tactic:
rcases eq_or_ne x ⊥ with (rfl | hx)
  · simp [h1, bot_le.trans_lt h2]
  · lift x to ℝ using ⟨h1.ne_top, hx⟩
    calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup (u ∘ v) f ≤ limsup u g

Tactic:
by
  rw [limsup_comp]
  exact limsup_le_limsup_of_le hv

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i ↦ f (i + k)) atTop = liminf f atTop

Tactic:
by
  rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ a

Tactic:
refine liminf_le_of_le hu_le fun b hb ↦ ?_

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, u i ≤ a
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
b : α
hb : ∀ᶠ (n : ι) in f, b ≤ u n
⊢ b ≤ a