mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [orthonormal_iff_ite]
  simp

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
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

Tactic:
refine ⟨fun h => h.comp f f.injective, fun h => ?_⟩

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
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 Subtype.val
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
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫ = ∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
⊢ ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
← sub_nonneg,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
h₂ : ∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫ = ∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫
h₃ : ∀ (z : 𝕜), re (z * (starRingEnd 𝕜) z) = ‖z‖ ^ 2
hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
⊢ 0 ≤ ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : TopologicalSpace M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : TopologicalSpace N
inst✝⁸ : Module R N
inst✝⁷ : AddCommMonoid O
inst✝⁶ : TopologicalSpace O
inst✝⁵ : Module R O
𝕜 : Type u_6
H : Type u_7
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid H
inst✝² : UniformSpace H
inst✝¹ : Module 𝕜 H
inst✝ : CompleteSpace H
K : ClosedSubmodule 𝕜 H
⊢ IsComplete (↑K).carrier

Tactic:
exact K.isClosed'.isComplete

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

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
K : Submodule 𝕜 E
a✝ b✝ : E
hx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
u : E
hu : u ∈ K
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
𝕜 : 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
K : Submodule 𝕜 E
a✝ b✝ : E
hx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
u : E
hu : u ∈ K
⊢ 0 = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪v, u⟫ = 0

Tactic:
rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hx : x ∈ Kᗮ
y : E
hy : y ∈ K.topologicalClosure
⊢ Continuous fun a ↦ ⟪a, x⟫

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hx : x ∈ Kᗮ
y : E
hy : y ∈ K.topologicalClosure
⊢ Continuous fun a ↦ 0

Tactic:
by fun_prop

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ⟪T x, y⟫ = (⟪T (x + y), x + y⟫ - ⟪T (x - y), x - y⟫ - 0 + 0) / 4

Tactic:
sub_zero,

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ⟪T x, y⟫ = (⟪T (x + y), x + y⟫ - ⟪T (x - y), x - y⟫ + 0) / 4
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re (↑(re ⟪T y, x⟫) + 0)) = ↑(re ⟪T y, x⟫) + 0

Tactic:
add_zero

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re ↑(re ⟪T y, x⟫)) = ↑(re ⟪T y, x⟫)
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x x✝¹ x✝ : E
⊢ ⟪↑(((rankOne 𝕜) x) x) x✝¹, x✝⟫_𝕜 = ⟪x✝¹, ↑(((rankOne 𝕜) x) x) x✝⟫_𝕜

Tactic:
by simp [inner_smul_left, inner_smul_right, mul_comm]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
⊢ y + z ∈ K

Tactic:
have hz' : z = 0 := by
      have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_symm]
      simpa [inner_add_right, hyz] using hv z hz

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hv : y + z ∈ Kᗮᗮ
hz' : z = 0
⊢ y + z ∈ K
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
⊢ ‖f x - d • y‖ = ‖f x₁ - (a + d • y) - (f x₂ - a)‖

Tactic:
congr 1

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
⊢ f x - d • y = f x₁ - (a + d • y) - (f x₂ - a)
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₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥K₂ + 0 = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂

Tactic:
add_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 ↥K₁
hd : finrank 𝕜 ↥K₂ = finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u : ↥K
v : E
⊢ ⟪K.starProjection v, ↑u⟫ = ⟪K.starProjection v, ↑u⟫ + 0

Tactic:
add_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
u : ↥K
v : E
⊢ ⟪K.starProjection v, ↑u⟫ = ⟪K.starProjection v, ↑u⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case add
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
hy : (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) y) = y i
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp ∞ (α × β)
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
by simpa only [ENNReal.coe_one, one_mul] using prod_lipschitzWith_ofLp ∞ α β x y

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ ‖toLp p (x₁ - x₂, 0 - 0)‖₊ = ‖x₁ - x₂‖₊

Tactic:
sub_zero,

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ ‖toLp p (x₁ - x₂, 0)‖₊ = ‖x₁ - x₂‖₊
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ ‖toLp p (0 - 0, y₁ - y₂)‖₊ = ‖y₁ - y₂‖₊

Tactic:
sub_zero,

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ ‖toLp p (0, y₁ - y₂)‖₊ = ‖y₁ - y₂‖₊
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝¹³ : DecidableEq n
inst✝¹² : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : StarRing A
inst✝⁵ : StarRing B
inst✝⁴ : StarRing R
inst✝³ : StarModule R A
inst✝² : StarModule R B
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : Uᴴ * U = 1 ∧ U * Uᴴ = 1
hV : Vᴴ * V = 1 ∧ V * Vᴴ = 1
⊢ (U ⊗ₖₜ[R] V)ᴴ * U ⊗ₖₜ[R] V = 1 ∧ U ⊗ₖₜ[R] V * (U ⊗ₖₜ[R] V)ᴴ = 1

Tactic:
simp [conjTranspose_kroneckerTMul, ← mul_kroneckerTMul_mul, hU, hV]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ toLp p (x.fst + 0, x.snd) = x

Tactic:
add_zero

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ toLp p (x.fst, x.snd) = x
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 (dist f g)

Tactic:
dist_eq_iSup

Goal state after:
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))
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ spectrum 𝕜 f = spectrum 𝕜 ↑f

Tactic:
ext μ

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
μ : 𝕜
⊢ μ ∈ spectrum 𝕜 f ↔ μ ∈ spectrum 𝕜 ↑f
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp p β
i : ι
⊢ ‖x.ofLp i‖ ≤ ‖x‖

Tactic:
simpa using dist_apply_le x 0 i

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

Goal state before:
pp: case inr
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
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ (∑ i,
        ‖((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                    (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
                  x').ofLp
              i‖ ^
          p.toReal) ^
      (1 / p.toReal) =
    (∑ i, ‖x'.ofLp i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
congr 1

Goal state after:
case inr.e_a
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
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ∑ i,
      ‖((WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
                  (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
                x').ofLp
            i‖ ^
        p.toReal =
    ∑ i, ‖x'.ofLp i‖ ^ p.toReal
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝) →
    ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i

Tactic:
rintro ⟨g, hg, rfl⟩

Goal state after:
case mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
hg : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1
⊢ ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ ∑ i, g i = ∑ i, t i • v i
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
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
hp : 1 ≤ p.toReal
this : 0 < p.toReal
hpt : p ≠ ∞
⊢ ↑‖(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:
congr 1

Goal state after:
case inr
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
hp : 1 ≤ p.toReal
this : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(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‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
i : ι
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

Tactic:
specialize h i
      rcases le_total (a i) 0 with hai | hai
      · rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
        exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
      · rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
        exact ⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
i : ι
_H : i ∈ Finset.univ
⊢ Continuous fun t ↦ t i • b i

Tactic:
by fun_prop

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Semiring 𝕜
inst✝² : (i : ι) → AddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : (i : ι) → TopologicalSpace (β i)
⊢ Continuous[Pi.topologicalSpace, topologicalSpace p β] fun a ↦ toLp p a

Tactic:
by fun_prop

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Semiring 𝕜
inst✝¹ : (i : ι) → NormedAddCommGroup (β i)
inst✝ : (i : ι) → Module 𝕜 (β i)
i : ι
⊢ Continuous[topologicalSpace p β, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ a.ofLp i

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ ∑' (x : ℕ), μ s = ∑' (n : ℕ), μ ({u n} + s)

Tactic:
congr 1

Goal state after:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ (fun x ↦ μ s) = fun n ↦ μ ({u n} + s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)

Tactic:
refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p ↦ Real.lt✝ (f p.1) p.2) (μ.prod volume)

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p ↦ Real.lt✝ p.2 (g p.1)) (μ.prod volume)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (fun p ↦ f p.1) (μ.prod volume)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (fun p ↦ g p.1) (μ.prod volume)

Tactic:
by fun_prop

Goal state after: