mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

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

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
C : Set α
inst✝² : T1Space α
inst✝¹ : ConnectedSpace α
inst✝ : Nontrivial α
⊢ Nontrivial α

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊔ g) μ

Tactic:
refine
    ⟨fun n => hf.approx n ⊔ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩
  refine (measure_mono (support_sup _ _)).trans_lt ?_
  exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ C = V ∩ C ∪ D

Tactic:
· rw [inter_comm, inter_union_sdiff]

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

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

Tactic:
· filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ CompactSpace ↑I

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ 1 - ↑x ≤ 1

Tactic:
simpa using x.2.1

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mp.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t * a ≤ 1

Tactic:
mul_comm

Goal state after:
case mp.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ a * t ≤ 1
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case mpr.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t * a ≤ 1
⊢ a * t ≤ 1

Tactic:
mul_comm

Goal state after:
case mpr.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : a * t ≤ 1
⊢ a * t ≤ 1
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ Subtype.val ⁻¹' Ioi ↑x = Ioc x 1

Tactic:
by
  rw [preimage_subtype_val_Ioi]
  exact Ioc_top.symm

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b

Tactic:
obtain ⟨m, hm⟩ := Archimedean.arch (b - a) hδ

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ False

Tactic:
refine apply_firstDiff_ne h ?_

Goal state after:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ x (firstDiff x z) = z (firstDiff x z)
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

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

Tactic:
infer_instance

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), IsCompletelyPseudoMetrizableSpace (X i)
this : (i : ι) → UpgradedIsCompletelyPseudoMetrizableSpace (X i) := fun i ↦ upgradeIsCompletelyPseudoMetrizable (X i)
⊢ IsCompletelyPseudoMetrizableSpace ((i : ι) → X i)

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyPseudoMetrizableSpace Y := upgradeIsCompletelyPseudoMetrizable Y
this✝ : PseudoMetricSpace X := ⋯.comapPseudoMetricSpace
this : CompleteSpace X
⊢ TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

Tactic:
let := upgradeIsCompletelyPseudoMetrizable Y
  let : PseudoMetricSpace X := hf.isEmbedding.comapPseudoMetricSpace
  have : CompleteSpace X := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
  infer_instance

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : IsCompletelyPseudoMetrizableSpace X
inst✝ : T0Space X
this : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ CompleteSpace X

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyMetrizableSpace X
this : UpgradedIsCompletelyMetrizableSpace X := upgradeIsCompletelyMetrizable X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
infer_instance

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), IsCompletelyMetrizableSpace (X i)
this : (i : ι) → UpgradedIsCompletelyMetrizableSpace (X i) := fun i ↦ upgradeIsCompletelyMetrizable (X i)
⊢ IsCompletelyMetrizableSpace ((i : ι) → X i)

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace.IsCompletelyMetrizableSpace Y
f : X → Y
hf : IsClosedEmbedding f
this✝¹ : UpgradedIsCompletelyMetrizableSpace Y := upgradeIsCompletelyMetrizable Y
this✝ : MetricSpace X := IsEmbedding.comapMetricSpace f ⋯
this : CompleteSpace X
⊢ TopologicalSpace.IsCompletelyMetrizableSpace X

Tactic:
infer_instance

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 p q

Tactic:
by
  cases p <;> cases q <;> first | rfl | simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝² : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this✝¹ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this✝ : SecondCountableTopology α
this : CompleteSpace α
⊢ PolishSpace α

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
u : ι → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), (fun i ↦ (u i).toTopologicalSpace) i ≤ t₀
hut : ∀ (i : ι), (u i).toTopologicalSpace = (fun i ↦ (u i).toTopologicalSpace) i
⊢ (⨅ i, 𝓤 α).IsCountablyGenerated

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : u.toTopologicalSpace = ⨅ i, t i
this✝¹ : SecondCountableTopology α
this✝ : TopologicalSpace α := t i₀
this : PolishSpace α
⊢ T1Space α

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : u.toTopologicalSpace = ⨅ i, t i
this✝ : SecondCountableTopology α
this : T1Space α
⊢ PolishSpace α

Tactic:
infer_instance

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

Goal state before:
pp: case refine_4.refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ t ∈ 𝓝 x

Tactic:
simp only [dist_eq, one_div] at hε

Goal state after:
case refine_4.refine_2
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist ↑x ↑y + |(infDist (↑x) (↑s)ᶜ)⁻¹ - (infDist (↑y) (↑s)ᶜ)⁻¹| < ε → y ∈ t
⊢ t ∈ 𝓝 x
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mpr.inr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff x y)

Tactic:
rw [firstDiff_comm]

Goal state after:
case mpr.inr
E : ℕ → Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : ((n : ℕ) → E n) → α
H : ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
x y : (n : ℕ) → E n
hne : x ≠ y
⊢ y ∈ cylinder x (firstDiff y x)
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 (map f μa)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : StandardBorelSpace α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ MeasurableEq α

Tactic:
infer_instance

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

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
have A : (s ∩ cylinder x (longestPrefix x s)).Nonempty :=
          inter_cylinder_longestPrefix_nonempty hs hne x

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : p
⊢ IsProbabilityMeasure (μ h✝)

Tactic:
infer_instance

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

Goal state before:
pp: case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst✝¹ : ∀ (h : p), IsProbabilityMeasure (μ h)
inst✝ : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h✝ : ¬p
⊢ IsProbabilityMeasure (ν h✝)

Tactic:
infer_instance

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

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : p
⊢ IsProbabilityMeasure μ

Tactic:
infer_instance

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

Goal state before:
pp: case isFalse
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ✝ : Measure α
s : Set α
p : Prop
inst✝² : Decidable p
μ ν : Measure α
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h✝ : ¬p
⊢ IsProbabilityMeasure ν

Tactic:
infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
⊢ IsZeroOrProbabilityMeasure 0

Tactic:
infer_instance

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h✝ : NeZero μ
h : μ univ = ∞
⊢ IsZeroOrProbabilityMeasure 0

Tactic:
infer_instance

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
h✝ : NeZero μ
h : μ univ < ∞
this : IsFiniteMeasure μ
⊢ IsZeroOrProbabilityMeasure ((μ univ)⁻¹ • μ)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
by_cases hsc : c ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
⊢ count s = ∞

Tactic:
refine top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑n ≤ count s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgle : g ≤ f
hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
· exact ⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
⊢ ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε

Tactic:
have hN_meas : Measurable N := measurableSet_spanningSetsIndex μ

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
s : ℕ → Set α := disjointed (spanningSets μ)
this : ∀ (n : ℕ), μ (s n) < ∞
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
δsum : ∑' (i : ℕ), μ (s i) * ↑(δ i) < ε
N : α → ℕ := spanningSetsIndex μ
hN_meas : Measurable N
⊢ ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : 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
⊢ L < μ s * ↑c

pp: case h0
α : 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
⊢ ↑c ≠ 0 ∨ L ≠ 0

pp: case ht
α : 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
⊢ ↑c ≠ ∞ ∨ L ≠ ∞

Tactic:
mul_comm

Goal state after:
α : 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
⊢ L < ↑c * μ s

case h0
α : 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
⊢ ↑c ≠ 0 ∨ L ≠ 0

case ht
α : 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
⊢ ↑c ≠ ∞ ∨ L ≠ ∞
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → EMetricSpace (F i)
⊢ ∀ {x y : (i : ι) → F i}, edist x y = 0 → x = y

Tactic:
by simp [edist_eq_tsum, funext_iff]

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
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous[inst✝⁵, inst✝²] f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen[inst✝²] U
hUne : U.Nonempty
⊢ μ (f ⁻¹' U) ≠ 0

Tactic:
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ν T * μ (toMeasurable μ s) = μ (toMeasurable μ s) * ν T

Tactic:
mul_comm

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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x | ν t ≤ f x}
hss' : s ⊆ s'
⊢ μ s' * ν t = ν t * μ s'

Tactic:
mul_comm

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun x ↦ ν (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x | ν t ≤ f x}
hss' : s ⊆ s'
⊢ ν t * μ s' = ν t * μ s'
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 ν
this : μ.prod ν = sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (sum fun p ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₁).2)⁻¹ ∈ ↑H

pp: case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₂).2)⁻¹ ∈ ↑H

Tactic:
· -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
      rw [equiv_snd_eq_inv_mul]; simp

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₂).2)⁻¹ ∈ ↑H
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 α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (sfiniteSeq μ i.2) t * (sfiniteSeq ν i.1) s = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
mul_comm

Goal state after: