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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif false then μ else ν) ∧ AEStronglyMeasurable f (bif true then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
and_comm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᵐ[μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ g (f a) = g (f' a)

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ = ν
x✝¹ : α → ℝ≥0∞
x✝ : Measurable x✝¹
⊢ ∫⁻ (a : α), x✝¹ a ∂μ = ∫⁻ (a : α), x✝¹ a ∂ν

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
t : β → Set α
hd : (↑s).Pairwise (AEDisjoint μ on t)
hm : ∀ b ∈ s, NullMeasurableSet (t b) μ
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

Tactic:
by
  simp only [← Finset.mem_coe, lintegral_biUnion₀ s.countable_toSet hm hd, ← Finset.tsum_subtype']

Goal state after:
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
⊢ ‖∑' (i : ι), f i‖ₑ ≤ a

Tactic:
by
  by_cases hf : Summable f
  · exact hf.hasSum.enorm_le_of_bounded hg h
  · simp [tsum_eq_zero_of_not_summable hf]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y : ↑(Icc a b)
h : x ≤ y
t : ↑unitInterval
⊢ x ≤ convexComb x y t

Tactic:
← Subtype.coe_le_coe

Goal state after:
a b : ℝ
x y : ↑(Icc a b)
h : ↑x ≤ ↑y
t : ↑unitInterval
⊢ ↑x ≤ ↑(convexComb x y t)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: a b : ℝ
x y : ↑(Icc a b)
h : x ≤ y
t : ↑unitInterval
⊢ convexComb x y t ≤ y

Tactic:
← Subtype.coe_le_coe

Goal state after:
a b : ℝ
x y : ↑(Icc a b)
h : ↑x ≤ ↑y
t : ↑unitInterval
⊢ ↑(convexComb x y t) ≤ ↑y
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x n.succ = res y n.succ

Tactic:
rw [h]

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

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i = j
⊢ E j = E i

Tactic:
rw [h]

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

Goal state before:
pp: case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑x) n)

Tactic:
← hyx

Goal state after:
case refine_1.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : res (↑y) n = res (↑x) n
⊢ (inducedMap A).snd y ∈ A (res (↑y) n)
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ < 1

Tactic:
rw [h]

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist ⟨i, x⟩ ⟨j, y⟩ = 0
⊢ 0 < 1
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ i > 0, {p | dist p.1 p.2 < i} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}

Tactic:
intro ε εpos

Goal state after:
case a
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
⊢ {p | dist p.1 p.2 < ε} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ CauchySeq u

Tactic:
Metric.cauchySeq_iff

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
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
y : (n : ℕ) → E n
hy : y ∈ s
⊢ f y ∈ s

Tactic:
fs y hy

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
y : (n : ℕ) → E n
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = s

Tactic:
rw [h]

Goal state after:
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ range Empty.elim = ∅
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
by
  rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ

Tactic:
rw [h]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ 0 ⟂ₘ 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₂ ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Tactic:
and_comm

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x y : α
s : Set α
hs : s ∈ measurableAtoms
hsy : points ⟨s, hs⟩ = y
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
⊢ y = points ⟨measurableAtom x, ⋯⟩

Tactic:
rw [← hsy]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x y : α
s : Set α
hs : s ∈ measurableAtoms
hsy : points ⟨s, hs⟩ = y
hyx : ¬y = points ⟨measurableAtom x, ⋯⟩
hyx' : y ∈ measurableAtom x
⊢ points ⟨s, hs⟩ = points ⟨measurableAtom x, ⋯⟩
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this : Countable ↑b
s : ↑b
⊢ MeasurableSet (rangeFactorization f ⁻¹' ↑s)

Tactic:
exact hf.subtype_mk (hb.isOpen s.2).measurableSet

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

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ ⋃ n, s n ⊆ ⋃ m, ⋂ n, u m n

pp: case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint (⋃ m, t m) (⋃ m, ⋂ n, u m n)

pp: case refine_3
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ MeasurableSet (⋃ m, ⋂ n, u m n)

Tactic:
· refine iUnion_subset fun m => subset_iUnion_of_subset m ?_
    exact subset_iInter fun n => hsu m n

Goal state after:
case refine_2
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint (⋃ m, t m) (⋃ m, ⋂ n, u m n)

case refine_3
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ MeasurableSet (⋃ m, ⋂ n, u m n)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
⊢ (c • m).join = c • m.join

Tactic:
ext s hs
  simp [hs]

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
hF : IsClosed[inst✝¹] F
h : F = univ
⊢ F =ᵐ[μ] univ

Tactic:
rw [h]

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

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝³ : Encodable ι
inst✝² : (i : ι) → MetricSpace (Y i)
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace separating_f
⊢ IsHomeomorph toPiNat

Tactic:
rw [isHomeomorph_iff_continuous_bijective]

Goal state after:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝³ : Encodable ι
inst✝² : (i : ι) → MetricSpace (Y i)
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace separating_f
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toPiNat ∧ Bijective toPiNat
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (map Prod.fst (μ.prod ν)) s = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr
α : 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 : Set α
hKU : K ⊆ U
hKc : p K
hrK : μ U - ε < μ K
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : μ = ν
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (s ×ˢ t) = ν (s ×ˢ t)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv g).2 = ⟨1, h1⟩

Tactic:
ext
  rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ g ∈ S → ↑(hST.equiv g).1 = g

Tactic:
intro h
    rw [hST.equiv_fst_eq_self_of_mem_of_one_mem h1 h]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h : μ = ν
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Continuous f'

Tactic:
rw [h]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Continuous ⇑f
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
by
  rw [Measure.prod] at *
  rw [lintegral_bind Measurable.map_prodMk_left.aemeasurable hf]
  apply lintegral_congr_ae
  filter_upwards [Measurable.map_prodMk_left.aemeasurable.ae_of_bind hf] with a ha
  exact lintegral_map' ha (by fun_prop)

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

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

Tactic:
exists_prop,

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict Sᶜ, ENNReal.ofReal (-f x) = 0 x

Tactic:
exact
      (ae_restrict_mem hS.compl).mono fun x hx =>
        ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := ⋯
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ {x | f x ≠ 0} ∩ s

Tactic:
exact ⟨fx, hx⟩

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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν'.inv A < ∞
⊢ ∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

Tactic:
simp only [ν'.inv_apply] at h3A

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⁻¹ < ∞
⊢ ∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 ↦ x_1 * 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) ↔ ∃ x, ∃ (_ : x ⊆ univ) (_ : IsCompact x), ¬μ x = 0

Tactic:
exists_prop,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ (∃ i, ∃ (_ : j ≤ i), x ∈ {x | (↑n)⁻¹ < edist (f i x) (g x)}) ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)

Tactic:
exists_prop,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ (∃ i, j ≤ i ∧ x ∈ {x | (↑n)⁻¹ < edist (f i x) (g x)}) ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply Measurable.ennreal_induction

Goal state after:
case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ map (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop

Tactic:
simp_rw [← Function.comp_def]

Goal state after:
⊢ map (NNReal.toReal ∘ ⇑NNReal.sqrt ∘ toNNReal) atTop = atTop
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ comap (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop

Tactic:
simp_rw [← Function.comp_def]

Goal state after:
⊢ comap (NNReal.toReal ∘ ⇑NNReal.sqrt ∘ toNNReal) atTop = atTop
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ f * i ≤ f * g

Tactic:
by grw [hi]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b

Tactic:
rw [Rat.smul_def, Rat.smul_def]; exact mul_lt_mul_of_pos_left hab <| Rat.cast_pos.2 hq

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
s : Set α
h : μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
⊢ SFinite μ

Tactic:
rw [h]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
s : Set α
h : μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
⊢ SFinite (sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₃

Tactic:
rw [h]

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₂ * C₁
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Monoid R
inst✝⁶ : Monoid A
inst✝⁵ : MulAction R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : StarMul R
inst✝¹ : StarMul A
inst✝ : StarModule R A
r : R
a : A
hr : r ∈ unitary R
ha : a ∈ unitary A
⊢ r • a ∈ unitary A

Tactic:
simp [mem_iff, smul_smul, mul_smul_comm, smul_mul_assoc, hr, ha]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (r • z) = r * re z

Tactic:
by
  rw [real_smul_eq_coe_mul, re_ofReal_mul]

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

Goal state before:
pp: z : ℂ
hz : z.re = re 0 → z.im ≠ im 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0

Tactic:
simp_all only [ne_eq, zero_re, zero_im, neg_re, Left.neg_pos_iff, neg_im, neg_eq_zero]

Goal state after:
z : ℂ
hz : z.re = 0 → ¬z.im = 0
⊢ (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0
Module: Mathlib.LinearAlgebra.Complex.Module

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

Tactic:
simp [-re_add_im, realPart_I_smul, mul_comm _ I, ← smul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z

Tactic:
apply im_sq_le_normSq

Goal state after: