mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
· have h := hg.ae_eq_mk
    rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at h
    rw [ae_restrict_iff' hs.compl]
    filter_upwards [h] with x hx
    intro hx_mem
    rw [Set.mem_compl_iff] at hx_mem
    simp only [hx_mem, not_false_eq_true, Set.piecewise_eq_of_notMem, hx hx_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a

Tactic:
refine fun a =>
      le_antisymm (le_iInf fun n => iInf_le _ _)
        (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f (Directed.sequence f h_directed (Encodable.encode b + 1)) a ≤ f b a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddCancelMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n ↦ (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x ↦ (φ n) x + g x) atTop (𝓝 (f + g))
n : ℕ
⊢ Measurable fun x ↦ (φ n) x + g x

Tactic:
exact hg.simpleFunc_add _

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ Measurable f ∧ IsSeparable (range f)

Tactic:
refine ⟨hf.measurable, ?_⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst✝³, inst✝¹] f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (range f)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ 1 / ↑n
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Tactic:
· refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩
    rw [tsub_eq_zero_of_le hC_lt]
    exact zero_le

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ∞ = 0

Tactic:
← h h0,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ μ (μ.sigmaFiniteSetWRT ν)ᶜ = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
⊢ Measurable (uncurry u)

Tactic:
refine measurable_of_tendsto_metrizable (fun n => ?_) h_tendsto

Goal state after:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
⊢ Measurable (U n)
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
⊢ N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
hn

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
⊢ N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N
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 ∂μ
⊢ Tendsto (fun i ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
Int_eq

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∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
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 ∂μ
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: t : ↑I
⊢ ↑t + 1 / 2 ≤ 1 ↔ ↑t ≤ 1 / 2

Tactic:
← le_sub_iff_add_le,

Goal state after:
t : ↑I
⊢ ↑t ≤ 1 - 1 / 2 ↔ ↑t ≤ 1 / 2
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 : X
z : Y
⊢ glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inr z).swap ≤
    glueDist Ψ Φ ε (Sum.inr x).swap (Sum.inl y).swap + glueDist Ψ Φ ε (Sum.inl y).swap (Sum.inr z).swap

Tactic:
apply glueDist_triangle_inl_inr_inl

Goal state after:
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 : X
z : Y
⊢ ∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

Tactic:
· by_cases ht : (t : ℝ) = 1
    · simp [ht]
    · have : (1 - s * t : ℝ) ≠ 0 := by
        intro h
        have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
        grind
      field_simp
      ring_nf

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ¬↑z - ↑x = 0
⊢ ↑y = (1 - (↑y - ↑x) / (↑z - ↑x)) * ↑x + (↑y - ↑x) / (↑z - ↑x) * ↑z

Tactic:
· field_simp
    ring_nf

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

Goal state before:
pp: case inr.inr.inr
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simp only [dist_eq_of_ne, hxz, hxy, hyz, inv_le_inv₀, one_div, inv_pow, zero_lt_two, Ne,
    not_false_iff, le_max_iff, pow_le_pow_iff_right₀, one_lt_two, pow_pos,
    min_le_iff.1 (min_firstDiff_le x y z hxz)]

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

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

Tactic:
convert! Metric.ediam_eball_le (x := x)

Goal state after:
case e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ε = 2 * (ε / 2)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
i n : ℕ
⊢ n ∈ Ici i → u i i = u n i

Tactic:
hn

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
i n : ℕ
hn : n ∈ Ici i
⊢ u i i = u n i
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SFinite μa
⊢ SFinite μb

Tactic:
by
  rw [← hf.map_eq]
  infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
⊢ μa (f ⁻¹' s) = μb s

Tactic:
rw [← hf.map_eq] at hs ⊢
  rw [map_apply₀ hf.1.aemeasurable hs]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ μ sᶜ = 1 ↔ μ s = 0

Tactic:
by
  rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous[w✝¹, inst✝²] g
hs : AnalyticSet (range g)
⊢ AnalyticSet (f ⁻¹' range g)

Tactic:
have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'

Goal state after:
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous[w✝¹, inst✝²] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
⊢ dist (g x) (g y) ≤ 4 * (1 / 2) ^ firstDiff ↑x ↑y

Tactic:
hn

Goal state after:
case inr
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
diff_pos : 0 < firstDiff ↑x ↑y
hn : firstDiff ↑x ↑y = n + 1
⊢ dist (g x) (g y) ≤ 4 * (1 / 2) ^ (n + 1)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ ∫⁻ (x : α) in s, c ∂μ < ∞

Tactic:
lintegral_const

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c * (μ.restrict s) univ < ∞
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a ↦ (μ a) s
h_univ : Measurable fun a ↦ (μ a) univ
s : Set β
f : ℕ → Set β
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun b ↦ (μ b) (f i)
⊢ Measurable fun b ↦ (μ b) (⋃ i, f i)

Tactic:
| iUnion f hfd hfm ihf =>

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (sum m).join s = (sum fun i ↦ (m i).join) s

Tactic:
simp_rw [sum_apply _ hs, join_apply hs, lintegral_sum_measure]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε

Tactic:
set s : ℕ → Set α := disjointed (spanningSets μ)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
⊢ ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), μ s ∂map (map f) μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ

Tactic:
lintegral_map (measurable_coe hs) (measurable_map f hf)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ
⊢ L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ

Tactic:
rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]

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

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed[inst✝³] F
⊢ μ F = 1 ↔ F = univ

Tactic:
rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]

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

Goal state before:
pp: case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < 2⁻¹ ^ encode i
x y : (i : ι) → F i
⊢ edist x y < 2⁻¹ ^ encode i → edist x y < ε → edist (x i) (y i) < ε

Tactic:
hn

Goal state after:
case right
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
i : ι
ε : ℝ≥0∞
hε₀ : 0 < ε
this : 0 < 2⁻¹ ^ encode i
x y : (i : ι) → F i
hn : edist x y < 2⁻¹ ^ encode i
⊢ edist x y < ε → edist (x i) (y i) < ε
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)

Tactic:
| iUnion f hfd hfm ihf =>

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 ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν
this : ∀ (x : α), Monotone fun n y ↦ f n (x, y)
x : α
| ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν

Tactic:
lintegral_iSup (fun n => (hf n).comp m) (this x)

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν
this : ∀ (x : α), Monotone fun n y ↦ f n (x, y)
x : α
| ⨆ n, ∫⁻ (a : β), (f n ∘ Prod.mk x) a ∂ν
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 β
⊢ (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

Tactic:
simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]

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

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

Tactic:
by
  simp_rw [prod_sum_left, prod_sum_right, sum_sum]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
⊢ H' = map H.subtype H''

Tactic:
simp [H'', h]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H

Tactic:
have : H.subtype '' (S * H'') = H.subtype '' S * H''.map H.subtype := image_mul H.subtype

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
this : ⇑H.subtype '' (S * ↑H'') = ⇑H.subtype '' S * ↑(map H.subtype H'')
⊢ ⇑H.subtype '' S * ↑(map H.subtype H'') = ↑H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H

Tactic:
have : Nat.card H'' * Nat.card S = Nat.card H := cmem.card_mul_card

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite ↑T ↔ H.FiniteIndex

Tactic:
← h.rightQuotientEquiv.finite_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (Quotient (QuotientGroup.rightRel H)) ↔ H.FiniteIndex