mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
⊢ ν (⇑f ⁻¹' {f x}) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← ae_iff.mp hf]

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
⊢ ν (⇑f ⁻¹' {f x}) ≤ ν {a | ¬0 a ≤ f a}
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hE : ¬CompleteSpace E
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
simp [integral, hE, setToFun]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

Tactic:
exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

Tactic:
conv in 𝓝 _ => rw [← sub_self (1 : β)]

Goal state after:
case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
simp only [integral_congr_ae hfg, integral_congr_ae (ae_mono hle hfg)]

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
⊢ ∫ (a : α), g a ∂μ ≤ ∫ (a : α), g a ∂ν
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : ClosedIciTopology E
f g : α → E
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g μ
h : f ≤ᵐ[μ] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
by
  by_cases hfi : Integrable f μ
  · exact integral_mono_ae hfi hgi h
  · exact integral_undef hfi ▸ integral_nonneg_of_ae (hf.trans h)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ 0 < ∫ (x : α), Real.exp (f x) ∂μ

Tactic:
rw [integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf]
  suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]
  ext1 x
  simp only [Function.mem_support, ne_eq, (Real.exp_pos _).ne', not_false_eq_true, Set.mem_univ]

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ ⇑f = ⇑f.contLinear + Function.const V (f 0)

Tactic:
rcases f with ⟨f, h⟩

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ⇑{ toAffineMap := f, cont := h } =
    ⇑{ toAffineMap := f, cont := h }.contLinear + Function.const V ({ toAffineMap := f, cont := h } 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ -f n x) atTop (𝓝 (-F x))

Tactic:
· filter_upwards [h_tendsto] with x hx using hx.neg

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Sub R
inst✝ : BoundedSub R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C
x y : X
⊢ dist ((f - g) x) ((f - g) y) ≤ C

Tactic:
exact hC (Set.sub_mem_sub (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
           (Set.sub_mem_sub (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun x_1 ↦ x - x_1) (cobounded R) (cobounded R)

Tactic:
by
  simpa only [sub_eq_add_neg] using! (tendsto_const_add_cobounded x).comp tendsto_neg_cobounded

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT (-f) = -(L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
setToFun_eq hT hf.neg,

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 (-f) ⋯) = -(L1.setToL1 hT) (Integrable.toL1 f hf)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ LinearMap.det ↑f

Tactic:
LinearMap.det_eq_det_toMatrix_of_finset b

Goal state after:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ ((LinearMap.toMatrix b b) ↑f).det
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ dist f g < C → ∀ (x : α), dist (f x) (g x) < C

Tactic:
intro w x
    exact lt_of_le_of_lt (dist_coe_le_dist x) w

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊔ ⇑g) x) ((⇑f ⊔ ⇑g) y) ≤ C

Tactic:
obtain ⟨C₁, hf⟩ := f.bounded

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊔ ⇑g) x) ((⇑f ⊔ ⇑g) y) ≤ C
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊓ ⇑g) x) ((⇑f ⊓ ⇑g) y) ≤ C

Tactic:
obtain ⟨C₁, hf⟩ := f.bounded

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊓ ⇑g) x) ((⇑f ⊓ ⇑g) y) ≤ C
Module: Mathlib.Topology.ContinuousMap.Bounded.Star

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : α →ᵇ β
⊢ ‖f‖ ≤ √‖star f * f‖

Tactic:
norm_le (Real.sqrt_nonneg _)

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : α →ᵇ β
⊢ ∀ (x : α), ‖f x‖ ≤ √‖star f * f‖
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δseq_lim : ∃ a, ∀ (b : ℕ), a ≤ b → |δseq b| < ε
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
rcases δseq_lim with ⟨N, hN⟩

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α → E
ι : Type u_7
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
hf : ∀ i ∈ s, Integrable f (μ i)
⊢ setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f

Tactic:
by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | @cons i s his hs' ih =>
    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using!
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
by
  by_cases hr : r = 0
  · suffices f =ᵐ[μ] 0 by
      rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
    rw [hr] at hf
    norm_cast at hf
    have hnegf : ∫ x, -f x ∂μ = 0 := by
      rw [integral_neg, neg_eq_zero]
      exact le_antisymm (integral_nonpos_of_ae hf) hfint'
    have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
    · filter_upwards [this] with ω hω
      rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
    · filter_upwards [hf] with ω hω
      rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]
  by_cases hμ : IsFiniteMeasure μ
  swap
  · have : μ Set.univ = ∞ := by
      by_contra hμ'
      exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
    rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
    · exact le_top
    · simp [hr]
    · simp
  have := hμ
  rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'
  have hposbdd : ∫ ω, max (f ω) 0 ∂μ ≤ μ.real Set.univ • (r : ℝ) := by
    rw [← integral_const]
    refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_
    filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
  rw [MemLp.eLpNorm_eq_integral_rpow_norm one_ne_zero ENNReal.one_ne_top
      (memLp_one_iff_integrable.2 hfint),
    ENNReal.ofReal_le_iff_le_toReal (by finiteness)]
  simp_rw [ENNReal.toReal_one, _root_.inv_one, Real.rpow_one, Real.norm_eq_abs, ←
    max_zero_add_max_neg_zero_eq_abs_self, ← Real.coe_toNNReal']
  rw [integral_add hfint.real_toNNReal]
  · simp only [Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.coe_toReal,
      toReal_ofNat] at hfint' ⊢
    grw [hfint']
    rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]
  · exact hfint.neg.sup (integrable_zero _ _ μ)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
s : Finset δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y

Tactic:
dsimp [lmarginal, updateFinset_def]; rcongr; exact h _ ‹_›

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this : Nonempty β
⊢ β

Tactic:
letI : TopologicalSpace α := Preorder.topology α

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this✝ : Nonempty β
this : TopologicalSpace α := Preorder.topology α
⊢ β
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
⊢ μ L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
have hL'U' : (L' : Set G) ⊆ (U' : Set G) := IsCompact.closure_subset_of_isOpen L.2 U'.2 hL.1

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
⊢ μ L' + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case hf
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
x : α
⊢ ‖f (g • x)‖ₑ = ‖f x‖ₑ

Tactic:
rw [hf]

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

Goal state before:
pp: case right.refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₃)⁻¹⁻¹ ∈ V

pp: case right.refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹

Tactic:
· simp only [inv_inv, h1g₃]

Goal state after:
case right.refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₃ * (g₁ * g₃)⁻¹ = g₁⁻¹
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
⊢ f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)

Tactic:
· have A : Disjoint (Ioo a b) {b} := by simp
    have D : f b - f a = f b - leftLim f b + (leftLim f b - f a) := by abel
    have := f.measure_Ioc a b
    simp only [← Ioo_union_Icc_eq_Ioc hab le_rfl, measure_singleton,
      measure_union A (measurableSet_singleton b), Icc_self] at this
    rw [D, ENNReal.ofReal_add, add_comm] at this
    · simpa only [ENNReal.add_right_inj ENNReal.ofReal_ne_top]
    · simp only [f.mono.leftLim_le le_rfl, sub_nonneg]
    · simp only [f.mono.le_leftLim hab, sub_nonneg]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : OrderBot R
this : Iic x = Icc ⊥ x
⊢ f.measure (Iic x) = ofReal (↑f x - l)

Tactic:
rw [atBot_eq_pure_of_isBot isBot_bot] at hf

Goal state after:
case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
x : R
this✝ : Nonempty R
val✝ : OrderBot R
hf : Tendsto (↑f) (pure ⊥) (𝓝 l)
this : Iic x = Icc ⊥ x
⊢ f.measure (Iic x) = ofReal (↑f x - l)
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ g₂ * g⁻¹ * (g * g₁) ∈ V

Tactic:
simp only [mul_assoc, hg₁, inv_mul_cancel_left]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
hf : Tendsto (↑f) atBot atBot
x : R
this : Nonempty R
val✝ : OrderBot R
⊢ f.measure (Iio x) = ∞

Tactic:
rw [atBot_eq_pure_of_isBot isBot_bot] at hf

Goal state after:
case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
x : R
this : Nonempty R
val✝ : OrderBot R
hf : Tendsto (↑f) (pure ⊥) atBot
⊢ f.measure (Iio x) = ∞
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ im ⟪x, x⟫ = 0

Tactic:
rw [← @ofReal_inj 𝕜, im_eq_conj_sub]
  simp [inner_conj_symm]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : Nonempty R
u : ℝ
hu : Tendsto (↑f) atTop (𝓝 u)
⊢ ∃ l, Tendsto (↑f) atBot (𝓝 l)

Tactic:
by
    rcases tendsto_atBot_of_monotone f.mono with H | H
    · obtain ⟨x, hx⟩ : ∃ x, f x ≤ - C - 1 := (tendsto_atBot.1 H (-C - 1)).exists
      grind
    exact H

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖

Tactic:
by rw [← inner_conj_symm, norm_conj]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
hxy : y ≤ x
⊢ ↑f x = ↑g x

Tactic:
| inr hxy =>

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_5
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
p✝ : ℝ≥0∞
μ✝ μ : Measure X
p : ℝ≥0∞
hp : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
⊢ ‖{ toFun := fun f ↦ MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ ‖f‖

Tactic:
exact norm_Lp_toLp_restrict_le s f

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁵ : CommSemiring 𝕝
inst✝⁴ : StarRing 𝕝
inst✝³ : Algebra 𝕝 𝕜
inst✝² : Module 𝕝 E
inst✝¹ : IsScalarTower 𝕝 𝕜 E
inst✝ : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪r • x, y⟫ = (starRingEnd 𝕝) r • ⟪x, y⟫

Tactic:
by
  rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]

Goal state after: