mathlib-initiative/mathlib-tactics huggingface dataset:
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
v : E
⊢ ‖K.orthogonalProjectionOnto v‖ ≤ ‖v‖

Tactic:
calc
  ‖orthogonalProjectionOnto K v‖ ≤ ‖orthogonalProjectionOnto K‖ * ‖v‖ :=
    K.orthogonalProjectionOnto.le_opNorm _
  _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjectionOnto_norm_le K
  _ = _ := by simp

Goal state after:
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
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
have fsumeq : ∀ n : ℕ, f (∑ i ∈ Finset.range n, u i) = y - h^[n] y := by
    intro n
    induction n with
    | zero => simp [f.map_zero]
    | succ n IH => rw [sum_range_succ, f.map_add, IH, iterate_succ_apply', sub_add]

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
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero 𝕜
i : ι
a : 𝕜
j : ι
⊢ Pi.single i a j = if j = i then a else 0

Tactic:
← Pi.single_apply i a j

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero 𝕜
i : ι
a : 𝕜
j : ι
⊢ Pi.single i a j = Pi.single i a j
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ (Finset.univ.sup fun b ↦ ‖f.ofLp b‖₊) = ⨆ i, ‖f.ofLp i‖₊

Tactic:
Finset.sup_univ_eq_ciSup

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ⨆ i, ‖f.ofLp i‖₊ = ⨆ i, ‖f.ofLp i‖₊
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1

Tactic:
parallelepiped,

Goal state after:
case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ (fun t ↦ ∑ i, t i • (b.reindex e) i) '' Icc 0 1 = Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
right

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ (parallelepiped fun x ↦ -1) = Icc (-1) 0

Tactic:
parallelepiped,

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ (fun a ↦ ∑ x, a x • -1) '' Icc 0 1 = Icc (-1) 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

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

Tactic:
· simp only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero,
      one_mul, nnnorm_eq_ciSup, Function.const_apply, ciSup_const]

Goal state after:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Tactic:
← AffineSubspace.direction_eq_top_iff_of_nonempty hne

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), ∃ z, ↑z = -(b.repr m) i + (b.repr n) i) ↔
    ∀ (i : ι), (⇑(-b.repr m) + ⇑(b.repr n)) i ∈ Set.range ⇑(algebraMap ℤ K)

Tactic:
Finsupp.coe_neg,

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), ∃ z, ↑z = -(b.repr m) i + (b.repr n) i) ↔
    ∀ (i : ι), (-⇑(b.repr m) + ⇑(b.repr n)) i ∈ Set.range ⇑(algebraMap ℤ K)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ i ∈ A, T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ s \ u ∪ ⋃ p ∈ A, s ∩ T p

Tactic:
right

Goal state after:
case pos
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p✝ : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p✝ x
T : ↑s × ↑s → Set ℝ := ⋯
u : Set ℝ := ⋯
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ i ∈ A, T i
p : ↑s × ↑s
pA : p ∈ A
xp : x ∈ T p
⊢ x ∈ ⋃ p ∈ A, s ∩ T p
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr.inr
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
hs : s.Nonempty
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
by_cases h : finrank ℝ E = 0

Goal state after:
case pos
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
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

case neg
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
hs : s.Nonempty
h : ¬finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (closedBall x r) - μ (ball x r) = 0

Tactic:
addHaar_ball_of_pos μ _ h,

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ μ (closedBall x r) - ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1) = 0
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
l u : ι → ℝ
⊢ mk' l u = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
mk'

Goal state after:
ι : Type u_1
l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ mk' l u = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper

Tactic:
mk'

Goal state after:
ι : Type u_1
l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
      ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
l u : ι → ℝ
⊢ ↑(mk' l u) = univ.pi fun i ↦ Ioc (l i) (u i)

Tactic:
mk'

Goal state after:
ι : Type u_1
l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    univ.pi fun i ↦ Ioc (l i) (u i)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
⊢ π.biUnionIndex πi J ≤ I

Tactic:
by_cases hJ : J ∈ π.biUnion πi

Goal state after:
case pos
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

case neg
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I
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 u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
T : (R * r) • t' = r • t
⊢ (R * r) • u' = r • u

Tactic:
rw [mul_comm, hu', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
exact sup_union

Goal state after:
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:
← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective

Goal state after:
ι : 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 ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm = ↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
inst✝ : Fintype ι
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion

Tactic:
exact sup_union

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ (b.repr v).ofLp i = ⟪EuclideanSpace.single i 1, b.repr v⟫

Tactic:
EuclideanSpace.inner_single_left

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : E
i : ι
⊢ (b.repr v).ofLp i = (starRingEnd 𝕜) 1 * (b.repr v).ofLp i
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ Orthonormal 𝕜 ⇑b

Tactic:
rw [orthonormal_iff_ite]
    intro i j
    rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
      EuclideanSpace.inner_single_left, PiLp.single_apply, map_one, one_mul]

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 | _

Goal state after:
case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ I.splitLower i x ≠ I.splitUpper i x

case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ I.splitUpper i x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
right

Goal state after:
case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitUpper i x
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Tactic:
exact h₃.not_gt h₂.2

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

Goal state before:
pp: case inr
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x} ∨ ↑J₁ = ↑I ∩ {y | x < y i}

Tactic:
right

Goal state after:
case inr
ι : Type u_1
I J : Box ι
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | x < y i}
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ (isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1

Tactic:
simp [Complex.isometryOfOrthonormal, ← v.sum_repr_symm]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hιY : Fintype.card ι = Y.card := by
    refine card_ι.symm.trans ?_
    exact Module.finrank_eq_card_finset_basis b₀.toBasis

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
⊢ ∃ b, ∀ i ∈ s, b i = v i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
⊢ (prepartition n B).IsPartition

Tactic:
refine fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ (⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 = 0 ∨ ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) = 0) ∨ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
right

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
right

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
right

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
right

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (↑((∏ i, w i)⁻¹ * ∏ i, w i) • (e.unitsSMul w).det)

Tactic:
simp only [inv_mul_cancel, Units.val_one, one_smul]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (e.unitsSMul w).det
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
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
⊢ HasIntegral I l f₁ vol₁ y ↔ HasIntegral I l f₂ vol₂ y

Tactic:
unfold HasIntegral
  refine Filter.tendsto_congr (fun π ↦ integralSum_congr hf (hvol.mono ?_))
  intro J hJ
  simp [π.le_of_mem' J hJ]

Goal state after: