mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Continuity

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

Tactic:
by
  obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
  choose g hg using v_in
  exact
    ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
      fun n hn => by simpa [hg] using hv_pos n hn⟩

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✝³ : SMul M N
inst✝² : UniformContinuousConstSMul M X
inst✝¹ : UniformContinuousConstSMul N X
inst✝ : IsScalarTower M N X
m : M
n : N
x : Completion X
⊢ (m • n) • x = m • n • x

Tactic:
have : _ = (_ : Completion X → Completion X) :=
      map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)
    refine Eq.trans ?_ (congr_fun this.symm x)
    exact congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})

Tactic:
refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_

Goal state after:
case refine_1
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun x_1 ↦ edist (x_1 x) (x_1 y)

case refine_2
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun x_1 ↦ ↑K * edist x y
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
by
  refine mul_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (mul_lt_mul a_x b_x)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ dist (p.1 + p.2) (q.1 + q.2) ≤ ↑2 * dist p q

Tactic:
simp only [Real.dist_eq, Prod.dist_eq, NNReal.coe_ofNat,
      add_sub_add_comm, two_mul]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x✝² x✝¹ : ℚ
x✝ : |x✝²| ≤ |x✝¹|
⊢ ‖x✝²‖ ≤ ‖x✝¹‖

Tactic:
simpa only [norm, ← Rat.cast_abs, Rat.cast_le]

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖

Tactic:
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
  refine le_trans (solid ?_) (norm_add_le |a - c| |b - d|)
  rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
  calc
    |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_inf_sub_inf_le_abs _ _ _
      · rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ LipschitzWith K f⁻¹ ↔ LipschitzWith K f

Tactic:
by simp [LipschitzWith]

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‖₊, ⋯⟩
⊢ ∃ a, ⟨‖x‖₊, ⋯⟩ < a ∧ a < ⟨‖y‖₊, ⋯⟩

Tactic:
let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy

Goal state after:
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‖₊, ⋯⟩
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
abel_nf

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

Goal state before:
pp: case inl
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
a : α
ha : IsEmpty (ι a)
⊢ ∃ a ∈ Finset.univ, ⨆ i, f a i = 0

Tactic:
exact ⟨a, by simp⟩

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

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
inst✝ : DecidableEq ι
v : TProd α (i :: l)
⊢ v.elim ⋯ = v.1

Tactic:
by simp [TProd.elim]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
by
    refine uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_
    · refine Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_
      simpa
    · apply Metric.closedBall_mem_nhds
      simpa

Goal state after:
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 ≠ ⊥

Tactic:
Ne,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬cobounded E = ⊥
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖f x‖ = ‖(↑n)⁻¹ • f (n • x)‖

Tactic:
by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]

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

Goal state before:
pp: ⊢ ∀ (x y : SignType), -x * y = -(x * y)

Tactic:
by rintro ⟨_⟩ ⟨_⟩ <;> rfl

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

Goal state before:
pp: ⊢ ∀ (x y : SignType), x * -y = -(x * y)

Tactic:
by rintro ⟨_⟩ ⟨_⟩ <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.le]
  · simp [← h]
  · simp [h, h.not_ge]

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

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

Tactic:
Ne,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬(↑x✝).abs = 0
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
h : Semicontinuous r
b : β
⊢ IsOpen[inst✝] {x | r x b}

Tactic:
by simpa [isOpen_iff_mem_nhds, Filter.Eventually] using fun x hx ↦ h x b hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
x : α
⊢ LowerHemicontinuousWithinAt f s x ↔
    ∀ (u : Set β), IsOpen[inst✝] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ u).Nonempty

Tactic:
simp +contextual [SemicontinuousWithinAt]

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

Goal state before:
pp: ⊢ ↑1⁻¹ = 1

Tactic:
_root_.inv_one,

Goal state after:
⊢ ↑1 = 1
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [lowerHemicontinuousWithinAt_iff, compl_surjective.forall]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), IsOpen[inst✝] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

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

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' ↦ ⨆ i, f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  rw [← nhdsWithin_univ] at bdd
  exact lowerSemicontinuousWithinAt_ciSup bdd h

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

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ∞
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε

Tactic:
by
  lift w to ι → ℝ≥0 using hw
  rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
  have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)
  refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩
  refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum
  rw [coe_div (this i).ne']
  refine mul_le_of_le_div' ?_
  grw [← le_max_right]

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

Goal state before:
pp: α : Type u_2
f : Filter α
m : α → EReal
a b : EReal
hm : Tendsto m f (𝓝 a)
h₁ : a ≠ 0 ∨ b ≠ ⊥
h₂ : a ≠ 0 ∨ b ≠ ⊤
⊢ Tendsto (fun x ↦ m x * b) f (𝓝 (a * b))

Tactic:
simpa only [mul_comm] using EReal.Tendsto.const_mul hm h₁.symm h₂.symm

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ x ∈ t, f x ∈ π x
hti : ∀ y ∈ t, y = i
hi : i ∉ t
⊢ ⋂ x ∈ t, f x ∈ π i ∨ ⋂ x ∈ t, f x ∈ {univ}

Tactic:
· have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
      simp [ht_empty, iInter_univ, Set.mem_singleton univ]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t

Tactic:
rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
H : s ≤ᵐ[μ] t
⊢ μ (s ∪ t) = μ (t ∪ s \ t)

Tactic:
by rw [union_sdiff_self, Set.union_comm]

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

Goal state before:
pp: α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ generateFrom {s} = MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤

Tactic:
refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_

Goal state after:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ MeasurableSpace.comap (fun x ↦ x ∈ s) ⊤ ≤ generateFrom {s}
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ∀ (i : Set α), s ⊆ i → MeasurableSet i → m i = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ∞

Tactic:
exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ map (⇑e.symm) (map (⇑e) μ) = μ

Tactic:
simp [map_map e.symm.measurable e.measurable]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k) '' s =ᵐ[μ] s

Tactic:
rw [Equiv.image_eq_preimage_symm]
  obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
  · replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage_symm] at hs
    replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
    rwa [Equiv.Perm.iterate_eq_pow e⁻¹ k, inv_pow e k] at he'
  · rw [zpow_neg, zpow_natCast]
    replace hs : e ⁻¹' s =ᵐ[μ] s := by
      convert! he.preimage_ae_eq hs.symm
      rw [Equiv.preimage_image]
    replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
    rwa [Equiv.Perm.iterate_eq_pow e k] at he

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

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ g ≠ 1

Tactic:
Ne,

Goal state after:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g = 1
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ ∑' (i : ι), μ (s i) ≤ μ univ

Tactic:
apply tsum_measure_le_measure_univ hs

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ Pairwise (AEDisjoint μ on s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
⊢ Pairwise (AEDisjoint μ on s)

Tactic:
intro i j hij

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
H : ∀ (i j : ι), i ≠ j → s i ∩ s j = ∅
i j : ι
hij : i ≠ j
⊢ (AEDisjoint μ on s) i j
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ (μ.restrict (toMeasurable μ s)) t = μ (t ∩ s)

Tactic:
restrict_apply' (measurableSet_toMeasurable _ _),

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ μ (t ∩ toMeasurable μ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case hs
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ Antitone fun i ↦ ⋂ j, ⋂ (_ : j ≤ i), f j

pp: case hsm
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ ∀ (i : ι), NullMeasurableSet (⋂ j, ⋂ (_ : j ≤ i), f j) μ

pp: case hfin
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ ∃ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j) ≠ ∞

Tactic:
· exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl

Goal state after:
case hsm
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ ∀ (i : ι), NullMeasurableSet (⋂ j, ⋂ (_ : j ≤ i), f j) μ

case hfin
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ ∃ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case h₂
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≤ μ (⋃₀ D)

pp: case hsm
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ NullMeasurableSet (⋃₀ D) μ

pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≠ ∞

Tactic:
· rw [hD, show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp]
    apply le_biSup (f := fun D ↦ μ (⋃₀ D))
    simp [D_mem.2, insert_subset_iff, hs, D_mem.1]

Goal state after:
case hsm
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ NullMeasurableSet (⋃₀ D) μ

case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⋯
D : Set (Set α)
D_mem : D ∈ {D | D ⊆ C ∧ D.Countable}
hD : μ (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ μ (s ∪ ⋃₀ D) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0

Tactic:
simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhdsWithin

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

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

Tactic:
toMeasure_toOuterMeasure (ms := m)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ μ.trim = μ.trim
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case e_a.e_6
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Tactic:
simp [and_comm]

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

Goal state before:
pp: case e_a.e_6
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Tactic:
simp [and_comm]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
x : α
hx : ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
⊢ f x ∈ s → g x ∈ s → f x = g x

Tactic:
hxf

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
f g : α → β
p : Set β → Prop
s : Set β
h' : HasCountableSeparatingOn β p s
hf : ∀ᶠ (x : α) in l, f x ∈ s
hg : ∀ᶠ (x : α) in l, g x ∈ s
h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U
S : Set (Set β)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
x : α
hx : ∀ s ∈ S, f x ∈ s ↔ g x ∈ s
hxf : f x ∈ s
⊢ g x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
⊢ measurableAtom x = countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1

Tactic:
have hA : ∀ n, MeasurableSet (A n) := measurableSet_natGeneratingSequence

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
⊢ measurableAtom x = countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ MeasurableSet u

Tactic:
simp only [memPartition_zero, mem_singleton_iff] at hun
      rw [hun]
      exact MeasurableSet.univ

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ (∀ (i : Bool), AEMeasurable f (bif i then μ else ν)) ↔ AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
Bool.forall_bool,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (bif false then μ else ν) ∧ AEMeasurable f (bif true then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν