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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫

pp: case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0

pp: case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0

Tactic:
· rw [inner_smul_right]

Goal state after:
case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0

case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2 ↔ ‖y‖ • x = ‖x‖ • y

Tactic:
add_pow_two,

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ‖x‖ * ‖y‖ + ‖y‖ ^ 2 ↔ ‖y‖ • x = ‖x‖ • y
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝ : RCLike 𝕜
x y z : 𝕜
⊢ y * star (z • x) = (starRingEnd 𝕜) z * (y * star x)

Tactic:
by rw [star_def, smul_eq_mul, map_mul, mul_left_comm]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
⊢ w' - v = w

Tactic:
simp only [w', add_neg_cancel_right, sub_eq_add_neg]

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
G : Type u_8
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
y : F
f : E →L[𝕜] G
⊢ (f ∘SL toSpanSingleton 𝕜 x) ∘SL (innerSL 𝕜) y = toSpanSingleton 𝕜 (f x) ∘SL (innerSL 𝕜) y

Tactic:
comp_toSpanSingleton

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
⊢ (1 / ⟪b, b⟫_𝕜) • ⟪b, b⟫_𝕜 • a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c

Tactic:
by simp only [h, smul_smul]; ring_nf

Goal state after:
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 t : ClosedSubmodule R N
⊢ ↑(s ⊔ t) = closure (↑s ⊔ ↑t).carrier

Tactic:
simp only [← coe_toSubmodule, toSubmodule_sup]
  simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

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
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ ⟪v, u⟫ = 0

Tactic:
by
  rw [inner_eq_zero_symm]; exact inner_right_of_mem_orthogonal hu hv

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₂ : ClosedSubmodule 𝕜 E
inst✝¹ : (↑K₁).HasOrthogonalProjection
inst✝ : (↑K₂).HasOrthogonalProjection
h : K₁ᗮ = K₂ᗮ
⊢ K₁ = K₂

Tactic:
simpa using congr($hᗮ)

Goal state after:
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⟫ + ⟪v - K.starProjection v, ↑u⟫

Tactic:
rw [starProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_zero]

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

Goal state before:
pp: case mp.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
⊢ ∀ (i : { x // x ∈ insert e v }), ‖↑i‖ = 1

Tactic:
rintro ⟨a, ha'⟩
      rcases eq_or_mem_of_mem_insert ha' with ha | ha
      · simp [ha, he]
      · exact hv.1 ⟨a, ha⟩

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

Goal state before:
pp: a b : ℝ
⊢ volume.real (Ico a b) = max (b - a) 0

Tactic:
by
  simp [measureReal_def, ENNReal.toReal_ofReal']

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

Goal state before:
pp: a b : ℝ
⊢ volume.real (Icc a b) = max (b - a) 0

Tactic:
by
  simp [measureReal_def, ENNReal.toReal_ofReal']

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 ∈ Icc 0 1, x = ∑ i, t i • b i) ↔ x ∈ {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}

Tactic:
mem_ofPred_eq,

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

Goal state before:
pp: a b : ℝ
⊢ volume.real (Ioo a b) = max (b - a) 0

Tactic:
by
  simp [measureReal_def, ENNReal.toReal_ofReal']

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

Goal state before:
pp: a b : ℝ
⊢ volume.real (Ioc a b) = max (b - a) 0

Tactic:
by
  simp [measureReal_def, ENNReal.toReal_ofReal']

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✝⁵ : Fintype ι
inst✝⁴ : Semiring 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (α i)
inst✝ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
e : (i : ι) → α i ≃ₗᵢ[𝕜] β i
x : (i : ι) → α i
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i)).symm
⊢ ‖toLp ∞ ((LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) x)‖ = ‖toLp ∞ x‖

Tactic:
PiLp.norm_toLp,

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (α i)
inst✝ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
e : (i : ι) → α i ≃ₗᵢ[𝕜] β i
x : (i : ι) → α i
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i)).symm
⊢ ‖(LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) x‖ = ‖x‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
⊢ Measure.map (⇑(toLin' t.toMatrix)) volume = volume

Tactic:
refine (pi_eq fun s hs ↦ ?_).symm

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i, volume (s i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
⊢ ‖toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
rcases p.dichotomy with (h | h)

Goal state after:
case inl
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
⊢ ‖toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h.left.right
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ≤ 1

Tactic:
· change ∀ x : ι ⊕ ι', Sum.elim t s x ≤ 1
      aesop

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

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = uIcc (fun i ↦ 0) fun i ↦ 1

Tactic:
convert! parallelepiped_single (ι := ι) 1

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ #({J ∈ π.boxes | x ∈ Box.Icc J})

Tactic:
by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩

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
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ μ (s ∩ ({x} + r • t)) = μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n)) ∪ s ∩ ({x} + r • (t \ closedBall 0 ↑n)))

Tactic:
← inter_union_distrib_left,

Goal state after:
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
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ μ (s ∩ ({x} + r • t)) = μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n) ∪ ({x} + r • (t \ closedBall 0 ↑n))))
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁷ : RCLike 𝕜
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_6
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
h : (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b = (fun b i ↦ b.repr.symm (EuclideanSpace.single i 1)) b'
⊢ ↑b.repr.symm = ↑b'.repr.symm

Tactic:
by
      classical
        rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
        simp +instances only
        refine LinearMap.pi_ext fun i k => ?_
        have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
        rw [this, Pi.single_smul]
        replace h := congr_fun h i
        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
          coe_symm_linearEquiv, PiLp.toLp_single,
          LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
        rw [h]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rcases le_or_gt x (I.lower i) with h | _
  · rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
    exact WithBot.bot_ne_coe
  · refine (disjoint_splitLower_splitUpper I i x).ne ?_
    rwa [Ne, splitLower_eq_bot, not_le]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : π ∈ {π | l.MemBaseSet I c r π ∧ π.iUnion = ⊤.iUnion}
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}

Tactic:
mem_ofPred_eq,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
c : ℝ≥0
π₀ : Prepartition J := Prepartition.single J I h
r : (ι → ℝ) → ↑(Set.Ioi 0)
hr : l.RCond r
π : TaggedPrepartition I
hπ : l.MemBaseSet I c r π ∧ π.iUnion = ⊤.iUnion
⊢ (embedBox I J h) π ∈ {π | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
⊢ dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ↑ε * ‖y‖

Tactic:
dsimp [integralSum]

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
⊢ dist (∑ J ∈ π.boxes, μ.real ↑J • s.indicator (fun x ↦ y) (π.tag J)) (μ.real (s ∩ ↑I) • y) ≤ ↑ε * ‖y‖
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ I ∈
      { boxes := Finset.image (fun ν ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun I ↦ if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose,
        tag_mem_Icc := ⋯ } ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
TaggedPrepartition.mem_mk,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ I ∈ { boxes := Finset.image (fun ν ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯ } ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ (∀ (i : ι), (((Pi.basisFun ℝ ι).isUnitSMul ⋯).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Tactic:
Module.Basis.repr_isUnitSMul,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ (∀ (i : ι), ⋯.unit⁻¹ • ((Pi.basisFun ℝ ι).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
⊢ ‖integralSum f μ.toBoxAdditive.toSMul (π.filter fun x ↦ N (π.tag x) = n)‖ ≤ ↑(δ n)

Tactic:
dsimp [integralSum]

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
⊢ ‖∑ J ∈ (π.filter fun x ↦ N (π.tag x) = n).boxes, μ.toBoxAdditive J • f ((π.filter fun x ↦ N (π.tag x) = n).tag J)‖ ≤
    ↑(δ n)
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 ι
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π

Tactic:
by
  simp only [integralSum, Pi.add_apply, (vol _).map_add, Finset.sum_add_distrib]

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

Goal state before:
pp: case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det = f.toBasis.det

Tactic:
e.toBasis.det.eq_smul_basis_det f.toBasis

Goal state after:
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = f.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det = -f.toBasis.det

Tactic:
e.toBasis.det.eq_smul_basis_det f.toBasis

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = -f.toBasis.det