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

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
⊢ ∃ x ∈ s, l ≤ 𝓝 x
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
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]

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

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

Tactic:
induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Goal state after:
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:
by
  obtain ⟨u : ℕ → E, u_in : ∀ n, u n ∈ s, lim_u : Tendsto u atTop (𝓝 a)⟩ :=
    mem_closure_iff_seq_limit.mp hg
  obtain ⟨n₀, hn₀⟩ : ∃ n₀, ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0 :=
    haveI : { x | ‖x⁻¹ * a‖ < b 0 } ∈ 𝓝 a := by
      simp_rw [← dist_eq_norm_inv_mul]
      exact Metric.ball_mem_nhds _ (b_pos _)
    Filter.tendsto_atTop'.mp lim_u _ this
  set z : ℕ → E := fun n => u (n + n₀)
  have lim_z : Tendsto z atTop (𝓝 a) := lim_u.comp (tendsto_add_atTop_nat n₀)
  have mem_𝓤 : ∀ n, { p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1) } ∈ 𝓤 E := fun n => by
    simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)
  obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)⟩ :=
    lim_z.cauchySeq.subseq_mem mem_𝓤
  set w : ℕ → E := z ∘ φ
  have hw : Tendsto w atTop (𝓝 a) := lim_z.comp φ_extr.tendsto_atTop
  set v : ℕ → E := fun i => if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
  refine ⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
  · apply hw.congr (fun n ↦ ?_)
    rw [Finset.prod_range_succ']
    have : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n := by
      apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)
      simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]
      group
    simp [this]
  · rintro ⟨⟩
    · change w 0 ∈ s
      apply u_in
    · exact s.mul_mem (s.inv_mem (u_in _)) (u_in _)
  · intro l hl
    obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := Nat.exists_eq_succ_of_ne_zero hl.ne'
    rw [← norm_inv']
    simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right,
      mul_inv_rev, inv_inv, v]
    apply hφ

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
⊢ ∃ R, ∃ᶠ (n : ι) in l, R < x n

Tactic:
by_contra! h
  refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
  simp only [eventually_map, ENNReal.coe_le_coe]
  filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)

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

Goal state before:
pp: case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
obtain ⟨q, hq⟩ := exists_rat_lt R

Goal state after:
case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
· rcases le_or_gt x b with hxb | hbx
    · lift x to Icc a b using ⟨hax, hxb⟩
      rw [IccExtend_val, comp_apply]
    · simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]

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

Goal state before:
pp: case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x = 0
⊢ ‖x‖ ≠ 1

Tactic:
simp [hx]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
h x y

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ ↑(r * nndist x y) = ↑(r * nndist x y)
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ
⊢ ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
by simpa [enorm_eq_nnnorm, ← ENNReal.coe_mul, ENNReal.coe_le_coe] using! h

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖

Tactic:
calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' t i ×ˢ Set.tprod l t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
TProd.mk,

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ (fun f ↦ (f i, TProd.mk l f)) ⁻¹' t i ×ˢ Set.tprod l t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
⊢ Tendsto (fun y ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)

Tactic:
rcases basis_sets _ |>.map _ |>.disjoint_iff nhds_basis_ball
    |>.mp (hf x hx) with ⟨U, hUx, r, hr₀, hr⟩

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
⊢ Tendsto (fun y ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Preorder β
f g : α → β
s : Set α
a : α
h : LowerSemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
hx : f x = g x
⊢ ∀ (y : β), f x > y ↔ g x > y

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
hx : f x = g x
⊢ ∀ (y : Set β), IsOpen[inst✝] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst✝] y ∧ (g x ∩ y).Nonempty

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
x : α
hx : f x = g x
⊢ ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ⊥) ↔ Tendsto f l atBot

Tactic:
by
  rw [tendsto_nhds_bot_iff_real, atBot_basis_Iio.tendsto_right_iff]; simp

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

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

Tactic:
exact ((Continuous.prodMk_left y).tendsto x).eventually (hf (x, y) (fun _ => hy))

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.23
f : β → α
h : Monotone m ∨ Surjective f
⊢ m (f '' ∅) = 0

Tactic:
simp; simp [m_empty]

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

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = #(Finset.range n) • 1

Tactic:
nsmul_one,

Goal state after:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = ↑(#(Finset.range n))
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
by
  simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
  rw [mul_assoc, mul_comm]
  convert! edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
  rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m (∅ ∩ s) = 0

Tactic:
simp; simp [m_empty]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
⊢ ⋂ i, s i ⊆ dissipate s x

Tactic:
simp only [dissipate, subset_iInter_iff]
  exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ ∑ i ∈ Finset.range n.succ, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n.succ), s i)

Tactic:
rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
      m.measure_inter_union _ (h n), add_comm]

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ s n ∩ ⋃ k, ⋃ (_ : k < n), s k ⊆ ∅
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
a : Set α
h : d.Has aᶜ
⊢ d.Has a

Tactic:
simpa using d.has_compl h

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ μ (aeSeqSet hf p)ᶜ = 0

Tactic:
by
  rw [aeSeqSet, compl_compl, measure_toMeasurable]
  have hf_eq := fun i => (hf i).ae_eq_mk
  simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
  exact Filter.Eventually.and hf_eq hp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ ↑(g '' Bᶜ) ≃ᵐ ↑Bᶜ

Tactic:
exact (hg.equivImage _).symm

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
hb : IsSuccPrelimit b
⊢ Tendsto f l (comap Subtype.val (𝓝[<] b)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] b)

Tactic:
tendsto_comap_iff,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
hb : IsSuccPrelimit b
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] b) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] b)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto f l (comap Subtype.val (𝓝[>] a)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
tendsto_comap_iff,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Ioi a)
ha : IsPredPrelimit a
⊢ Tendsto f l (comap Subtype.val (𝓝[>] a)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
tendsto_comap_iff,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Ioi a)
ha : IsPredPrelimit a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Iio a)
ha : IsSuccPrelimit a
⊢ Tendsto f l (comap Subtype.val (𝓝[<] a)) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] a)

Tactic:
tendsto_comap_iff,

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → ↑(Iio a)
ha : IsSuccPrelimit a
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] a) ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[<] a)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
← ENNReal.sub_sub_cancel hk (iInf_le (fun i => μ (s i)) k),

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (⋂ i, s i) = μ (s k) - (μ (s k) - ⨅ i, μ (s i))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∑' (x : ℕ), μ (f x) ≠ ∞

Tactic:
← MeasureTheory.measure_iUnion hf₂ hf₁

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ μ (⋃ i, f i) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Goal state after:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
measure_iUnion_eq_iSup_accumulate

Goal state after:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (⨆ i, μ (accumulate f i)))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (u ∩ t) = ν (u ∩ t)
⊢ μ (uᶜ ∩ t) = ν (uᶜ ∩ t)

Tactic:
| compl u hu ihu =>

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ (μ.trim hm).toOuterMeasure = μ.trim

Tactic:
Measure.trim,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ (μ.toMeasure ⋯).toOuterMeasure = μ.trim
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
⊢ (μ.trim hm) s = μ s

Tactic:
Measure.trim,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
⊢ (μ.toMeasure ⋯) s = μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' (i : ℕ), (μ₁ (s i) + μ₂ (s i))

Tactic:
ENNReal.tsum_add,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁✝ μ₂✝ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
x✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑' (a : ℕ), μ₁ (s a) + ∑' (a : ℕ), μ₂ (s a)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ (sInf (toOuterMeasure '' {μ, ν})) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Tactic:
OuterMeasure.sInf_apply
    (image_nonempty.2 <| insert_nonempty μ {ν})

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) =
    sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet t μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.mono_ac absolutelyContinuous_restrict⟩

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet t μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
by
    rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]

Goal state after: