mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors ∣
    ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
h_not_dvd :
  ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
← Associates.mk_dvd_mk

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ∣
    Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1)) ∣
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False

Tactic:
by simp [hr] at h

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors

Tactic:
rw [← hJv]

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ (Associates.mk J).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk J).count (Associates.mk I).factors
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ (Associates.mk J).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk J).count (Associates.mk I).factors

Tactic:
apply Ideal.finprod_count
    ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI

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

Goal state before:
pp: b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < ↑k
this : 0 < ↑k
⊢ (↑k)⁻¹ < b

Tactic:
inv_lt_comm₀ this hb

Goal state after:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < ↑k
this : 0 < ↑k
⊢ b⁻¹ < ↑k
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:
coe_sSup_apply hs,

Goal state after:
E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ ⨆ p, ↑p x = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
⊢ ∃ n, ↑r < ↑n

Tactic:
rcases exists_nat_gt r with ⟨n, hn⟩

Goal state after:
r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
refine ciSup_le fun p ↦ (map_add_le_max p.1 x y).trans ?_

Goal state after:
case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ max (↑p x) (↑p y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)
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:
coe_sSup_apply hs,

Goal state after:
E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ ⨆ p, ↑p x = sSup ((fun x_1 ↦ x_1 x) '' s)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

Tactic:
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs

Goal state after:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ∞
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs

Goal state after:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
have : Nonempty {i // p i} := nonempty_subtype.2 h

Goal state after:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 → x ∈ Iio 0

pp: case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0

Tactic:
· rintro ⟨y, ⟨_, hy0⟩, rfl⟩
    lift y to ℝ using by aesop
    simpa using hy0

Goal state after:
case mpr
x : ℝ
⊢ x ∈ Iio 0 → x ∈ toReal '' Ioo ⊥ 0
Module: Mathlib.Data.EReal.Basic

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

Tactic:
WithTop.image_coe_Ico,

Goal state after:
x y : ℝ
⊢ WithBot.some '' Ico ↑x ↑y = Ico ↑x ↑y
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)
⊢ count K v ↑w.asIdeal = 0

Tactic:
count_well_defined K v hw_ne_zero hw_fact,

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).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {1})).factors) =
    0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = c / a

Tactic:
rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']

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

Goal state before:
pp: case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
hv : v ∈ mulSupport fun v ↦ ↑v.asIdeal ^ exps v
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False

Tactic:
rw [mem_mulSupport, h, zpow_zero] at hv

Goal state after:
case e'_2.h
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 → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
hv : 1 ≠ 1
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
rw [dist_comm z]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
by rw [Real.coe_toNNReal _ (hf x hxs)]

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

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
by rw [Real.coe_toNNReal _ (hf x hxs)]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Tactic:
by
  refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
  rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
  exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

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

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

Tactic:
← not_iff_not

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

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

Tactic:
← not_iff_not

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∉ ball x r
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

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

Tactic:
simp [forall_lt_iff_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)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Set.univ.pi fun b ↦ closedBall (x b) r

Tactic:
ext p
  simp [dist_pi_le_iff hr]

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

Goal state before:
pp: case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
← eventually_countable_forall

Goal state after:
case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ y ∈ s

Tactic:
have : IsClosed (s ∩ Icc a y) := by
    suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc
    grind [inter_assoc, inter_eq_self_of_subset_right, Icc_subset_Icc_right]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst✝²] (s ∩ Icc a y)
⊢ y ∈ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖

Tactic:
by simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

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

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ

Tactic:
by
  rw [← enorm_inv', inv_div]

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

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ENormedMonoid E
a : E
⊢ ‖a‖ₑ = 0 ↔ a = 1

Tactic:
simp [ENormedMonoid.enorm_eq_zero]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ range f → ∀ ⦃y : α⦄, y ∈ range f → dist x y ≤ C) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C

Tactic:
by simp only [forall_mem_range]

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
this : StrictAntiOn f (Icc s t) → False
hf_mono_st : StrictMonoOn f (Icc s t)
⊢ f x < f y

Tactic:
have hsx : s ≤ x := min_le_right a x

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
this : StrictAntiOn f (Icc s t) → False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
⊢ f x < f y
Module: Mathlib.Topology.MetricSpace.Bounded

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

Tactic:
by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
  · exact isCompact_empty
  · rcases hb.subset_closedBall x with ⟨r, hr⟩
    exact (isCompact_closedBall x r).of_isClosed_subset hc hr

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
⊢ False

Tactic:
have h : a ≤ g / (a ^ k) := by
      refine a_min ⟨?_, ?_⟩
      · exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
      · exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)

Goal state after:
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
⊢ False
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
by
  rcases le_or_gt 0 r with (hr | hr)
  · rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
    positivity
  · rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith

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

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Tactic:
induction s using Finset.cons_induction with

Goal state after:
case cons
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ Finset.cons i s hi, f i)⁻¹ = ∏ i ∈ Finset.cons i s hi, (f i)⁻¹
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: case mp
h : ⊤ + ⊥ = ⊤
⊢ False

Tactic:
add_bot

Goal state after:
case mp
h : ⊥ = ⊤
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)

Tactic:
refine isBoundedUnder_of_eventually_le (a := U * V) ?_

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h_empty
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
iInf_of_empty

Goal state after:
case h_empty
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⊤
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : BoundedLENhdsClass α
inst✝ : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a✝ : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun x1 x2 ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x.1 ×ˢ 𝓝 x.2)

Tactic:
exact ⟨(a, b), ha.prod_mk hb⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)

Tactic:
apply le_trans (edist_triangle _ (f a₂ b₁) _)

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ limsup s cofinite = {x | {n | x ∈ s n}.Infinite}

Tactic:
by
  simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

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

Goal state before:
pp: α : Type u_3
t : Finset (Finset α)
x✝¹ : Finset α
hu : t.sup id ⊆ x✝¹
x✝ : Finset α
hv : x✝ ∈ t
⊢ x✝ ∈ x✝¹.powerset

Tactic:
exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
⊢ (L.map f).support = ⇑f '' L.support

Tactic:
ext c
  rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc
  · simp [support]
  · exact ⟨fun hc' ↦ have := hc'.exists; by grind, by grind⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∉ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
· have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∉ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: n x : ℕ
⊢ x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)

Tactic:
simp [Nat.lt_succ_iff]

Goal state after: