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

Goal state before:
pp: case zero
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 : FractionalIdeal R⁰ K
⊢ count K v (I ^ 0) = ↑0 * count K v I

Tactic:
| zero =>

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(∞ * ↑x) = ↑↑x * ↑∞

Tactic:
coe_ennreal_top_mul,

Goal state after:
x : ℝ≥0
⊢ ⊤ * ↑↑x = ↑↑x * ↑∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ StrictAnti Inv.inv

Tactic:
intro a

Goal state after:
a : ℝ≥0∞
⊢ ∀ ⦃b : ℝ≥0∞⦄, a < b → b⁻¹ < a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
b : ℝ≥0∞
h₀ : 0 = 0 → b = 0
h₁ : 0 = ∞ → b = 0
⊢ 0 / (0 / b) = b

Tactic:
simp [h₀]

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

Goal state before:
pp: a b : ℝ≥0∞
h₀ : a ≠ 0
h₁ : a ≠ ∞
⊢ a = 0 → b = 0

Tactic:
simp [h₀]

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

Goal state before:
pp: a : ℝ≥0∞
ha : IsUnit a
⊢ a ≠ ∞

Tactic:
obtain ⟨u, rfl⟩ := ha

Goal state after:
u : ℝ≥0∞ˣ
⊢ ↑u ≠ ∞
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
⊢ ∀ (a b : α), b ≤ a

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a : α
⊢ ∀ (b : α), b ≤ a
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inr
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
h✝ : Nonempty γ
⊢ BddAbove (f '' S)

Tactic:
exact h.mono (by grind)

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
r : ℝ≥0
hr : 0 < r
⊢ nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
eq_iff_le_not_lt,

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ nndist f g ≤ r ∧ ¬nndist f g < r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
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 y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp

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
⊢ ∀ (a : ℕ → α),
    StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo ⋯.choose x ∩ s) ∧ Tendsto a atTop (𝓝 x) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Iio x ∩ s) ∧ Tendsto a 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, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
by
  rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩
  have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
  have huf (n : ℕ) : u n ∈ range f := (huxf n).2
  choose v hv using huf
  obtain rfl : f ∘ v = u := funext hv
  exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s

Tactic:
bddBelow_prod,

Goal state after:
α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : Monotone f
⊢ {x | ¬ContinuousAt f x}.Countable

Tactic:
by
  simpa [continuousWithinAt_univ] using (hf.monotoneOn univ).countable_not_continuousWithinAt

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
⊢ ∀ {a b : αᵒᵈ}, IsCompact (Icc a b)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
a : αᵒᵈ
⊢ ∀ {b : αᵒᵈ}, IsCompact (Icc a b)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
this : Nonempty α
a : α
ha : IsLeast t a
b : α
hb : b < a
⊢ s ∈ atBot

Tactic:
exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩

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

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

Tactic:
rw [← dist_one, dist_eq_norm_inv_mul, dist_eq_norm_inv_mul']
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
⊢ ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u

Tactic:
simp [u]

Goal state after:
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:
norm_mul_eq_norm_left

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

case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
by
  simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ ‖(∏ x ∈ s, (f x)⁻¹) * ∏ b ∈ s, a b‖ ≤ ∑ b ∈ s, d b

Tactic:
← Finset.prod_mul_distrib

Goal state after:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ ‖∏ x ∈ s, (f x)⁻¹ * a x‖ ≤ ∑ b ∈ s, d b
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ i ∈ {v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset, i.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

pp: case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ (mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)) ⊆ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset

Tactic:
← Finset.prod_set_coe,

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ i, (↑i).maxPowDividing (map (algebraMap S R) p) = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ (mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)) ⊆ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset
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 δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
⊢ StrictMono f

Tactic:
intro a

Goal state after:
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a : α
⊢ ∀ ⦃b : α⦄, a < b → f a < f b
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
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p ↑n

Tactic:
rw [← Int.comap_cast_atBot (R := R)]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsDiscrete (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
· exact hsd.mono Set.inter_subset_right

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
by
  contrapose! Hle
  apply ENNReal.sum_lt_sum_of_nonempty hs Hle

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le
  obtain ⟨V, hV⟩ := h₄.frequently_le
  refine IsCoboundedUnder.of_frequently_le (a := U * V) ?_
  apply (hV.and_eventually (hU.and (h₁.and h₃))).mono
  intro x ⟨x_V, x_U, u_0, v_0⟩
  exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V (u_0.trans x_U))

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

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
hI : ∀ (i : ι), I i = ⊥
⊢ ∃ i, I i = ⊥

Tactic:
exact ⟨Classical.ofNonempty, hI _⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ ∀ (i : α),
    (∀ᶠ (n : β) in f, u n ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (n : β) in g, u n ≤ i_1) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ i ⊔ i_1

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
⊢ (∀ᶠ (n : β) in f, u n ≤ a) → ∀ (i : α), (∀ᶠ (n : β) in g, u n ≤ i) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
hy : 0 ≤ ⊤
⊢ (↑a✝ - ⊤).toENNReal = (↑a✝).toENNReal - ⊤.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case top.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ - ↑a✝).toENNReal = ⊤.toENNReal - (↑a✝).toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
have A : s ∩ Metric.eball x δ ∈ 𝓝[s] x :=
    inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ δpos)

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: ⊢ ∀ {a b : EReal}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
intro a

Goal state after:
a : EReal
⊢ ∀ {b : EReal}, a * b = 0 → a = 0 ∨ b = 0
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}

Tactic:
intro a

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
i : α
⊢ ∀ᶠ (s : Finset α) in atTop, i ∈ s

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.simpa
   "simpa"
   []
   []
   (Tactic.simpaArgsRest
    (Tactic.optConfig [])
    []
    []
    []
    ["using"
     (Term.app
      `eventually_finset_atTop_subset
      [(choice
        («term{_}» "{" [`i] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields [(Term.structInstField (Term.structInstLVal `i []) [])])
         (Term.optEllipsis [])
         []
         "}"))])]))])

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

Goal state before:
pp: case zero
x : EReal
⊢ 0 • x = ↑0 * x

Tactic:
| zero =>

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
x : α
hy : (∃ a ∈ t, g a = g x) ∨ g x ∈ s
hyt : ¬∃ a ∈ t, g a = g x
⊢ ∃ a ∈ t, g a = g x

Tactic:
exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: 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' s_nemp fun i ↦ limsup (F i) f

Tactic:
← limsup_finset_sup' s_nemp h₁ h₂

Goal state after:
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 = limsup (fun a ↦ s.sup' s_nemp fun i ↦ F i a) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : Multipliable f L
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
exact h.map_tprod g hge.continuous

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : HasProd f a L
⊢ HasProd (fun x ↦ f x ^ 0) (a ^ 0) L

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1 L
⊢ f = 1

Tactic:
ext i
    exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e

Tactic:
· obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he
    obtain ⟨s, hs⟩ := vanish o ho
    refine ⟨s, fun t hts ↦ oe ?_⟩
    by_cases ht : Multipliable fun a : t ↦ f a
    · classical
      refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
      rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
      apply hs
      simp_rw [Finset.mem_map]
      rintro _ ⟨b, -, rfl⟩
      exact hts b.prop
    · exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case neg
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
⊢ Tendsto (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [Finset.multipliable_compl_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
⊢ b' ≠ b → (if b' = b then a b' else 1) = 1

Tactic:
hb'

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a b' else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
⊢ b' ≠ b → (if b = b' then a b' else 1) = 1

Tactic:
hb'

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b = b' then a b' else 1) = 1