mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ
hN_meas : Measurable N
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (x : α), ↑((δ ∘ N) x) ∂μ < ε

Tactic:
simp_rw [Function.comp_apply, ← Function.comp_apply (f := (fun n ↦ (↑(δ n) : ℝ≥0∞))),
    lintegral_comp measurable_from_nat.coe_nnreal_ennreal hN_meas]

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
hNs : ∀ (n : ℕ), N ⁻¹' {n} = s n
⊢ ∫⁻ (n : ℕ), ↑(δ n) ∂map N μ < ε
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) μ = μ.join (f ⁻¹' s)

Tactic:
join_apply (hf hs),

Goal state after:
α : 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) ∂μ
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
this : Tendsto (fun n ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ dist (y m) (y n) ≤ 2 * u m

Tactic:
rcases I m n with ⟨z, zsm, zsn⟩

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
this : Tendsto (fun n ↦ 2 * u n) atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
z : γ
zsm : z ∈ ↑(s m)
zsn : z ∈ ↑(s n)
⊢ dist (y m) (y n) ≤ 2 * u m
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
← measure_toMeasurable s,

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ (toMeasurable μ s)
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
c : G
⊢ μ (c • s) = 0 ↔ μ s = 0

Tactic:
measure_smul

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
c : G
⊢ μ s = 0 ↔ μ s = 0
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : μ K ≠ 0
hU : IsOpen[inst✝²] U
hne : U.Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, g • U
hμU : μ U = 0
x✝¹ : G
x✝ : x✝¹ ∈ ↑t
⊢ μ (x✝¹ • U) = 0

Tactic:
measure_smul

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : μ K ≠ 0
hU : IsOpen[inst✝²] U
hne : U.Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, g • U
hμU : μ U = 0
x✝¹ : G
x✝ : x✝¹ ∈ ↑t
⊢ μ U = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
U' : Set α
hsU' : U' ⊇ U \ s
hU'o : IsOpen[inst✝¹] U'
hμU' : μ U' < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
replace hsU' := sdiff_subset_comm.1 hsU'

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst✝¹] U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
⊢ ∀ (U : Set α),
    IsOpen[inst✝²] U →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε

Tactic:
intro U hU ε hε
    rcases H.exists_subset_lt_add isClosed_empty hU hfin hε with ⟨F, hsF, hFc, hF⟩
    exact ⟨F, hsF, U, Subset.rfl, hFc, hU, hF.le, le_self_add⟩

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

Goal state before:
pp: case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
⊢ Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ℕ), MeasurableSet (s i)) →
      (∀ (i : ℕ) (ε : ℝ≥0∞),
          ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε) →
        ∀ (ε : ℝ≥0∞),
          ε ≠ 0 →
            ∃ F ⊆ ⋃ i, s i,
              ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Tactic:
hsd

Goal state after:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
⊢ (∀ (i : ℕ), MeasurableSet (s i)) →
    (∀ (i : ℕ) (ε : ℝ≥0∞),
        ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε) →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ ⋃ i, s i,
            ∃ U ⊇ ⋃ i, s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
⊢ f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k

Tactic:
by
  ext x
  simp only [mlconvolution_def]
  conv in f _ * (∫⁻ _, _ ∂μ) =>
    rw [← lintegral_const_mul'' _ (by fun_prop), ← lintegral_mul_left_eq_self _ y⁻¹]
  conv in (∫⁻ _, _ ∂μ) * k _ =>
    rw [← lintegral_mul_const'' _ (by fun_prop)]
  rw [lintegral_lintegral_swap]
  · simp [mul_assoc]
  simpa [mul_assoc] using by fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
have R : restrict μ A V ≠ ∞ := by
    rw [restrict_apply hV.measurableSet]
    exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
R : (μ.restrict A) V ≠ ∞
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
have : ∀ᵐ x ∂μ, .ofReal (f x).toReal = f x := by filter_upwards [hf] with x hx; simp [hx]
  simp [hasFiniteIntegral_iff_enorm, Real.enorm_of_nonneg ENNReal.toReal_nonneg,
    lintegral_congr_ae this, lt_top_iff_ne_top]

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

Goal state before:
pp: x : ℝ≥0
⊢ sqrt (x * x) = x

Tactic:
by rw [← sq, sqrt_sq]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ x ∧ 0 ≤ x * (x - 1) ↔ x = 0 ∨ 1 ≤ x

Tactic:
grind [mul_nonneg_iff]

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ |z.re| + |z.im|

Tactic:
simpa [re_add_im] using norm_add_le (z.re : ℂ) (z.im * I)

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

Goal state before:
pp: z : ℂ
⊢ z.im ^ 2 ≤ normSq z

Tactic:
by
    rw [normSq_apply, ← sq, ← sq]
    exact le_add_of_nonneg_left (sq_nonneg _)

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
simp only [HasFiniteIntegral]
  calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ ‖z - 1‖ ^ 2 = 2 * (1 - z.re)

Tactic:
have : z.im * z.im = 1 - z.re * z.re := by
    replace hz := sq_eq_one_iff.mpr (.inl hz)
    rw [Complex.sq_norm, normSq_apply] at hz
    linarith
  simp [Complex.sq_norm, normSq_apply, this]
  ring

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x))

Tactic:
refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩
  · rw [withDensity_apply']
    apply setLIntegral_lt_top_of_bddAbove
    · exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne
    · exact ⟨n, forall_mem_image.2 fun x hx ↦ hx.2⟩
  · rw [iUnion_eq_univ_iff]
    refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩
    · exact mem_spanningSets_of_index_le _ _ (le_max_left ..)
    · simp [Nat.le_ceil]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᵐ[μ] fun x ↦ ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity f)

Tactic:
withDensity_congr_ae this

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᵐ[μ] fun x ↦ ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x).toNNReal)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n = 0
⊢ n = 0

Tactic:
rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h

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

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]

Goal state after:
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (a, a⁻¹ * x)) (μ.prod μ)

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1 * g z.2) (μ.prod μ)

case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ φ (z.1 * z.2)) (μ.prod μ)
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖

Tactic:
rw [norm_star_mul_self, norm_star]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = 1

Tactic:
· calc
        U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
        _ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
        _ = 1 := by rw [hB₂, mul_one, hA₂]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ ⟨φ (v₁ + v₂), ⋯⟩ = ⟨φ v₁, ⋯⟩ + ⟨φ v₂, ⋯⟩

Tactic:
by
    ext
    simp only [map_add, AddSubgroup.coe_add]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).re = (r • s • x).re

Tactic:
simp [smul_re, smul_im, smul_assoc]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).im = (r • s • x).im

Tactic:
simp [smul_re, smul_im, smul_assoc]

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

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ RCLike.re x = y ↔ x = ↑y

Tactic:
exact RCLike.re_eq_ofReal_of_isSelfAdjoint hx

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖(starRingEnd K) x + x‖ ^ 2 = re ((starRingEnd K) x + x) ^ 2

Tactic:
rw [add_comm, norm_sq_re_add_conj]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ e.target

Tactic:
by
      rw [h']
      exact mem_univ _

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
domRestrict_eq,

Goal state after:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (↑e.toPartialEquiv ∘ Subtype.val)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
hz : 0 < z
hw : 0 < w
⊢ 0 < z * w

Tactic:
lt_iff_re_im,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z w : K
hz : re 0 < re z ∧ im 0 = im z
hw : re 0 < re w ∧ im 0 = im w
⊢ re 0 < re (z * w) ∧ im 0 = im (z * w)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
obtain hx | hx | hx := lt_trichotomy x 0

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x < 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

case inr.inl
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : x = 0
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

case inr.inr
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0
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
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (↑e ∘ f) univ x

Tactic:
e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h'

Goal state after:
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
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousWithinAt (↑e ∘ f) univ x ↔ ContinuousWithinAt (↑e ∘ f) univ x
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []

Tactic:
pn.out,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range ↑0 = []
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')

Tactic:
pn.out,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range ↑nn = 0 :: List.map Nat.succ (List.range n')
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0

Tactic:
pn.out,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range ↑0 = 0
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range n = n' ::ₘ Multiset.range n'

Tactic:
pn.out,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range ↑nn = n' ::ₘ Multiset.range n'
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅

Tactic:
pn.out,

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range ↑0 = ∅