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

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
⊢ Function.Bijective ⇑(algebraMap K A)

Tactic:
let f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap.comp (sec K A _)

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
⊢ Function.Bijective ⇑(algebraMap K A)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
· rw [ramificationIdx_of_not_isPrime, ramificationIdx_of_not_isPrime] <;> simpa

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ a ∉ S i

Tactic:
aesop

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

Goal state before:
pp: case h
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₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
a : A
hz : a • z = 0
hy : a • y = 0
ha : a ∈ I ^ max n₁ n₂
⊢ a • (y + z) = 0

Tactic:
aesop

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

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := ⋯
S : Finset (HeightOneSpectrum A) := ⋯
x : A
⊢ x ∈ ⨅ i, i.maxPowDividing (span {a}) → x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a})

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos.e_s
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ t.inf' ⋯ S = {x ∈ s.biUnion S | ∀ i ∈ t, x ∈ S i}

Tactic:
aesop

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

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

Tactic:
exact mod_cast hi _ ij

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 : Ideal R
hI : I ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)

Tactic:
rw [HasFiniteMulSupport, mulSupport]

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 : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) ≠ 1}.Finite
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 : Ideal R
hI : I ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))

Tactic:
rw [HasFiniteMulSupport, mulSupport]

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 : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite
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 : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite

Tactic:
zpow_neg,

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 : Ideal R
hI : I ≠ 0
⊢ {x | (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors))⁻¹ ≠ 1}.Finite
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b c : ℝ≥0
h : a ≠ 0
⊢ b = c ∨ a = 0 ↔ b = c

Tactic:
or_iff_left h

Goal state after:
a b c : ℝ≥0
h : a ≠ 0
⊢ b = c ↔ b = c
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
aesop

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

Goal state before:
pp: case inr
r✝ : ℝ
r : ℝ≥0
⊢ ∃ x, -↑r = ↑x ∨ -↑r = -↑x

Tactic:
aesop

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i, i.maxPowDividing I → x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I

Tactic:
aesop

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
⊢ (sSup s) x = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
rw [coe_sSup_apply hs, ← sSup_range]

Goal state after:
E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ (sSup (range fun i ↦ f i)) x = ⨆ i, (f i) x

Tactic:
coe_sSup_apply h

Goal state after:
E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x
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
⊢ P ∉ f.support → φ ↑(f P) = 0

Tactic:
aesop

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
⊢ (sSup s) x = sSup ((fun x_1 ↦ x_1 x) '' s)

Tactic:
rw [coe_sSup_apply hs, ← sSup_range]

Goal state after:
E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ sSup (range fun p ↦ ↑p x) = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ (sSup (range fun i ↦ f i)) x = ⨆ i, (f i) x

Tactic:
coe_sSup_apply h

Goal state after:
E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ⨆ p, ↑p x = ⨆ i, (f i) x
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:
have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h

Goal state after:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
hb : b ≠ ∞
⊢ a - c - (a - b) = b - c
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b ≤ a

Tactic:
exact mod_cast h

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
by
  rw [add_comm, iInf_add]; simp [add_comm]

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

Goal state before:
pp: case bot
p : EReal → Prop
hr : p ⊥
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
aesop

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

Goal state before:
pp: case coe
p : EReal → Prop
a✝ : ℝ
hr : p ↑a✝
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
aesop

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

Goal state before:
pp: case top
p : EReal → Prop
hr : p ⊤
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
aesop

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

Goal state before:
pp: x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
aesop

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

Goal state before:
pp: x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
aesop

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

Goal state before:
pp: y : EReal
hy0 : 0 < y
right✝ : y < ⊤
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
aesop

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

Goal state before:
pp: y : EReal
left✝ : ⊥ < y
hy0 : y < 0
⊢ y ≠ ⊤ ∧ y ≠ ⊥

Tactic:
aesop

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

Goal state before:
pp: x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
induction a with

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

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' Ioc ↑x ↑y = Ioc ↑x ↑y

Tactic:
WithBot.image_coe_Ioc

Goal state after:
x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' Ioo ↑x ↑y = Ioo ↑x ↑y

Tactic:
WithBot.image_coe_Ioo

Goal state after:
x y : ℝ
⊢ Ioo ↑↑x ↑↑y = Ioo ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' Ioo ↑x ⊤ = Ioo ↑x ⊤

Tactic:
WithBot.image_coe_Ioo

Goal state after:
x : ℝ
⊢ Ioo ↑↑x ↑⊤ = Ioo ↑x ⊤
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0
  · simp_all
  obtain rfl | hb := eq_or_ne b ⊤
  · simp_all
  · simp [mul_assoc, ENNReal.mul_inv_cancel, *]

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ (Associates.mk v.asIdeal).count (Associates.mk w.asIdeal).factors = 0

Tactic:
← pow_one (Associates.mk w.asIdeal),

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ (Associates.mk v.asIdeal).count (Associates.mk w.asIdeal ^ 1).factors = 0
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
exps : HeightOneSpectrum R →₀ ℤ
⊢ ∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v

Tactic:
classical simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
      exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, (↑n)⁻¹ * a < b

Tactic:
by
  rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
  use n, npos
  rw [← ENNReal.div_eq_inv_mul]
  exact div_lt_of_lt_mul' hn

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

Goal state before:
pp: case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ {x}.Subsingleton

Tactic:
exact subsingleton_singleton

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹

Tactic:
← Real.toNNReal_inv

Goal state after:
x : ℝ
hx : 0 < x
⊢ x⁻¹.toNNReal = x⁻¹.toNNReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), dist a b ≤ C

Tactic:
← isBounded_univ,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ Bornology.IsBounded univ ↔ ∃ C, ∀ (a b : α), dist a b ≤ C
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C

Tactic:
← isBounded_univ,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ Bornology.IsBounded univ ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_1
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
⊢ p.asIdeal < 1

Tactic:
rw [Ideal.one_eq_top, lt_top_iff_ne_top]

Goal state after:
case refine_1
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
⊢ p.asIdeal ≠ ⊤
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
⊢ sSup (a • s) = a • sInf s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
  · rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_smul_set hs, zero_smul]
    exact csSup_singleton 0
  by_cases h : BddBelow s
  · exact ((OrderIso.smulRightDual ℝ ha').map_csInf' hs h).symm
  · rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
← Finset.insert_Ico_right_eq_Ico_add_one hle,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ insert n (Finset.Ico m n), dist (f i) (f (i + 1))
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

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

Tactic:
Prod.map_snd

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
← Finset.insert_Ico_right_eq_Ico_add_one hle,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ insert n (Finset.Ico m n), edist (f i) (f (i + 1))
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ interior (Icc a b)

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ Icc a b ∈ 𝓝 x
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ interior (Ico a b)

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ Ico a b ∈ 𝓝 x
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ interior (Ioc a b)

Tactic:
mem_interior_iff_mem_nhds

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ Ioc a b ∈ 𝓝 x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {x} ⊔ Ideal.span {y} = Ideal.span {x, y_1}

Tactic:
← Ideal.span_union,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span ({x} ∪ {y}) = Ideal.span {x, y_1}
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ := exists_lt x

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
huf : ∀ (n : ℕ), u n ∈ range f
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
choose v hv using huf

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : ℕ → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
huf : ∀ (n : ℕ), u n ∈ range f
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
choose v hv using huf

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : ℕ → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case h'
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := ⋯
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := ⋯
⊢ ∀ x_1 ∈ x '' t, x_1 < y (f x_1)

Tactic:
rintro a ⟨c, hc, rfl⟩
    rw [hfx _ hc]
    exact hxy _ hc

Goal state after: