mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ i, t i, _] (I'.attach.sup fs) ∧ I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ

Tactic:
constructorm* _ ∧ _

Goal state after:
case h.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ i, t i, _] (I'.attach.sup fs)

case h.right.left
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ I'.attach.sup fs x = 0

case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∏ i,
      ∫ (v : E i),
        cexp (↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) v) * I) ∂μ i

Tactic:
← integral_fintype_prod_eq_prod,

Goal state after:
p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      ∏ i,
        cexp
          (↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) (x i)) *
            I) ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:

Tactic:
κ B ≤ ν (thickening s.toReal B) + s :=
      right_measure_le_of_levyProkhorovEDist_lt lt_s B_mble
    _ ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s := by
      grw [right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet]
    _ = μ (thickening r.toReal (thickening s.toReal B)) + (s + r) := by rw [add_assoc, add_comm r]
    _ ≤ μ (thickening (r.toReal + s.toReal) B) + (s + r) := by grw [thickening_thickening_subset]
    _ = μ (thickening (s.toReal + r.toReal) B) + (s + r) := by rw [add_comm r.toReal]

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

Goal state before:
pp: case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ AEStronglyMeasurable (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) volume

pp: case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖ν.real (thickening ε {a_1 | a ≤ f a_1})‖ ≤ ν.real univ

Tactic:
· apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)

Goal state after:
case f_bdd
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖ν.real (thickening ε {a_1 | a ≤ f a_1})‖ ≤ ν.real univ
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹¹ : Group A
inst✝¹⁰ : Group B
inst✝⁹ : Group C
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁵ : IsTopologicalGroup A
inst✝⁴ : IsTopologicalGroup B
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝ : NormedSpace ℝ E
f : CompactlySupportedContinuousMap B E
b : B
a : A
ha : φ a = (Function.invFun (⇑ψ) (ψ b))⁻¹ * b
⊢ ∫ (x : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) (a * x) ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

Tactic:
simp [pullback_def, ha, mul_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹¹ : Group A
inst✝¹⁰ : Group B
inst✝⁹ : Group C
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁵ : IsTopologicalGroup A
inst✝⁴ : IsTopologicalGroup B
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝ : NormedSpace ℝ E
f : CompactlySupportedContinuousMap B E
b : B
⊢ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

Tactic:
have h : ψ ((Function.invFun ψ (ψ b))⁻¹ * b) = 1 := by simp [Function.apply_invFun_apply]
  rw [← ψ.mem_ker, H.mulExact.monoidHom_ker_eq] at h
  obtain ⟨a, ha⟩ := h
  rw [← integral_mul_left_eq_self _ a]
  simp [pullback_def, ha, mul_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
g : G
s : Set A
this : (DomMulAct.mk g • μ) s = μ (g • s)
⊢ ↑((distribHaarChar A) g) * μ s = μ (g • s)

Tactic:
eq_comm,

Goal state after:
G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
g : G
s : Set A
this : (DomMulAct.mk g • μ) s = μ (g • s)
⊢ μ (g • s) = ↑((distribHaarChar A) g) * μ s
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε

Tactic:
have hS {x} (hx : x ∈ U₀) {y} (hy : y ∉ S) : H.pullback f x y = 0 := by
        contrapose! hy
        exact Set.mem_mul.mpr ⟨x⁻¹, Set.inv_mem_inv.mpr hx, x * φ y,
          not_imp_comm.mp (hf₀ (x * φ y)) hy, inv_mul_cancel_left x (φ y)⟩

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
δ : ℝ
hδ0 : δ > 0
hδ : ENNReal.ofReal δ * μA S < ENNReal.ofReal ε
hS : ∀ {x : B}, x ∈ U₀ → ∀ {y : A}, y ∉ S → (H.pullback f x) y = 0
⊢ ∀ᶠ (x : B) in nhds b, dist (∫ (a : A), (H.pullback f x) a ∂μA) (∫ (a : A), (H.pullback f b) a ∂μA) < ε
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
U : Set B
hU : IsOpen U
b : B
hb✝ : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
hf0 : 0 ≤ (H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }
⊢ 0 < (RealRMK.rieszMeasure { toLinearMap := H.integrate μA μC, monotone' := ⋯ }) U

Tactic:
← RealRMK.le_rieszMeasure_tsupport_subset (f := ⟨f, hf2⟩) _ hf4 hf3,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
U : Set B
hU : IsOpen U
b : B
hb✝ : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
hf0 : 0 ≤ (H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }
⊢ 0 <
    ENNReal.ofReal
      ({ toLinearMap := H.integrate μA μC, monotone' := ⋯ } { toContinuousMap := f, hasCompactSupport' := hf2 })
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) ∂μ =
    ∫ (y : ℝ), if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I) ∂μ

Tactic:
congr with y
    by_cases hy : y = 0
    · simp [hy, two_mul]
    simp only [mul_eq_zero, hr.ne', hy, or_self, ↓reduceIte, ofReal_inv]
    have h := intervalIntegral.integral_deriv_smul_comp (E := ℂ) (a := -r) (b := r)
      (f := fun x ↦ y * x) (f' := fun _ ↦ y) (g := fun x ↦ cexp (x * I)) ?_ (by fun_prop)
      (by fun_prop)
    swap
    · intro x hx
      simp_rw [mul_comm y]
      exact hasDerivAt_mul_const _
    simp only [Function.comp_apply, ofReal_mul, real_smul, intervalIntegral.integral_const_mul,
      mul_neg] at h
    rw [← h, ← mul_assoc]
    norm_cast
    simp [mul_comm _ y, mul_inv_cancel₀ hy]

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

Goal state before:
pp: case e_a
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ ∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ = 1 - ∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ

Tactic:
· rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case Hi
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ -(ContinuousLinearMap.apply ℝ F) (1, 0) ∘SL dη a
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' : (fun a ↦ (f' a) (1, 0) + (g' a) (0, 1)) =ᵐ[volume.restrict (Icc 0 1)] 0
this : ∫ (a : ℝ × ℝ) in Icc 0 1, (f' a) (1, 0) + (g' a) (0, 1) = 0
hηc : ContinuousOn η (Icc 0 1)
⊢ IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Icc 0 1) volume

Tactic:
rw [integrableOn_congr_fun_ae hf'g']
      apply integrableOn_zero

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
x y : ℝ
hx : (x, y).1 ∈ Icc 0.1 1.1
hy : (x, y).2 ∈ Icc 0.2 1.2
⊢ (fun x ↦ IccExtend ⋯ (⇑(φ.extend x.1)) x.2) (x, y) =
    (fun x ↦ (lineMap ((lineMap a b) x.2) ((lineMap a c) x.2)) x.1) (x, y)

Tactic:
lift x to I using hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
y : ℝ
x : { x // x ∈ I }
hy : (↑x, y).2 ∈ Icc 0.2 1.2
⊢ (fun x ↦ IccExtend ⋯ (⇑(φ.extend x.1)) x.2) (↑x, y) =
    (fun x ↦ (lineMap ((lineMap a b) x.2) ((lineMap a c) x.2)) x.1) (↑x, y)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case e_f
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
i : ℕ
⊢ ∑ q ∈ Q.parts, f (↑q ⊓ ↑(s' i)) = ∑ p ∈ (P i).parts, f ↑p

Tactic:
exact (Q.sum_restrict _ (fun p => f p) hf').symm

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
⊢ x ∈ (μ.restrict s).support ↔ ∃ᶠ (u : Set X) in (𝓝[s] x).smallSets, 0 < μ u

Tactic:
rw [nhds_basis_opens x |>.mem_measureSupport,
    (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < (μ.restrict s) i) ↔
    ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ (i ∩ s)
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ (μ.restrict s).support ⊆ closure[inst✝²] s ∩ μ.support

Tactic:
refine Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_)
    (support_mono restrict_le_self)

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ closure[inst✝²] s ∈ ae (μ.restrict s)
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ n, f n) \ ⋃ n ∈ Finset.range (N + 1), f n)).toReal +
      (μ ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)).toReal <
    ε

Tactic:
rw [← add_halves ε]

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ n, f n) \ ⋃ n ∈ Finset.range (N + 1), f n)).toReal +
      (μ ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)).toReal <
    ε / 2 + ε / 2
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
this : μ s ≤ μ univ
⊢ μ univ = 1

Tactic:
rw [h] at this

Goal state after:
case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
this : 1 ≤ μ univ
⊢ μ univ = 1
Module: Mathlib.MeasureTheory.Measure.WithDensityFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ.restrict μ.sigmaFiniteSetᶜ = ∞ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ

Tactic:
by
  rw [Measure.sigmaFiniteSet,
    restrict_compl_sigmaFiniteSetWRT (Measure.AbsolutelyContinuous.refl μ)]
  ext t ht
  simp only [Measure.smul_apply, smul_eq_mul]
  rw [Measure.restrict_apply ht, Measure.restrict_apply ht]
  by_cases hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
  · rw [hμt, toFinite_absolutelyContinuous μ hμt]
  · rw [ENNReal.top_mul hμt, ENNReal.top_mul]
    exact fun h ↦ hμt (absolutelyContinuous_toFinite μ h)

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

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
exact generateFrom_mono <| le_trans self_subset_generateSetAlgebra <|
        generateSetAlgebra_mono <| subset_union_left ..

Goal state after: