mathlib-initiative/mathlib-tactics huggingface dataset:
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x = (Algebra.linearMap P.Ring (Localization M')) x

Tactic:
rfl

Goal state after:
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := ⋯
M' : Submonoid P.Ring := ⋯
fQ : Localization M' →ₐ[R] T := ⋯
Q : Extension R T := ⋯
f : P.Hom Q := ⋯
this✝⁹ : FormallySmooth R P.Ring
this✝⁸ : FormallySmooth P.Ring (Localization M')
this✝⁷ : FormallySmooth R Q.Ring
this✝⁶ : Module.Flat S T
this✝⁵ : Algebra P.Ring Q.Ring := ⋯
this✝⁴ : Algebra P.Ring T := ⋯
this✝³ : Algebra (Localization M') T := ⋯
this✝² : IsScalarTower P.Ring S T
this✝¹ : IsScalarTower P.Ring (Localization M') T
this✝ : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
x✝ : ↥P.ker
⊢ ↑(F x✝) =
    ↑((↑(LinearEquiv.restrictScalars P.Ring
              (LinearEquiv.ofEq
                (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                  (Algebra.linearMap P.Ring S).ker)
                (RingHom.ker fQ) this)) ∘ₗ
          Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)
        x✝)

Tactic:
rfl

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

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
hc : ∃ n, ∀ a ∈ I ^ n, a • c = 0
⊢ ∃ n, ∀ a ∈ I ^ n, φ (a • c) = 0

Tactic:
obtain ⟨n, hn⟩ := hc

Goal state after:
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ a ∈ I ^ n, a • c = 0
⊢ ∃ n, ∀ a ∈ I ^ n, φ (a • c) = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case h
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ a ∈ I ^ n, a • c = 0
⊢ ∀ a ∈ I ^ n, φ (a • c) = 0

Tactic:
grind

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

Goal state before:
pp: case mp.refine_2
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
exact ((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).2

Goal state after:
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₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s * t⁻¹) = sInf s / sSup t

Tactic:
csInf_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₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf s * sInf t⁻¹ = sInf s / sSup t
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:
simp_rw [Int.natCast_eq_zero]

Goal state after:
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}
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ 0 = ⊥

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i ↦ s i)) = sSup (Set.range fun i ↦ ↑(s i))

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i ↦ s i)) = sInf (Set.range fun i ↦ ↑(s i))

Tactic:
rfl

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = 0⁻¹

Tactic:
inv_zero,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ x⁻¹.toNNReal = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

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

Goal state before:
pp: ⊢ ⟨1, ⋯⟩ = 1

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
⊢ ⟨|x| * |y|, ⋯⟩ = ⟨|x|, ⋯⟩ * ⟨|y|, ⋯⟩

Tactic:
rfl

Goal state after:
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:
by
  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: α : Type u_1
⊢ 0 = ⊥

Tactic:
rfl

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

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ { toFun := fun x ↦ ⨆ p, ↑p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } x = ⨆ p, ↑p x

Tactic:
rfl

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

Goal state before:
pp: t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : ↑z ∈ Icc ↑x ↑y
⊢ ↑z ∈ ofNNReal '' t

Tactic:
exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

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

Goal state before:
pp: a b : ℝ≥0
⊢ (↑a + ↑b).toReal = (↑a).toReal + (↑b).toReal

Tactic:
rfl

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
p : NonarchAddGroupSeminorm E
⊢ ⇑p.toZeroHom = ⇑p

Tactic:
rfl

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✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0

Tactic:
rfl

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
Q : HeightOneSpectrum A
hQ : Q ∈ f.support \ {P}
⊢ Q ≠ P

Tactic:
grind

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ { toFun := fun x ↦ ⨆ p, ↑p x, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } x = ⨆ p, ↑p x

Tactic:
rfl

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

Goal state before:
pp: r₁ r₂ : ℝ≥0
⊢ (↑r₁ + ↑r₂).toNNReal = (↑r₁).toNNReal + (↑r₂).toNNReal

Tactic:
rfl

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

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
⊢ a - c - (a - b) = b - c

Tactic:
by
  have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  cases c
  · simp
  · norm_cast
    rw [tsub_tsub_tsub_cancel_left]
    exact mod_cast h

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, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
by
  simp_rw [iInf₂_add, add_iInf₂]
  exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

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

Goal state before:
pp: case bot.bot
⊢ ⊥ * ⊥ = ⊥ * ⊥

Tactic:
rfl

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ ⊥ * ↑a✝ = ↑a✝ * ⊥

Tactic:
rfl

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

Goal state before:
pp: case bot.top
⊢ ⊥ * ⊤ = ⊤ * ⊥

Tactic:
rfl

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ ↑a✝ * ⊥ = ⊥ * ↑a✝

Tactic:
rfl

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹

Tactic:
rfl

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ ↑a✝ * ⊤ = ⊤ * ↑a✝

Tactic:
rfl

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

Goal state before:
pp: case top.bot
⊢ ⊤ * ⊥ = ⊥ * ⊤

Tactic:
rfl

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ ⊤ * ↑a✝ = ↑a✝ * ⊤

Tactic:
rfl

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

Goal state before:
pp: case top.top
⊢ ⊤ * ⊤ = ⊤ * ⊤

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ x.swap ∈ {x | d x.1 x.2 < r}

Tactic:
mem_ofPred,

Goal state after:
X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ d x.swap.1 x.swap.2 < r
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(↑x).toReal = ↑x

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' WithTop.some '' Ici x = Ico ↑x ⊤

Tactic:
WithTop.image_coe_Ici,

Goal state after:
x : ℝ
⊢ WithBot.some '' Ico ↑x ⊤ = Ico ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Ico ↑↑x ↑⊤ = Ico ↑x ⊤

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
⊢ Ioo ⊥ ↑↑x = Ioo ⊥ ↑x

Tactic:
rfl

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(↑x).toReal = ↑↑x

Tactic:
rfl

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

Goal state before:
pp: case succ
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
⊢ count K v (I ^ (n + 1)) = ↑(n + 1) * count K v I

Tactic:
classical rw [pow_succ, count_mul']

Goal state after:
case succ
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
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top.top
⊢ ↑(∞ + ∞) = ↑∞ + ↑∞

Tactic:
rfl

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

Goal state before:
pp: case top.coe
x✝ : ℝ≥0
⊢ ↑(∞ + ↑x✝) = ↑∞ + ↑↑x✝

Tactic:
rfl

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

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
⊢ ↑(↑x✝ + ∞) = ↑↑x✝ + ↑∞

Tactic:
rfl

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

Goal state before:
pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ↑(↑x✝¹ + ↑x✝) = ↑↑x✝¹ + ↑↑x✝

Tactic:
rfl

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

Goal state before:
pp: case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑∞ = ⊤

Tactic:
rfl

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

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

Tactic:
rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]

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

Goal state before:
pp: case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
rw [coe_lt_coe] at h

Goal state after:
case coe
a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α✝
α : Type u
edist : α → α → ℝ≥0∞
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝ : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle

Tactic:
rfl

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support,
      ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a

Tactic:
rfl

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

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

Tactic:
by simpa only [mul_comm a] using mul_iInf' hinfty h₀

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

Goal state before:
pp: γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))
  exact h _ hR

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

Goal state before:
pp: α : Type u_3
d : α → α → ℝ≥0
⊢ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]
  refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
  · rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩
    refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)
    exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε
  · lift ε to ℝ≥0 using le_of_lt hε
    refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)
    exact fun _ => ENNReal.coe_lt_coe.1

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 : α
⊢ dist x z ≤ dist x y + dist y z

pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ 0 ≤ dist x y + dist y z

Tactic:
· exact dist_triangle _ _ _

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ 0 ≤ dist x y + dist y z
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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 α✝
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ PseudoMetricSpace.toBornology = PseudoMetricSpace.toBornology

Tactic:
rfl

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

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = toUniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

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 α✝
α : Type u_3
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ PseudoMetricSpace.toUniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range (Nat.cast ∘ f))

Tactic:
rfl

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

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

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

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

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

Tactic:
by
  simpa only [mul_comm] using iInf_mul f a

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

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ |x✝ - x| = r ↔ x✝ = x - r ∨ x✝ = x + r

Tactic:
grind

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

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto ((fun p ↦ dist p.1 p.2) ∘ f) p (𝓝 0) ↔ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0)

Tactic:
Function.comp_def

Goal state after:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0) ↔ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto ((fun x ↦ dist x a) ∘ f) x (𝓝 0) ↔ Tendsto (fun b ↦ dist (f b) a) x (𝓝 0)

Tactic:
Function.comp_def

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto (fun x ↦ dist (f x) a) x (𝓝 0) ↔ Tendsto (fun b ↦ dist (f b) a) x (𝓝 0)
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
t : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
⊢ (pseudoMetrizableSpaceUniformity X).toTopologicalSpace = t

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto ((fun p ↦ dist p.1 p.2) ∘ Prod.map u u) atTop (𝓝 0) ↔ Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
Function.comp_def

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} ⊆ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
simp only [subset_def, Prod.forall]; rfl

Goal state after: