mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊓ g) μ

Tactic:
refine
    ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩
  refine (measure_mono (support_inf _ _)).trans_lt ?_
  exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∑' (n : α), f n x

Tactic:
simp_rw [← continuousOn_univ] at hf ⊢
  exact continuousOn_tsum hf hu fun n x _ => hfu n x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
⊢ CauchySeq (f ∘ u)

Tactic:
rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
  refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
  · exact fun n ↦ mul_nonneg (by positivity) (b_nonneg n)
  · exact fun n m N hn hm ↦ hf.dist_le_mul_of_le (hb n m N hn hm)
  · rw [← mul_zero (K : ℝ)]
    exact blim.const_mul _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf✝ : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
ε : ℝ
hε : ε > 0
hε' : ball x ε ∩ s ⊆ t
⊢ ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
exact ⟨ε, hε, K, hf.mono hε'⟩

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ 1 - ↑x ≤ 1

Tactic:
by simpa using x.2.1

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 p q

Tactic:
cases p <;> cases q

Goal state after:
case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) y = Sum.dist y (Sum.inl val✝)

Tactic:
cases y

Goal state after:
case inl.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inl val✝¹)

case inl.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inl val✝¹)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) y = Sum.dist y (Sum.inr val✝)

Tactic:
cases y

Goal state after:
case inr.inl
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inr val✝¹)

case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inr val✝¹)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ dist x ⋯.some + 1

Tactic:
← le_add_of_nonneg_left dist_nonneg

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ 1
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝, snd✝⟩ y < 1
⊢ ⟨fst✝, snd✝⟩.fst = y.fst

Tactic:
cases y

Goal state after:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ < 1
⊢ ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∃ C, ∀ (a b : (n : ℕ) → E n), dist a b ≤ C

Tactic:
use 1

Goal state after:
case h
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (a b : (n : ℕ) → E n), dist a b ≤ 1
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
obtain ⟨u, -, upos', hu⟩ := exists_seq_strictAnti_tendsto' (zero_lt_one' ℝ≥0∞)

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ (map f μa) s

Tactic:
exact le_map_apply hf.aemeasurable _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst✝ : IsZeroOrProbabilityMeasure 0
hμs : p < 0 s
⊢ 0 sᶜ < 1 - p

Tactic:
simp at hμs

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i = ↑(∑' (i : α), a i)

Tactic:
simp_rw [Function.comp_apply]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), ↑(a i) = ↑(∑' (i : α), a i)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
i : ↑(↑K)ᶜ
⊢ min (2⁻¹ ^ encode ↑i) (edist (x ↑i) (y ↑i)) ≤ 2⁻¹ ^ encode ↑i

Tactic:
· apply min_le_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (map f (sum fun i ↦ m i)).join = sum fun i ↦ (map f (m i)).join

Tactic:
map_sum h,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ map f (m i)).join = sum fun i ↦ (map f (m i)).join
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : F =ᵐ[μ] univ
⊢ F = univ

Tactic:
ae_eq_univ,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : μ Fᶜ = 0
⊢ F = univ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ S.ncard = H.index

Tactic:
← Nat.card_coe_set_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
h : IsComplement S ↑H
⊢ Nat.card ↑S = H.index
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ T.ncard = H.index

Tactic:
← Nat.card_coe_set_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Nat.card ↑T = H.index
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
⊢ range f ⊆ ⋂ n, F n

pp: case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
⊢ ⋂ n, F n ⊆ range f

Tactic:
· rintro x ⟨y, rfl⟩
    refine mem_iInter.2 fun n => ?_
    obtain ⟨s, sb, ys, hs⟩ : ∃ (s : Set γ), s ∈ b ∧ y ∈ s ∧ s ⊆ ball y (u n / 2) := by
      apply hb.mem_nhds_iff.1
      exact ball_mem_nhds _ (half_pos (u_pos n))
    have diam_s : diam s ≤ u n := by
      apply (diam_mono hs isBounded_ball).trans
      convert! diam_ball (x := y) (half_pos (u_pos n)).le
      ring
    refine mem_iUnion.2 ⟨⟨s, sb⟩, ?_⟩
    refine mem_iUnion.2 ⟨⟨isBounded_ball.subset hs, diam_s⟩, ?_⟩
    apply mem_inter (subset_closure (mem_image_of_mem _ ys))
    refine mem_iInter.2 fun t => mem_iInter.2 fun ht => ⟨?_, ?_⟩
    · apply hq1
      exact mem_image_of_mem _ ys
    · apply disjoint_left.1 (hq2 ⟨(t, ⟨s, sb⟩), ht.symm⟩)
      exact mem_image_of_mem _ ys

Goal state after:
case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
⊢ ⋂ n, F n ⊆ range f
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ f ⁻¹' U ⊇ A

Tactic:
by rwa [ge_iff_le, ← image_subset_iff]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : ↥H
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ (h * h') • a = a

Tactic:
mul_smul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : ↥H
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ h • h' • a = a
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ μ (closure[inst✝²] k) = μ k

Tactic:
by
  apply le_antisymm ?_ (measure_mono subset_closure)
  simp only [measure_eq_iInf_isOpen k, le_iInf_iff]
  intro u ku u_open
  exact measure_mono (hk.closure_subset_of_isOpen u_open ku)

Goal state after:
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ μ (c • s) = μ s

Tactic:
by
  simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s

Goal state after:
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: M : Type v
α : Type w
m : MeasurableSpace α
inst✝² : SMul M α
inst✝¹ : MeasurableConstSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
exact SMulInvariantMeasure.measure_preimage_smul c hs

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ (map (fun x ↦ f g * x) μ) (⇑f '' s) = μ (⇑f '' s)

pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ MeasurableSet (⇑f '' s)

Tactic:
IsMulLeftInvariant.map_mul_left_eq_self

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ μ (⇑f '' s) = μ (⇑f '' s)

G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
this : ⇑f '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ f g * x) ⁻¹' ⇑f '' s
⊢ MeasurableSet (⇑f '' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_6
E : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableMul₂ E
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f g : ι → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᵐ[μ] g i
⊢ AEMeasurable (fun x ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
use (fun x => ∏'[L] i, g i x), Measurable.tprod hg_meas

Goal state after:
case right
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableMul₂ E
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f g : ι → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᵐ[μ] g i
⊢ (fun x ↦ ∏'[L] (i : ι), f i x) =ᵐ[μ] fun x ↦ ∏'[L] (i : ι), g i x
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map Prod.snd (map Prod.swap ρ) = ρ.fst

Tactic:
Measure.map_map measurable_snd measurable_swap

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.snd ∘ Prod.swap) ρ = ρ.fst
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)

Tactic:
have ⟨N, hN⟩ := (ENNReal.tendsto_atTop ENNReal.zero_ne_top).1
    (measure_notConvergentSeq_tendsto_zero hf hsm hs hfg n) (.ofReal (ε * 2⁻¹ ^ n))
      (by positivity)

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (0 + ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ 0 < z.im * z.im ↔ z.im ≠ 0

Tactic:
mul_self_pos

Goal state after:
z : ℂ
⊢ z.im ≠ 0 ↔ z.im ≠ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
⊢ x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]]

Tactic:
simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
      exists_eq_right_right, mem_preimage] at hx

Goal state after:
case mpr
a b₁ b₂ : ℝ
x : ℂ
hx : x.im ∈ [[b₁, b₂]] ∧ a = x.re
⊢ x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]]
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ f x * ∫⁻ (y : β), φ (x, y) ∂ν = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ ↑(#s) • a ≤ ∑ i ∈ s, (fun i ↦ f i) i

Tactic:
rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h

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

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
← RCLike.re_add_im a,

Goal state after:
case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re (↑(RCLike.re a) + ↑(RCLike.im a) * RCLike.I)) +
        ↑(RCLike.im (↑(RCLike.re a) + ↑(RCLike.im a) * RCLike.I)) * I‖ =
    ‖↑(RCLike.re a) + ↑(RCLike.im a) * RCLike.I‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖

Tactic:
filter_upwards [h₁, h₂] with x hx₁ hx₂ using
    calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ C j ≤ sSup (C '' ↑s)

Tactic:
rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]

Goal state after:
case hbc
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
hj : j ∈ s
⊢ ∃ b ∈ s, C j ≤ C b
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x ↦ ‖x‖) 1) j‖ < ε

Tactic:
convert ε0.lt

Goal state after:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x ↦ ‖x‖) 1) j‖ = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos x - cos y) = ↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
by simp [cos_sub_cos]

Goal state after: