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

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
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 ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ∞

Tactic:
filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
rw [Measure.sigmaFiniteSet]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT μ))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  have hF'_le : F ≤ᵐ[μ] F' := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact ge_of_tendsto' h_tendsto (fun m ↦ h_le _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ by
    refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm
    exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
by_cases x = y <;> by_cases x = z <;> by_cases y = z <;> simp_all

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

Goal state before:
pp: E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : E n
i : ℕ
hi : i < n
⊢ update x n y i = x i

Tactic:
by simp [hi.ne]

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

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ BoundedSpace ((n : ℕ) → E n)

Tactic:
by
  rw [Metric.boundedSpace_iff]
  use 1
  apply PiNat.dist_le_one

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

Goal state before:
pp: case hfh.true
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
n : ℕ
hm : n.succ ≠ 0
⊢ ediam (D (true :: PiNat.res x n)) ≤ u (n + 1)

Tactic:
convert! (h1 _ _ _).2.2.2

Goal state after:
case e'_4
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
x : ℕ → Bool
n : ℕ
hm : n.succ ≠ 0
⊢ n = (PiNat.res x n).length
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
p : α → Prop
f : β → α
⊢ ∀ (a : α), a ∈ range ⇑MeasurableEquiv.ulift

Tactic:
simp [Function.Surjective.range_eq <| EquivLike.surjective _]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
| (1 / 2) ^ n = 2 * ↑((1 / 2) ^ (n + 1))

Tactic:
enter [1, 1]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
| 1 / 2
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
A : ∀ (n : ι), ∃ x, f n x = y
⊢ y ∈ range F

Tactic:
choose x hx using A

Goal state after:
case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := fun x ↦ f i₀ (↑x i₀)
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ y ∈ range F
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

Tactic:
rintro f g - hf - h2f h2g

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν
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
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ 1 * 1 = 1

Tactic:
mul_one

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
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ 1 = 1
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
a : ↑S × ↑univ
h✝ : (fun x ↦ ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Tactic:
exact ⟨a.1.1, a.1.2⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

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

Tactic:
rw [equiv_fst_eq_mul_inv]

Goal state after:
case mpr.py₁
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (g₁ * (↑(hSK.equiv g₁).2)⁻¹)⁻¹ * g₁ ∈ ↑K
Module: Mathlib.GroupTheory.Complement

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

Tactic:
rw [equiv_fst_eq_mul_inv]

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (g₂ * (↑(hSK.equiv g₂).2)⁻¹)⁻¹ * g₁ * (g₁⁻¹ * g₂) ∈ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1

Tactic:
rw [equiv_fst_eq_mul_inv]

Goal state after:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g (g * (↑(hSK.equiv g).2)⁻¹)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
⊢ hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)

Tactic:
have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst :=
    hSK.equiv_fst_eq_iff_leftCosetEquivalence.2
      (by simp [LeftCosetEquivalence, leftCoset_eq_iff])

Goal state after:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
γ : 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 γ
⊢ x ∈ range f

Tactic:
let z := limUnder atTop y

Goal state after:
case h₂
γ : 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
⊢ x ∈ range f
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
⊢ ?m.15 ∈ cocompact ?m.13

Tactic:
by
        simpa only [preimage_image_preimage, preimage_compl] using
          mem_map.mp
            (cocompact_tendsto f <|
              mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ t.indicator (fun x ↦ (sfiniteSeq μ i) s) y = t.indicator (fun j ↦ (sfiniteSeq μ i) s * 1) y

Tactic:
mul_one

Goal state after:
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ᶜ + ε

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 ≠ ∞
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ) (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ f i, ∃ U ⊇ f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (f i) ≤ μ F + ε ∧ μ U ≤ μ (f i) + ε) →
          ∀ (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ ⋃ i, f i,
                ∃ U ⊇ ⋃ i, f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, f i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, f i) + ε

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:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ) (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ f i, ∃ U ⊇ f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (f i) ≤ μ F + ε ∧ μ U ≤ μ (f i) + ε) →
          ∀ (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ ⋃ i, f i,
                ∃ U ⊇ ⋃ i, f i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, f i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, f i) + ε
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsInvInvariant
A : Set G
⊢ μ.inv A = μ A

Tactic:
inv_eq_self

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsInvInvariant
A : Set G
⊢ μ A = μ A
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ μ s * 1 = μ s

Tactic:
mul_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ μ s = μ s
Module: Mathlib.MeasureTheory.Measure.Regular

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

Tactic:
← measure_univ_eq_zero,

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : R1Space α
inst✝ : BorelSpace α
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hK : IsCompact K
hμK : μ A < μ K + ε
⊢ μ A < μ (closure[inst✝³] K) + ε

Tactic:
by rwa [hK.measure_closure]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity f = 0 ↔ f =ᵐ[μ] 0

Tactic:
← measure_univ_eq_zero,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) univ = 0 ↔ f =ᵐ[μ] 0
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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s) * 1) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
mul_one

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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Regular

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

Tactic:
← measure_univ_eq_zero,

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEMeasurable (fun x ↦ ↑(f x) * g x) μ

Tactic:
rcases t with ⟨f', hf'_m, hf'_ae⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEMeasurable (fun x ↦ ↑(f x) * g x) μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ x = 1 * 1 ↔ x = 1

Tactic:
mul_one

Goal state after:
x : ℝ
⊢ x = 1 ↔ x = 1
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ 1 * 1 = x ↔ x = 1

Tactic:
by rw [eq_comm, mul_one]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1 by
    refine (withDensity_mono this).trans ?_
    rw [withDensity_one]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ ↑(#s) • a

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ #s • a
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ ↑(#s) • a ≤ ∑ i ∈ s, (fun i ↦ f i) i

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun i ↦ f i) i
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

Goal state after: