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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ tF = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
suffices WithSeminorms (fun (i : Fin 1) ↦ p) by
    rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
    simp

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ WithSeminorms fun i ↦ p
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖

Tactic:
← norm_mul

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖
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 : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪∑ i ∈ s, l i • v i, v i⟫ = (starRingEnd 𝕜) (l i)

Tactic:
by
  classical
  simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole,
    Finset.sum_ite_eq', if_true]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ (∑ j ∈ s, ∑ i ∈ s, if i = j then ⟪(V i) (l₁ i), (V j) (l₂ j)⟫ else 0) = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫

Tactic:
simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
⊢ Submodule.map (↑↑↑f) U ⟂ Submodule.map (↑↑↑f) V ↔ U ⟂ V

Tactic:
by
  refine ⟨fun h ↦ ?_, IsOrtho.map f.toLinearIsometry⟩
  have hf : ∀ p : Submodule 𝕜 E,
      (p.map (f : E →ₗ[𝕜] F)).comap (f.toLinearIsometry : E →ₗ[𝕜] F) = p :=
    comap_map_eq_of_injective f.injective
  simpa only [hf] using h.comap f.toLinearIsometry

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
v : E
⊢ K.starProjection v = 0 ↔ v ∈ Kᗮ

Tactic:
by
  refine ⟨fun h w hw => ?_, fun hv => ?_⟩
  · rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]
  · simp [starProjection_apply, orthogonalProjectionOnto_apply_of_mem_orthogonal hv]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ (single p i a).ofLp i = a

Tactic:
ofLp_single,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ Pi.single i a i = a
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ (single p i a).ofLp i' = 0

Tactic:
ofLp_single,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ Pi.single i a i' = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ (single p i a).ofLp i' = 0

Tactic:
ofLp_single,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ Pi.single i a i' = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h

Tactic:
· simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
      calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

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✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
rw [edist_eq_iSup, dist_eq_iSup]
      cases isEmpty_or_nonempty ι
      · simp
      · refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
        have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _
        simp [ciSup_le_iff this]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ (Finset.univ.sup fun b ↦ edist (x.ofLp b) (y.ofLp b)) ≤ edist x y

Tactic:
Finset.sup_le_iff,

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ b ∈ Finset.univ, edist (x.ofLp b) (y.ofLp b) ≤ edist x y
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1✝ x2✝ : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist (WithLp.map p (Prod.map f g) x1✝) (WithLp.map p (Prod.map f g) x2✝) = edist x1✝ x2✝

Tactic:
· simp [WithLp.prod_edist_eq_add hp, hf.edist_eq, hg.edist_eq]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
⊢ Isometry (WithLp.map p (Prod.map f g))

Tactic:
by
  intro _ _
  rcases p.trichotomy with rfl | rfl | hp
  · absurd hp.elim; simp
  · simp [WithLp.prod_edist_eq_sup, hf.edist_eq, hg.edist_eq]
  · simp [WithLp.prod_edist_eq_add hp, hf.edist_eq, hg.edist_eq]

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

Goal state before:
pp: a : ℝ
h : a ≠ 0
| ofReal |a⁻¹| • volume

Tactic:
← Real.smul_map_volume_mul_left h,

Goal state after:
a : ℝ
h : a ≠ 0
| ofReal |a⁻¹| • ofReal |a| • Measure.map (fun x ↦ a * x) volume
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ (∑ i_1, ‖(single (↑p) i b).ofLp i_1‖₊ ^ (↑p).toReal) ^ (1 / (↑p).toReal) = ‖b‖₊

Tactic:
ENNReal.coe_toReal,

Goal state after:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ (∑ i_1, ‖(single (↑p) i b).ofLp i_1‖₊ ^ ↑p) ^ (1 / ↑p) = ‖b‖₊
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
⊢ Measure.map (⇑(toLin' A ∘ₗ toLin' B)) volume = ofReal |(A.det * B.det)⁻¹| • volume

Tactic:
LinearMap.coe_comp,

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
⊢ Measure.map (⇑(toLin' A) ∘ ⇑(toLin' B)) volume = ofReal |(A.det * B.det)⁻¹| • volume
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
dsimp only [regionBetween, preimage_ofPred_eq]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (x : α), volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
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 (fract b m)) i = Int.fract ((b.repr m) i)

Tactic:
fract,

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 - ↑(floor b m))) i = Int.fract ((b.repr m) i)
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 ι
⊢ E ⧸ span ℤ (Set.range ⇑b) ≃ ↑(fundamentalDomain b)

Tactic:
refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩

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 ι
⊢ E ⧸ span ℤ (Set.range ⇑b) → ↑(fundamentalDomain b)

case refine_2
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 ι
x y : E ⧸ span ℤ (Set.range ⇑b)
⊢ ?refine_1 x = ?refine_1 y → x = y

case refine_3
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 ι
x : ↑(fundamentalDomain b)
⊢ ∃ a, ?refine_1 a = x
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 ι
x : ↑(fundamentalDomain b)
⊢ ↑x = fract b ↑x

Tactic:
exact (fract_eq_self.mpr x.prop).symm

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

Goal state before:
pp: ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (⇑((b.constr ℕ) v) ∘ ⇑b)

Tactic:
exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm

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

Goal state before:
pp: case refine_1.refine_2
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
⊢ fract b x ∈ ↑L

Tactic:
fract,

Goal state after:
case refine_1.refine_2
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
⊢ x - ↑(floor b x) ∈ ↑L
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 ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ μ u * (μ u)⁻¹ - μ (vᶜ ∩ u) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹

Tactic:
rw [← ENNReal.sub_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
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 ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ (μ u - μ (vᶜ ∩ u)) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹

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 ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ 0 < μ (vᶜ ∩ u) → μ (vᶜ ∩ u) < μ u → (μ u)⁻¹ ≠ ∞
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : a ∉ s
hs : (splitMany I s).IsPartition
⊢ (splitMany I (insert a s)).IsPartition

Tactic:
simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

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

Goal state before:
pp: case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J ↦ splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J ↦ splitMany J (insert p s)

Tactic:
| insert p s _ ihp =>

Goal state after:
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
x : ↥L
i✝ i : ι
⊢ (↑ℤ ↑(ofZLatticeBasis K L b).repr ∘ₗ L.subtype) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)

Tactic:
LinearMap.coe_comp,

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 : ↥L
i✝ i : ι
⊢ (⇑(↑ℤ ↑(ofZLatticeBasis K L b).repr) ∘ ⇑L.subtype) (b i) =
    (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K)) ∘ ⇑↑b.repr) (b i)
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : ⊤.compl.distortion ≤ c
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
hs : ∀ π ∈ {π₁, π₂}, (π.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π.iUnion
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
clear hs

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case neg
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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T = ∅
⊢ ∃ r > 0, K ⊆ S r

Tactic:
use 1, one_pos, subset_trans hT (by simp [T_nonempty])

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν

Tactic:
refine mem_box_iff.mpr fun _ ↦ ?_
  rw [tag, add_div]
  have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  exact ⟨lt_add_of_pos_right _ (by positivity), le_rfl⟩

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ ν ≠ ν' ↔ Disjoint ↑(box n ν) ↑(box n ν')

Tactic:
rw [not_iff_comm, Set.not_disjoint_iff]

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ (∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')) ↔ ν = ν'
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:
exact gramSchmidt_orthogonal 𝕜 f hij

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case intro.h
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✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (Orientation.map ι f) (rayOfNeZero R g hg) = (LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg

Tactic:
Orientation.map_apply,

Goal state after:
case intro.h
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✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ rayOfNeZero R (g.compLinearMap ↑f.symm) ⋯ = (LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg
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 : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ (↑m).toReal * ↑n ≤ ↑(δ n)

Tactic:
ENNReal.coe_toReal,

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 : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ ↑m * ↑n ≤ ↑(δ n)