mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
have : FiniteDimensional ℝ (ι → ℝ) := by infer_instance

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
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
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
ι' : Type u_4
e : ι ≃ ι'
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b

Tactic:
ext

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
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ x✝ ∈ fundamentalDomain (b.reindex e) ↔ x✝ ∈ fundamentalDomain b
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
⊢ fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x ↦ Set.Ico 0 1

Tactic:
ext

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
x✝ : ι → ℝ
⊢ x✝ ∈ fundamentalDomain (Pi.basisFun ℝ ι) ↔ x✝ ∈ Set.univ.pi fun x ↦ Set.Ico 0 1
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 : E
i : ι
⊢ (b.repr m - b.repr ↑(floor b m)) i = Int.fract ((b.repr m) i)

Tactic:
Finsupp.coe_sub,

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 : E
i : ι
⊢ (⇑(b.repr m) - ⇑(b.repr ↑(floor b m))) i = Int.fract ((b.repr m) i)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : 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
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x

Tactic:
constructor

Goal state after:
case left
μ : 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
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x

case right
μ : 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
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x ↦ Set.Ico 0 1
⊢ fundamentalDomain b = ⇑↑b.equivFun ⁻¹' D

Tactic:
ext

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x ↦ Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ⇑↑b.equivFun ⁻¹' D
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| * ∏ i, 1 = ENNReal.ofReal |(Matrix.of ⇑b).det|

Tactic:
Finset.prod_const_one,

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| * 1 = ENNReal.ofReal |(Matrix.of ⇑b).det|
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ volume.real (fundamentalDomain b) = |(Matrix.of ⇑b).det|

Tactic:
simp [measureReal_def]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
⊢ μ (symmDiff (fundamentalDomain b) (parallelepiped ⇑b)) = 0

Tactic:
symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
⊢ μ (parallelepiped ⇑b \ fundamentalDomain b) = 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
⊢ Subtype.val ∘ ⇑(quotientEquiv b) '' ↑(Submodule.map (span ℤ (Set.range ⇑b)).mkQ L) ⊆ fundamentalDomain b ∩ ↑L

Tactic:
rintro _ ⟨_, ⟨⟨x, ⟨h_mem, rfl⟩⟩, rfl⟩⟩

Goal state after:
case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ (Subtype.val ∘ ⇑(quotientEquiv b)) ((span ℤ (Set.range ⇑b)).mkQ x) ∈ fundamentalDomain b ∩ ↑L
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).iUnion = ↑J

Tactic:
by simp [iUnion_def]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ π₁ ≤ π₂ → (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion

case mpr
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion → π₁ ≤ π₂
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (π.biUnion fun x ↦ ⊤) = π

Tactic:
ext

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
J✝ : Box ι
⊢ (J✝ ∈ π.biUnion fun x ↦ ⊤) ↔ J✝ ∈ π
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') ↔ ∃ J' ∈ π₁, J ∈ πi₂ J'

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'

case mpr
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.closedBall 0 r = {x | ∑ i, x.ofLp i ^ 2 ≤ r ^ 2}

Tactic:
ext

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ i, x.ofLp i ^ 2 ≤ r ^ 2}
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 ι
I J : Finset ι'
hIJ : I ⊆ J
x y : EuclideanSpace 𝕜 ↥J
⊢ toLp 2 (Finset.restrict₂ hIJ (x + y).ofLp) =
    toLp 2 (Finset.restrict₂ hIJ x.ofLp) + toLp 2 (Finset.restrict₂ hIJ y.ofLp)

Tactic:
ext

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 ι
I J : Finset ι'
hIJ : I ⊆ J
x y : EuclideanSpace 𝕜 ↥J
i✝ : ↥I
⊢ (toLp 2 (Finset.restrict₂ hIJ (x + y).ofLp)).ofLp i✝ =
    (toLp 2 (Finset.restrict₂ hIJ x.ofLp) + toLp 2 (Finset.restrict₂ hIJ y.ofLp)).ofLp i✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) ↔ ∃ J', (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1) → ∃ J', (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J'

case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', (∃ J'_1 ∈ π, J' ∈ πi J'_1) ∧ J ∈ πi' (π.biUnionIndex πi J') J') → ∃ J' ∈ π, ∃ J'_1 ∈ πi J', J ∈ πi' J' J'_1
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 ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace 𝕜 ↥J
⊢ toLp 2 (Finset.restrict₂ hIJ (m • x).ofLp) = (RingHom.id 𝕜) m • toLp 2 (Finset.restrict₂ hIJ x.ofLp)

Tactic:
ext

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 ι
I J : Finset ι'
hIJ : I ⊆ J
m : 𝕜
x : EuclideanSpace 𝕜 ↥J
i✝ : ↥I
⊢ (toLp 2 (Finset.restrict₂ hIJ (m • x).ofLp)).ofLp i✝ =
    ((RingHom.id 𝕜) m • toLp 2 (Finset.restrict₂ hIJ x.ofLp)).ofLp i✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict J

case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (∀ J ∈ π, πi J ≤ π'.restrict J) → π.biUnion π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 ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
⊢ U.orthogonalProjectionOnto = ∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ ↑(U.orthogonalProjectionOnto x✝) = ↑((∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)) x✝)
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 ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
⊢ U.starProjection = ∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
x✝ : E
⊢ U.starProjection x✝ = (∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)) x✝
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
⊢ ∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) (b i) = ContinuousLinearMap.id 𝕜 E

Tactic:
ext

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
x✝ : E
⊢ (∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) (b i)) x✝ = (ContinuousLinearMap.id 𝕜 E) x✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
⊢ ⇑(OrthonormalBasis.singleton ι 𝕜) = 1

Tactic:
ext

Goal state after:
ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
x✝ : ι
⊢ (OrthonormalBasis.singleton ι 𝕜) x✝ = 1 x✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
⊢ (Pi.orthonormalBasis B).toBasis = (Pi.basis fun i ↦ (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm

Tactic:
ext

Goal state after:
η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i✝¹ : (i : η) × ι i
i✝ : η
⊢ ((Pi.orthonormalBasis B).toBasis i✝¹).ofLp i✝ =
    (((Pi.basis fun i ↦ (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm) i✝¹).ofLp 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
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
A : Tendsto (fun r ↦ μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (fun a ↦ μ (closedBall x a) / μ (closedBall x a) - μ (s ∩ closedBall x a) / μ (closedBall x a)) (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ μ (closedBall x r) / μ (closedBall x r) - μ (s ∩ closedBall x r) / μ (closedBall x r) =
    μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)

Tactic:
convert!
      I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne
        hs.compl

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
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
A : Tendsto (fun r ↦ μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (fun a ↦ μ (closedBall x a) / μ (closedBall x a) - μ (s ∩ closedBall x a) / μ (closedBall x a)) (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ s = sᶜᶜ
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ Set.range ⇑(ofZLatticeBasis K L b) = ⇑L.subtype '' Set.range ⇑b

Tactic:
ext

Goal state after:
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x✝ : E
⊢ x✝ ∈ Set.range ⇑(ofZLatticeBasis K L b) ↔ x✝ ∈ ⇑L.subtype '' Set.range ⇑b
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
⊢ inner ℝ x ((basisFun ι ℝ) i) = x.ofLp i

Tactic:
real_inner_comm,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
i : ι
⊢ inner ℝ ((basisFun ι ℝ) i) x = x.ofLp i
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝¹⁴ : NormedField K
inst✝¹³ : LinearOrder K
inst✝¹² : IsStrictOrderedRing K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
⊢ ofZLatticeBasis K (ZLattice.comap K L ↑↑e) (ofZLatticeComap K L (↑e) b) = (ofZLatticeBasis K L b).map ↑e.symm

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹⁴ : NormedField K
inst✝¹³ : LinearOrder K
inst✝¹² : IsStrictOrderedRing K
inst✝¹¹ : HasSolidNorm K
inst✝¹⁰ : FloorRing K
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace K E
inst✝⁷ : FiniteDimensional K E
inst✝⁶ : ProperSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace K F
inst✝³ : FiniteDimensional K F
inst✝² : ProperSpace F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
i✝ : ι
⊢ (ofZLatticeBasis K (ZLattice.comap K L ↑↑e) (ofZLatticeComap K L (↑e) b)) i✝ =
    ((ofZLatticeBasis K L b).map ↑e.symm) i✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Measure

Goal state before:
pp: ι : Type u_1
inst✝¹ : Finite ι
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
J : Box ι
x✝ : ↑J ≤ ⊤
π : Prepartition J
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, μ.real ↑Ji = μ.real ↑J

Tactic:
rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ENNReal.ofReal ((a - r) / 2) > 0

Tactic:
by simp [ar]

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 ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis (↥(Classical.choose ⋯)) 𝕜 E := Classical.choose ⋯
⊢ OrthonormalBasis (Fin (Fintype.card ↥(Classical.choose ⋯))) 𝕜 E

Tactic:
exact b.reindex (Fintype.equivFinOfCardEq rfl)

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 ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
⊢ LeftInverse (fun b ↦ ⟨(sigmaOrthonormalBasisIndexEquiv hn hV hV') ⟨i, b⟩, ⋯⟩) fun a ↦
    Fin.cast ⋯ ((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm ↑a).snd

Tactic:
grind [subordinateOrthonormalBasisIndex_def, Fin.cast_eq_self]

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
m : Type u_7
n : Type u_8
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
⊢ (toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) = vecMulVec (star ⇑b₂) (star (b.repr x).ofLp)

Tactic:
ext

Goal state after:
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
i✝ : m
j✝ : n
⊢ (toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) i✝ j✝ = vecMulVec (star ⇑b₂) (star (b.repr x).ofLp) i✝ j✝