mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b

Tactic:
have := (IsLocalization.mk'_surjective p.primeCompl).exists.mp (H.2 (algebraMap _ _ x))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
this :
  ∃ x_1,
    (localRingHom p q (algebraMap R S) ⋯)
        (match x_1 with
        | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m) =
      (algebraMap S (Localization.AtPrime q)) x
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b
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
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange T (map R R S T))

Tactic:
rw [← tensorH1CotangentOfIsLocalization_toLinearMap R T M]

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
M : Submonoid S
inst✝ : IsLocalization M T
⊢ Function.Bijective ⇑↑(tensorH1CotangentOfIsLocalization R T M)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |(fun i ↦ ↑(f i)) j - (fun i ↦ ↑(f i)) i| < ε

Tactic:
dsimp; exact lt_trans (mod_cast hi _ ij) δε

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

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

Tactic:
have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x - y) ≤ max (f x) (f y)

Tactic:
by
  rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
  exact map_add_le_max _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ x, ⨅ (_ : x ≠ ∞), f x = ⨅ x, f ↑x

Tactic:
rw [iInf_subtype', cinfi_ne_top]

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
simp only [count, dif_neg hI]

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑J * ↑(Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
lift f to ι → ℝ≥0 using hf
    simp_rw [← coe_iInf, toNNReal_coe]

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

Goal state before:
pp: a c : ℝ≥0∞
hac : a < c
d : ℝ≥0∞
had : a < d
hdc : d < c
⊢ ⨅ b, ⨅ (_ : a < b), b < c

Tactic:
exact (iInf₂_le_of_le d had le_rfl).trans_lt hdc

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)⁻¹ * (spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * (↑J' * ↑J)) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
← mul_assoc,

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)⁻¹ * spanSingleton R⁰ ((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
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]

Goal state after:
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: case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

Tactic:
rintro rfl
    exact bot_lt_coe

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

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ ↑x

Tactic:
WithTop.image_coe_Iic,

Goal state after:
x : ℝ
⊢ WithBot.some '' Iic ↑x = Ioc ⊥ ↑x
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
← mul_assoc,

Goal state after:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ x * x⁻¹ * y ≤ x * z ↔ y ≤ x * z
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

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

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

Tactic:
rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]
    ring

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

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ a * (b * b⁻¹) = b⁻¹

pp: a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞

Tactic:
← mul_assoc,

Goal state after:
a b : ℝ≥0∞
h : a * b = 1
⊢ a * b * b⁻¹ = b⁻¹

a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ r * (r⁻¹ * b)

Tactic:
← mul_assoc,

Goal state after:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ r * a ≤ r * r⁻¹ * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 2⁻¹ + 2⁻¹ = 1

Tactic:
by
  rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]

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

Goal state before:
pp: case e_edist
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
⊢ edist✝¹ = edist✝

Tactic:
ext x y : 2

Goal state after:
case e_edist
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
x y : α
⊢ edist✝¹ x y = edist✝ x y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
dist_comm y

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

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

Tactic:
refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)

Goal state after:
case refine_1
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.1 p.2) < ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε'}
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * (p.asIdeal * ∏ x ∈ s \ {p}, x.asIdeal) < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1

Tactic:
← mul_assoc,

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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * p.asIdeal * ∏ x ∈ s \ {p}, x.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r y : ℝ
⊢ |x - y| < r ↔ y ∈ Ioo (x - r) (x + r)

Tactic:
abs_sub_lt_iff,

Goal state after:
x r y : ℝ
⊢ x - y < r ∧ y - x < r ↔ y ∈ Ioo (x - r) (x + r)
Module: Mathlib.Data.Real.Pointwise

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

Tactic:
by
  simp only [Real.mul_iInf_of_nonpos ha, mul_comm]

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

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h

Tactic:
by
  rw [iInf_mul]
  exact le_ciInf H

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
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ a q ∈ J * p

Tactic:
refine Ideal.mul_mono_right ?_ (ha q hq.1)

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
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ ∏ q ∈ s \ {q}, q.asIdeal ≤ p
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable (f '' s)

Tactic:
by
  rw [image_eq_range, ← image_univ]
  exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.domRestrict

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Ici a) = {a}

Tactic:
simp [frontier, ha]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Iic a) = {a}

Tactic:
simp [frontier, ha]

Goal state after:
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
b : β
⊢ edist (f b) (g b) ≤ ↑(nndist f g)

Tactic:
← edist_nndist

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toUniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
by
  simp +instances [replaceDist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toBornology = PseudoMetricSpace.toBornology

Tactic:
by
  simp +instances [replaceDist_eq]

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a *
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
          FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den)) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))

Tactic:
← mul_assoc,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ↑a.num * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))

Tactic:
← mul_assoc,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ↑a.num * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den)
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * I' = spanSingleton R⁰ (I'.divMod I J') * (J * I')
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
← mul_assoc,

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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * I' = spanSingleton R⁰ (I'.divMod I J') * J * I'
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
refine (norm_mul_le' _ _).trans_eq' ?_

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

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

Tactic:
refine (norm_mul_le' _ _).trans_eq' ?_

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹ * v * v⁻¹‖ = ‖u⁻¹‖