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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
have : 𝓝[≠] x ≤ 𝓟 U := by
    rw [le_principal_iff]
    exact mem_nhdsWithin_of_mem_nhds hU
  rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]
  exact h_acc

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
⊢ ∀ a ∈ v, (a ∩ C).Countable

Tactic:
· exact sep_subset_ofPred _ _

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 : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x ↦ ∑ n ∈ t, f n x) (fun x ↦ ∑' (n : α), f n x) atTop s

Tactic:
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
  filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx
  have A : Summable fun n => ‖f n x‖ :=
    .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n => hfu n x hx) hu
  rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl t, add_sub_cancel_left]
  apply lt_of_le_of_lt _ ht
  apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
  exact (A.subtype _).tsum_le_tsum (fun n => hfu _ _ hx) (hu.subtype _)

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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ g' i a

pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a

Tactic:
· exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y z : X
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inl z)

Tactic:
by
    simp only [← glueDist_swap Φ]
    apply glueDist_triangle_inl_inr_inr

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
⊢ TopologicalSpace.PseudoMetrizableSpace X

Tactic:
let := upgradeIsCompletelyPseudoMetrizable X
  infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
n : ℕ
⊢ 1 / C ≤ infDist (↑(u n)) (↑s)ᶜ

Tactic:
have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s)ᶜ
n : ℕ
this : 0 < infDist (↑(u n)) (↑s)ᶜ
⊢ 1 / C ≤ infDist (↑(u n)) (↑s)ᶜ
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ let D := closure (eball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ ediam D ≤ ε

Tactic:
have : x ∈ Metric.eball x (ε / 2) := by
    apply Metric.mem_eball_self
    rw [ENNReal.div_pos_iff]
    exact ⟨ne_of_gt ε_pos, by simp⟩
  have := hC.closure_nhds_inter x xC this Metric.isOpen_eball
  refine ⟨this.1, this.2, ?_, ?_⟩
  · rw [IsClosed.closure_subset_iff hC.closed]
    apply inter_subset_right
  rw [Metric.ediam_closure]
  apply le_trans (Metric.ediam_mono inter_subset_left)
  convert! Metric.ediam_eball_le (x := x)
  rw [mul_comm, ENNReal.div_mul_cancel] <;> norm_num

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ map id μa = μa

Tactic:
map_id

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ μa = μa
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

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

Tactic:
rcases h with h | h

Goal state after:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous[_, inst✝] f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ univ = 0

Tactic:
← Set.union_compl_self s,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ (s ∪ sᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

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

Tactic:
by_cases h : a ∈ s; · rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
  rw [indicator_of_notMem h, ← nonpos_iff_eq_zero]
  calc
    dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
    _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ count (f '' s) = count s

Tactic:
by
  classical
  by_cases hs : s.Finite
  · lift s to Finset β using hs
    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]
    simpa only [Finset.coe_image] using fs_mble
  · rw [count_apply_infinite hs]
    rw [← finite_image_iff hf.injOn] at hs
    rw [count_apply_infinite hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ SigmaFinite count

Tactic:
by simp [sigmaFinite_iff_measure_singleton_lt_top]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Tactic:
rwa [ae_dirac_eq]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)),
                  indicator_eq_one_iff_mem] using obs

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

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
⊢ μ = ∑ a ∈ s, μ {a} • dirac a

Tactic:
ext t ht

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ t = (∑ a ∈ s, μ {a} • dirac a) t
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t \ (↑s)ᶜ) = (∑ a ∈ s, μ {a} • dirac a) t

Tactic:
Set.sdiff_compl,

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ ↑s) = (∑ a ∈ s, μ {a} • dirac a) t
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

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

Tactic:
by
  rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ (m.bind f) s ≤ ∫⁻ (a : α), (f a) s ∂m

Tactic:
rw [bind, join_apply hs]
  apply lintegral_map_le

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = (map id μ).join

Tactic:
map_id

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = μ.join
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
x y : PiNatEmbed X Y f
hxy : x.ofPiNat = y.ofPiNat
⊢ x = y

Tactic:
by
  cases x; congr!

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
⊢ S.Nonempty

pp: case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

pp: case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement S univ

Tactic:
· obtain ⟨a, _⟩ := h.2 1
    exact ⟨a.1.1, a.1.2⟩

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S univ
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement S univ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)

pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H) (↑h * g) g

Tactic:
· ext
    · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]
    · rw [this]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H) (↑h * g) g
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSpace H
inst✝² : Inv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : SFinite μ
⊢ SFinite μ.inv

Tactic:
rw [Measure.inv]; infer_instance

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
⊢ μ.inv.IsMulLeftInvariant

Tactic:
by
  constructor
  intro g
  conv_rhs => rw [← map_mul_right_eq_self μ g⁻¹]
  simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
rcases eq_or_ne (μ s) 0 with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

case inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ μ K + ν K' ≤ (μ + ν) (K ∪ K')

Tactic:
simp only [Measure.coe_add, Pi.add_apply]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ μ K + ν K' ≤ μ (K ∪ K') + ν (K ∪ K')
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
⊢ μ.withDensity (r • f) = r • μ.withDensity f

Tactic:
refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.coe_smul, Pi.smul_apply, withDensity_apply _ hs,
    smul_eq_mul, ← lintegral_const_mul' r f hr]
  simp only [Pi.smul_apply, smul_eq_mul]

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

Goal state before:
pp: case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
rw [ae_restrict_iff' A]

Goal state after:
case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0} → (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ 0 ≤ 1 + x / 2

Tactic:
by linarith

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 : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ

Tactic:
rw [lintegral_const_mul']

Goal state after:
case hr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 2 ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_const_mul']

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

case hr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_const_mul']

Goal state after:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

case hr
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ‖c‖ₑ ≠ ∞
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: n : ℕ
| I ^ n

Tactic:
rw [← Nat.div_add_mod n 4]

Goal state after:
n : ℕ
| I ^ (4 * (n / 4) + n % 4)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℂ
⊢ normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
by
  rw [sub_eq_add_neg, normSq_add]
  simp only [map_neg, mul_neg, neg_re, normSq_neg]
  ring

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
this : c • μ = c • 1 • μ
⊢ SFinite ((c • 1) • μ)

Tactic:
← withDensity_const

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
this : c • μ = c • 1 • μ
⊢ SFinite (μ.withDensity fun x ↦ c • 1)
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 φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

Tactic:
refine lintegral_congr (fun x ↦ ?_)

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 * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
refine lintegral_congr (fun x ↦ ?_)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
exact expect_le hs h

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

Goal state before:
pp: ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖1‖₊ = 1 ^ n

Tactic:
nnnorm_one,

Goal state after:
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ 1 = 1 ^ n