mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ)
⊢ Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i

Tactic:
convert! ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i

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 = (∫⁻ (x : X), ‖f x‖ₑ ∂μ i).toReal

ι : 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 μ)
⊢ ∑' (x : ι), ∫⁻ (x : X), ‖f x‖ₑ ∂μ x ≠ ∞
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨C, mul_lip⟩ := ‹LipschitzMul R›.lipschitz_mul

Goal state after:
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
⊢ Bornology.IsBounded (s * t)
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
⊢ IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

Tactic:
rw [isInducing_iff_nhds]
  refine fun f => eq_of_forall_le_iff fun l => ?_
  rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
    UniformFun.tendsto_iff_tendstoUniformly]
  simp [comp_def]

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

Goal state before:
pp: case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤
    max (dist g₁ g₂) (dist (h₁.domRestrict (range ⇑f)ᶜ) (h₂.domRestrict (range ⇑f)ᶜ))

Tactic:
simp only [extend_apply' hx]

Goal state after:
case refine_1.inr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ y, f y = x
⊢ dist (h₁ x) (h₂ x) ≤ max (dist g₁ g₂) (dist (h₁.domRestrict (range ⇑f)ᶜ) (h₂.domRestrict (range ⇑f)ᶜ))
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₂ : α →ᵇ β
x : α
⊢ dist ((c • f₁) x) ((c • f₂) x) ≤ dist c 0 * dist f₁ f₂

Tactic:
refine (dist_smul_pair c (f₁ x) (f₂ x)).trans ?_

Goal state after:
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₂ : α →ᵇ β
x : α
⊢ dist c 0 * dist (f₁ x) (f₂ x) ≤ dist c 0 * dist f₁ f₂
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
c : ℝ
hc : 0 ≤ c
⊢ ‖f + g‖ ≤ c ↔ max ‖f‖ ‖g‖ ≤ c

Tactic:
simp_rw [norm_le hc, hfg', max_le_iff, norm_le hc, forall_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E✝ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : SeminormedAddCommGroup E✝
inst✝² : Nonempty α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : Nontrivial E
⊢ NontrivialTopology C(α, E)

Tactic:
by
  simpa [nontrivialTopology_iff_exists_norm_ne_zero] using exists_ne (0 : C(α, E))

Goal state after:
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 α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  -- integrability for `μ` implies integrability for `μ'`.
  have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg =>
    Integrable.of_measure_le_smul hc' hμ'_le hg
  -- We use `Integrable.induction`
  apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
  · intro c s hs hμs
    have hμ's : μ' s ≠ ∞ := by
      refine ((hμ'_le s).trans_lt ?_).ne
      rw [Measure.smul_apply, smul_eq_mul]
      exact ENNReal.mul_lt_top hc'.lt_top hμs
    rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
  · intro f₂ g₂ _ hf₂ hg₂ h_eq_f h_eq_g
    rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]
  · refine isClosed_eq (continuous_setToFun hT) ?_
    have :
      (fun f : α →₁[μ] E => setToFun μ' T hT' f) = fun f : α →₁[μ] E =>
        setToFun μ' T hT' ((h_int f (L1.integrable_coeFn f)).toL1 f) := by
      ext1 f; exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
    rw [this]
    exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)
  · intro f₂ g₂ hfg _ hf_eq
    have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
    rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), max (-f a) 0 ∂μ ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ ∫ (a : α), max (f a) 0 ∂μ + ∫ (a : α), max (f a) 0 ∂μ ≤ 2 * (μ univ).toReal * ↑r

Tactic:
rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
rw [h'α.topology_eq_generate_intervals] at h
  simp [leftLim, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = f a

Tactic:
rw [h'α.topology_eq_generate_intervals] at h
  simp [leftLim, h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with y (hy : x ≤ y)

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ rightLim f y ∈ s
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
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
hx : ∀ (y : R), y ≤ x
y : R
hy : x ≤ y
⊢ y = x

Tactic:
exact le_antisymm (hx y) hy

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
a b : R
this : Nonempty R
a' b' : R
h : Ioc a b \ botSet ⊆ Ioc a' b'
ab : a < b
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal

Tactic:
simp only [Ioc_sdiff_botSet] at h

Goal state after:
case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
this : Nonempty R
a' b' : R
ab : a < b
h : Ioc a b ⊆ Ioc a' b'
⊢ (↑f b - ↑f a).toNNReal ≤ (↑f b' - ↑f a').toNNReal
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✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
⊢ NullMeasurableSet (⋃ g, g • s) μ

Tactic:
exact .iUnion h_meas

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : μ.innerContent U ≤ μ K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
exact ⟨K, h1K, by grw [h2K, μ.le_outerMeasure_compacts K]⟩

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 : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂ν = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂ν

Tactic:
← lintegral_sum_measure,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂ν = ∫⁻ (a : α), f a ∂sum fun g ↦ ν.restrict (g • s)
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
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by
  let k := f ⁻¹' {0}
  have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
  calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_sdiff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, Set.mem_sdiff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_sdiff hk (h'aux.mono hts le_rfl)]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : Set G
f : Compacts G → ℝ
⊢ f ∈ haarProduct K₀ ↔ ∀ (K : Compacts G), f K ∈ Icc 0 ↑(index (↑K) K₀)

Tactic:
by
  simp only [haarProduct, Set.pi, forall_prop_of_true, mem_univ, mem_ofPred_eq]

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
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : Nonempty R
H : ∃ l, Tendsto (↑f) atTop (𝓝 l)
⊢ ∃ u, Tendsto (↑f) atTop (𝓝 u)

Tactic:
exact H

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
C : ℝ
h : ∀ (x : R), |↑f x| ≤ C
h✝ : Nonempty R
u : ℝ
hu : Tendsto (↑f) atTop (𝓝 u)
H : ∃ l, Tendsto (↑f) atBot (𝓝 l)
⊢ ∃ l, Tendsto (↑f) atBot (𝓝 l)

Tactic:
exact H

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

Goal state before:
pp: case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H✝ : Integrable f μ
g : X → ℝ := fun x ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∉ s
⊢ g x ≤ ENNReal.toReal 1

Tactic:
apply le_trans _ zero_le_one

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H✝ : Integrable f μ
g : X → ℝ := ⋯
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∉ s
⊢ g x ≤ 0
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₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
_h₁ : IsClosed[inst✝¹] ↑K₁
h₂ : IsClosed[inst✝¹] ↑K₂
⊢ ⟨chaar K₀ (K₁ ⊔ K₂), ⋯⟩ = ⟨chaar K₀ K₁, ⋯⟩ + ⟨chaar K₀ K₂, ⋯⟩

Tactic:
by simp only [chaar_sup_eq h]; rfl

Goal state after:
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
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarMeasure K₀).Regular

Tactic:
apply Regular.smul

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ ≠ ∞
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : ↑K
this : ⟪u - v, ↑w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, ↑w - v⟫_ℝ

Tactic:
by linarith

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ⨅ w, ‖u - ↑w‖ ≤ (fun w ↦ ‖u - ↑w‖) ⟨v, hv⟩

Tactic:
apply ciInf_le

Goal state after:
case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ BddBelow (Set.range fun w ↦ ‖u - ↑w‖)
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
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
    replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
    simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d

Tactic:
have h₄ := calc
    b = (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b := by simp_all
    _ = (1 / ⟪a, a⟫_𝕜) • (⟪a, a⟫_𝕜 • b) := by simp only [smul_smul]; ring_nf
    _ = ((⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d := by
      simp_rw [h₂, h₃, inner_smul_right, smul_smul]; ring_nf

Goal state after:
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
F : Type u_8
H : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
⊢ ∃ α β, ∃ (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
inst✝¹ : ContinuousAdd N
inst✝ : ContinuousConstSMul R N
s : ClosedSubmodule R N
⊢ (↑s).closure = s

Tactic:
ext x; simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
inst✝² : Module R N
f : M ≃L[R] N
inst✝¹ : T1Space M
inst✝ : T1Space N
⊢ (mapEquiv f) ⊥ = ⊥

Tactic:
ext x; simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : Module R N
f : M ≃L[R] N
⊢ (mapEquiv f) ⊤ = ⊤

Tactic:
ext x; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
this : s₁ ⊓ s₂ ⊆ s₁
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2

Tactic:
· exact fun i => sq_nonneg _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∀ (i : ι), 0 ≤ ‖f i‖ ^ 2

Tactic:
· exact fun i => sq_nonneg _

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊤ᗮ = ⊥

Tactic:
ext x; simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
ext x; simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }

Tactic:
ext x; simp

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂

Tactic:
rw [Submodule.mem_sup]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
inst✝ : (↑K).HasOrthogonalProjection
⊢ Kᗮᗮ = K

Tactic:
ext x; simp

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = ↑((-1) ^ finrank 𝕜 ↥Kᗮ)

Tactic:
Units.val_pow_eq_pow_val

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = ↑(-1) ^ finrank 𝕜 ↥Kᗮ