mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

Tactic:
simp only [edist_nndist]
  norm_cast
  apply dist_vadd_vadd_le

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
⊢ δ ≠ 0 → MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g

Tactic:
δpos

Goal state after:
case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
δ : ℝ≥0∞
δpos : δ ≠ 0
⊢ MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g
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 ∂μ))
this : Tendsto (fun n ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by
      simpa [neg_neg] using this

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ ^ p.toReal

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p.toReal) μ
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inr.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
i₀ : ι
ι' : Type (max 0 u_1) := { x // x ≠ i₀ }
val✝ : Fintype ι
this : Fintype ι'
⊢ IsOpen[Pi.topologicalSpace] {p | LinearIndependent 𝕜 fun i ↦ p ↑i -ᵥ p i₀}

Tactic:
convert_to!
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})

Goal state after:
case inr.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
i₀ : ι
ι' : Type (max 0 u_1) := { x // x ≠ i₀ }
val✝ : Fintype ι
this : Fintype ι'
⊢ IsOpen[Pi.topologicalSpace] ((fun p i ↦ p ↑i -ᵥ p i₀) ⁻¹' {p | LinearIndependent 𝕜 p})
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f₁ f₂ : α →ᵇ β
⊢ dist (c • f₁) (c • f₂) ≤ dist c 0 * dist f₁ f₂

Tactic:
by
    rw [dist_le (mul_nonneg dist_nonneg dist_nonneg)]
    intro x
    refine (dist_smul_pair c (f₁ x) (f₂ x)).trans ?_
    gcongr
    apply dist_coe_le_dist

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

Goal state before:
pp: case inr
α : 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun i ↦ setToFun μ T hT ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT f))

Tactic:
rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]

Goal state after:
case inr
α : 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
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun i ↦ setToFun μ T hT ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT ↑↑(Integrable.toL1 f hfi)))
Module: Mathlib.Topology.ContinuousMap.Star

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
𝕜 : Type u_3
inst✝⁶ : CommSemiring 𝕜
A : Type u_4
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : IsTopologicalSemiring A
inst✝² : StarRing A
inst✝¹ : ContinuousStar A
inst✝ : Algebra 𝕜 A
f : X ≃ₜ Y
g : C(Y, A)
⊢ (ContinuousMap.compStarAlgHom' 𝕜 A ↑f.symm) ((ContinuousMap.compStarAlgHom' 𝕜 A ↑f) g) = g

Tactic:
by
      simp only [ContinuousMap.compStarAlgHom'_apply, ContinuousMap.comp_assoc,
        toContinuousMap_comp_symm, ContinuousMap.comp_id]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
x : α
⊢ Tendsto (fun i ↦ (thickenedIndicator ⋯ E) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))

Tactic:
show indicator (closure E) (fun _ => (1 : ℝ≥0)) x =
        (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal
      by refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
x : α
⊢ Tendsto (fun i ↦ (thickenedIndicator ⋯ E) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x).toNNReal)
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 α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ T hT f

Tactic:
refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Goal state after:
α : 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ ≤ 1 • (μ + μ')
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 α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ' T hT f

Tactic:
refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf

Goal state after:
α : 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ 1 • (μ + μ')
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : 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
⊢ infEDist y E * (↑δ.toNNReal)⁻¹ ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEDist x E * (↑δ.toNNReal)⁻¹

Tactic:
by
      rw [← add_mul, edist_comm]
      gcongr
      exact infEDist_le_edist_add_infEDist

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
δ : ℝ
⊢ x ∉ thickening δ E →
    δ ∈ Ioi 0 →
      (thickening δ E).mulIndicator f x =
        (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
x_notin_thE

Goal state after:
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
δ : ℝ
x_notin_thE : x ∉ thickening δ E
⊢ δ ∈ Ioi 0 →
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
filter_upwards [univ_mem] with δ _

Goal state after:
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
a✝ : δ ∈ univ
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
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 α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[<] c = ⊥
⊢ leftLim f c ∈ id s

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
⊢ leftLim f c ∈ id s

Tactic:
· simpa [h'c, leftLim_eq_of_eq_bot] using hu hc

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
⊢ leftLim f c ∈ id s
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 : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ univ ≤ 0

Tactic:
← measure_congr h.iUnion_smul_ae_eq

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ (⋃ g, g • s) ≤ 0
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 : Set α
μ : Measure α
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s μ
g g' : G
⊢ (fun g' ↦ g⁻¹ * g' * g) ((fun g' ↦ g * g' * g⁻¹) g') = g'

Tactic:
by
      simp [mul_assoc]

Goal state after:
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
inst✝ : WeaklyLocallyCompactSpace G
⊢ μ.measure.Regular

Tactic:
by
  have : IsFiniteMeasureOnCompacts μ.measure := by
    refine ⟨fun K hK => ?_⟩
    apply (measure_mono subset_closure).trans_lt _
    rw [measure_apply _ isClosed_closure.measurableSet]
    exact μ.outerMeasure_lt_top_of_isCompact hK.closure
  refine ⟨fun U hU r hr => ?_⟩
  rw [measure_apply _ hU.measurableSet, μ.outerMeasure_of_isOpen U hU] at hr
  simp only [innerContent, lt_iSup_iff] at hr
  rcases hr with ⟨K, hKU, hr⟩
  refine ⟨K, hKU, K.2, hr.trans_le ?_⟩
  exact (μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)

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

Goal state before:
pp: case refine_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ.measure ↑K ≤ μ K

pp: case refine_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ K ≤ μ.measure ↑K

Tactic:
· apply ENNReal.le_of_forall_pos_le_add
    intro ε εpos _
    obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)
    calc
      μ.measure ↑K ≤ μ.measure (interior ↑K') := measure_mono K'_hyp.1
      _ ≤ μ K' := by
        rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
        exact μ.outerMeasure_interior_compacts K'
      _ ≤ μ K + ε := K'_hyp.right

Goal state after:
case refine_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ K ≤ μ.measure ↑K
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case left
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
⊢ ∃ x ∈ K₁.carrier, ∃ y, y⁻¹ ∈ V ∧ x * y = g₁⁻¹

Tactic:
refine ⟨_, h2g₂, (g₁ * g₂)⁻¹, ?_, ?_⟩
    · simp only [inv_inv, h1g₂]
    · simp only [mul_inv_rev, mul_inv_cancel_left]

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

Tactic:
simp only [inv_inv, h1g₃]

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

Goal state before:
pp: case refine_1
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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ g, (fun x ↦ g • x) '' A n
⊢ μ (Quotient.mk α_mod_G '' A n) < ∞

Tactic:
have measπAn : MeasurableSet (π '' A n) := by
      rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
      apply MeasurableSet.iUnion
      exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g

Goal state after:
case refine_1
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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ g, (fun x ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ μ (Quotient.mk α_mod_G '' A n) < ∞
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝¹ : PartialOrder X
x y : X
inst✝ : NullSingletonClass μ
⊢ ∫ (t : X) in Ioo x y, f t ∂μ = ∫ (t : X) in Ioc x y, f t ∂μ

Tactic:
integral_Ioc_eq_integral_Ioo

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝¹ : PartialOrder X
x y : X
inst✝ : NullSingletonClass μ
⊢ ∫ (t : X) in Ioo x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
by_cases h'f : AEStronglyMeasurable f (μ.restrict s); swap
  · rw [integral_non_aestronglyMeasurable h'f]
    apply integral_nonneg_of_ae
    apply (ae_restrict_iff₀ ?_).2
    · filter_upwards with x hx using (hf x hx).trans (h x hx)
    · exact nullMeasurableSet_le aemeasurable_const hg.aemeasurable
  refine integral_mono_of_nonneg ?_ hg ?_
  · apply (ae_restrict_iff₀ ?_).2
    · filter_upwards with x hx using hf x hx
    · exact nullMeasurableSet_le aemeasurable_const h'f.aemeasurable
  · apply (ae_restrict_iff₀ ?_).2
    · filter_upwards with x hx using h x hx
    · exact nullMeasurableSet_le h'f.aemeasurable hg.aemeasurable

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
x : E
| ‖⟪x, x⟫‖

Tactic:
rw [← inner_self_ofReal_re]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
| ‖↑(re ⟪x, x⟫)‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

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

Tactic:
real_inner_self_eq_norm_mul_norm

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
by
  constructor
  · intro hv i j
    split_ifs with h
    · simp [h, inner_self_eq_norm_sq_to_K, hv.norm_eq_one]
    · exact hv.inner_eq_zero h
  · intro h
    constructor
    · intro i
      have h' : ‖v i‖ ^ 2 = 1 ^ 2 := by
        rw [@norm_sq_eq_re_inner 𝕜, h i i]; simp
      have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _
      have h₂ : (0 : ℝ) ≤ 1 := zero_le_one
      rwa [sq_eq_sq₀ h₁ h₂] at h'
    · intro i j hij
      simpa [hij] using h i j

Goal state after: