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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q

Tactic:
rw [eq₁, le_add_iff_nonneg_right] at this

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
key : ⟪v i, (linearCombination 𝕜 v) l⟫ = ⟪v i, 0⟫
⊢ l i = 0 i

Tactic:
simpa only [hv.inner_right_finsupp, inner_zero_right] using! key

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

Goal state before:
pp: case mpr.a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ ≤ ⨅ w, ‖u - ↑w‖

Tactic:
apply le_ciInf

Goal state after:
case mpr.a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ∀ (x : ↑K), ‖u - v‖ ≤ ‖u - ↑x‖
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
this : ∃ m, s ⊆ m ∧ Maximal (fun x ↦ x ∈ {b | Orthonormal 𝕜 Subtype.val}) m
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
obtain ⟨b, hb⟩ := this

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
b : Set E
hb : s ⊆ b ∧ Maximal (fun x ↦ x ∈ {b | Orthonormal 𝕜 Subtype.val}) b
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
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_assoc,

Goal state after:
𝕜 : 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
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : Module R N
f : M ≃L[R] N
s t : ClosedSubmodule R M
x : N
⊢ x ∈ (↑((mapEquiv f) (s ⊓ t))).carrier ↔ x ∈ (↑((mapEquiv f) s ⊓ (mapEquiv f) t)).carrier

Tactic:
simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe, toSubmodule_inf,
    Submodule.coe_inf, Set.mem_inter_iff, mem_mapEquiv_iff, mem_inf]

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

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
x : E
⊢ K.reflection x = x ↔ x ∈ K

Tactic:
rw [← starProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
    two_smul ℕ, ← two_smul 𝕜]
  refine (smul_right_injective E ?_).eq_iff
  exact two_ne_zero

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

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

Tactic:
one_mul,

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ ⟪U.subtype ((U.projectionOnto V hUV) ↑⟨v, hv⟩), ↑⟨u, hu⟩⟫ = 0

Tactic:
Submodule.projectionOnto_apply_right hUV ⟨v, hv⟩,

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : (U.subtype ∘ₗ U.projectionOnto V hUV).IsSymmetric
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ ⟪U.subtype 0, ↑⟨u, hu⟩⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ 1 * (-1).det = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
one_mul,

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) := (finBasis 𝕜 ↥K).prod (finBasis 𝕜 ↥Kᗮ)
this : (LinearMap.toMatrix b b) (↑e.symm ∘ₗ ↑K.reflection.toLinearEquiv ∘ₗ ↑e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1)
⊢ (-1).det = (-1) ^ finrank 𝕜 ↥Kᗮ
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2) ≤ 1 * edist x y

Tactic:
one_mul,

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ max (edist x.ofLp.1 y.ofLp.1) (edist x.ofLp.2 y.ofLp.2) ≤ edist x y
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ (b.reindex e).addHaar = b.addHaar

Tactic:
rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]

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

Goal state before:
pp: case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |B.det⁻¹ * A.det⁻¹| • volume = ofReal |(A.det * B.det)⁻¹| • volume

pp: case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

pp: case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)

Tactic:
mul_comm,

Goal state after:
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |A.det⁻¹ * B.det⁻¹| • volume = ofReal |(A.det * B.det)⁻¹| • volume

case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)

Tactic:
have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
h : x ∈ s
hx : {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = Ioo (f x) (g x)
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = ofReal (g x - f x)
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
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
x : E
⊢ f x = (↑e.symm ∘ₗ g ∘ₗ ↑e) x

Tactic:
simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
      LinearEquiv.symm_apply_apply, hg]

Goal state after:
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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ f.toEquiv.symm x ∈ fundamentalDomain b

Tactic:
← Set.mem_image_equiv

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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
x : F
⊢ x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ ⇑f.toEquiv '' fundamentalDomain b
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
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 ι
q : E ⧸ span ℤ (Set.range ⇑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ fractRestrict b x✝¹ = fractRestrict b x✝

Tactic:
rw [Subtype.mk.injEq, fractRestrict_apply, fractRestrict_apply, fract_eq_fract]

Goal state after:
case refine_1
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 ι
q : E ⧸ span ℤ (Set.range ⇑b)
x✝¹ x✝ : E
h : x✝¹ ≈ x✝
⊢ -x✝¹ + x✝ ∈ span ℤ (Set.range ⇑b)
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
⊢ μ (closedBall 0 1) = μ (ball 0 1)

Tactic:
apply le_antisymm _ (measure_mono ball_subset_closedBall)

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
⊢ μ (closedBall 0 1) ≤ μ (ball 0 1)
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✝³ : Finite ι
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
⊢ VAddInvariantMeasure (↥(span ℤ (Set.range ⇑b))) E μ

Tactic:
exact inferInstanceAs <| VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ

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
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
addHaar_closedBall' μ x hr,

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
x : E
r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)
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
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ 0 - b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))

Tactic:
zero_sub,

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
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ -b i ∉ span ℝ (⇑b '' (Set.univ \ {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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ 1 * (μ s * (μ t)⁻¹) = μ s / μ t

pp: case h0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0

pp: case ht
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ∞

Tactic:
one_mul,

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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ μ s * (μ t)⁻¹ = μ s / μ t

case h0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0

case ht
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ∞
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : ↑I ⊆ ↑J₁
h₂ : ↑I ⊆ ↑J₂
⊢ ↑I ⊆ ↑J₁ ∩ ↑J₂

Tactic:
exact subset_inter h₁ h₂

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i)
        (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
split_ifs with hs <;> simp only [hs, iff_true, iff_false, not_lt]

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i

case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2
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
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
⊢ Function.Injective b

Tactic:
· exact Subtype.coe_injective.comp (Basis.injective _)

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 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 : ℝ
⊢ (R * r) • t' = r • t

Tactic:
mul_comm,

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 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 : ℝ
⊢ (r * R) • t' = r • t
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:
mul_comm,

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 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
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ π.iUnion ⊆ ↑I ∧ ↑I ⊆ π.iUnion

Tactic:
π.iUnion_subset,

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (∀ x ∈ I, ∃ J ∈ π, x ∈ J) ↔ True ∧ ↑I ⊆ π.iUnion
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∀ (i j : ι), 1 * (single j 1).ofLp i = if i = j then 1 else 0

Tactic:
one_mul,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∀ (i j : ι), (single j 1).ofLp i = if i = j then 1 else 0
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
⊢ ∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion

Tactic:
by
  have := fun J => Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic J r
  choose! πi πip πiH πir _ πid using this
  refine ⟨π.biUnionTagged πi, biUnion_le _ _, isHenstock_biUnionTagged.2 fun J _ => πiH J,
    isSubordinate_biUnionTagged.2 fun J _ => πir J, ?_, π.iUnion_biUnion_partition fun J _ => πip J⟩
  rw [distortion_biUnionTagged]
  exact sup_congr rfl fun J _ => πid J

Goal state after: