mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Tactic:
rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
    exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

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

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

Tactic:
← Real.coe_toNNReal x hx

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal)⁻¹.toNNReal = x.toNNReal⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case ha
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0

Tactic:
apply Associates.finprod_ne_zero I

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

Goal state before:
pp: case refine_2.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
z : ℝ
⊢ (z ∈ range fun q ↦ f ↑↑q) → Set.Nonempty.some hf ≤ z

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case refine_2.refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
u : { q' // x < ↑q' }
⊢ Set.Nonempty.some hf ≤ (fun q ↦ f ↑↑q) u
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p + q).toNNReal = p.toNNReal + q.toNNReal

Tactic:
Real.toNNReal_add hp hq

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p.toNNReal + q.toNNReal = p.toNNReal + q.toNNReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal ≤ b.toReal ↔ a ≤ b

Tactic:
by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal < b.toReal ↔ a < b

Tactic:
by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast

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
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
by
        by_cases hx : x = 0
        · rw [if_pos hx, hx, zero_add, zero_add]
        · rw [if_neg hx]
          refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
← coe_natCast,

Goal state after:
m n : ℕ
⊢ ↑↑(m - n) = ↑m - ↑n
Module: Mathlib.Data.ENNReal.Operations

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

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

Tactic:
· rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal
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'
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have ha'_ne_zero : Associates.mk (Ideal.span {a'} : Ideal R) ≠ 0 := by
    rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact 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
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
⊢ count K v (I * I') = count K v I + count K v I'
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ioi ↑x = Ioi x

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (WithBot.some (WithTop.some x))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
by
  rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

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:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε

Tactic:
exact (add_tsub_cancel_of_le (mem_eball.mp h).le).le

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
by
  cases n <;> simp [ENNReal.inv_pow]

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

Goal state before:
pp: case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)

Tactic:
simpa only [div_eq_mul_inv, ← inv_mul_cancel x] using h₂ x y x⁻¹

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
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
      0

Tactic:
by
  have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ
  have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
  have h_subset :
    {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count (Associates.mk J).factors : ℤ) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0} ⊆
    {v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪
      {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}} := by
    intro v hv
    have hv_irred : Irreducible v.asIdeal := v.irreducible
    by_contra h_notMem
    rw [mem_union, mem_ofPred_eq, mem_ofPred_eq] at h_notMem
    push Not at h_notMem
    rw [← Associates.count_ne_zero_iff_dvd ha_ne_zero hv_irred, not_not,
      ← Associates.count_ne_zero_iff_dvd hJ_ne_zero hv_irred, not_not] at h_notMem
    rw [mem_ofPred_eq, h_notMem.1, h_notMem.2, sub_self] at hv
    exact hv (Eq.refl 0)
  exact Finite.subset (Finite.union (Ideal.finite_factors (ideal_factor_ne_zero hI haJ))
    (Ideal.finite_factors (constant_factor_ne_zero hI haJ))) h_subset

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

Goal state before:
pp: case a
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
simpa only [div_eq_mul_inv, ← inv_mul_cancel x] using h₂ x y x⁻¹

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s

Tactic:
rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
a : α
⊢ comap (fun x ↦ dist x a) (𝓝 0) = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, dist_comm]

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 α
⊢ (𝓝[≠] x).NeBot

Tactic:
by
  refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_
  obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs
  obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩
  obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b
  rcases ne_or_eq x y with (xy | rfl)
  · exact ⟨y, us ⟨hab hy, xy.symm⟩⟩
  obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1
  exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ closure[inst✝⁴] (Ioo a b) = Icc a b

Tactic:
closure_Ioo contra.ne

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ Icc a b = Icc a b
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r = ‖r‖

Tactic:
rw [Real.norm_eq_abs r, abs_of_nonneg hr]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅

Tactic:
exact isCompact_empty

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

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s

Tactic:
exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

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

Goal state before:
pp: case refine_3
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 = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯)
        (Submodule.comap (↑I').subtype ↑J').mkQ.ker) =
    ⊥

Tactic:
Submodule.ker_mkQ,

Goal state after:
case refine_3
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 = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap (LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯)
        (Submodule.comap (↑I').subtype ↑J')) =
    ⊥
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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 = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J' ≤
    (Submodule.comap (↑I).subtype ↑J).mkQ.ker

Tactic:
Submodule.ker_mkQ,

Goal state after:
case refine_3
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 = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J' ≤
    Submodule.comap (↑I).subtype ↑J
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
exact this.2

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

Goal state before:
pp: case refine_4
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 = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤
    Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔
      (Submodule.comap (↑I').subtype ↑J').mkQ.ker

Tactic:
Submodule.ker_mkQ,

Goal state after:
case refine_4
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 = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤ Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J'
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ edist a b = ‖a⁻¹ * b‖ₑ

Tactic:
by
  rw [edist_dist, dist_eq_norm_inv_mul, ofReal_norm']

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖

Tactic:
by
  rw [dist_eq_norm_inv_mul', div_eq_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ sphere 1 r} = sphere a r

Tactic:
by
  ext x
  rw [mem_sphere_iff_norm']
  simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : 0 < ↑n
⊢ ↑n * ‖a⁻¹ * b‖ < ↑n * r

Tactic:
nlinarith

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
⊢ (𝓤 E).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | ‖p.1 / p.2‖ < ε}

Tactic:
by
  simpa [norm_inv_mul] using NormedGroup.uniformity_basis_dist (E := E)

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
⊢ f x < f y

Tactic:
have (h : StrictAntiOn f (Icc s t)) : False := by
    have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
    replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
    replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
    exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
this : StrictAntiOn f (Icc s t) → False
⊢ f x < f y
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r

Tactic:
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ f x * r
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case inl
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hb : Bornology.IsBounded ∅
⊢ IsCompact ∅

Tactic:
exact isCompact_empty

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Ico a b = Ico (f a) (f b)

Tactic:
by
  rcases le_or_gt a b with hab | hab
  · exact hf_c.continuousOn.image_Ico_of_strictMonoOn hab (hf.strictMonoOn _)
  · simp [lt_asymm hab, lt_asymm (hf hab)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝³] (⇑e ⁻¹' s)

Tactic:
rintro s ⟨a, rfl | rfl⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Ioi a)

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv

Tactic:
filter_upwards [hu, hv] with _ using sup_le_sup

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

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal

Tactic:
by
  induction x <;> induction y <;> try {· simp_all}
  norm_cast
  simp_rw [real_coe_toENNReal]
  simp_all [ENNReal.ofReal_add]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
⊢ SupConvergenceClass ((i : ι) → α i)

Tactic:
refine ⟨fun f s h => ?_⟩
  simp only [isLUB_pi, ← range_domRestrict] at h
  exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).domRestrict _) (h i)

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

Goal state before:
pp: case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

Tactic:
obtain rfl := htop rfl rfl
      simpa

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ n * f)

Tactic:
exact (LipschitzWith.pow_end h n).mul_end h

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

Goal state before:
pp: a b c : EReal
hc : c < a + b
⊢ ∃ a' < a, c < a' + b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)

Goal state after:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' + b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

Tactic:
apply le_limsup_of_frequently_le _ h₂

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ z, y < z ∧ z < x
⊢ ∃ᶠ (i : α) in f, x ≤ u i