mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I : Ideal B✝
hI : IsNilpotent I
B : Type u_1
inst✝ : CommRing B
⊢ ∀ (I J : Ideal B),
    I ≤ J →
      (∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst : Algebra R (B ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
I

Goal state after:
case h₂
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B✝ : Type u_1
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u_1
inst✝ : CommRing B
I : Ideal B
⊢ ∀ (J : Ideal B),
    I ≤ J →
      (∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst : Algebra R (B ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
⊢ ∀ (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
I

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
⊢ I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
⊢ ∀ (x y : P), 1 ⊗ₜ[P] (D R P) x = 0 → 1 ⊗ₜ[P] (D R P) y = 0 → 1 ⊗ₜ[P] (D R P) (x + y) = 0

Tactic:
· intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_add]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
⊢ Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) (S ⊗[P] Ω[P⁄R])

Tactic:
letI := Submodule.liftQ ((RingHom.ker (algebraMap P S) ^ 2).restrictScalars R)
    (((mk P S _ 1).restrictScalars R).comp (KaehlerDifferential.D R P).toLinearMap)
  refine ⟨this ?_, ?_, ?_⟩
  · rintro x hx
    simp only [Submodule.restrictScalars_mem, pow_two] at hx
    simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Derivation.coeFn_coe, Function.comp_apply, mk_apply]
    refine Submodule.smul_induction_on hx ?_ ?_
    · intro x hx y hy
      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def,
        mul_one, RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]
    · intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_add]
  · change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0; simp
  · intro a b
    obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective _ a
    obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective _ b
    change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P (a * b) =
      Ideal.Quotient.mk _ a • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P b) +
      Ideal.Quotient.mk _ b • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P a)
    simp only [← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul,
      Derivation.leibniz, tmul_add, tmul_smul]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝³ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝² : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝¹ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0

Tactic:
let := (isField_of_isAlgClosed_of_isLocalRing (AlgebraicClosure K)
    (A := Localization.AtPrime M)).toField

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝⁴ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝³ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝² : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝¹ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this✝ : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
this : Field (Localization.AtPrime M) := ⋯.toField
⊢ y = 0
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
⊢ x ∈ (algebraMap K L).range

Tactic:
have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ x ∈ (algebraMap K L).range
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ht S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
· obtain ⟨i, hi⟩ := ht
        simp only [prod_const_one, prod_indicator_apply]
        simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one,
          mul_zero, ite_smul, zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]
        congr
        aesop

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬(Associates.mk v.asIdeal).count (Associates.mk I).factors = 0} ↔ v ∈ {v | v.asIdeal ∣ I}

Tactic:
exact Associates.count_ne_zero_iff_dvd hI v.irreducible

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

Goal state before:
pp: p q : ℝ≥0
h1p : 0 < p
h2p : p ≤ q
⊢ q⁻¹ ≤ p⁻¹

Tactic:
exact inv_anti₀ h1p h2p

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

Goal state before:
pp: s : Set ℝ
⊢ sInf (-s) = -sSup s

Tactic:
by
  rw [← neg_eq_iff_eq_neg, ← Real.sSup_neg, neg_neg]

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

Goal state before:
pp: r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ p.toNNReal ↔ ↑r ≤ p

Tactic:
by
  rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]

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

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - ↑q.den

Tactic:
norm_cast at hq ⊢

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < q
⊢ 1 ≤ q * ↑q.den - ↑q.den
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ ↑q.num - ↑q.den

Tactic:
norm_cast at hq ⊢

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < q.num
⊢ 1 ≤ q.num - ↑q.den
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ (f ↑g)⁻¹ < 1

Tactic:
inv_lt_one_iff hfg0,

Goal state after:
case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ 1 < f ↑g
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ ∀ i ∈ s, p i = 0

Tactic:
have hSupIndep : iSupIndep fun i : HeightOneSpectrum A ↦ torsionBySet A M ↑(i.asIdeal ^ m) := by
    rw [iSupIndep_iff_supIndep]
    exact fun _ ↦ supIndep_torsionBySet_ideal
      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
hSupIndep : iSupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)
⊢ ∀ i ∈ s, p i = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
    exact le_max_left _ _

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

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIoo x y = uIoo ↑x ↑y

Tactic:
simp [uIoo]

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ i, ⨅ j, ⨅ i_1, ⨅ j_1, f i j + g i_1 j_1

Tactic:
exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

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

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
by_cases hy_top : y = ⊤

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

case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else if 0 < n then 0 else ∞

Tactic:
by
  obtain ((_ | n) | n) := n <;> simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: n : ℤ
⊢ ∞ ^ n = if n = 0 then 1 else if 0 < n then ∞ else 0

Tactic:
by
  obtain ((_ | n) | n) := n <;> simp [-Nat.cast_add, -Int.natCast_add]

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

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

Tactic:
simp only [true_and, mem_Ici, mem_eball]

Goal state after:
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
v : HeightOneSpectrum R
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ 0 ≤ count K v ↑J'

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
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0

Tactic:
· exact count_coe_nonneg K v J'

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
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

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

Goal state before:
pp: s : Set ℕ
⊢ ∀ a ∈ upperBounds (Nat.cast '' s), ⌊a⌋₊ ∈ upperBounds s

Tactic:
by simp [upperBounds, Nat.le_floor_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : EMetricSpace α
⊢ Nontrivial α ↔ NontrivialTopology α

Tactic:
simp_rw [nontrivial_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable,
    EMetric.inseparable_iff, edist_eq_zero]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : (x : α) → x ∈ s → Set α
hs : IsCompact s
hc : ∀ (x : α) (hx : x ∈ s), c x hx ∈ 𝓝[s] x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ y, eball x δ ∩ s ⊆ c ↑y ⋯

Tactic:
by
  simpa only [eball, UniformSpace.ball, preimage_ofPred_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin' hs hc

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

Goal state before:
pp: a b x✝ : ℝ≥0
⊢ nndist a b ≤ x✝ ↔ a ≤ x✝ + b ∧ b ≤ x✝ + a

Tactic:
simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, abs_sub_le_iff,
      tsub_le_iff_right, NNReal.coe_add]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1} =
    ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
iInf_comm

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ ⨅ j, ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j} =
    ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ i, ⨅ (_ : 0 < ε), 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
iInf_comm

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ (_ : 0 < ε), ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]
  simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]
  intro h
  refine exists_congr fun b => ?_
  apply (and_iff_right <| h _).symm

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

Goal state before:
pp: X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m

Tactic:
by ext : 2; exact hd

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

Goal state before:
pp: X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m

Tactic:
by ext : 2; exact hd

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

Goal state before:
pp: X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m

Tactic:
by ext : 2; exact hd

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

Goal state before:
pp: X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m

Tactic:
by ext : 2; exact hd

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u

Tactic:
· filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy
    exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, f b < u
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : univ ⊆ s
h_empty : t = ∅
⊢ s ∈ atBot

Tactic:
univ_subset_iff

Goal state after:
case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : s = univ
h_empty : t = ∅
⊢ s ∈ atBot
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
hs : IsCompact ∅
⊢ BddBelow ∅

pp: case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s

Tactic:
· exact bddBelow_empty

Goal state after:
case inr
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : s.Nonempty
⊢ BddBelow s
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
h : ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε

Tactic:
prod_atTop_atTop_eq

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
h : ∀ᶠ (m : β × β) in atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a * b‖ ≤ ‖a‖ + ‖b‖

Tactic:
by
  simpa [dist_eq_norm_inv_mul] using dist_triangle a⁻¹ 1 b

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k := by
    intro k
    rw [eventually_atTop]
    obtain ⟨N, hN⟩ := hu (b k) (hb k)
    exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
hu' : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k
⊢ ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsCobounded s ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Tactic:
by
  rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
  apply exists_congr
  intro r
  rw [compl_subset_comm]

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

Goal state before:
pp: n : ℤ
⊢ ↑↑n.natAbs = ↑↑n.natAbs

Tactic:
by simp only [Int.cast_natCast, NNReal.coe_natCast]

Goal state after: