mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
⊢ ∀ (p : A), ∃ q, (↑q).1 = (↑p).1 + 1 ∧ (↑q).2.1 ∈ cylinder (↑p).2.1 (↑p).1 ∧ (↑q).2.2 ∈ cylinder (↑p).2.2 (↑p).1

Tactic:
rintro ⟨⟨n, x, y⟩, hp⟩

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
n : ℕ
x y : ℕ → ℕ
hp : ¬MeasurablySeparable (f '' cylinder (n, x, y).2.1 (n, x, y).1) (g '' cylinder (n, x, y).2.2 (n, x, y).1)
⊢ ∃ q,
    (↑q).1 = (↑⟨(n, x, y), hp⟩).1 + 1 ∧
      (↑q).2.1 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.1 (↑⟨(n, x, y), hp⟩).1 ∧
        (↑q).2.2 ∈ cylinder (↑⟨(n, x, y), hp⟩).2.2 (↑⟨(n, x, y), hp⟩).1
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : 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)
i : ℕ
⊢ AEMeasurable (fun a ↦ a (f i)) m

Tactic:
exact (measurable_coe (hf i)).aemeasurable

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
⊢ ∫⁻ (a : α) in s, min (f a) ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Tactic:
have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) ↑n ∂μ ≠ ∞
⊢ ∫⁻ (a : α) in s, min (f a) ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
x y z : (i : ι) → F i
⊢ ∑' (i : ι), min (2⁻¹ ^ encode i) (edist (x i) (z i)) ≤
    ∑' (i : ι), (min (2⁻¹ ^ encode i) (edist (x i) (y i)) + min (2⁻¹ ^ encode i) (edist (y i) (z i)))

Tactic:
by
      gcongr with n; grw [edist_triangle _ (y n), min_add_distrib, min_le_right]

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

Goal state before:
pp: case hd
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
this : ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
x✝ : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) S

Tactic:
exact directed_of_isDirected_le hS_mono

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 ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
by
  simp_rw [Measure.prod, bind_apply hs (Measurable.map_prodMk_left (ν := ν)).aemeasurable,
    map_apply measurable_prodMk_left 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 β
inst✝ : SFinite ν
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
hs : μ s ≠ 0
⊢ NullMeasurableSet t ν

Tactic:
rcases h with ⟨u, hum, hu⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᵐ[μ.prod ν] u
⊢ NullMeasurableSet t ν
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U = 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
refine ⟨∅, empty_subset _, h0, ?_⟩

Goal state after:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
h₀ : μ U = 0
⊢ μ U < μ ∅ + ε
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ T, IsComplement (↑H) T ∧ g ∈ T

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩
  by_cases hq : q = Quotient.mk'' g
  · exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
  · simp [Function.update, dif_neg hq, q.out_eq']

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
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:
· simp [RightCosetEquivalence, ← smul_smul]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ ((↑(hS.toLeftFun g))⁻¹ * g)⁻¹ = g⁻¹ * ↑(hS.toLeftFun g)

Tactic:
rw [mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ (g * (↑(hT.toRightFun g))⁻¹)⁻¹ = ↑(hT.toRightFun g) * g⁻¹

Tactic:
rw [mul_inv_rev, inv_inv]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
⊢ IsComplement (f • ↑T) ↑H

Tactic:
refine isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_

Goal state after:
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
⊢ ∃! s, (↑s)⁻¹ * g ∈ ↑H
Module: Mathlib.GroupTheory.Complement

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

Tactic:
specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])

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

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

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

Tactic:
mul_assoc (↑h) (↑h') g

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

Goal state before:
pp: case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
h_eq ν hs ht hu

Goal state after:
case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)

Tactic:
h_eq ν hs ht hu

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
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 γ := ⋯
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 β := ⋯
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := ⋯
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
⊢ ↑(s n) ⊆ ball z δ

Tactic:
intro a ha

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 γ := 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 }
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 β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
δ : ℝ
δpos : δ > 0
hδ : ball z δ ⊆ f ⁻¹' v
n : ℕ
hn : u n + dist (y n) z < δ
a : γ
ha : a ∈ ↑(s n)
⊢ a ∈ ball z δ
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 μ
ν' : Measure β
inst✝ : SFinite ν'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ (sfiniteSeq μ i.1) s * (sfiniteSeq ν i.2) t + (sfiniteSeq μ i.1) s * (sfiniteSeq ν' i.2) t =
    (sfiniteSeq μ i.1) s * ((sfiniteSeq ν i.2) t + (sfiniteSeq ν' i.2) t)

Tactic:
left_distrib

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

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

Tactic:
have ε0' : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'

Goal state after:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
⊢ ∃ F ⊆ ⋃ i, s i,
    ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε
Module: Mathlib.MeasureTheory.Measure.Prod

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

Tactic:
rw [Measure.fst, Measure.map_map measurable_fst measurable_swap]
  rfl

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 μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s = 0

Tactic:
rw [← inv_inv s]

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
hs : μ s⁻¹ = 0
⊢ μ s⁻¹⁻¹ = 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
⊢ μ (s * closure[inst✝³] {1}) = μ s

Tactic:
by
  apply le_antisymm ?_ (measure_mono (subset_mul_closure_one s))
  conv_rhs => rw [measure_eq_iInf]
  simp only [le_iInf_iff]
  intro t kt t_meas
  apply measure_mono
  rw [← t_meas.mul_closure_one_eq]
  exact smul_subset_smul_right kt

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

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ (map (⇑f) μ) K < ∞

Tactic:
← hK.measure_closure,

Goal state after:
G : Type u_1
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : Group G
inst✝⁸ : TopologicalSpace G
μ : Measure G
inst✝⁷ : μ.IsHaarMeasure
inst✝⁶ : BorelSpace G
inst✝⁵ : ContinuousMul G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : MeasurableSpace H
inst✝¹ : BorelSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁸, inst✝³] ⇑f
h_surj : Surjective ⇑f
h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ (map (⇑f) μ) (closure[inst✝³] K) < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ μ ({x | f x ≠ 0} ∩ s) = 0 → (μ.withDensity f) s = 0

Tactic:
· intro hs
    let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)
    have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_ofPred_eq, or_true]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
    apply measure_mono_null A (measure_union_null _ _)
    · apply withDensity_absolutelyContinuous
      rwa [measure_toMeasurable]
    rcases hf with ⟨g, hg, hfg⟩
    have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      rw [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
    rw [measure_congr t, withDensity_congr_ae hfg]
    have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
    rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
    filter_upwards [ae_restrict_mem M]
    simp only [imp_self, Pi.zero_apply, imp_true_iff]

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ae μ' ≤ ae ν'

Tactic:
refine (absolutelyContinuous_of_isMulLeftInvariant μ' ν' ?_).ae_le

Goal state after:
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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ν' ≠ 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

Tactic:
by
  simpa [hasFiniteIntegral_iff_enorm, lt_top_iff_ne_top, ENNReal.mul_eq_top,
    or_iff_not_imp_left, isFiniteMeasure_iff] using fun h h' ↦ (hc h').elim

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ √x

Tactic:
unfold sqrt
  exact NNReal.coe_nonneg _

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

Goal state before:
pp: ⊢ √0 = 0

Tactic:
simp [Real.sqrt]

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

Goal state before:
pp: ⊢ √1 = 1

Tactic:
simp [Real.sqrt]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ NNReal.sqrt (x.toNNReal * y.toNNReal) = NNReal.sqrt x.toNNReal * NNReal.sqrt y.toNNReal

Tactic:
NNReal.sqrt_mul

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

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2)

Tactic:
by
      gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]

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

Goal state before:
pp: r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = 0

Tactic:
← (Complex.le_def.1 hz).2,

Goal state after:
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ (↑r).im = 0