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

Goal state before:
pp: α : 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))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
suffices Tendsto (fun n ↦ ∫ x, - -f n x ∂μ) atTop (𝓝 (∫ x, - -F x ∂μ)) by
      simpa [neg_neg] using this

Goal state after:
α : 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))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : f z = ↑‖z‖ / ↑r * f z₁
⊢ ‖z‖ * ‖f z₁‖ / r ≤ c * ‖z‖ / r

Tactic:
mul_comm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : f z = ↑‖z‖ / ↑r * f z₁
⊢ ‖f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 ≤ ‖d • x - y‖

Tactic:
calc
    1 = ‖c‖ / R * (R / ‖c‖) := by field
    _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
    _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
      simp only [norm_smul]
      ring
    _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
    _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
⊢ ∀ (i : n ⊕ p) (j : l ⊕ m), Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) i j

Tactic:
rintro (i | i) (j | j) <;> refine Continuous.matrix_elem ?_ i j <;> assumption

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : CompleteSpace G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : ↥(Lp G' 1 μ)
hf : 0 ≤ f
⊢ 0 ≤ (setToL1 hT) f

Tactic:
by
  suffices ∀ f : { g : α →₁[μ] G' // 0 ≤ g }, 0 ≤ setToL1 hT f from
    this (⟨f, hf⟩ : { g : α →₁[μ] G' // 0 ≤ g })
  refine fun g =>
    @isClosed_property { g : α →₁ₛ[μ] G' // 0 ≤ g } { g : α →₁[μ] G' // 0 ≤ g } _ _
      (fun g => 0 ≤ setToL1 hT g)
      (denseRange_coeSimpleFuncNonnegToLpNonneg 1 μ G' one_ne_top) ?_ ?_ g
  · exact (isClosed_Ici (a := 0)).preimage ((setToL1 hT).continuous.comp continuous_induced_dom)
  · intro g
    have : (coeSimpleFuncNonnegToLpNonneg 1 μ G' g : α →₁[μ] G') = (g : α →₁ₛ[μ] G') := rfl
    rw [this, setToL1_eq_setToL1SCLM]
    exact setToL1S_nonneg (fun s => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg g.2

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ ∫ (x : X), ‖f x‖ ∂μ i = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal

Tactic:
← integral_toReal ?_ (by simp)

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ ∫ (x : X), ‖f x‖ ∂μ i = ∫ (a : X), ‖f a‖ₑ.toReal ∂μ i

ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : Integrable f (Measure.sum μ)
i : ι
⊢ AEMeasurable (fun x ↦ ‖f x‖ₑ) (μ i)
Module: Mathlib.Topology.Algebra.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
obtain h | h := hx

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ ContinuousAt (s.mulIndicator f) x

case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ μ.real univ * C = C * μ.real univ

Tactic:
mul_comm

Goal state after:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ C * μ.real univ = C * μ.real univ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Tactic:
rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]

Goal state after:
case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : Integrable f (μ a✝) ∧ ∀ x ∈ s✝, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a✝ + ∑ x ∈ s✝, μ x) = ∫ (a : α), f a ∂μ a✝ + ∫ (a : α), f a ∂∑ i ∈ s✝, μ i
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖t i‖ * ‖g i‖ ≤ ‖g‖ * ‖t‖

Tactic:
mul_comm

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ * ‖g i - f i‖ ≤ ‖g i - f i‖ * ‖v - u‖

Tactic:
mul_comm

Goal state after:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
⊢ ‖u e‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M * ‖e‖₊

Tactic:
by
    set φ := v.equivFunL.toContinuousLinearMap
    calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]

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
        obtain ⟨C₂, hg⟩ := g.bounded
        refine ⟨C₁ + C₂, fun x y ↦ ?_⟩
        simp_rw [dist_eq_norm_sub] at hf hg ⊢
        exact (norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _))

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 : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ (fun f ↦ f.toFun) (f + h) t ≤ (fun f ↦ f.toFun) (g + h) t

Tactic:
simpa using h₁ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
by
  simp [← isometryEquivBoundedOfCompact α β |>.dist_eq f g,
    BoundedContinuousFunction.dist_eq_iSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_add
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
⊢ Integrable g₂ μ →
    setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
      setToFun μ T hT g₂ = setToFun μ' T hT' g₂ → setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)

Tactic:
hg₂

Goal state after:
case pos.h_add
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
⊢ setToFun μ T hT f₂ = setToFun μ' T hT' f₂ →
    setToFun μ T hT g₂ = setToFun μ' T hT' g₂ → setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ 1 ≤ (↑δ.toNNReal)⁻¹ * edist x y + infEDist x E * (↑δ.toNNReal)⁻¹

Tactic:
mul_comm

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ 1 ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEDist x E * (↑δ.toNNReal)⁻¹
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : 𝓝[<] a = ⊥
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
simp only [MapClusterPt, ClusterPt, h', leftLim_eq_of_eq_bot, A]

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✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
g : ℕ → R × R
hg : ∀ (i : ℕ), Icc a' b ∩ s i ⊆ Iotop (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)
I_subset : Icc a' b ⊆ ⋃ i, Iotop (g i).1 (g i).2
⊢ ∑' (i : ℕ), (f.length (s i) + ↑(ε' i)) + ↑δ = ∑' (i : ℕ), f.length (s i) + ∑' (i : ℕ), ↑(ε' i) + ↑δ

Tactic:
by rw [ENNReal.tsum_add]

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableConstSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x ↦ g⁻¹ • x
⊢ AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t))) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
← image_smul,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝⁴ : MeasurableConstSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x ↦ g⁻¹ • x
⊢ AEStronglyMeasurable f (μ.restrict ((fun x ↦ g⁻¹ • x) '' (g • s ∩ t))) ↔
    AEStronglyMeasurable f (μ.restrict (g • s ∩ t))
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ s.card * t.card

Tactic:
mul_comm

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
⊢ index (↑K) V ≤ t.card * s.card
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

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

Tactic:
hg₂

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
this : Fact (ν 𝓕 < ∞)
⊢ IsFiniteMeasure (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))

Tactic:
infer_instance

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
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : IsEmpty R
⊢ IsFiniteMeasure f.measure

Tactic:
infer_instance

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
⊢ re ((starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫) = ‖(starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫‖

Tactic:
mul_comm

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫) = ‖⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, 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 y : F
t : ℝ
⊢ ↑t * ⟪x, y⟫ = ⟪x, y⟫ * ↑t

Tactic:
mul_comm

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ ⟪x, y⟫ * ↑t = ⟪x, y⟫ * ↑t
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ((starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫) = ‖(starRingEnd 𝕜) ⟪y, x⟫ * ⟪y, x⟫‖

Tactic:
mul_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫) = ‖⟪y, x⟫ * (starRingEnd 𝕜) ⟪y, x⟫‖
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : SecondCountableTopology G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ SigmaFinite (haarMeasure K₀)

Tactic:
infer_instance

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
⊢ ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)

Tactic:
by
  rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]

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

Goal state before:
pp: E : Type u_4
𝕜 : Type u_7
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
⊢ ⟪x, v⟫ = 0

Tactic:
by rw! [← inner_conj_symm]; simp [-inner_conj_symm, h, hv]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x y : 𝕜
⊢ (starRingEnd 𝕜) x * y = y * (starRingEnd 𝕜) x

Tactic:
mul_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x y : 𝕜
⊢ y * (starRingEnd 𝕜) x = y * (starRingEnd 𝕜) x
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
G : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x + y, z⟫_ℝ = ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ

Tactic:
simp +instances only [Inner.rclikeToReal, inner_add_left, map_add]

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

Goal state before:
pp: x y : ℝ
⊢ inner ℝ x y = x * y

Tactic:
mul_comm

Goal state after:
x y : ℝ
⊢ inner ℝ x y = y * x