mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Tactic:
rw [restrict_map hg hs, lintegral_map hf hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Tactic:
by
  rw [restrict_map hg hs, lintegral_map hf hg]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ AnalyticSet s ↔ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

Tactic:
by
  constructor
  · intro h
    rw [AnalyticSet] at h
    rcases h with h | h
    · refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩
      rw [h]
      exact range_eq_empty _
    · exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩
  · rintro ⟨β, h, h', f, f_cont, f_range⟩
    rw [← f_range]
    exact analyticSet_range_of_polishSpace f_cont

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Tactic:
rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
let := TopologicalSpace.upgradeIsCompletelyMetrizable α
  obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc
  obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty
  exact ⟨f, hfD.trans hDC, hf⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
⊢ IsProbabilityMeasure (dite p μ ν)

Tactic:
by split <;> infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure (if p then μ else ν)

Tactic:
by split <;> infer_instance

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ univ - μ s = 1 - μ s

Tactic:
measure_univ

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ 1 - μ s = 1 - μ s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = s.indicator 1 a

Tactic:
rw [indicator_of_notMem h, ← nonpos_iff_eq_zero]

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s ≤ 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ AnalyticSet s

Tactic:
by
  have : PolishSpace s := hs.polishSpace
  rw [← @Subtype.range_val α s]
  exact analyticSet_range_of_polishSpace continuous_subtype_val

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ ⋃ n, s n ⊆ ⋃ m, ⋂ n, u m n

Tactic:
refine iUnion_subset fun m => subset_iUnion_of_subset m ?_

Goal state after:
case refine_1
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
m : ι
⊢ s m ⊆ ⋂ n, u m n
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Function.onFun Disjoint f) →
        ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m

Tactic:
intro f hf h

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
⊢ ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Finset α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}

Tactic:
by
  simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t r : ℝ
ht : t ∈ Ioc 0 K
hr : r ≤ R
rneg : r < 0
this : t * r < 0
⊢ μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)

Tactic:
simp only [closedBall_eq_empty.2 this, measure_empty, zero_le]

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ s ⊆ S

Tactic:
apply subset_toMeasurable

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

Goal state before:
pp: case ht
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := ⋯
T : Set β := ⋯
⊢ t ⊆ T

Tactic:
apply subset_toMeasurable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι' : Type u_4
inst✝¹ : Countable ι'
m : Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), (sum m') (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m

Tactic:
Measure.sum_apply _ (M _)

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι' : Type u_4
inst✝¹ : Countable ι'
m : Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), ∑' (i : ι'), (m' i) (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum fun i ↦ sum fun p ↦ (m i).prod (m' p)) = sum fun p ↦ (m p.1).prod (m' p.2)

Tactic:
sum_sum

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
⊢ (map (⇑f) μ).InnerRegularWRT pb qb

Tactic:
intro U hU r hr
  rw [f.map_apply U] at hr
  rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
  refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
  rwa [f.map_apply, f.preimage_image]

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

Goal state before:
pp: case right
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen[inst✝¹] U
hU : μ U < μ A + ε
⊢ μ (U \ A) < ε

Tactic:
exact measure_sdiff_lt_of_lt_add hA.nullMeasurableSet hAU hA' hU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc (Prod.mk a ⁻¹' (fun p ↦ (f p.1, g p.1 p.2)) ⁻¹' s) = μc (g a ⁻¹' Prod.mk (f a) ⁻¹' s)

Tactic:
preimage_preimage,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
h✝ : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ μc ((fun x ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) = μc (g a ⁻¹' Prod.mk (f a) ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
⊢ Measure.map ((fun x ↦ f g * x) ∘ ⇑f) μ = Measure.map (⇑f ∘ fun x ↦ g * x) μ

Tactic:
congr 2

Goal state after:
case e_f
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
⊢ (fun x ↦ f g * x) ∘ ⇑f = ⇑f ∘ fun x ↦ g * x
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : ¬AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ

Tactic:
have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hX
      exact measurable_fst.comp_aemeasurable hX
    simp [map_of_not_aemeasurable, hX, this]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ ∫⁻ (y : G), μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) ∂μ = 0

Tactic:
preimage_preimage,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ ∫⁻ (y : G), μ ((fun x ↦ (y * x, x⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) ∂μ = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ (Inv.inv ⁻¹' (fun x ↦ y⁻¹ * x) ⁻¹' Inv.inv ⁻¹' s) = 0

Tactic:
preimage_preimage,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ ((fun x ↦ (y⁻¹ * x⁻¹)⁻¹) ⁻¹' s) = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
this : ∀ {s : Set G}, μ' s ≠ ∞ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s) < ∞
⊢ s ⊆ toMeasurable μ' s

Tactic:
apply subset_toMeasurable

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y ↦ y * x) ⁻¹' s) < ∞
⊢ ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s)) = f x

Tactic:
ENNReal.mul_div_cancel (measure_mul_right_ne_zero ν' h2s _) hx.ne

Goal state after:
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 ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) ≤ 0

Tactic:
← hfg

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 ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
⊢ μ (s ∩ ⋂ j, notConvergentSeq f g n j) ≤ μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)}
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0

Tactic:
rw [quadratic_eq_zero_iff ha hs]

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:

Tactic:
(∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
      lintegral_mono_ae <| ae_norm_ofReal_f_le_bound h_bound h_lim
    _ < ∞ := by
      rw [← hasFiniteIntegral_iff_ofReal]
      · exact bound_hasFiniteIntegral
      exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h

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

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

Tactic:
have := hi x
    simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this
    simp [this]

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

Goal state before:
pp: n : ℤ
hn : 0 ≤ n
⊢ ↑|n| = ↑n

Tactic:
abs_of_nonneg hn

Goal state after:
n : ℤ
hn : 0 ≤ n
⊢ ↑n = ↑n
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
this : IsAbsoluteValue fun x ↦ ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x ↦ ‖x‖) (limAux f)) x✝).im = (↑(const (fun x ↦ ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).im

Tactic:
by simp [limAux, cauSeqIm, ofReal]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ SFinite (c • μ)

Tactic:
by
  have : c • μ = c • ((1 : ℝ≥0∞) • μ) := by simp
  rw [this, ← smul_assoc, ← withDensity_const]
  infer_instance

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ μ.prod (c • ν) = c • μ.prod ν

Tactic:
ext s hs
  have A (s : Set β) : c • ν s = (c • 1) * ν s := by simp
  simp_rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs, A]
  rw [lintegral_const_mul, smul_one_mul]
  exact measurable_measure_prodMk_left hs

Goal state after:
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
e : A ≃⋆* B
b : B
⊢ e.symm.toFun (star b) = star (e.symm.toFun b)

Tactic:
simpa only [EquivLike.apply_inv_apply, EquivLike.inv_apply_apply] using!
        congr_arg (EquivLike.inv e) (map_star e (EquivLike.inv e b)).symm

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Tactic:
induction n with
  | zero => simp only [pow_zero, pow_one]
  | succ k hk =>
    rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + -(↑(im z) * I) = ↑(re z) - ↑(im z) * I

Tactic:
sub_eq_add_neg

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + -(↑(im z) * I) = ↑(re z) + -(↑(im z) * I)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = -(I * ((starRingEnd K) z - z) / 2)

Tactic:
← neg_div,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -I * (starRingEnd K) z) / 2 = -(I * ((starRingEnd K) z - z)) / 2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -(I * (starRingEnd K) z)) / 2 = (I * z - I * (starRingEnd K) z) / 2

Tactic:
sub_eq_add_neg

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -(I * (starRingEnd K) z)) / 2 = (I * z + -(I * (starRingEnd K) z)) / 2
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ z ∈ slitPlane ∨ -z ∈ slitPlane

Tactic:
mem_slitPlane_iff,

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ -z ∈ slitPlane
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z w : ℝ
⊢ 0 (z * w) = (AddMonoidHom.id ℝ) z * 0 w + 0 z * (AddMonoidHom.id ℝ) w

Tactic:
simp only [add_zero, zero_mul, mul_zero, AddMonoidHom.zero_apply]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ True ∧ ↑e.symm (↑e y) ∈ s ∧ ↑e.symm (↑e y) ∈ f ⁻¹' t

Tactic:
true_and,

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
y : X
hy : y ∈ e.source
hyu : y ∈ s → y ∈ f ⁻¹' t
⊢ ↑e.symm (↑e y) ∈ s ↔ ↑e.symm (↑e y) ∈ s ∧ ↑e.symm (↑e y) ∈ f ⁻¹' t
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w -
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
exact h.mul_re_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ (∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
eventually_principal

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ (∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ (∃ c, ∀ᶠ (x : α) in 𝓟 s, ‖f x‖ ≤ c * ‖g x‖) ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
eventually_principal

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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x * v x‖ ≤ c * ‖v x‖

Tactic:
refine (norm_mul_le _ _).trans ?_

Goal state after:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
x : α
hx : ‖φ x‖ ≤ c
⊢ ‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
use fun x => u x / v x

Goal state after:
case h
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ (∀ᶠ (x : α) in l, ‖(fun x ↦ u x / v x) x‖ ≤ c) ∧ u =ᶠ[l] (fun x ↦ u x / v x) * v
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (sinh ↑x) = sinh ↑x

Tactic:
rw [← sinh_conj, conj_ofReal]

Goal state after: