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

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty
⊢ dist (g ⟨x, I⟩) y ≤ 0

Tactic:
have J : ∀ n : ℕ, dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n := fun n =>
      calc
        dist (g ⟨x, I⟩) y ≤ dist (g ⟨x, I⟩) (u (x n)) + dist y (u (x n)) :=
          dist_triangle_right _ _ _
        _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A ⟨x, I⟩ n) (hx n)

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
y : α
x : ℕ → ℕ
hx : ∀ (n : ℕ), y ∈ closedBall (u (x n)) ((1 / 2) ^ n)
I : (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty
J : ∀ (n : ℕ), dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n
⊢ dist (g ⟨x, I⟩) y ≤ 0
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
    add_comm]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
⊢ ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m

Tactic:
lintegral_iSup _ hm

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
⊢ ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ n, ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ ↦ ∑ r ∈ s n, r * f n r μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ = 0

Tactic:
simp [lintegral_congr_ae hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (Prod.snd ⁻¹' s) = 0

Tactic:
← univ_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) = 0
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x ↦ ↑x.1 * ↑x.2) y = x * g
⊢ x ∈ S

Tactic:
conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x ↦ ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ x ∈ S
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H

Tactic:
let H'' : Subgroup H := H'.comap H.subtype

Goal state after:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁.refine_1
γ : 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 β := ⋯
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
t : ↑b
ht : Disjoint ↑⟨s, sb⟩ ↑t
⊢ f y ∈ f '' ↑(↑⟨(⟨s, sb⟩, t), ht⟩).1

Tactic:
exact mem_image_of_mem _ ys

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
⊢ ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H

Tactic:
let H'' : Subgroup H := H'.comap H.subtype

Goal state after:
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁.refine_2
γ : 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 β := ⋯
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
t : ↑b
ht : Disjoint ↑⟨s, sb⟩ ↑t
⊢ f y ∈ f '' ↑(↑⟨(t, ⟨s, sb⟩), ⋯⟩).2

Tactic:
exact mem_image_of_mem _ ys

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ g₁⁻¹ * g₂ ∈ K

Tactic:
rw [← hSK.equiv_fst_mul_equiv_snd g₂, ← hSK.equiv_fst_mul_equiv_snd g₁, ← h,
      mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ ↑((hSK.equiv g₁).2⁻¹ * (hSK.equiv g₂).2) ∈ K
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Tendsto f' (cocompact α) (cocompact β)

Tactic:
simp_rw [h]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Tendsto (⇑f) (cocompact α) (cocompact β)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ

Tactic:
refine le_antisymm ?_ (borel_anti hle)
  intro s hs
  have e := @Continuous.measurableEmbedding
    _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl)
    t _ (@borel _ t) (@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id
  convert! e.measurableSet_image.2 hs
  simp only [id_eq, image_id']

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

Goal state before:
pp: case mpr
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
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s

Tactic:
intro ⟨y, yins, hy⟩

Goal state after:
case mpr
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
x✝ : H
y : G
yins : y ∈ s
hy : f y = (fun x ↦ f g * x) x✝
⊢ x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}

Tactic:
rcases l.exists_antitone_basis with ⟨u, hu⟩

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n ↦ f n x) l (𝓝 c)}
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mpr
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✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ x * f g) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ x * g) ⁻¹' s

Tactic:
intro ⟨y, yins, hy⟩

Goal state after:
case mpr
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✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
y : G
yins : y ∈ s
hy : f y = (fun x ↦ x * f g) x✝
⊢ x✝ ∈ ⇑f '' (fun x ↦ x * g) ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν) (Prod.snd ⁻¹' s) = ν s

Tactic:
← univ_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν) (univ ×ˢ s) = ν s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' Prod.snd ⁻¹' s) = μ (Y ⁻¹' s)

Tactic:
← univ_prod,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' univ ×ˢ s) = μ (Y ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬∀ i ⊆ univ, IsCompact i → μ i = 0

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x, ∃ (_ : x ⊆ univ) (_ : IsCompact x), ¬μ x = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
map_map f.symm.continuous.measurable f.continuous.measurable

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:

Tactic:
μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFA : F ⊆ A
hFc : IsClosed[inst✝²] F
hF : μ A < μ F + ε
⊢ ∃ F ⊆ A, IsClosed[inst✝²] F ∧ μ (A \ F) < ε

Tactic:
exact ⟨F, hFA, hFc, measure_sdiff_lt_of_lt_add hFc.nullMeasurableSet hFA
    (ne_top_of_le_ne_top h'A <| measure_mono hFA) hF⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬∀ i ⊆ univ, IsCompact i → μ i = 0

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ∃ x, ∃ (_ : x ⊆ univ) (_ : IsCompact x), ¬μ x = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
map_map f.symm.continuous.measurable f.continuous.measurable

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ sqrt (x * x) = x

Tactic:
rw [← sq, sqrt_sq]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ≥0
⊢ sqrt (x * y) ≤ max x y

Tactic:
rw [sqrt_le_iff_le_sq, sq]; gcongr <;> simp

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ comap (fun x ↦ √x) atTop = atTop

Tactic:
by
  unfold sqrt
  simp_rw [← Function.comp_def]
  simp [← comap_comap]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral f μ

Tactic:
hasFiniteIntegral_iff_norm

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
· rw [← abs_le, ← sq_abs]
    exact (le_sqrt (abs_nonneg x) h).mp

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ a < (a.sqrt + 1) ^ 2

Tactic:
exact Nat.lt_succ_sqrt' a

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ f x * (f x)⁻¹ = 1 x

Tactic:
ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ 1 = 1 x
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg.refine_1
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ 0 = y → 0 = e.symm y

pp: case neg.refine_2
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y

Tactic:
· rintro rfl
      simp

Goal state after:
case neg.refine_2
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑im

Tactic:
intro x y
  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
  calc ‖im x - im y‖ₑ
  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
← mul_right_inj' (neg_ne_zero.mpr this)

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ ≤ im z ↔ -I * z = -I * (I * ↑‖z‖)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tanh (x * I) = tan x * I

Tactic:
rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =o[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =o[l] g'

Tactic:
simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]

Goal state after:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith c l (fun x ↦ f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x i) g'
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = sin x

Tactic:
← tan_mul_cos hx.ne',

Goal state after:
x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = tan x * cos x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
t : rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
simpa [mul_div_assoc] using t

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
zpow_add' (by simp [em']),

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ k * a ^ k ↔ a ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp x / x ^ n ∈ Set.Ici C

Tactic:
Set.mem_Ici,

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ C ≤ rexp x / x ^ n
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty

Tactic:
exact ⟨0, f.ker.zero_mem⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (range cos).Infinite

Tactic:
rw [Real.range_cos]

Goal state after:
⊢ (Icc (-1) 1).Infinite