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

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)
  · rw [iInf_eq_bot.2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]
    simp [Real.iInf_nonpos' ⟨i, hi⟩]
  replace h i : 0 ≤ f i := le_of_not_ge fun hi ↦ h ⟨i, hi⟩
  refine eq_of_forall_le_iff fun a ↦ ?_
  obtain rfl | ha := eq_or_ne a ∞
  · simp
  rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]
  · exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm
  · exact Real.iInf_nonneg h

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

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

Tactic:
simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]

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

Goal state before:
pp: case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
· exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx

Goal state after:
case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal
Module: Mathlib.Data.EReal.Basic

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

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ici (WithBot.some (WithTop.some x))) = _

Goal state after:
x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ici ↑↑x = Ici x
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
ENNReal.inv_mul_le_iff h1 h2,

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

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

Tactic:
ENNReal.mul_inv htop hzero,

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ b⁻¹⁻¹ * a⁻¹ = a⁻¹ * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
a c : ℝ≥0∞
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ∞ ∨ c ≠ ∞
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

Tactic:
simp [div_zero hc]

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

Goal state before:
pp: a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
cases b with
  | top =>
    lift c to ℝ≥0 using ht.neg_resolve_left rfl
    rw [div_top, nonpos_iff_eq_zero]
    rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
  | coe b => ?_
  rcases eq_or_ne b 0 with (rfl | hb)
  · have hc : c ≠ 0 := h0.neg_resolve_left rfl
    simp [div_zero hc]
  · rw [← coe_ne_zero] at hb
    rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v 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, hv⟩ ∉ {⟨Associates.mk w.asIdeal, hw'⟩}

Tactic:
Multiset.mem_singleton

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, hv⟩ = ⟨Associates.mk w.asIdeal, hw'⟩
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε

Tactic:
by
  rw [mem_closedEBall, edist_self]; apply zero_le

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

Goal state before:
pp: case negSucc.ofNat.refine_1
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)

Tactic:
exact one_le_pow_of_one_le' hx _

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

Goal state before:
pp: case negSucc.ofNat.refine_2
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b

Tactic:
exact one_le_pow_of_one_le' hx _

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

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

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

Tactic:
· exact ((OrderIso.smulRightDual ℝ ha').map_csInf' hs h).symm

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
⊢ sSup (a • s) = a • sInf s
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
hq : p' ∈ s
⊢ a p' = a p' + ∑ x ∈ s \ {p'}, a x - ∑ q ∈ s \ {p'}, a q

Tactic:
add_sub_cancel_right

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
hq : p' ∈ s
⊢ a p' = a p'
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' ball a r = ball (↑a) r ∩ {a | p a}

Tactic:
rw [← preimage_ball, image_preimage_eq_inter_range, range_val_subtype]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ max (dist x' x.1) (dist y' x.2) = r ↔ dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r

Tactic:
max_eq_iff

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
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
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr
  exact nndist_pi_le_iff

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

Goal state before:
pp: case refine_3
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (Pi.single i a) (Pi.single j b)

Tactic:
· simpa [h, nndist_comm] using nndist_le_pi_nndist (Pi.single i a : β → Y) (Pi.single j b) j

Goal state after:
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
  apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp
  simp_all

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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (c.divMod b a) * b = c

Tactic:
divMod,

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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (if h : a ≤ c ∧ a ≠ 0 ∧ b ≠ 0 then ⋯.choose else 0) * b = c
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r

Tactic:
by
  rw [mem_closedBall, dist_eq_norm_inv_mul]

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

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

Tactic:
by simpa [neg_le] using hn

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
refine ⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩

Goal state after:
α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s → BddBelow s ∧ BddAbove s
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
refine hf.exists_forall_le' (x₀ := x₀) ?_
  have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β := by
    refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
    simp only [Set.compl_ofPred, not_lt]
    exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h
  filter_upwards [hU] with x hx using hx.le

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

Goal state before:
pp: case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
rw [Finset.forall_mem_cons] at hk

Goal state after:
case cons
ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
R : Type u_6
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f u
hv : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ ∃ᶠ (x : α) in f, U + V ≤ (u + v) x

Tactic:
exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ediam (f '' s) ≤ ↑K * ediam s

Tactic:
apply Metric.ediam_le
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
  exact hf.edist_le_mul_of_le (Metric.edist_le_ediam_of_mem hx hy)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
⊢ LipschitzWith 1 fun a ↦ (a, b)

Tactic:
by
  simpa only [max_eq_left zero_le_one] using! LipschitzWith.id.prodMk (LipschitzWith.const b)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x

Tactic:
exact (hK.continuousOn).continuousAt ht

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x

Tactic:
contrapose! h
  apply limsSup_le_of_le hu
  simpa using h

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

Goal state before:
pp: x y : EReal
⊢ (∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩

Goal state after:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ ∀ (z : WithTop ℝ), ↑z < y → ↑z ≤ x
Module: Mathlib.Data.EReal.Operations

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

Tactic:
simp_rw [add_comm a] at hc ⊢

Goal state after:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_neg
x✝ : ℝ
hx : x✝ < 0
⊢ 0 < ⊤ * ↑x✝ ↔ 0 < ⊤ ∧ 0 < ↑x✝ ∨ ⊤ < 0 ∧ ↑x✝ < 0

Tactic:
| top_neg _ hx =>

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

Goal state before:
pp: case neg
β : Type u_2
L : SummationFilter β
h : ¬L.filter = ⊥
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
exact .inl ⟨⟨h⟩⟩

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
⊢ (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
rw [or_iff_not_imp_left]
  intro hb
  filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb

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

Goal state before:
pp: case inr
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ (L.map f).support ↔ c ∈ ⇑f '' L.support

Tactic:
exact ⟨fun hc' ↦ have := hc'.exists; by grind, by grind⟩

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

Goal state before:
pp: case top_neg
x✝ : ℝ
hx : x✝ < 0
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

Tactic:
| top_neg _ hx =>

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

Goal state before:
pp: a b : EReal
⊢ a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff,
    neg_lt_comm, lt_neg_comm, neg_zero]
  tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (sᶜ.mulIndicator f) a₂

Tactic:
Set.mulIndicator_compl

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f * (s.mulIndicator f)⁻¹) a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
· by_cases hL : L.NeBot
    · exact hg.hasProd.one_le h
    · simpa [tprod_bot hL] using one_le_finprod' h

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g L
⊢ 1 ≤ ∏'[L] (i : ι), g i
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
⊢ (CauchySeq fun s ↦ ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

case refine_2
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s, f x

Tactic:
← prod_attach

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s.attach, f ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (z : A × A), f z.1 * g z.2 = ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
← HasAntidiagonal.sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (c : (n : A) × ↥(antidiagonal n)),
      f (HasAntidiagonal.sigmaAntidiagonalEquivProd c).1 * g (HasAntidiagonal.sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)

pp: case inr
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)

Tactic:
· simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
    exact nhds_bot_basis_Iic

Goal state after:
case inr
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, hn n le_rfl⟩

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ⊢ ContinuousOn (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)}

Tactic:
rw [ContinuousOn]

Goal state after:
⊢ ∀ x ∈ {p | p ≠ (∞, ∞)}, ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
⊢ ∃ R, ∃ᶠ (n : ι) in l, x n < R

Tactic:
by_contra! h
  refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
  simp only [eventually_map, ENNReal.coe_le_coe]
  filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun i ↦ |x i|
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
rw [isBoundedUnder_le_abs, not_and_or] at hbdd
  obtain hbdd | hbdd := hbdd
  · obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
    obtain ⟨q, hq⟩ := exists_rat_gt R
    refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
    · refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
    · simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q + 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx
  · obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf
    obtain ⟨q, hq⟩ := exists_rat_lt R
    refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
    · simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q - 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx
    · refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
x : ↑(Ici a)
⊢ projIci a ↑x = x

Tactic:
by cases x; apply projIci_of_mem

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case h
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
n : ℕ
ihn : ∀ m < n, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
x y : X
l : List X
hn : l.length = n
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
| h n ihn =>

Goal state after: