mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case inr.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using!
        exists_lt_of_lt_csSup (h.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ s ∈ atBot

Tactic:
refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)

Goal state after:
case refine_1
α : 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_empty : t = ∅
⊢ s ∈ atBot

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
⊢ s ∈ atBot
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:

Tactic:
edist a b ≤ ediam s := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + (edist x y + ediam t) := le_self_add
      _ = ediam s + edist x y + ediam t := (add_assoc _ _ _).symm

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
⊢ IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp only [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff,
    nontrivial_iff_exists_lt, not_exists, not_and]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
⊢ (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun a ↦ x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a)
    id

Tactic:
simp_rw [← and_assoc]
  apply (nhds_basis_opens x).restrict fun s hs ↦ ?_
  exact ⟨s ∩ Metric.ball x 1,
    by aesop (add safe apply IsOpen.inter),
    by simpa using Metric.isBounded_ball.subset Set.inter_subset_right⟩

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto f l atBot

Tactic:
rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]

Goal state after:
α : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s

Tactic:
compl_subset_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ (closedBall c r)ᶜ ⊆ s ↔ (closedBall c r)ᶜ ⊆ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : 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
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
h : Nontrivial α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
obtain ⟨a, b, hab⟩ := exists_pair_lt α
    exact H hab

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
filter_upwards [hs, Ico_mem_nhdsGE hac]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
⊢ ContinuousAdd ℝ≥0∞

Tactic:
refine ⟨continuous_iff_continuousAt.2 ?_⟩
  rintro ⟨_ | a, b⟩
  · exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl
  rcases b with (_ | b)
  · exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl
  simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff,
    Function.comp_def, tendsto_coe, tendsto_add]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

Tactic:
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
  exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ liminf f v = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Tactic:
simp_rw [liminf_eq, hv.eventually_iff]
  congr 1
  ext x
  simp only [mem_ofPred_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists,
    exists_prop]

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

Goal state before:
pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal (x - y) = (↑x).toENNReal - (↑y).toENNReal

Tactic:
ofReal_sub x (EReal.coe_nonneg.mp hy)

Goal state after:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal x - ENNReal.ofReal y = (↑x).toENNReal - (↑y).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y x : ℝ≥0
h_le : ↑y ≤ ↑x
⊢ ↑(↑x - ↑y) = ↑↑x - ↑↑y

Tactic:
| coe x =>

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

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

Tactic:
nth_rw 1 [← neg_zero]
  rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

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

Goal state before:
pp: a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [sub_eq_add_neg, left_distrib_of_nonneg hb (by simpa)]

Goal state after:
a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ a * b + a * -c = a * b - a * c
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
⊢ Finite ι

Tactic:
have H : ∀ s : Finset ι, #s • b ≤ ∑' _ : ι, b := fun s ↦ by
    simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
⊢ Finite ι
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:
intro b' hb'; simp [hb']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∀ (b' : β), b' ≠ b → Pi.mulSingle b a b' = 1

Tactic:
intro b' hb'; simp [hb']

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F✝ : Type u_5
G : Type u_6
F : Type u_7
inst✝ : NormedGroup F
⊢ ∀ (x y : F), ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Tactic:
by simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
⊢ HasProd g a

Tactic:
by
  classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
by
    rw [uniformContinuous_dom₂]
    exact uniformContinuous_mk.comp uniformContinuous_div

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ UniformContinuousOn (Function.uncurry fun x1 x2 ↦ x1 • x2) s

Tactic:
rw [Metric.uniformContinuousOn_iff_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
⊢ ContinuousInf α

Tactic:
refine ⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_sub_tendsto_zero.2 <| ?_⟩

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
q : α × α
⊢ Filter.Tendsto (fun e ↦ ‖e.1 ⊓ e.2 - (fun p ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist (a / b) c = dist a (c * b)

Tactic:
by
  rw [← dist_mul_right _ _ b, div_mul_cancel]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ CauchySeq (d * fun n ↦ ∏ k ∈ range (n + 1), v k)

Tactic:
suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ ∀ n ≥ N, d n = d N
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ update x i y = updateFinset x {i} (uniqueElim y)

Tactic:
congr with j
  by_cases hj : j = i
  · cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
    exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y
  · simp [hj, updateFinset]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ UniformContinuousOn Inv.inv s

Tactic:
rw [Metric.uniformContinuousOn_iff_le]

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
⊢ ∀ {x y : E}, dist x y = 0 → x = y

Tactic:
by
      let := SeminormedAddCommGroup.ofCore core.toCore
      intro x y h
      rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
      exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
⊢ ∀ {x y : E}, dist x y = 0 → x = y

Tactic:
by
      let := SeminormedAddCommGroup.ofCore core.toCore
      intro x y h
      rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
      exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ∀ {x y : E}, dist x y = 0 → x = y

Tactic:
by
      let := SeminormedAddCommGroup.ofCore core.toCore
      intro x y h
      rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
      exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ ∀ {x y : E}, dist x y = 0 → x = y

Tactic:
by
      let := SeminormedAddCommGroup.ofCore core.toCore
      intro x y h
      rw [← sub_eq_zero, ← core.norm_eq_zero_iff, ← norm_neg_add]
      exact h

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
s t : Set α
m : OuterMeasure α
⊢ ((restrict s) m) t = m (t ∩ s)

Tactic:
by
  simp [restrict, inter_comm t]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
by
  simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]; exact measurable_id

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
i i' : δ
h : i = i'
⊢ Measurable ⋯.mp

Tactic:
by
  cases h
  exact measurable_id

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (map (↑f) s).topologicalClosure = ⊤

Tactic:
by
  rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq,
    Subalgebra.coe_map] at hs ⊢
  exact hf'.dense_image f.continuous hs

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

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (⊤ * ↑x✝).abs = ⊤.abs * (↑x✝).abs

Tactic:
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ (x * y).abs = x.abs * y.abs

Tactic:
induction x, y using induction₂_symm_neg with

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

Goal state before:
pp: x y : EReal
⊢ sign (x * y) = sign x * sign y

Tactic:
induction x, y using induction₂_symm_neg with

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]
  exact tendsto_cofinite_zero_of_tsum_ne_top hf

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

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
right; right; simpa using h

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

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ b * c

Tactic:
mul_comm b c,

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -(↑a✝)⁻¹

Tactic:
← coe_inv _,

Goal state after:
case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -↑a✝⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
x : ℝ
⊢ ⊥ < (↑x)⁻¹

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
x : ℝ
⊢ (↑x)⁻¹ < ⊤

Tactic:
| coe x =>

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
· refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz, hz.trans_le hy]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
by
  refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_
  rcases lt_or_ge d 0 with d0 | d0
  · exact d0.le.trans hc
  obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab
  obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab
  exact dab.le.trans (h a' aa' b' bb')

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
a✝ : α × γ
h₂ : a✝.1 ∈ s → z < f a✝.1
h₃ : a✝.2 < y'
⊢ a✝.1 ∈ s → a✝.2 < f a✝.1

Tactic:
h₄

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
a✝ : α × γ
h₂ : a✝.1 ∈ s → z < f a✝.1
h₃ : a✝.2 < y'
h₄ : a✝.1 ∈ s
⊢ a✝.2 < f a✝.1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)
⊢ Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)

Tactic:
rw [this, ← coe_zero, tendsto_coe]

Goal state after:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
this : (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)
⊢ Tendsto (fun n ↦ C.toReal / ↑n) atTop (𝓝 0)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
A2 : min (g z) (g x) ∈ v
this : (min (f z) (f x), min (g z) (g x)) ∈ u ×ˢ v
⊢ f z + g z > y

Tactic:
calc
        y < min (f z) (f x) + min (g z) (g x) := h this
        _ ≤ f z + g z := add_le_add (min_le_left _ _) (min_le_left _ _)

Goal state after: