mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
by_cases hf : ∀ i, f i = 0
  · simp [hf]
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  obtain rfl | ha := eq_or_ne a ∞
  · obtain ⟨i, hi⟩ := not_forall.1 hf
    simpa [iSup_eq_zero.not.2 hf, eq_comm (a := ⊤)]
      using le_iSup_of_le (f := fun i => ⊤ * f i) i (top_mul hi).ge
  · exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

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

Goal state before:
pp: case e_toBornology
α : 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
⊢ toBornology✝¹ = toBornology✝

Tactic:
· ext : 2
    rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε - ε / 2

Tactic:
sub_self_div_two

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Tactic:
by
  rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_ofPred_eq,
    compl_compl]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : Tendsto f l (𝓝 0)
⊢ (𝓤 α).HasBasis p fun i ↦ {x | dist x.1 x.2 < f i}

Tactic:
apply Metric.mk_uniformity_basis hf₀
  rw [nhds_basis_closedBall.tendsto_right_iff] at hf
  refine fun ε hε ↦ hf₁.and (hf ε hε) |>.exists.imp fun i ↦ and_imp.mpr fun hp hi ↦ ?_
  exact ⟨hp, by
    simpa [Metric.mem_closedBall, Real.dist_eq, abs_of_nonneg (hf₀ i hp).le] using hi⟩

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 \ {p'}
⊢ a q ∈ J * p

Tactic:
Finset.mem_sdiff,

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'}
⊢ a q ∈ J * p
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 * ⨅ x, (↑x).asIdeal

Tactic:
Ideal.mul_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
⊢ a p' ∈ ⨅ i, J * (↑i).asIdeal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hIJ : I ≤ J
hI : I ≠ 0
⊢ ∃ a, I ⊔ Ideal.span {a} = J

Tactic:
by
  classical
  obtain ⟨I, rfl⟩ := Ideal.dvd_iff_le.mpr hIJ
  simp only [ne_eq, mul_eq_zero, not_or] at hI
  obtain ⟨hJ, hI⟩ := hI
  suffices ∃ a, ∃ K, J * K = Ideal.span {a} ∧ I + K = ⊤ by
    obtain ⟨a, K, e, e'⟩ := this
    exact ⟨a, by rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]⟩
  let s := (I.finite_factors hI).toFinset
  have : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal := by
    intro p hps
    conv_rhs => rw [← mul_one (J * _)]
    rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem hps, ← mul_assoc,
      mul_right_comm _ p.asIdeal]
    refine mul_lt_mul_of_pos_left ?_ ?_
    · rw [Ideal.one_eq_top, lt_top_iff_ne_top]
      exact p.2.ne_top
    · rw [Ideal.zero_eq_bot, bot_lt_iff_ne_bot, ← Ideal.zero_eq_bot,
        mul_ne_zero_iff, Finset.prod_ne_zero_iff]
      exact ⟨hJ, fun x _ ↦ x.3⟩
  choose! a ha ha' using fun p hps ↦ SetLike.exists_of_lt (this p hps)
  obtain ⟨K, hK⟩ : J ∣ Ideal.span {∑ p ∈ s, a p} := by
    rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
    exact sum_mem fun p hp ↦ Ideal.mul_le_left (ha p hp)
  refine ⟨_, _, hK.symm, ?_⟩
  by_contra H
  obtain ⟨p, hp, h⟩ := Ideal.exists_le_maximal _ H
  let p' : HeightOneSpectrum R := ⟨p, hp.isPrime, fun e ↦ hI (by simp_all)⟩
  have hp's : p' ∈ s := by simpa [p', s, Ideal.dvd_iff_le] using le_sup_left.trans h
  have H₁ : J * K ≤ J * p := Ideal.mul_mono_right (le_sup_right.trans h)
  replace H₁ := hK.trans_le H₁ (Ideal.mem_span_singleton_self _)
  have H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p := by
    refine sum_mem fun q hq ↦ ?_
    rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
    refine Ideal.mul_mono_right ?_ (ha q hq.1)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))
  apply ha' _ hp's
  have := IsDedekindDomain.inf_pow_eq_prod_of_prime s (fun i ↦ i.asIdeal) (fun _ ↦ 1)
    (fun i _ ↦ i.prime) (fun i _ j _ e ↦ mt HeightOneSpectrum.ext e)
  simp only [pow_one] at this
  have inst : Nonempty {x // x ∈ s} := ⟨_, hp's⟩
  rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]
  rintro ⟨q, hq⟩
  by_cases hqp : q = p'
  · subst hqp
    convert! sub_mem H₁ H₂
    rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem hp's, add_sub_cancel_right]
  · refine Ideal.mul_mono_right ?_ (ha p' hp's)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := q) (by simpa [hq] using hqp))

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

Tactic:
rw [closure_Ioo hab]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ico a b) ↔ b ≤ a

Tactic:
by
  refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this
  exact this hab.le

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 : β
⊢ ↑(nndist (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) ≤ ↑(nndist f g)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Goal state after:
case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
hs : IsPreconnected ∅
⊢ ∅ ∈
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}

case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ sSup (f x' '' K) < z

Tactic:
hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn

Goal state after:
case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen[inst✝] u
left✝ : IsOpen[inst✝¹] v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ x ∈ K, f x' x < z
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
by
  rw [div_eq_mul_inv, norm_mul_eq_norm_left]
  rwa [norm_inv']

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ ball a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ < ‖a‖ + r

Tactic:
by simp [mem_ball_iff_norm_inv_mul_lt.1 h]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
⊢ False

Tactic:
have : t ∈ A := by
    refine ⟨⟨by order, ht.le.trans (min_le_right _ _)⟩, fun t' ht' ↦ ?_⟩
    rcases le_or_gt t' t₁ with h't' | h't'
    · exact ht₁ ⟨ht'.1, h't'⟩
    · exact H ⟨h't', ht'.2.trans_lt <| ht.trans_le <| min_le_left ..⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
this : t ∈ A
⊢ False
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
⊢ ↑J' ≤ ↑I'

Tactic:
exact h'

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r

Tactic:
by simpa [neg_le]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h✝ : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
h' : ¬a ≤ g / a ^ k
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a
⊢ Dense ↑S

Tactic:
refine S.dense_of_not_isolated_one fun ε ε1 => ?_

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a
ε : G
ε1 : ε > 1
⊢ ∃ g ∈ S, g ∈ Ioo 1 ε
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l v

Tactic:
by
  apply hu.imp
  exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

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

Goal state before:
pp: case mpr.bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
obtain ⟨t, ht⟩ := cobdd
  rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
  · exact ⟨t, .of_forall fun r ↦ tbot r⟩
  refine ⟨t', fun ev ↦ ?_⟩
  specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
  exact not_lt_of_ge ht ht'

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
⊢ z < l

Tactic:
by_contra con

Goal state after:
R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
con : ¬z < l
⊢ False
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I ↦ sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}

Tactic:
filter_upwards [I_mem_F] with i hi

Goal state after:
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I ↦ sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ x ∈ s, a

Tactic:
exact (biSup_const (nonempty_of_mem hs)).symm

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

Goal state before:
pp: case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ x < ⊤ + (t - z)

Tactic:
top_add_of_ne_bot

Goal state after:
case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ x < ⊤

case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ t - z ≠ ⊥
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c, ∃ (_ : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}), b < c

Tactic:
simp_rw [exists_prop]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}, b < c
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: ⊢ (conditional ℕ).filter = Filter.map Finset.range atTop

Tactic:
have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ_iff]

Goal state after:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ (conditional ℕ).filter = Filter.map Finset.range atTop
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
rcases Finset.eq_empty_or_nonempty s with (rfl | s_nemp)

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
h✝ : f.NeBot
h₁ : ∀ i ∈ ∅, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ ∅, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ limsup (fun a ↦ ∅.sup fun i ↦ F i a) f = ∅.sup fun i ↦ limsup (F i) f

case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

Tactic:
exact h'

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g → Multipliable f L

Tactic:
· rintro ⟨hgf, a, ha⟩
    use a
    have := hgf.hasProd
    simp_rw [comp_apply, ← ha] at this
    exact (hg.hasProd_iff f a).mp this

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)

Goal state after:
case inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏ b, a = a ^ Nat.card β
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

Tactic:
refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩

Goal state after:
case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ ↑x.natAbs = x