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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < μ u

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v

Tactic:
· exact u_open.measure_pos μ ⟨x, xu⟩

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < ν v
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
have : BorelSpace Y := ⟨rfl⟩

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this✝ : MeasurableSpace Y := borel Y
this : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (map (⇑f) μ) U
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K

Tactic:
rw [f.map_apply U] at hr

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (⇑f ⁻¹' U)
⊢ ∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K
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
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H

Tactic:
rw [← this]

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'' * Nat.card ↑S
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
⊢ μ.InnerRegularWRT p q'

Tactic:
intro U hU r hr
  rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩; rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩
  exact ⟨K, hKF.trans hFU, hpK, hrK⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
S : Set G
inst✝ : H.FiniteIndex
h : IsComplement S ↑H
⊢ ↑S.ncard = ↑H.index

Tactic:
h.ncard_left

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
S : Set G
inst✝ : H.FiniteIndex
h : IsComplement S ↑H
⊢ ↑H.index = ↑H.index
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
⊢ IsOpen[inst✝²] u → μ (closure[inst✝²] k) ≤ μ u

Tactic:
u_open

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
u_open : IsOpen[inst✝²] u
⊢ μ (closure[inst✝²] k) ≤ μ u
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝² : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝¹ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this✝ : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
this : f z = x
⊢ x ∈ range f

Tactic:
rw [← this]

Goal state after:
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝² : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝¹ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this✝ : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
this : f z = x
⊢ f z ∈ range f
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : ⇑f.symm '' K = ⇑f ⁻¹' K
⊢ IsCompact (⇑f ⁻¹' K)

Tactic:
rw [← this]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : ⇑f.symm '' K = ⇑f ⁻¹' K
⊢ IsCompact (⇑f.symm '' K)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet
    {x | ∃ i, True ∧ ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}

Tactic:
Set.ofPred_exists,

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet
    (⋃ i, {x | True ∧ ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}})
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed[w✝] s
right✝ : IsOpen[w✝] s
⊢ StandardBorelSpace ↑s

Tactic:
have := s_closed.polishSpace

Goal state after:
α : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed[w✝] s
right✝ : IsOpen[w✝] s
this : PolishSpace ↑s
⊢ StandardBorelSpace ↑s
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
⊢ μ ≪ map (fun h ↦ g * h⁻¹) μ

Tactic:
rw [← this]

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
⊢ μ ≪ map (fun x ↦ g * x) (map Inv.inv μ)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
trim_measurableSet_eq _ hs,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
⊢ HasFiniteIntegral f μ

Tactic:
simp only [hasFiniteIntegral_iff_enorm] at *
  calc
    (∫⁻ a, ‖f a‖ₑ ∂μ) ≤ ∫⁻ a : α, ‖g a‖ₑ ∂μ := lintegral_mono_ae h
    _ < ∞ := hg

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), a * (x * x) + b * x + c ≤ 0
⊢ ∀ (x : K), 0 ≤ -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_nonneg]

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

Goal state before:
pp: case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
· rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
    exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

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).withDensity fun x ↦ (f x)⁻¹) ≤ μ

Tactic:
rw [← withDensity_mul₀ hf hf.fun_inv]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun x ↦ (f x)⁻¹) = μ

Tactic:
rw [← withDensity_mul₀ hf hf.fun_inv]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) = μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite μ

Tactic:
← Measure.restrict_add_restrict_compl (μ := μ) measurableSet_sigmaFiniteSetWRT,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (sigmaFiniteSetWRT ?m.15 ?m.16) + μ.restrict (sigmaFiniteSetWRT ?m.15 ?m.16)ᶜ)

α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ Measure α

α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ Measure α
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝¹ : ℝ
x✝ : 𝕜
⊢ (RCLike.complexRingEquiv h).toFun (x✝¹ • x✝) = (RingHom.id ℝ) x✝¹ • (RCLike.complexRingEquiv h).toFun x✝

Tactic:
simp [RCLike.smul_re, RCLike.smul_im, ofReal_mul]; ring

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
  · rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]
    simp
  exact (RCLike.complexLinearIsometryEquiv h).norm_map a

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star x) = star (φ x)

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]
    simp [(ℜ x).2.map' φ, IsSelfAdjoint.star_eq, (ℑ x).2.map' φ]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝 x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
refine eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => ?_)

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
y : X
hy : ↑e.symm (↑e y) = y
⊢ p (↑e.symm (↑e y)) ↔ p y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
⊢ ↑x * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0

Tactic:
simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x

Tactic:
refine ⟨(e.continuousAt hx).comp_continuousWithinAt, fun fe_cont => ?_⟩
  rw [← continuousWithinAt_inter' h] at fe_cont ⊢
  have : ContinuousWithinAt (e.symm ∘ e ∘ f) (s ∩ f ⁻¹' e.source) x :=
    haveI : ContinuousWithinAt e.symm univ (e (f x)) :=
      (e.continuousAt_symm (e.map_source hx)).continuousWithinAt
    ContinuousWithinAt.comp this fe_cont (subset_univ _)
  exact this.congr (fun y hy => by simp [e.left_inv hy.2]) (by simp [e.left_inv hx])

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
by
    conv in _ ≤ _ => rw [RCLike.le_iff_re_im]
    simp_rw [Set.ofPred_and]
    refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> fun_prop

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
E' : Type u_6
F'' : Type u_10
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun x ↦ 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

Tactic:
simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mp.succ
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
⊢ ∀ᶠ (x : α) in l, ↑(n + 1) * ‖f x‖ ≤ ‖g x‖

Tactic:
have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos

Goal state after:
case mp.succ
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
this : 0 < ↑n.succ
⊢ ∀ᶠ (x : α) in l, ↑(n + 1) * ‖f x‖ ≤ ‖g x‖
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e = univ

Tactic:
rw [← coe_toIsometryEquiv]

Goal state after:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e.toIsometryEquiv = univ
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁵ : Semiring R
inst✝³⁴ : Semiring R₂
inst✝³³ : Semiring R₃
inst✝³² : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁸ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁷ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁶ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁵ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁴ : RingHomInvPair σ₄₁ σ₁₄
inst✝²³ : RingHomInvPair σ₂₄ σ₄₂
inst✝²² : RingHomInvPair σ₄₂ σ₂₄
inst✝²¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝²⁰ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁴ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹² : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup E₂
inst✝⁹ : SeminormedAddCommGroup E₃
inst✝⁸ : SeminormedAddCommGroup E₄
inst✝⁷ : Module R E
inst✝⁶ : Module R₂ E₂
inst✝⁵ : Module R₃ E₃
inst✝⁴ : Module R₄ E₄
inst✝³ : NormedAddCommGroup F
inst✝² : Module R F
e : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝¹ : TopologicalSpace α
inst✝ : Module R E₂
⊢ ∀ (x : E × E₂), ‖(LinearEquiv.prodComm R E E₂) x‖ = ‖x‖

Tactic:
by intro; simp [norm, sup_comm]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ (fun H ↦ ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖) =ᶠ[l] fun H ↦ ‖B i H‖ + ∑ j ∈ s, ‖B j H‖

Tactic:
by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

Goal state after: