mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU✝ : π.iUnion = ↑I \ π₁.iUnion
hπU : π.iUnion = ↑I \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂

Tactic:
]

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c₁ c₂ : ℝ≥0
ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
hpos₁ : 0 < ε₁
hpos₂ : 0 < ε₂
h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁
h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂
HU : π₁.iUnion = π₂.iUnion
π : Prepartition I
hπU✝ : π.iUnion = ↑I \ π₁.iUnion
hπU : π.iUnion = ↑I \ π₂.iUnion
hπc₁ : l.bDistortion = true → π.distortion ≤ c₁
hπc₂ : l.bDistortion = true → π.distortion ≤ c₂
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
πr : TaggedPrepartition I := π.toSubordinate r
H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU✝ r)) (integral I l f vol) ≤ ε₁
⊢ dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = n✝ + 1)
o : Orientation ℝ E (Fin (n✝ + 1))
b : OrthonormalBasis (Fin (n✝ + 1)) ℝ E
v : Fin (n✝ + 1) → E
⊢ |b.toBasis.det v| = |b.toBasis.det v|

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < Fintype.card ι

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ 0 < Fintype.card ι
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
⊢ LinearMap.det ↑f < 0 ↔ LinearMap.det ↑f < 0

Tactic:
]

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

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
⊢ ∏ x, |⟪b x, v x⟫| ≤ ∏ i, ‖v i‖

Tactic:
]

Goal state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
⊢ ∏ x, |⟪b x, v x⟫| ≤ ∏ i, ‖v i‖
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) +
        dist (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) +
      dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    μ.real ↑I * ↑ε + ↑ε + ↑ε

Tactic:
]

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) +
        dist (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) +
      dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    μ.real ↑I * ↑ε + ↑ε + ↑ε
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case right
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε / 2 + ε / 2}

Tactic:
]

Goal state after:
case right
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε / 2 + ε / 2}
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (v.prod w) (Sum.inl a) =
        Sum.elim (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w)
          (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (v.prod w) (Sum.inr b) =
        Sum.elim (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ (∀ (a : ι₁),
      (v.prod w) (Sum.inl a) =
        Sum.elim (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w)
          (Sum.inl a)) ∧
    ∀ (b : ι₂),
      (v.prod w) (Sum.inr b) =
        Sum.elim (WithLp.toLp 2 ∘ ⇑(LinearMap.inl 𝕜 E F) ∘ ⇑v) (WithLp.toLp 2 ∘ ⇑(LinearMap.inr 𝕜 E F) ∘ ⇑w) (Sum.inr b)
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).fst‖ ^ 2 +
      ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).snd‖ ^ 2 =
    ‖K.orthogonalProjectionOnto x✝‖ ^ 2 + ‖Kᗮ.orthogonalProjectionOnto x✝‖ ^ 2

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).fst‖ ^ 2 +
      ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).snd‖ ^ 2 =
    ‖K.orthogonalProjectionOnto x✝‖ ^ 2 + ‖Kᗮ.orthogonalProjectionOnto x✝‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
⊢ ∏ x, |⟪b x, v x⟫| = ∏ i, ‖v i‖

Tactic:
]

Goal state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
⊢ ∏ x, |⟪b x, v x⟫| = ∏ i, ‖v i‖
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun p ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤
    𝓤 F

Tactic:
]

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun p ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤
    𝓤 F
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ 0 = 0

pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ ‖v i‖ = 0

pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪b i, v i⟫| = 0

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ ‖v i‖ = 0

case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪b i, v i⟫| = 0
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
⊢ ‖y‖ = ⨅ x, ‖↑(f y) - ↑x‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
⊢ ‖y‖ = ⨅ x, ‖↑(f y) - ↑x‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖

pp: case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)

Tactic:
]

Goal state after:
case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖

case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: case e'_3
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑((Equiv.neg ↥K) x)‖ = ⨅ a, ‖↑(f y) + ↑a‖

Tactic:
]

Goal state after:
case e'_3
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑((Equiv.neg ↥K) x)‖ = ⨅ a, ‖↑(f y) + ↑a‖
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (∑ J ∈ π.boxes, (μ.toBoxAdditive.toSMul J) (g (π.tag J)))
      (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) ≤
    ∑ i ∈ π.boxes, μ.real ↑i * ↑ε

Tactic:
]

Goal state after:
case refine_1
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
⊢ dist (∑ J ∈ π.boxes, (μ.toBoxAdditive.toSMul J) (g (π.tag J)))
      (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) ≤
    ∑ i ∈ π.boxes, μ.real ↑i * ↑ε
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
⊢ (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) e.toBasis.orientation

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
⊢ (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) e.toBasis.orientation
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
y : E ⧸ K
⊢ ‖y‖ ^ 2 = ‖y‖ ^ 2

Tactic:
]

Goal state after: