mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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₁
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δ Q P') ⟨Extension.Cotangent.mk x, hx⟩

Tactic:
rw [δ_eq_δAux, δ_eq_δAux]

Goal state after:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • ↑b • (c • 1) ⊗ₜ[S] Cotangent.mk d = 0

Tactic:
← TensorProduct.tmul_smul,

Goal state after:
case tmul.tmul
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • (c • 1) ⊗ₜ[S] (↑b • Cotangent.mk d) = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ C 0 ∈ Q.toExtension.ker ^ 2

Tactic:
RingHom.map_zero

Goal state after:
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₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in✝ : x ∈ P.toExtension.ker
x_in : x ∈ RingHom.ker (aeval P.val)
property✝ : Extension.Cotangent.mk ⟨x, x_in✝⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ 0 ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Unramified.LocalRing

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
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
hx : (awayMap (algebraMap R S) r') (IsLocalization.mk' (Away r') x w✝) = 0
⊢ IsLocalization.mk' (Away r') x w✝ = 0

Tactic:
simp only [awayMap, IsLocalization.Away.map, IsLocalization.map_mk',
    IsLocalization.mk'_eq_zero_iff] at hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
hx : ∃ m, ↑m * (algebraMap R S) x = 0
⊢ IsLocalization.mk' (Away r') x w✝ = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

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
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ s ^ k * (↑(∏ i, m i) ^ k * (r' ^ n * x)) = 0

Tactic:
hk,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑(∏ i, m i) ^ k * (r' ^ n * x) = 0
⊢ s ^ k * 0 = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

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
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H✝ : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
H : (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range
x : S
n : ℕ
y : Away r'
hy : (awayMap (algebraMap R S) r') y = (algebraMap S (Away ((algebraMap R S) r'))) x
⊢ (algebraMap S (Away ((algebraMap R S) r'))) x * (awayMap (algebraMap R S) r') (Away.invSelf r' ^ n) =
    IsLocalization.mk' (Away ((algebraMap R S) r')) x ⟨(algebraMap R S) r' ^ n, ⋯⟩

Tactic:
simp [Away.invSelf, Localization.mk_eq_mk', awayMap, IsLocalization.Away.map,
    IsLocalization.map_mk', ← Algebra.smul_def, IsLocalization.smul_mk', ← IsLocalization.mk'_pow]

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

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ IsCauSeq abs fun n ↦ ↑(f n) / ↑n

Tactic:
intro ε

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
⊢ ε > 0 → ∃ i, ∀ j ≥ i, |(fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) i| < ε
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ
⊢ motive r

Tactic:
obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy
  all_goals simp_all

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

Goal state before:
pp: a b : ℝ≥0∞
h : a < b
⊢ ∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
    rcases exists_between h with ⟨c, pc, cb⟩
    rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
    rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
    exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = I

Tactic:
hk,

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ k
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:

Tactic:
[[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
      _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'

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

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a

Tactic:
biSup_add hs

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

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

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_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
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
if_neg h_neg,

Goal state after:
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
I : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = ↑(n + 1) * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ b = 0 → a = 0

Tactic:
by simp [hb₀]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m < ↑n ↔ m < n

Tactic:
Nat.cast_lt

Goal state after:
m n : ℕ
⊢ m < n ↔ m < n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹

Tactic:
exact ENNReal.sub_mul (by simpa using h)

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv]
  exact ENNReal.sub_mul (by simpa using h)

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
n : ℤ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ n) = n * count K v I

Tactic:
obtain n | n := n
  · rw [ofNat_eq_natCast, zpow_natCast]
    exact count_pow K v n I
  · rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]
    ring

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
  constructor
  · 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.out H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ ball x ε ↔ dist x y < ε

Tactic:
rw [dist_comm, mem_ball]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : Tendsto f l (𝓝 0)
⊢ (𝓤 α).HasBasis p fun i ↦ {x | dist x.1 x.2 < f i}

Tactic:
by
  apply Metric.mk_uniformity_basis hf₀
  rw [nhds_basis_closedBall.tendsto_right_iff] at hf
  refine fun ε hε ↦ hf₁.and (hf ε hε) |>.exists.imp fun i ↦ and_imp.mpr fun hp hi ↦ ?_
  exact ⟨hp, by
    simpa [Metric.mem_closedBall, Real.dist_eq, abs_of_nonneg (hf₀ i hp).le] using hi⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
⊢ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
intro ε

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
⊢ ε > 0 → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ‖r‖ₑ = ENNReal.ofReal |r|

Tactic:
rw [← enorm_eq_ofReal (abs_nonneg _), enorm_abs]

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

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Tactic:
by
  rw [dist_eq_norm_inv_mul, Set.apply_mulIndicator_symmDiff norm_inv']
  simp only [Set.mulIndicator, mul_ite, mul_one]
  split_ifs <;> simp

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

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ ‖(∏ b ∈ s, f b)⁻¹ * ∏ b ∈ s, a b‖ ≤ ∑ b ∈ s, d b

Tactic:
← Finset.prod_inv_distrib,

Goal state after:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ ‖(∏ x ∈ s, (f x)⁻¹) * ∏ b ∈ s, a b‖ ≤ ∑ b ∈ s, d b
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
⊢ Ioi (f a) ⊆ f '' Ioi a

Tactic:
intro y hy
  have := intermediate_value_Ici hf htop (mem_Ici_of_Ioi hy)
  grind

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p ↑n

Tactic:
rw [← Int.comap_cast_atTop (R := R)]; exact h.comap _

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ ∀ (a c : α), 0 ≤ c → (a + k ≤ c ↔ a ≤ c - k)

Tactic:
simp [le_sub_iff_add_le]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)

Tactic:
exact fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst✝] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst✝] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ f '' (U ∩ s) ⊆ tᶜ
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
rw [← Nat.cofinite_eq_atTop] at hf

Goal state after:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ -a < b ↔ -b < a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Tactic:
by
  simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_ofPred_eq]

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

Goal state before:
pp: a b : EReal
⊢ a < -b ↔ b < -a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

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

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

Tactic:
lt_neg_comm,

Goal state after:
a : EReal
⊢ a < -0 ↔ a < 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f

Tactic:
rw [limsup_eq]

Goal state after:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

Tactic:
rw [limsup_eq]

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c, ∃ (_ : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}), b < c

Tactic:
simp_rw [exists_prop]
    exact exists_lt_of_lt_csSup hu h

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

Goal state before:
pp: a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -(a' + b')

Tactic:
rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]

Goal state after:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_zero
⊢ (⊤ * 0).toReal = ⊤.toReal * toReal 0

Tactic:
| top_zero =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

Tactic:
apply le_limsup_of_frequently_le _ h₂
    push +distrib Not at h'
    rcases h' with ⟨z, z_x, hz⟩
    exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ j, ⨆ i, ⨆ (_ : j ∈ decode₂ β i), f j = ⨆ b, f b

Tactic:
simp only [mem_decode₂, iSup_iSup_eq_right]

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

Goal state before:
pp: case top_zero
⊢ 0 < ⊤ * 0 ↔ 0 < ⊤ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 < 0

Tactic:
| top_zero =>

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

Goal state before:
pp: case top_zero
⊢ -⊤ * 0 = -(⊤ * 0)

Tactic:
| top_zero =>

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

Goal state before:
pp: a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
lt_neg_comm,

Goal state after:
a b : EReal
⊢ 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 < a ∧ 0 < -b ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
lt_neg_comm,

Goal state after:
a b : EReal
⊢ 0 < a ∧ b < -0 ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_zero
⊢ ⊤ * 0 = ⊤ ↔ ⊤ = ⊥ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 = ⊥ ∨ ⊤ = ⊤ ∧ 0 < 0 ∨ 0 < ⊤ ∧ 0 = ⊤

Tactic:
| top_zero =>

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

Goal state before:
pp: a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ -0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ 0 < -a ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
lt_neg_comm,

Goal state after:
a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ -0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < -0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
if_neg H'

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i