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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ 0 < (μ.restrict s) (support f) ↔ 0 < μ (support f ∩ s)

Tactic:
Measure.restrict_apply₀

Goal state after:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ 0 < μ (support f ∩ s) ↔ 0 < μ (support f ∩ s)

X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (support f) (μ.restrict s)
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
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ ν (⋃ i, (fun x ↦ i • x) '' A n ∩ s) ≤ ν (A n)

Tactic:
rw [fund_dom_s.measure_eq_tsum (A n)]

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)
⊢ ν (⋃ i, (fun x ↦ i • x) '' A n ∩ s) ≤ ∑' (g : G), ν (g • A n ∩ s)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᵐ[μ.restrict s] g
hE : CompleteSpace E
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᵐ[μ.restrict s] g
hE : ¬CompleteSpace E
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
· exact integral_mono_ae hf hg h

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᵐ[μ.restrict s] g
hE : ¬CompleteSpace E
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ re (inner 𝕜 x x)

Tactic:
rw [← InnerProductSpace.norm_sq_eq_re_inner]; apply sq_nonneg

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

Goal state before:
pp: case hs
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᵐ[μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
x : X
hx : x ∈ s
⊢ 1 ≤ ENNReal.ofReal (f x)

Tactic:
simpa using ENNReal.ofReal_le_ofReal (hs x hx)

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
inst✝ : Nonempty R
hf : Tendsto (↑f) atTop atTop
⊢ f.measure univ = ∞

Tactic:
inhabit R
  rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf default]
  exact measure_mono (subset_univ _)

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 : 𝕝
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = lintegral μ (E.indicator fun x ↦ 1)

pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Tactic:
· rw [lintegral_indicator E_mble]
    simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Goal state after:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
⊢ tF = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
by
  let p : Seminorm 𝕜 F := @normSeminorm 𝕜 F _ cd.toNormedAddCommGroup.toSeminormedAddCommGroup
    InnerProductSpace.Core.toNormedSpace
  suffices WithSeminorms (fun (i : Fin 1) ↦ p) by
    rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
    simp
  have : p.ball 0 1 = {v | re (cd.inner v v) < 1} := by
    ext v
    simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_ofPred_eq, p]
    change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1
    conv_lhs => rw [show (1 : ℝ) = √1 by simp]
    rw [sqrt_lt_sqrt_iff]
    exact InnerProductSpace.Core.inner_self_nonneg
  rw [withSeminorms_iff_mem_nhds_isVonNBounded, this]
  refine ⟨?_, h'⟩
  have A : ContinuousAt (fun (v : F) ↦ re (cd.inner v v)) 0 := by fun_prop
  have B : Set.Iio 1 ∈ 𝓝 (re (cd.inner 0 0)) := by
    simp only [InnerProductSpace.Core.inner_zero_left, map_zero]
    exact Iio_mem_nhds (by positivity)
  exact A B

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
K₀ : PositiveCompacts G
g : G
K : Compacts G
⊢ (haarContent K₀) (Compacts.map (fun x ↦ g * x) ⋯ K) = (haarContent K₀) K

Tactic:
simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using!
    is_left_invariant_chaar g K

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 y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
⊢ x = y

Tactic:
by
  rw [← sub_eq_zero]; exact hS.eq_zero_of_inner_right 𝕜 (by simpa [inner_sub_right, sub_eq_zero])

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

Goal state before:
pp: Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
⊢ ∀ᶠ (x : X) in 𝓝[s] q, ‖∫ (y : Y), (L (g y)) (f x y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε

Tactic:
filter_upwards [v_mem, self_mem_nhdsWithin] with p hp h'p

Goal state after:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y ↦ (L (g y)) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖∫ (y : Y), (L (g y)) (f p y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

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

Tactic:
simpa [hij] using h i j

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0

Tactic:
orthonormal_iff_ite

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq E
s : Set E
⊢ (∀ (i j : { x // x ∈ s }), ⟪↑i, ↑j⟫ = if i = j then 1 else 0) ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0
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
ι' : Type u_5
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
⊢ Orthonormal 𝕜 (v ∘ f)

Tactic:
orthonormal_iff_ite

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
⊢ ∀ (i j : ι'), ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0
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 : ι → E
hv : Function.Injective v
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

Tactic:
let f : ι ≃ Set.range v := Equiv.ofInjective v hv

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v
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 : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ Orthonormal 𝕜 w

Tactic:
orthonormal_iff_ite

Goal state after:
𝕜 : 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
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
⊢ ⟪f x, y⟫ = ⟪x, f.symm y⟫

Tactic:
conv_lhs => rw [← f.apply_symm_apply y, f.inner_map_map]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → re ⟪T x, y⟫_𝕜 ≤ C
⊢ ‖T‖ ≤ C

Tactic:
refine opNorm_le_of_unit_norm hC fun x hx ↦ ?_
  by_cases hTx : ‖T x‖ = 0
  · rwa [hTx]
  · specialize h x (((‖T x‖⁻¹ : ℝ) : 𝕜) • T x) hx (by simp [norm_smul, hTx])
    rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner ℝ ((↑ℝ T) x) y = inner ℝ x ((↑ℝ T) y)

Tactic:
by simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
h : S.range ≤ T.range
v : E
hv : T v = 0
y : E
hy : T y = S (S v)
⊢ S v = 0

Tactic:
← inner_self_eq_zero (𝕜 := 𝕜),

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
S T : E →ₗ[𝕜] E
hS : S.IsSymmetric
hT : T.IsSymmetric
h : S.range ≤ T.range
v : E
hv : T v = 0
y : E
hy : T y = S (S v)
⊢ ⟪S v, S v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
hqp : q ∘ₗ p = p
x y : E
⊢ ⟪y, p (q x)⟫ = ⟪y, p x⟫

Tactic:
← hp.isSymmetric _,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
hqp : q ∘ₗ p = p
x y : E
⊢ ⟪p y, q x⟫ = ⟪p y, x⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ ≤ K.topologicalClosure

Tactic:
convert Submodule.orthogonal_orthogonal_monotone K.le_topologicalClosure

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = K.topologicalClosureᗮᗮ
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g h : PiLp ∞ β
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl.inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g h : PiLp ∞ β
h✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)

case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g h : PiLp ∞ β
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case neg
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h✝ : ¬p = ∞
⊢ 0 ≤ (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact rpow_nonneg (Fintype.sum_nonneg fun i ↦ by positivity) (1 / p.toReal)

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl.inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α✝
inst✝⁵ : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝⁴ : SeminormedAddCommGroup α
inst✝³ : SeminormedAddCommGroup β
R : Type u_6
inst✝² : NormedField R
inst✝¹ : NormedSpace R α
inst✝ : NormedSpace R β
this : SeminormedAddCommGroup (α × β) := seminormedAddCommGroupToProd p α β
⊢ NormedSpace R (α × β)

Tactic:
exact ⟨fun x y ↦ norm_smul_le x (toLp p y)⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ : WithLp p (α × β)
⊢ ∀ (x2 : WithLp p (α × β)), edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2) = edist x1✝ x2

Tactic:
_

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ x2✝ : WithLp p (α × β)
⊢ edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2✝) = edist x1✝ x2✝
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r

Tactic:
· lift r to ℝ≥0 using hr
    rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ((∀ (i : ι), 0 ≤ t i) ∧ ∀ (i : ι), t i ≤ 1 i) ∧ ∀ (i : ι), (b.repr x) i = t i) ↔
    ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1

Tactic:
Pi.one_apply,

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ((∀ (i : ι), 0 ≤ t i) ∧ ∀ (i : ι), t i ≤ 1) ∧ ∀ (i : ι), (b.repr x) i = t i) ↔
    ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun x ↦ a * x) volume) s = ofReal |a⁻¹| * volume s

Tactic:
by rw [map_volume_mul_left h]; rfl

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 x ≤ t x ∧ t x ≤ 1 x) ∧ x = ∑ x, Pi.single x (t x • a x)) ↔
    ∀ (x_1 : ι), min (0 x_1) (a x_1) ≤ x x_1 ∧ x x_1 ≤ max (0 x_1) (a x_1)

Tactic:
Pi.one_apply,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 x ≤ t x ∧ t x ≤ 1) ∧ x = ∑ x, Pi.single x (t x • a x)) ↔
    ∀ (x_1 : ι), min (0 x_1) (a x_1) ≤ x x_1 ∧ x x_1 ≤ max (0 x_1) (a x_1)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
ι✝ : Type u_2
α✝ : ι✝ → Type u_3
β : ι✝ → Type u_4
hp : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : Type u_6
p : ℝ≥0∞
α : ι ⊕ κ → Type u_7
inst✝⁴ : Fintype ι
inst✝³ : Fintype κ
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)
inst✝ : (i : ι ⊕ κ) → Module 𝕜 (α i)
x : (i : ι ⊕ κ) → α i
⊢ ‖(WithLp.linearEquiv p 𝕜 ((i : ι ⊕ κ) → α i) ≪≫ₗ LinearEquiv.sumPiEquivProdPi 𝕜 ι κ α ≪≫ₗ
            (WithLp.linearEquiv p 𝕜 ((s : ι) → α (Sum.inl s))).symm.prodCongr
              (WithLp.linearEquiv p 𝕜 ((t : κ) → α (Sum.inr t))).symm ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 (WithLp p ((s : ι) → α (Sum.inl s)) × WithLp p ((t : κ) → α (Sum.inr t)))).symm)
        ((WithLp.linearEquiv p 𝕜 ((i : ι ⊕ κ) → α i)).symm x)‖ =
    ‖(WithLp.linearEquiv p 𝕜 ((i : ι ⊕ κ) → α i)).symm x‖

Tactic:
obtain rfl | hp := p.dichotomy
    · simp [← Finset.univ_disjSum_univ, Finset.sup_disjSum, Pi.norm_def]
    · have : 0 < p.toReal := by positivity
      have hpt : p ≠ ⊤ := (toReal_pos_iff_ne_top p).mp this
      simp_rw [← coe_nnnorm]; congr 1 -- convert to nnnorm to avoid needing positivity arguments
      simp [nnnorm_eq_sum hpt, WithLp.prod_nnnorm_eq_add hpt, NNReal.rpow_inv_rpow this.ne']

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

Goal state before:
pp: case mpr.refine_2.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≠ 0
⊢ x i = x i / a i * a i

Tactic:
div_mul_cancel₀ _ hai

Goal state after:
case mpr.refine_2.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≠ 0
⊢ x i = x i