mathlib-initiative/mathlib-tactics huggingface dataset:
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
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : (aeval x) m * (aeval x) q = 0
⊢ ¬q ^ 2 ∣ p

Tactic:
← map_mul,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝³ : FiniteType K A
this✝² : Module.Finite K (Localization.AtPrime Q)
this✝¹ : IsField (Localization.AtPrime Q)
this✝ : Field (Localization.AtPrime Q) := this✝¹.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : (aeval x) (m * q) = 0
⊢ ¬q ^ 2 ∣ p
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
⊢ r' ^ (k + n) * x = 0

Tactic:
rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]

Goal state after:
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
hRS : (RingHom.ker (algebraMap R S)).FG
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')

Tactic:
classical
  obtain ⟨s, hs⟩ := hRS
  have (x : s) : algebraMap R (Localization.AtPrime p) x.1 = 0 := by
    apply H
    simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]
  choose m hm using fun x ↦ (IsLocalization.map_eq_zero_iff p.primeCompl _ _).mp (this x)
  have H : RingHom.ker (algebraMap R S) ≤ RingHom.ker
      (algebraMap R (Localization.Away (∏ i, m i).1)) := by
    rw [← hs, Ideal.span_le]
    intro x hxs
    refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩
    simp only [pow_one]
    rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      mul_zero]
  refine ⟨_, (∏ i : s, m i).2, ?_⟩
  rintro r' ⟨s, e⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  obtain ⟨x, _, rfl⟩ := IsLocalization.exists_mk'_eq (.powers r') x
  simp only [awayMap, IsLocalization.Away.map, IsLocalization.map_mk',
    IsLocalization.mk'_eq_zero_iff] at hx
  obtain ⟨⟨_, n, rfl⟩, hn⟩ := hx
  simp only [← map_pow, ← map_mul] at hn
  obtain ⟨⟨_, k, rfl⟩, hk⟩ := (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mp (H hn)
  refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩
  dsimp only at hk ⊢
  rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
x✝ : (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0
n : ℕ
h✝ : ∀ a ∈ I ^ n, a • x = 0
right✝ : ∀ a ∈ J, a • x = 0
⊢ x = 0

Tactic:
specialize this n

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
x : M
x✝ : (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0
n : ℕ
this : Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
h✝ : ∀ a ∈ I ^ n, a • x = 0
right✝ : ∀ a ∈ J, a • x = 0
⊢ x = 0
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup (s * t⁻¹) = sSup s / sInf t

Tactic:
csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv,

Goal state after:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup s * sSup t⁻¹ = sSup s / sInf t
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

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

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

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

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

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

Goal state before:
pp: Γ₀ : 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⁻¹
hfu : f ↑u < 1
⊢ ∃ d, f ↑d < r

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hr hfu

Goal state after:
Γ₀ : 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⁻¹
hfu : f ↑u < 1
n : ℕ
hn : f ↑u ^ n < r
⊢ ∃ d, f ↑d < r
Module: Mathlib.Data.ENNReal.Basic

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

Tactic:
ENNReal.toNNReal_eq_one_iff

Goal state after:
x : ℝ≥0∞
⊢ x = 1 ↔ x = 1
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ↑n ≤ ↑r ↔ ↑n ≤ r

Tactic:
simp [← coe_le_coe]

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ↑r ≤ ↑n ↔ r ≤ ↑n

Tactic:
simp [← coe_le_coe]

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

Goal state before:
pp: a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + ↑r < a
⊢ ∃ ε, 0 < ε ∧ b < ∞ ∧ b + ↑ε < a

Tactic:
exact ⟨r, hr0, h.trans_le le_top, hr⟩

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ⋃ n, Ioo a ↑n = Ioi a \ {∞}

Tactic:
by
  simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, sdiff_eq]

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

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
h : a = ∞ → ↑b = ∞
h_nnreal : a ≠ ∞ → ↑b ≠ ∞ → a.toNNReal ≤ (↑b).toNNReal
hlt : ↑b < a
⊢ False

Tactic:
lift a to ℝ≥0 using mt h coe_ne_top

Goal state after:
b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ False
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
x : E
⊢ ⨅ x_1, p x_1⁻¹ + q (x⁻¹ / x_1⁻¹) = ⨅ y, p y + q (x / y)

Tactic:
by
          simp_rw [map_inv_eq_map p, ← inv_div', map_inv_eq_map q]

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

Goal state before:
pp: case mp
a b : ℝ≥0∞
h : a * b < ∞
⊢ ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞

Tactic:
intro hb ha

Goal state after:
case mp
a b : ℝ≥0∞
h : a * b < ∞
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ∞ ∧ b < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i

Tactic:
exact Real.iInf_nonneg h

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulActionWithZero 𝕜 G
inst✝ : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha

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
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
coeIdeal_mul,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * (↑J * ↑J')
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ 0 = ⊥

pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, a - f i < b

Tactic:
bot_eq_zero

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ 0 = 0

case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, a - f i < b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
lift x to ℝ using ⟨hx_top, hx_bot⟩

Goal state after:
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
⊢ (↑x).toReal = y.toReal ↔ ↑x = y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]
  rfl

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

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

Tactic:
by
  rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]

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

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c * (b * c)⁻¹ = a * b⁻¹

Tactic:
ENNReal.mul_inv (Or.inr hc') (Or.inr hc),

Goal state after:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c * (b⁻¹ * c⁻¹) = a * b⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : ∞ ≠ 0
⊢ 0 < 1 ∧ 1 * a < ∞

Tactic:
simpa [lt_top_iff_ne_top]

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

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

Tactic:
refine ⟨n, lt_trans ?_ hn⟩

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

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))

Tactic:
refine ⟨n, ?_, ?_⟩

Goal state after:
case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑y ^ n ≤ ↑x

case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Tactic:
refine ⟨n, ?_, ?_⟩

Goal state after:
case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
obtain hx | hx := lt_or_ge 0 x

Goal state after:
case inl
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

case inr
x : ℝ
hx : x ≤ 0
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Tactic:
let x' := Finv (F ⟨x, xs⟩)

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩
  choose s hsc y hys hyx using H ε' (mod_cast ε'0)
  refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩
  exact mod_cast hyx x

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

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

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

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)
ε : ℝ≥0∞
⊢ (fun j ↦ ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε}) = fun x ↦ 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
funext εpos

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∞
εpos : 0 < ε
⊢ ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε} = 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ dist _r _y = ‖-_r + _y‖

Tactic:
rw [Real.dist_eq, ← abs_neg, neg_sub, add_comm, sub_eq_add_neg, norm_eq_abs]

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

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
⊢ (N, N) ≤ b → ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u

Tactic:
hb

Goal state after:
case h
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
hb : (N, N) ≤ b
⊢ ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
⊢ b ∈ s

Tactic:
rcases eq_or_lt_of_le c_le with hc | hc

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s

case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊤ ↔ Nonempty α

Tactic:
by
  simp +contextual [IsCobounded,
    exists_true_iff_nonempty]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ liminf u ⊤ = ⨅ i, u i

Tactic:
rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨅ (_ : True), sSup (u '' Ici i) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
simp only [sSup_image, iInf_const]; rfl

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_1
inst✝ : EMetricSpace β
f : α → β
⊢ LipschitzWith 0 f ↔ ∀ (x y : α), f x = f y

Tactic:
simp [LipschitzWith]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
⊢ (∀ᶠ (n : β) in g, u n ≤ b) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
hb : ∀ᶠ (n : β) in g, u n ≤ b
⊢ sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊥ ≠ 0

Tactic:
simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]

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

Goal state before:
pp: case coe.bot.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊥ ≠ 0

Tactic:
simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ (unconditional β).comap f = unconditional γ

Tactic:
by
  classical
  simp only [unconditional, comap]
  congr 1 with s
  simp only [mem_map, mem_atTop_sets, mem_preimage]
  constructor <;> rintro ⟨t, ht⟩
  · refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
    simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left
  · exact ⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
⊢ L = unconditional β

Tactic:
have := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
rw [← Finset.sup'_eq_sup s_nemp fun i ↦ limsup (F i) f, ← limsup_finset_sup' s_nemp h₁ h₂]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = limsup (fun a ↦ s.sup' s_nemp fun i ↦ F i a) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
⊢ b ∉ {b ∈ t | g b = f b} → g b = 1

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ {b ∈ t | g b = f b}
⊢ g b = 1
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ Filter.map Real.toNNReal atTop = atTop

Tactic:
rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]

Goal state after: