mathlib-initiative/mathlib-tactics huggingface dataset:
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 ↑(ceil b m)) i = ↑⌈(b.repr m) i⌉

Tactic:
by
  classical simp only [ceil, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
    Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
    Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

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 ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑b))

Tactic:
convert! DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_

Goal state after:
case convert_1
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 ⇑(Pi.basisFun ℝ ι)))

case convert_2
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 ℝ ι)))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun) (↑(span ℤ (Set.range ⇑b))) (↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) h)
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
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ (sphere x r) = 0

Tactic:
rcases eq_or_ne r 0 with (rfl | h)
  · rw [sphere_zero, measure_singleton]
  · exact addHaar_sphere_of_ne_zero μ x h

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

Tactic:
ENNReal.mul_inv_cancel,

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
⊢ 1 * (μ 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: case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ∅ = univ.pi fun i ↦ Ioc (l i) (u i)

Tactic:
univ_pi_eq_empty

Goal state after:
case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ∅ = ∅

case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.47) (u ?m.47) = ∅

ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : 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
m✝ m : ℕ
⊢ ¬p (J m) → ¬p (J m.succ)

Tactic:
by simpa only [J_succ] using hs (J m) (hJle m)

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
t_bound : t ⊆ closedBall 0 1
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)

Tactic:
by
  have A : Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) := by
    apply
      tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h
        (Eventually.of_forall fun b => zero_le)
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    grw [t_bound]
    rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]
  have B :
    Tendsto (fun r : ℝ => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0)
      (𝓝 (μ (closedBall x 1) / μ ({x} + u))) := by
    apply tendsto_const_nhds.congr' _
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    have : closedBall x r = {x} + r • closedBall (0 : E) 1 := by
      simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero,
        mul_one, singleton_add_closedBall, smul_zero]
    simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']
    simp only [addHaar_closedBall_center, image_add_left, measure_preimage_add, singleton_add]
  have C : Tendsto (fun r : ℝ =>
        μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u)))
      (𝓝[>] 0) (𝓝 (0 * (μ (closedBall x 1) / μ ({x} + u)))) := by
    apply ENNReal.Tendsto.mul A _ B (Or.inr ENNReal.zero_ne_top)
    simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.ne]
  simp only [zero_mul] at C
  apply C.congr' _
  filter_upwards [self_mem_nhdsWithin]
  rintro r (rpos : 0 < r)
  calc μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u))
    _ = μ (closedBall x r) * (μ (closedBall x r))⁻¹ *
        (μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) := by simp only [div_eq_mul_inv]; ring
    _ = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u) := by
      rw [ENNReal.mul_inv_cancel (measure_closedBall_pos μ x rpos).ne'
          measure_closedBall_lt_top.ne,
        one_mul]

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 : ℝ
T : (R * r) • t' = r • t
U : (R * r) • u' = r • u
⊢ μ (s ∩ ({x} + (R * r) • t')) / μ ({x} + (R * r) • u') = μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)

Tactic:
rw [T, U]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

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

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (π.biUnionTagged πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

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

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J ↦ (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

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
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ (b.equiv b' e) x = ∑ i, (b.repr x).ofLp i • b' (e i)

Tactic:
nth_rw 1 [← b.sum_repr x, map_sum]
  simp_rw [map_smul, equiv_apply_basis]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case right
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₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
a : ℝ
δa : a > δ
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

Tactic:
← ha

Goal state after:
case right
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₁
δ : ℝ
δ0 : δ > 0
hδ : K ⊆ S δ
x : E
xK : x ∈ K
a : ℝ
δa : a > δ
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ ediam (f '' (eball x (ENNReal.ofReal δ) ∩ D)) ≤ ediam (f '' (eball x (ENNReal.ofReal a) ∩ D))
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 ι
inst✝ : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
w : E
i✝ : ι
⊢ ((orthonormalBasisSingleton ι 𝕜 h v hv).repr w).ofLp i✝ = (EuclideanSpace.single default ⟪v, w⟫).ofLp i✝

Tactic:
simp [OrthonormalBasis.repr_apply_apply, Unique.eq_default]

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ {ν | ↑(box n ν) ⊆ s}.Finite

Tactic:
refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
    (by simp) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
      (fun _ hν ↦ ?_)

Goal state after:
case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν) ∩ s) volume

case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝

case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ volume (⋃ i, ↑(box n i) ∩ s) ≠ ⊤

case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝ : ι → ℤ
hν : x✝ ∈ {ν | ↑(box n ν) ⊆ s}
⊢ x✝ ∈ {i | 1 / ↑n ^ card ι ≤ volume (↑(box n i) ∩ s)}
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
⊢ ⋃ i, ↑(box n i) ∩ s ⊆ s

Tactic:
simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑n * a + 1 ≤ ⌈↑n * x⌉

Tactic:
Int.add_one_le_iff,

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑n * a < ⌈↑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
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
⊢ (𝕜 ∙ gramSchmidt 𝕜 f j).orthogonalProjectionOnto (f i) = 0

Tactic:
apply orthogonalProjectionOnto_apply_of_mem_orthogonal

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
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
⊢ f i ∈ (𝕜 ∙ gramSchmidt 𝕜 f j)ᗮ
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
⊢ SameRay R ((g ⇑e • (LinearMap.det ↑f.symm * e.det ⇑e)) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)

Tactic:
Basis.det_self,

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
⊢ SameRay R ((g ⇑e • (LinearMap.det ↑f.symm * 1)) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
c : ℝ
hc : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ c
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ μ.real ↑I * c

Tactic:
simpa only [integral_const] using! norm_integral_le_of_norm_le hc μ (integrable_const c)

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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ (μ.real ↑I + 1 + 1) * ↑ε

Tactic:
have : ∀ x, ∃ N₁, N₀ ≤ N₁ ∧ dist (f N₁ x) (g x) ≤ ε := fun x ↦ by
    have : Tendsto (f · x) atTop (𝓝 <| g x) :=
      SimpleFunc.tendsto_approxOn hg.measurable _ (subset_closure (by simp))
    exact ((eventually_ge_atTop N₀).and <| this <| closedBall_mem_nhds _ ε0).exists

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this✝ : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
this : ∀ (x : ι → ℝ), ∃ N₁, N₀ ≤ N₁ ∧ dist ((f N₁) x) (g x) ≤ ↑ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum g μ.toBoxAdditive.toSMul π) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤ (μ.real ↑I + 1 + 1) * ↑ε
Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace

Goal state before:
pp: p : ℝ≥0∞
X : Type u_1
inst✝⁶ : MeasurableSpace X
Y : Type u_2
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : BorelSpace X
inst✝¹ : BorelSpace Y
inst✝ : SecondCountableTopologyEither X Y
⊢ MeasurableSpace.comap ofLp inferInstance = MeasurableSpace.comap ofLp (borel (X × Y))

Tactic:
BorelSpace.measurable_eq (α := X × Y)

Goal state after:
p : ℝ≥0∞
X : Type u_1
inst✝⁶ : MeasurableSpace X
Y : Type u_2
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : BorelSpace X
inst✝¹ : BorelSpace Y
inst✝ : SecondCountableTopologyEither X Y
⊢ MeasurableSpace.comap ofLp inferInstance = MeasurableSpace.comap ofLp (borel (X × Y))
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 J✝ : Box ι
π✝ : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
c c₁ c₂ : ℝ≥0
ε ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
inst✝ : CompleteSpace F
h : Integrable I l f vol
J : Box ι
hJ : ↑J ≤ ↑I
π : Prepartition J
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, integral Ji l f vol = integral J l f vol

Tactic:
by
    replace hπ := hπ.iUnion_eq; rw [← Prepartition.iUnion_top] at hπ
    rw [(h.to_subbox (WithTop.coe_le_coe.1 hJ)).sum_integral_congr hπ, Prepartition.top_boxes,
      sum_singleton]

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

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A : ⇑b = ⇑(b.reindex e) ∘ ⇑e
⊢ o.volumeForm.measure (parallelepiped ⇑b) = 1

Tactic:
rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
apply sum_le_sum_of_subset_of_nonneg
      · intro x hx
        simp only [mem_Ioo] at hx
        simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true, and_self_iff]
      · intro i _hi _hident
        positivity

Goal state after:
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ SMulAntidiagonal (hs.min hns • ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}

Tactic:
ext ⟨a, b⟩

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ (a, b) ∈ SMulAntidiagonal (hs.min hns • ht.min hnt) ⋯ ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this✝ : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
hk : k ∈ range n
v : ι → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-↑k) ↑k
this : ↑k + 1 ≤ |v j|
⊢ ↑(k + 1) ≤ |(b.repr (∑ i, v i • b i)) j|

Tactic:
by simpa [Finsupp.single_apply] using this

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), ↑k ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
gcongr
        refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)
        linarith

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

Goal state before:
pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ‖t‖ = 0
⊢ t ∈ ⇑(Function.Embedding.subtype fun x ↦ x ∈ L) ⁻¹' (Metric.closedBall 0 (2 * ‖x‖) ∩ ↑L)

Tactic:
simp [show t = 0 by simpa using ht₁]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ i ∈ f.support, (f i)! = ∏ i ∈ s, (f i)!

Tactic:
rw [Finset.prod_subset h]
    grind [Nat.factorial_eq_one]

Goal state after: