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

Goal state before:
pp: case left.hV
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
⊢ ∀ (i : ↑↑K), {p | edist (p.1 ↑i) (p.2 ↑i) < δ} ∈ ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 ↑i) (a.2 ↑i) < i_1}

pp: case left.hU
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
⊢ ⋂ i, {p | edist (p.1 ↑i) (p.2 ↑i) < δ} ⊆ {p | edist p.1 p.2 < ε}

Tactic:
· rintro ⟨i, hi⟩
        refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
        simp only [mem_principal, Subset.rfl]

Goal state after:
case left.hU
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
⊢ ⋂ i, {p | edist (p.1 ↑i) (p.2 ↑i) < δ} ⊆ {p | edist p.1 p.2 < ε}
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
⊢ (m.bind fun x ↦ 0) = 0

Tactic:
by simp

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

Goal state before:
pp: case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
have : L / c < μ s := by
      rwa [ENNReal.div_lt_iff, mul_comm]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]

Goal state after:
case const
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i j : ι
x✝ : j ≠ i
⊢ 0 ≤ 2⁻¹ ^ encode j

Tactic:
by simp

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

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
⊢ ∀ (x y : (i : ι) → F i), 0 ≤ dist x y

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : ε ∈ Ioi 0
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
⊢ ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)

Tactic:
t

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
this : ∀ (n : ℕ), ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
n : ℕ
hn : K < 2 ^ n
ε : ℝ
hε₀ : ε ∈ Ioi 0
hε : ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
x : α
t : ℝ
⊢ t ≤ K → μ (closedBall x (t * ε)) ≤ ↑(C ^ n) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝ : NullSingletonClass μ
x : α
y : β
⊢ μ {x} * ν {y} = 0

Tactic:
by simp

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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝ : NullSingletonClass ν
x : α
y : β
⊢ μ {x} * ν {y} = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Dynamics.Minimal

Goal state before:
pp: case mp
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
a✝ : IsMinimal M α
s✝ : Set α
⊢ IsClosed s✝ → (∀ (c : M), c • s✝ ⊆ s✝) → s✝ = ∅ ∨ s✝ = univ

Tactic:
exact eq_empty_or_univ_of_smul_invariant_closed M

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous[_, inst✝³] f ∧ range f = t
h : Disjoint ∅ t
⊢ Disjoint t ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst✝³] f
h : Disjoint (range f) ∅
⊢ Disjoint ∅ univ

Tactic:
by simp

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

Goal state before:
pp: γ : 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 γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
p : A
⊢ ∃ q, f '' ↑(↑p).1 ⊆ q ∧ Disjoint (f '' ↑(↑p).2) q ∧ MeasurableSet q

Tactic:
apply
      AnalyticSet.measurablySeparable ((hb.isOpen p.1.1.2).analyticSet_image f_cont)
        ((hb.isOpen p.1.2.2).analyticSet_image f_cont)

Goal state after:
γ : 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) := ⋯
p : A
⊢ Disjoint (f '' ↑(↑p).1) (f '' ↑(↑p).2)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
| μ.prod ν

Tactic:
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
| (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
⊢ μ ∅ = ν ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s ↦ (↑s)⁻¹ * g ∈ T) y → y = x
⊢ (fun x ↦ ↑x.1 * ↑x.2 = g) (x, ⟨(↑x)⁻¹ * g, hx⟩)

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t ↦ g * (↑t)⁻¹ ∈ S) y → y = x
⊢ (fun x ↦ ↑x.1 * ↑x.2 = g) (⟨g * (↑x)⁻¹, hx⟩, x)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ μ ∅ = ν ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
⊢ generateFrom {s | MeasurableSet s} = mα

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
⊢ ∀ (t : Set α),
    MeasurableSet s →
      MeasurableSet t →
        (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) =
          (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
t

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
⊢ MeasurableSet s →
    MeasurableSet t →
      (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) =
        (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ t, ∃ U ⊇ t, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ t ≤ μ F + ε ∧ μ U ≤ μ t + ε) →
        ∀ (ε : ℝ≥0∞),
          ε ≠ 0 → ∃ F ⊆ tᶜ, ∃ U ⊇ tᶜ, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ tᶜ ≤ μ F + ε ∧ μ U ≤ μ tᶜ + ε

Tactic:
rintro s hs H ε hε
    rcases H ε hε with ⟨F, hFs, U, hsU, hFc, hUo, hF, hU⟩
    refine
      ⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl,
        hFc.isOpen_compl, ?_⟩
    simp only [measure_compl_le_add_iff, *, hUo.measurableSet, hFc.measurableSet, true_and]

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
y : G
hy : y ∈ (fun x ↦ g * x) ⁻¹' s
⊢ f (g * y) = (fun x ↦ f g * x) (f y)

Tactic:
by simp

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ this.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ borel α = borel α

Tactic:
borel_eq_borel_of_le ht _ hle

Goal state after:
α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ this.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ borel α = borel α

α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ this.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed[t] s ∧ IsOpen[t] s
⊢ PolishSpace α
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∞
h : μ s = 0
hr : r < ν s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ν K
⊢ ν K ≤ (μ + ν) K

Tactic:
by simp

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∞
h : μ s ≠ 0
h' : ν s = 0
hr : r < μ s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < μ K
⊢ μ K ≤ (μ + ν) K

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ∅, f a ∂μ = 0

Tactic:
by simp

Goal state after:
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 β
inst✝ : μ.Regular
f : α ≃ₜ β
this : (map (⇑f) μ).OuterRegular
⊢ (map (⇑f) μ).Regular

Tactic:
have := IsFiniteMeasureOnCompacts.map μ f

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
this✝ : (map (⇑f) μ).OuterRegular
this : IsFiniteMeasureOnCompacts (map (⇑f) μ)
⊢ (map (⇑f) μ).Regular
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
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n)⁻¹ < edist (f k x) (g x)
⊢ (↑n)⁻¹ > 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
⊢ ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0

