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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x✝¹ : CommRing Q
x✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
let : Rₘ →ₐ[R] Q :=
    { IsLocalization.lift this with commutes' := IsLocalization.lift_eq this }

Goal state after:
R : Type u_4
Rₘ : Type u_6
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x✝¹ : CommRing Q
x✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let __src := IsLocalization.lift this✝;
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case 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)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
⊢ { toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ } ∘ₗ kerToTensor R P' S = LinearMap.id

Tactic:
ext1 x
    rw [H] at hl
    obtain ⟨x, rfl⟩ := e₁.surjective x
    exact DFunLike.congr_arg e₁ (LinearMap.congr_fun hl x)

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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : (RingHom.ker (algebraMap S (ResidueField S))).Cotangent
⊢ (KaehlerDifferential.kerCotangentToTensor R S (ResidueField S)) x = 0

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ (KaehlerDifferential.kerCotangentToTensor R S (ResidueField S))
      ((RingHom.ker (algebraMap S (ResidueField S))).toCotangent ⟨x, hx⟩) =
    0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ a x : S
hx : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑(maximalIdeal R))
a✝ : 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) (a • x) = 0

Tactic:
| smul a x hx _ =>

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

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct (Localization.AtPrime q) (Localization.AtPrime r)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r)) :=
  (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯).trans
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ (Module.length (Localization.AtPrime r)
        (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r))).toNat =
    q.ramificationIdx R * r.ramificationIdx S

Tactic:
ramificationIdx_eq (r.under R),

Goal state after:
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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct (Localization.AtPrime q) (Localization.AtPrime r)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r)) :=
  (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯).trans
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ (Module.length (Localization.AtPrime r)
        (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r))).toNat =
    (Module.length (Localization.AtPrime q)
          (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r))).toNat *
      r.ramificationIdx S
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = ↑0 ↔ r = 0

Tactic:
coe_inj

Goal state after:
r : ℝ≥0
⊢ r = 0 ↔ r = 0
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
coe_inj

Goal state after:
r : ℝ≥0
⊢ r = 1 ↔ r = 1
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩

Goal state after:
case refine_1
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1

Tactic:
norm_num

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      (↑(span {a}))⁻¹

Tactic:
← ha,

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      (∏ᶠ (v : HeightOneSpectrum R),
          ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors))⁻¹
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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q✝ : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
⊢ (⇑p ⊔ ⇑q) 1 = 0

Tactic:
rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : x + y = 0
⊢ 0 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬x + y = 0
⊢ 1 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 0

Tactic:
norm_num

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : x * y = 1
⊢ 0 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬x * y = 1
⊢ 1 ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : y = 1
⊢ 0 ≤ 0

Tactic:
norm_num

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

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬y = 1
⊢ 0 ≤ 1

Tactic:
norm_num

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

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

Goal state before:
pp: case bot
⊢ ⊥.toReal = 0 ↔ ⊥ = 0 ∨ ⊥ = ⊤ ∨ ⊥ = ⊥

Tactic:
norm_num

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (↑a✝).toReal = 0 ↔ ↑a✝ = 0 ∨ ↑a✝ = ⊤ ∨ ↑a✝ = ⊥

Tactic:
norm_num

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

Goal state before:
pp: case top
⊢ ⊤.toReal = 0 ↔ ⊤ = 0 ∨ ⊤ = ⊤ ∨ ⊤ = ⊥

Tactic:
norm_num

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

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

Tactic:
rw [WithTop.image_coe_Ici, WithBot.image_coe_Ico]

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

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

Tactic:
coe_ennreal_lt_coe_ennreal_iff

Goal state after:
x : ℝ≥0∞
⊢ 0 < x ↔ 0 < x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b

Tactic:
apply NNReal.inv_le_of_le_mul

Goal state after:
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

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

Goal state before:
pp: a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹

Tactic:
exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

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

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)

Tactic:
refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx

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

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

Tactic:
by
  lift x to ℝ≥0 using h'x
  lift y to ℝ≥0 using h'y
  have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
  obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) := by
    refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
  refine ⟨n, ?_, ?_⟩
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
    fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩

Goal state after:
a : ℝ≥0∞
ha : IsUnit a
⊢ a ≠ ∞
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y

Tactic:
apply dist_triangle

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ ball x 0 = ∅

Tactic:
ball_eq_empty

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ 0 ≤ 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : (ball x ε).Nonempty
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

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

Goal state before:
pp: x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)

Tactic:
exact Or.inl (le_refl _)

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

Goal state before:
pp: ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨆ i, f i * r

Tactic:
simp only [Real.mul_iSup_of_nonneg ha, mul_comm]

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

Goal state before:
pp: x y : ℝ
⊢ Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)

Tactic:
rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ (∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p ↦ dist p.1 p.2) ⁻¹' ball 0 i ⊆ s

Tactic:
simp [subset_def, Real.dist_0_eq_abs]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal

Tactic:
rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i).asIdeal
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ r', ⋃ (_ : r' < r), ball x r' = ball x r

Tactic:
by
  ext
  rw [← not_iff_not]
  simp [forall_lt_imp_le_iff_le_of_dense]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b✝ : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
⊢ s.Nonempty

Tactic:
obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b✝ : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
y : α
hy : a < y ∧ y < b
⊢ s.Nonempty
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
⊢ i ∈ closure[inst✝³] (f '' S) → i ≤ x

Tactic:
hi

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : i ∈ closure[inst✝³] (f '' S)
⊢ i ≤ x
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
⊢ nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
by simp [nndist_pi_def]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : SeparableSpace α
inst✝ : Nontrivial α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s

Tactic:
simpa using dense_univ.exists_countable_dense_subset_no_bot_top

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

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hki : k = i <;> by_cases hkj : k = j <;> simp_all [nndist_comm]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖

Tactic:
rw [add_comm]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ edist 1 a = ↑‖a‖₊

Tactic:
by
  rw [edist_nndist, nndist_one_left]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
h : J ≤ I
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J

Tactic:
by
  rw [← count_normalizedFactors_eq_multiplicity hJ,
    ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]
  exact Ideal.count_le_of_ideal_ge h hJ _

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)

Tactic:
rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
    ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
  case h => exact prod_inter_normalizedFactors_ne_zero I J
  rw [normalizedFactors_prod_inter_eq_inter]
  exact count_inter ..

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

Goal state before:
pp: z : ℤ
c : ℝ≥0
⊢ ↑z.natAbs ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Tactic:
Int.ofNat_le,

Goal state after:
z : ℤ
c : ℝ≥0
⊢ z.natAbs ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∏ i ∈ s, f i).toNNReal = ↑(∏ i ∈ s, (f i).toNNReal)

Tactic:
coe_inj

Goal state after:
α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, (f i).toNNReal