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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
⊢ HasProd f a

Tactic:
by
  classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop]
  intro u hu s
  rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
  obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 := by
    have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
    exact (A.and (Ici_mem_atTop _)).exists
  have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
      (𝓝 <| ∏ b ∈ t0, 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))
  have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
    ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
  obtain ⟨t, tv, st⟩ := this
  refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
  simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.2 ×ˢ ↑p.1 = map Prod.swap (↑p.1 ×ˢ ↑p.2)
⊢ ((𝓤 α).lift fun s ↦ 𝓟 {p | Prod.swap ⁻¹' Prod.swap ⁻¹' s ∈ ↑p.1 ×ˢ ↑p.2}) ≤ (𝓤 α).lift' gen

Tactic:
exact le_rfl

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

Goal state before:
pp: R : Type u_3
β : Type u_4
inst✝³ : DivisionRing R
inst✝² : UniformSpace R
inst✝¹ : UniformContinuousConstSMul Rᵐᵒᵖ R
inst✝ : UniformSpace β
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous fun x ↦ f x / a

Tactic:
simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹

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

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
n : β
hn : N ≤ n
k : β
hk : k ∈ Ici n
l : β
hl : l ∈ Ici n
⊢ edist (s k) (s l) ≤ ε

Tactic:
exact (hN _ (hn.trans hk) _ (hn.trans hl)).le

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ Completion.map (SMul.smul m ∘ SMul.smul n) x = Completion.map (SMul.smul n ∘ SMul.smul m) x

Tactic:
exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))

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

Goal state before:
pp: case inr.refine_1
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

Tactic:
exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x ↦ min a (f x)

Tactic:
by
  simpa only [min_comm] using hf.min_const a

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ↑(liminf u f) = liminf (fun i ↦ ↑(u i)) f

Tactic:
by
  refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
  rw [coe_le_coe, le_liminf_iff, le_liminf_iff]
  simp [forall_ennreal]

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

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

Tactic:
rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']

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

Goal state before:
pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
⊢ ‖x‖ = 1

Tactic:
simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this

Goal state after:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = ↑r * edist x y

Tactic:
refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist (e.symm.toFun (e.toEquiv x)) (e.symm.toFun (e.toEquiv y)) = ↑(ratio e)⁻¹ * edist (e.toEquiv x) (e.toEquiv y)
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = 0
⊢ edist (e x) (e y) = 0

Tactic:
simp [*, Dilation.ratio_ne_zero]

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = ∞
⊢ edist (e x) (e y) = ∞

Tactic:
simp [*, Dilation.ratio_ne_zero]

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ := e.surjective.forall₂.2 fun x y ↦ by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
hY : ∀ (x y : Y), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ (cobounded E).NeBot

Tactic:
rw [neBot_iff, Ne, cobounded_eq_bot_iff, ← isBounded_univ]
  exact NormedSpace.unbounded_univ 𝕜 E

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

Goal state before:
pp: case inr.refine_2
α : 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
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j

Tactic:
· rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
rcases (pi s t).eq_empty_or_nonempty with h | h
  · simp [h]
  · simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

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

Goal state before:
pp: s : SignType
k : ℕ
⊢ (s * s) ^ k * s = s

Tactic:
cases s

Goal state after:
case zero
k : ℕ
⊢ (zero * zero) ^ k * zero = zero

case neg
k : ℕ
⊢ (neg * neg) ^ k * neg = neg

case pos
k : ℕ
⊢ (pos * pos) ^ k * pos = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s * s) ^ k * s = s

Tactic:
cases s

Goal state after:
case inr.zero
k : ℤ
hs : zero ≠ 0
⊢ (zero * zero) ^ k * zero = zero

case inr.neg
k : ℤ
hs : neg ≠ 0
⊢ (neg * neg) ^ k * neg = neg

case inr.pos
k : ℤ
hs : pos ≠ 0
⊢ (pos * pos) ^ k * pos = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
⊢ s ^ n = 1

Tactic:
cases s

Goal state after:
case zero
n : ℕ
hn : Even n
hs : zero ≠ 0
⊢ zero ^ n = 1

case neg
n : ℕ
hn : Even n
hs : neg ≠ 0
⊢ neg ^ n = 1

case pos
n : ℕ
hn : Even n
hs : pos ≠ 0
⊢ pos ^ n = 1
Module: Mathlib.Data.Sign.Basic

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

Tactic:
cases s

Goal state after:
case zero
z : ℤ
hz : Even z
hs : zero ≠ 0
⊢ zero ^ z = 1

case neg
z : ℤ
hz : Even z
hs : neg ≠ 0
⊢ neg ^ z = 1

case pos
z : ℤ
hz : Even z
hs : pos ≠ 0
⊢ pos ^ z = 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
⊢ f ↑s = ↑s

Tactic:
cases s

Goal state after:
case zero
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑zero = ↑zero

case neg
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑neg = ↑neg

case pos
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑pos = ↑pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
s : SignType
⊢ ↑(-s) = -↑s

Tactic:
cases s

Goal state after:
case zero
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-zero) = -↑zero

case neg
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-neg) = -↑neg

case pos
α : Type u_2
inst✝¹ : One α
inst✝ : SubtractionMonoid α
⊢ ↑(-pos) = -↑pos
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ ↑(tsum f) = ∑' (a : α), ↑(f a)

Tactic:
rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i

Tactic:
· exact ENNReal.summable.hasSum

Goal state after:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s), SemicontinuousAt (s.domRestrict r) ⟨x, h⟩) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
refine forall₂_congr fun a ha ↦ forall₂_congr fun b _ ↦ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
a : α
ha : a ∈ s
b : β
x✝ : s.domRestrict r ⟨a, ha⟩ b
⊢ (∀ᶠ (x' : ↑s) in 𝓝 ⟨a, ha⟩, s.domRestrict r x' b) ↔ ∀ᶠ (x' : α) in 𝓝[s] a, r x' b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
a : ℝ
a_0 : 0 < ↑a
b_0 : 0 < ⊤
a_b : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹

Tactic:
exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := ⋯
ℱ : Filter α := ⋯
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun a ↦ φ (f ↑a)

Tactic:
change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
      exact Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)

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

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

Tactic:
mul_comm a

Goal state after:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ioo 0 b, c < b' * a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c

Tactic:
mul_comm a

Goal state after:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∀ (ε : ℝ≥0), 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
intro ε hε (hb : (∑' i, μ (s i)) < ∞)
        rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 hε).ne' ℕ with ⟨ε', hε', hl⟩
        grw [← hl]
        rw [← ENNReal.tsum_add]
        choose f hf using
          show ∀ i, ∃ f : ℕ → Set α, (s i ⊆ ⋃ i, f i) ∧ (∑' i, m (f i)) < μ (s i) + ε' i by
            intro i
            have : μ (s i) < μ (s i) + ε' i :=
              ENNReal.lt_add_right (ne_top_of_le_ne_top hb.ne <| ENNReal.le_tsum _)
                (by simpa using (hε' i).ne')
            rcases iInf_lt_iff.mp this with ⟨t, ht⟩
            exists t
            contrapose! ht
            exact le_iInf ht
        refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)
        rw [← ENNReal.tsum_prod, ← Nat.pairEquiv.symm.tsum_eq]
        refine iInf_le_of_le _ (iInf_le _ ?_)
        apply iUnion_subset
        intro i
        apply Subset.trans (hf i).1
        apply iUnion_subset
        simp only [Nat.pairEquiv_symm_apply]
        rw [iUnion_unpair]
        intro j
        apply subset_iUnion₂ i

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

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun x ↦ g x / f x) l (𝓝 a⁻¹)

Tactic:
simp_rw [← inv_div (f _)]
    exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ False

Tactic:
by_cases hr : 1 = |r|

Goal state after:
case pos
𝕜 : 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|
⊢ False

case neg
𝕜 : 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|
⊢ False
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
convert! edist_le_tsum_of_edist_le_of_tendsto _ hu ha _

Goal state after:
case e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ∞ ≤ ⊤ s

Tactic:
exact le_rfl

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

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

Tactic:
· dsimp only [boundedBy]
    congr with s : 1
    rw [image_nonempty]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
n : ι
⊢ (f ∘ Encodable.encode) n ≤ f (Encodable.encode n)

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
⊢ LowerSemicontinuousWithinAt (fun x ↦ min (f x) (g x)) s a

Tactic:
by
  intro b hb
  simp only [lt_inf_iff] at hb ⊢
  exact Eventually.and (hf b hb.1) (hg b hb.2)

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

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ m s h ≤ extend m s

Tactic:
simp only [extend, le_iInf_iff]

Goal state after:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ ∀ (i : P s), m s h ≤ m s i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m

Tactic:
by
  refine generateFrom_le ?_
  rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩
  refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_
  exact measurableSet_generateFrom (hft_mem_pi x hx_mem)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]

Goal state after:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n ↦ {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
exact
    d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n =>
      Encodable.iUnion_decode₂_cases d.has_empty h

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)

Tactic:
image_id

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Tactic:
← htm.1,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁ t = op (m₂.trim s) (m₃.trim s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ toMeasurable μ s =ᵐ[μ] s

Tactic:
toMeasurable_def,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose) =ᵐ[μ]
    s
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : Measure α
f : α → β
⊢ map f (c • μ) = c • map f μ

Tactic:
by
  suffices ∀ c : ℝ≥0∞, (c • μ).map f = c • μ.map f by simpa using this (c • 1)
  clear c; intro c
  rcases eq_or_ne c 0 with (rfl | hc); · simp
  by_cases hf : AEMeasurable f μ
  · have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]
    congr 1
    apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
    exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk
  · have hfc : ¬AEMeasurable f (c • μ) := by
      intro hfc
      exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩
    simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
⊢ ∀ ⦃a₂ : Measure α⦄, map f μ = map f a₂ → μ = a₂

Tactic:
ν

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
⊢ map f μ = map f ν → μ = ν
Module: Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ limsup s cofinite ⊆ ⋃ i, s ↑i

Tactic:
rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]

Goal state after:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ ⨅ i, ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a ⊆ ⋃ x, ⋃ (hx : x ∉ t), s ↑⟨x, hx⟩