Tactic:
by simp

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 : α → β
⊢ ∫⁻ (a : α), ‖(-f) a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
by simp

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

Goal state before:
pp: ⊢ sqrt 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ sqrt 1 = 1

Tactic:
by simp

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

Goal state before:
pp: a : ℕ
⊢ 0 ≤ ↑a

Tactic:
by simp

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

Goal state before:
pp: case inr
α : 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:
apply le_of_eq _

Goal state after:
α : 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
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℝ
⊢ z = w → ↑z = ↑w

Tactic:
by apply congrArg

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

Goal state before:
pp: ⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ (z * I).re = -z.im

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ (z * I).im = z.re

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = -z.im

Tactic:
by simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).im = z.re

Tactic:
by simp

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

Goal state before:
pp: ⊢ ∀ (x y : ℂ), equivRealProd.toFun (x + y) = equivRealProd.toFun x + equivRealProd.toFun y

Tactic:
by simp

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
⊢ μ ≪ μ.withDensity f

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)
  rw [withDensity_apply _ hs, lintegral_eq_zero_iff' hf.restrict,
    ae_eq_restrict_iff_indicator_ae_eq hs, Set.indicator_zero', Filter.EventuallyEq, ae_iff] at hμs
  simp only [ae_iff, ne_eq, not_not] at hf_ne_zero
  simp only [Pi.zero_apply, Set.indicator_apply_eq_zero, not_forall, exists_prop] at hμs
  have hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0} :=
    fun x hx ↦ or_iff_not_imp_right.mpr <| fun hnx ↦ ⟨hx, hnx⟩
  exact measure_mono_null hle <| nonpos_iff_eq_zero.1 <| le_trans (measure_union_le _ _)
    <| hμs.symm ▸ zero_add _ |>.symm ▸ hf_ne_zero.le

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

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
by simp

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

Goal state before:
pp: n : ℤ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
by simp

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

Goal state before:
pp: r : ℝ
⊢ ((starRingEnd ℂ) ↑r).re = (↑r).re ∧ ((starRingEnd ℂ) ↑r).im = (↑r).im

Tactic:
by simp

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

Goal state before:
pp: ⊢ ((starRingEnd ℂ) I).re = (-I).re ∧ ((starRingEnd ℂ) I).im = (-I).im

Tactic:
by simp

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

Goal state before:
pp: ⊢ (starRingEnd ℂ) (-I) = I

Tactic:
by simp

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

Goal state before:
pp: ⊢ re 0 * re 0 + im 0 * im 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ normSq 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ normSq 1 = 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ (-1) ^ 2 = 1

Tactic:
neg_one_sq

Goal state after:
⊢ 1 = 1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ normSq z⁻¹ = (normSq z)⁻¹

Tactic:
by simp

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

Goal state before:
pp: z w : ℂ
⊢ normSq (z / w) = normSq z / normSq w

Tactic:
by simp

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

Goal state before:
pp: a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ (fun x_1 ↦ ↑x_1 + ↑(equivRealProd x).2 * I) x.re = x

Tactic:
by simp

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

Goal state before:
pp: b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ (fun y ↦ ↑x.re + ↑y * I) x.im = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (a b : M), True → True → True

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ i ∈ s, True

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (a b : M), True → True → True

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ i ∈ s, True

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : StarAddMonoid A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousStar A
inst✝ : TrivialStar R
r : R
a : A
⊢ (AddEquiv.refl A).toFun (r • a) = (starRingEnd R) r • (AddEquiv.refl A).toFun a

Tactic:
by simp

Goal state after: