mathlib-initiative/mathlib-tactics huggingface dataset:
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
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
⊢ False

Tactic:
rcases lt_or_ge m n with hmn | hnm

Goal state after:
case inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hmn : m < n
⊢ False

case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ False
Module: Mathlib.Topology.Instances.Nat

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

Tactic:
← preimage_closedBall,

Goal state after:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ Nat.cast ⁻¹' closedBall (↑x) r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ ∞
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
by grind [Set.Pairwise]

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

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ 0
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
by grind [Set.Pairwise]

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

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rw [(H this).emultiplicity_eq_multiplicity, (H hI).emultiplicity_eq_multiplicity,
    (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]

Goal state after:
case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ ↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) =
    min ↑(multiplicity p.asIdeal I) ↑(multiplicity p.asIdeal J)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup u f = ⊥

Tactic:
by
    rw [limsup_congr h]
    exact limsup_const_bot

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

Tactic:
blimsup_eq_iInf_biSup

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
q : ι → Prop
hl : l.HasBasis q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ s ∈ l, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
Module: Mathlib.Data.EReal.Operations

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

Tactic:
rw [hy_top, top_add_of_ne_bot]
    · exact hx_top.lt_top
    · exact ne_bot_of_le_ne_bot (by simp) (sub_pos.mpr h').le

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case h₁
α : 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) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

pp: case h₂
α : 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) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
· apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_ofPred_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]

Goal state after:
case h₂
α : 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) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr.bot.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊥) = ↑x * ⊥ + ↑x * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.bot.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊥ + ↑a✝) = ↑x * ⊥ + ↑x * ↑a✝

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.bot.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊥ + ⊤) = ↑x * ⊥ + ↑x * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.coe.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊥) = ↑x * ↑a✝ + ↑x * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.coe.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑x * ↑a✝¹ + ↑x * ↑a✝

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.coe.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (↑a✝ + ⊤) = ↑x * ↑a✝ + ↑x * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.top.bot
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊥) = ↑x * ⊤ + ↑x * ⊥

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.top.coe
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝ : ℝ
⊢ ↑x * (⊤ + ↑a✝) = ↑x * ⊤ + ↑x * ↑a✝

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case inr.top.top
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (⊤ + ⊤) = ↑x * ⊤ + ↑x * ⊤

Tactic:
simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ (↑⋯.toFinset ∩ L.support).toFinset, f b

Tactic:
simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp

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

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
    have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
    simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat

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

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

pp: case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
· let : Fintype β := Fintype.ofFinite β
    rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
    simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]

Goal state after:
case inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
⊢ ∏' (x : β), a = a ^ Nat.card β
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
⊢ (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
  rw [hf.tsum_mul_tsum hg hfg, ← HasAntidiagonal.sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]
  exact (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg).tsum_sigma'
    (fun n ↦ (hasSum_fintype _).summable)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ Prod.map f f ⁻¹' {p | edist p.1 p.2 < (↑K)⁻¹ * ε} ⊆ {p | edist p.1 p.2 < ε}

Tactic:
refine fun x hx => (hf x.1 x.2).trans_lt ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < (↑K)⁻¹ * ε}
⊢ ↑K * edist (f x.1) (f x.2) < ε
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
refine
    ⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
  rintro s ⟨hbs, hsc⟩
  refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
  rw [← seqClosure_eq_closure]
  rintro ⟨u, hus, hu⟩
  exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
have ht : ∀ b : ℝ≥0∞, b ≠ 0 →
      Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb => by
    refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
    rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
    have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
    refine this.mono fun c hc => ?_
    exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)

Goal state after:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
⊢ Nonempty ↑s

Tactic:
simp only [hs, nonempty_coe_sort]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : ⟨‖x‖₊, ⋯⟩ < ⟨‖y‖₊, ⋯⟩
z : α
h : ↑⟨‖x‖₊, ⋯⟩ < ‖z‖₊ ∧ ‖z‖₊ < ↑⟨‖y‖₊, ⋯⟩
⊢ ∃ a, ⟨‖x‖₊, ⋯⟩ < a ∧ a < ⟨‖y‖₊, ⋯⟩

Tactic:
exact ⟨⟨‖z‖₊, z, rfl⟩, 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
F : Type u_6
𝕜 : Type u_7
E : Type u_8
G : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : FunLike F E G
inst✝ : LinearMapClass F 𝕜 E G
f : F
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.induced E G f
a : 𝕜
b : E
⊢ ‖a • b‖ ≤ ‖a‖ * ‖b‖

Tactic:
simpa only [← map_smul f a b] using! norm_smul_le a (f b)

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

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
have : ∃ i, x ∈ s i := by exists i

Goal state after:
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
this : ∃ i, x ∈ s i
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (a : SignType), -1 ≤ a

Tactic:
exact LE.of_neg

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
  | top_zero => simp only [mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

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

Goal state before:
pp: case mp
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_

Goal state after:
case mp.refine_1
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone fun s ↦ ∑ b ∈ s, f b

case mp.refine_2
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto Finset.range atTop atTop
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x : ℝ
x_pos : 0 < x
⊢ (⊤ * ↑x)⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]

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

Goal state before:
pp: a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ a⁻¹ < 0

Tactic:
lift a to ℝ using ⟨ne_top_of_lt h, h'⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_lt_zero.2 h

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ a, b ≤ |r| ^ a

Tactic:
exact ⟨n, le_of_lt hn⟩

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

Goal state before:
pp: r : ℝ≥0
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
by simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯) s ≤ (OuterMeasure.ofFunction m m_empty) (f '' s)

Tactic:
ofFunction_apply,

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ (OuterMeasure.ofFunction m m_empty) (f '' s)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ b < ∞, ∃ i, b < ∑ a ∈ Finset.range i, r ^ a

Tactic:
refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a ∈ Finset.range n, r ^ a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }

Tactic:
let f n := ε / 2 / 2 ^ n

Goal state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : s.Nonempty
hm : m = ∅
⊢ (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
by simp [hm, h]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
⊢ (map f) (⨅ i, (comap f) (m i)) = ⨅ i, (map f) ((comap f) (m i))

Tactic:
by
  refine (map_iInf_le _ _).antisymm fun s => ?_
  simp only [map_apply, comap_apply, iInf_apply, le_iInf_iff]
  refine fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (iInf_le_of_le ?_ ?_)
  · rw [← iUnion_union, Set.union_comm, ← inter_subset, ← image_iUnion, ←
      image_preimage_eq_inter_range]
    exact image_mono ht
  · refine ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono ?_
    simpa only [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      image_subset_iff] using subset_rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousWithinAt f univ x

Tactic:
continuousWithinAt_iff_lower_upperSemicontinuousWithinAt

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g

Tactic:
apply generateFrom_le

Goal state after:
case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ generatePiSystem g, MeasurableSet t
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)

Tactic:
apply generateFrom_le

Goal state after:
case a
α : Type u_1
g : Set (Set α)
⊢ ∀ t ∈ g, MeasurableSet t
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
t : Set α
ht : t ∈ {s}
⊢ (fun x ↦ x ∈ s) ⁻¹' {True} = t

Tactic:
by simp [ht.symm]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
by
  refine le_iInf ?_; intro h₂
  have :=
    extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
      (h₂.diff h₁)
  rw [union_sdiff_cancel hs] at this
  rw [← extend_eq m]
  exact le_iff_exists_add.2 ⟨_, this⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s

Tactic:
rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
⊢ μ (f '' f ⁻¹' s) = μ (s ∩ range f)

Tactic:
image_preimage_eq_inter_range

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
⊢ μ (s ∩ range f) = μ (s ∩ range f)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ comap Subtype.val (𝓝[>] a) = atBot

Tactic:
by
  refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual
  simpa only [OrderDual.exists, Ioo_toDual]

Goal state after: