mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ (∏ x ∈ v', f ↑x) * ∏ x ∈ v', f (Int.negSucc x) = ∏ b ∈ v', f ↑b * f (Int.negSucc b)

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')

Tactic:
prod_mul_distrib

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ (∏ x ∈ v', f ↑x) * ∏ x ∈ v', f (Int.negSucc x) = (∏ x ∈ v', f ↑x) * ∏ x ∈ v', f (Int.negSucc x)

case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ Disjoint (image Nat.cast v') (image Int.negSucc v')
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ (∏ x ∈ u1 ∪ u2, f x * if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Tactic:
prod_mul_distrib

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ((∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, 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 α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
  conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
  exact h.sigma' fun n ↦ (hasSum_fintype _).summable

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

Goal state before:
pp: f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)

Tactic:
← Nat.cofinite_eq_atTop

Goal state after:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ Metric.diam (f '' s) = Metric.diam s

Tactic:
rw [Metric.diam, Metric.diam, hf.ediam_image]

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

Goal state before:
pp: 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₄))
x y : X
l : List X
this✝ : IsTrans X fun x y ↦ d x y = 0
this : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
exact this _ rfl

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by
      refine frequently_atTop.2 fun a => ?_
      have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
      simp only [mem_Iic, eventually_atTop] at this
      obtain ⟨c, hc⟩ := this
      obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
      refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
      by_contra! hab
      simp_all [hc (c + j) (c.le_add_right j) b hab.le]
    obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this
    choose ψ hψ1 hψ2 using hφ.2
    have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id
    refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim
    exact specializes_iff_mem_closure.2 (hψ2 n)

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

Goal state before:
pp: a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)

Tactic:
exact tendsto_id

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

Goal state before:
pp: α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ HasProd f (a * b)

Tactic:
by
  have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) := by
    rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
    convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
    ext s
    simp
  simpa [Tendsto, ← Filter.map_map] using! this

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
⊢ UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'

Tactic:
refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩

Goal state after:
case refine_1
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

case refine_2
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
obtain ⟨u : ℕ → E, u_in : ∀ n, u n ∈ s, lim_u : Tendsto u atTop (𝓝 a)⟩ :=
    mem_closure_iff_seq_limit.mp hg

Goal state after:
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)

Tactic:
rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : ↑δ * C < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a✝ b✝ : E
r : ℝ
a b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
by simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖

Tactic:
by simpa only [mul_one] using norm_mul_le (1 : β) 1

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
a : IterateMulAct f
⊢ (a ^ (n + 1)).val = (a ^ n * a).val

Tactic:
apply Nat.succ_mul

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ b, f b)

Tactic:
rcases exists_surjective_nat ι with ⟨e, he⟩
    rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
    exact m.measurableSet_iUnion _ fun _ => h _

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

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ⟨k • e, hx⟩ ∈ Subtype.val ⁻¹' ball 0 ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}

Tactic:
rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]

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
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖

Tactic:
by
    simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
      NNReal.mul_finset_sup]
    exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _

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

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ c ∈ map (⇑(algebraMap 𝕜 𝕜')) (cobounded 𝕜)

Tactic:
rw [mem_map]

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ ⇑(algebraMap 𝕜 𝕜') ⁻¹' c ∈ cobounded 𝕜
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∉ range f
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
· rcases hyf with ⟨y, rfl⟩
    apply h

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∉ range f
⊢ MeasurableSet (f ⁻¹' {y})
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n < ∞ ↔ n < ⊤

Tactic:
simp [← toENNReal_lt]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x ↦ Nat.find ⋯

Tactic:
by
  refine measurable_to_nat fun x => ?_
  rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
  exact MeasurableSet.disjointed hm _

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t ≤ 0
⊢ μ s = 0

Tactic:
simp only [nonpos_iff_eq_zero] at hs

Goal state after:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
⊢ s ^ z = 1

Tactic:
by
  cases s <;> simp_all [Even.neg_one_zpow]

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

Goal state before:
pp: case zero
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i = 0
⊢ ∑ i ∈ s, f i = 0

Tactic:
exact Finset.sum_eq_zero h

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

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
· simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
    exact Finset.sum_pos h hs

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < 1 / (↑n + 1)

Tactic:
by
  rw [one_div]
  exact inv_pos_of_nat

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

Goal state before:
pp: x : ℝ
⊢ ↑(↑x).abs = ↑|x|

Tactic:
by
  rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]; rfl

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ∑' (x : α), c = ∞

Tactic:
have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) := by
    apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
    simp only [true_or, top_ne_zero, Ne, not_false_iff]

Goal state after:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
⊢ ∑' (x : α), c = ∞
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
← Nat.cofinite_eq_atTop

Goal state after:
f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
⊢ SemicontinuousWithinAt r' s a

Tactic:
by
  intro b hb
  simp_rw [← propext_iff, ← funext_iff] at hfg
  rw [← Filter.EventuallyEq.eq_of_nhdsWithin hfg has] at hb
  filter_upwards [hfg, h b hb] with x hx hxb
  exact hx ▸ hxb

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

Goal state before:
pp: a : EReal
⊢ ↑(sign a) * ↑a.abs⁻¹ = a⁻¹

Tactic:
by
  induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

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

Goal state before:
pp: a b : EReal
a_b : a < b
b_0 : 0 < b
a_0 : 0 < a
⊢ b⁻¹ < a⁻¹

Tactic:
lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩

Goal state after:
b : EReal
b_0 : 0 < b
a : ℝ
a_b : ↑a < b
a_0 : 0 < ↑a
⊢ b⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ StrictMono fun a ↦ a / b

Tactic:
by
  intro a a' a_lt_a'
  apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')
  intro hyp
  apply ne_of_lt a_lt_a'
  rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' h.ne', hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' h.ne']

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

Goal state before:
pp: a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)

Tactic:
exact tendsto_id

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m

Tactic:
by simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0

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

Goal state before:
pp: ⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop

Tactic:
exact tendsto_id

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

Goal state before:
pp: ⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Tactic:
exact tendsto_id

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:
norm_cast at h ⊢

Goal state after:
r : ℝ≥0
h : Tendsto (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2 ^ (-(↑m + 1)) = 1

Tactic:
ENNReal.zpow_neg,

Goal state after:
⊢ ∑' (m : ℕ), (2 ^ (↑m + 1))⁻¹ = 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
apply lt_of_lt_of_le _ lock

Goal state after:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < ↑(2 * max (x + 1) 0 / a) * ↑(a / 2)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuousAt (fun z ↦ f z + g z) x

Tactic:
by
  simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
  exact hf.add' hg hcont

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}

Tactic:
Finset.coe_singleton

Goal state after:
case refine_2.inl.refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ {i} ⊆ {i}
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ μ (s ∪ t) < ∞ ↔ μ s < ∞ ∧ μ t < ∞

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ s < ∞

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (s ∪ t) < ∞
⊢ μ t < ∞
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case mp
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
intro h t _ht
    exact h t

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i

Tactic:
by
  refine le_antisymm ?_ ?_
  · rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
    exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)
  · refine iSup₂_le fun i hi => ?_
    rw [← @generateFrom_measurableSet α (m i)]
    exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Tactic:
simp +singlePass only [iInf_comm]
  exact
    inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
      (fun _ _ _ _ h => measure_mono h) s

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ trim 0 = 0

Tactic:
by
  ext s
  exact nonpos_iff_eq_zero.1 <| (measure_mono (subset_univ s)).trans_eq <| trim_eq _ .univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
rintro _ ⟨s, hs, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f '' f ⁻¹' s)