mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a : ι → ℝ
⊢ (parallelepiped fun i ↦ Pi.single i (a i)) = uIcc 0 a

Tactic:
ext x
  simp_rw [Set.uIcc, mem_parallelepiped_iff, Set.mem_Icc, Pi.le_def, ← forall_and, Pi.inf_apply,
    Pi.sup_apply, ← Pi.single_smul', Pi.one_apply, Pi.zero_apply, ← Pi.smul_apply',
    Finset.univ_sum_single (_ : ι → ℝ)]
  constructor
  · rintro ⟨t, ht, rfl⟩ i
    specialize ht i
    simp_rw [smul_eq_mul, Pi.mul_apply]
    rcases le_total (a i) 0 with hai | hai
    · rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]
      exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩
    · rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]
      exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩
  · intro h
    refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩
    · specialize h i
      rcases le_total (a i) 0 with hai | hai
      · rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
        exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
      · rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
        exact ⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩
    · specialize h i
      simp only [smul_eq_mul, Pi.mul_apply]
      rcases eq_or_ne (a i) 0 with hai | hai
      · rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h
        rw [hai, ← h, zero_div, zero_mul]
      · rw [div_mul_cancel₀ _ hai]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
H : (interior (⇑b.equivFunL.symm.toHomeomorph '' Icc 0 1)).Nonempty
⊢ (interior (_root_.parallelepiped ⇑b)).Nonempty

Tactic:
dsimp only [_root_.parallelepiped]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
H : (interior (⇑b.equivFunL.symm.toHomeomorph '' Icc 0 1)).Nonempty
⊢ (interior ((fun t ↦ ∑ i, t i • b i) '' Icc 0 1)).Nonempty
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
NNReal.rpow_one,

Goal state after:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
⊢ ↑(Fintype.card ι) ^ (1 / p.toReal) * ‖b‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
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 n) i - (b.repr m) i) ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
Basis.mem_span_iff_repr_mem,

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 n) i - (b.repr m) i) ↔ ∀ (i : ι), (b.repr (-m + n)) i ∈ Set.range ⇑(algebraMap ℤ K)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_2.h
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 ι
a✝ b✝ : E
hxy : fract b a✝ = fract b b✝
⊢ -a✝ + b✝ ∈ span ℤ (Set.range ⇑b)

Tactic:
← fract_eq_fract

Goal state after:
case refine_2.h
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 ι
a✝ b✝ : E
hxy : fract b a✝ = fract b b✝
⊢ fract b a✝ = fract b b✝
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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : μ (symmDiff s t) = 0
⊢ μ (symmDiff (r • s) (r • t)) = 0

Tactic:
← smul_set_symmDiff₀ hr,

Goal state after:
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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : μ (symmDiff s t) = 0
⊢ μ (r • symmDiff s t) = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ μ (closedBall x r) = μ (closedBall 0 r)

Tactic:
have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall]
  rw [this, measure_preimage_add]

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✝ : Finite ι
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑b))

Tactic:
have h : Set.MapsTo b.equivFun (span ℤ (Set.range b)) (span ℤ (Set.range (Pi.basisFun ℝ ι))) := by
    intro _ hx
    rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢

Goal state after:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑b))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
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 : r < 0
⊢ μ (sphere x r) = 0

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
⊢ μ (sphere x r) = 0

Tactic:
· simp only [empty_sdiff, measure_empty, ← closedBall_sdiff_ball, closedBall_eq_empty.2 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
⊢ μ (sphere x r) = 0
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case zero
ι : Type u_1
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))
J : ℕ → Box ι := fun m ↦ (fun J ↦ J.splitCenterBox (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
⊢ (J 0).upper i - (J 0).lower i = (I.upper i - I.lower i) / 2 ^ 0

Tactic:
| zero =>

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'
i : ι
k : 𝕜
this : k = k • 1
⊢ (↑b.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i (k • 1)) =
    (↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (Pi.single i (k • 1))

Tactic:
Pi.single_smul

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'
i : ι
k : 𝕜
this : k = k • 1
⊢ (↑b.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (k • Pi.single i 1) =
    (↑b'.repr.symm ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm) (k • Pi.single i 1)
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
⊢ ∃ m, ∀ (i : ι), J.upper i - J.lower i = (J.upper i - J.lower i) / 2 ^ m

Tactic:
refine ⟨0, fun i => ?_⟩

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ Box.Icc J
HIcc : Box.Icc J ⊆ Box.Icc I ∧ Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ n
i : ι
⊢ J.upper i - J.lower i = (J.upper i - J.lower i) / 2 ^ 0
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ oscillation f x = 0

Tactic:
rw [← continuousWithinAt_univ f x] at hf
  exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i : ι
inst✝ : Finite ι
f : Box ι → M
I₀ : WithTop (Box ι)
hf :
  ∀ (I : Box ι),
    ↑I ≤ I₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
⊢ ι →ᵇᵃ[I₀] M

Tactic:
classical
  refine ⟨f, ?_⟩
  replace hf (I : Box ι) (hI : ↑I ≤ I₀) (s) : ∑ J ∈ (splitMany I s).boxes, f J = f I := by
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s _ ihs =>
      rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
      refine Finset.sum_congr rfl fun J' hJ' => ?_
      by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
      · rw [sum_split_boxes]
        exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
      · rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
  intro I hI π hπ
  have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
  rcases hπ.exists_splitMany_le with ⟨s, hs⟩
  rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
  exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm

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

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

Tactic:
intro _ hI

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ (prepartition n B).tag J✝ ∈ Box.Icc J✝
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
⊢ (prepartition n B).IsSubordinate fun x ↦ ⟨r, hr⟩

Tactic:
intro _ hI

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
J✝ : Box ι
hI : J✝ ∈ prepartition n B
⊢ Box.Icc J✝ ⊆ Metric.closedBall ((prepartition n B).tag J✝) ↑((fun x ↦ ⟨r, hr⟩) ((prepartition n B).tag J✝))
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
⊢ ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
intro a

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
a : ι
⊢ ∀ (b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
I : Box ι
hI : I ∈ {x ∈ (prepartition n B).boxes | (prepartition n B).tag x ∈ s}
⊢ ∃ a, ∃ (_ : a ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset), box n (index n a) = I

pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
⊢ F x✝ / ↑n ^ card ι = volume.real ↑(box n (index n x✝)) * F ((prepartition n B).tag (box n (index n x✝)))

Tactic:
· rw [Finset.mem_filter] at hI
    refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
    rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]
    exact tag_mem_smul_span _ _

Goal state after:
case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
⊢ F x✝ / ↑n ^ card ι = volume.real ↑(box n (index n x✝)) * F ((prepartition n B).tag (box n (index n x✝)))
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
⊢ ∀ c ∈ Finset.Iio n, (𝕜 ∙ gramSchmidt 𝕜 f c).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
intro a

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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
a : ι
⊢ a ∈ Finset.Iio n → (𝕜 ∙ gramSchmidt 𝕜 f a).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
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
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne,
    not_false_iff]

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

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)

Tactic:
refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ (vol J') (f ((π.biUnionTagged πi).tag J')) = (vol J') (f ((πi J).tag J'))
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case e'_5
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s = ∫ (x : ι → ℝ) in s, 1

Tactic:
rw [setIntegral_const, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ False

Tactic:
have H : LinearIndependent R ![f x, 1] := by
    convert! h.map' f.toLinearMap f.ker
    ext i
    fin_cases i <;> simp [f]

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H : LinearIndependent R ![f x, 1]
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Orientation

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

Tactic:
e.toBasis.orientation_eq_iff_det_pos

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ E [⋀^Fin 0]→ₗ[ℝ] ℝ

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case neg
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))).orientation = x

Tactic:
rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]

Goal state after:
case neg
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ e.orientation ≠ x
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_

Goal state after:
case pos
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : Integrable I l g μ.toBoxAdditive.toSMul
π : TaggedPrepartition I
J : Box ι
x✝ : J ∈ π.boxes
⊢ 0 ≤ (μ.toBoxAdditive.toSMul J) (g (π.tag J))
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
h : ∃ i, v i = 0
⊢ ∏ x, |⟪b x, v x⟫| = ∏ i, ‖v i‖

Tactic:
obtain ⟨i, hi⟩ := h
    rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)] <;>
      simp [hi]

Goal state after: