mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1

Tactic:
rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
      simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

Goal state after:
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
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ (p.toReal⁻¹ * p.toReal)

Tactic:
inv_mul_cancel₀ hp0.ne',

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal = ‖c‖₊ ^ p.toReal * (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
⊢ ∏ _i, ↑1 * ediam s = ediam s ^ Fintype.card ι

Tactic:
by
      simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]

Goal state after:
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
hp✝ : Fact (1 ≤ p✝)
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
hp : p ≠ ∞
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊

Tactic:
· have : 0 < p.toReal := (toReal_pos_iff_ne_top _).mpr hp
      simp [nnnorm_eq_sum hp, this.ne', ← Finset.univ_sigma_univ, Finset.sum_sigma, Sigma.curry]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = (Measure.pi fun i ↦ volume) (univ.pi s)

Tactic:
← lintegral_indicator_one h2s

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.map (⇑(toLin' t.toMatrix)) volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ max 0 0
hai : a i = 0
⊢ x i = x i / a i * a i

Tactic:
sup_idem,

Goal state after:
case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ 0
hai : a i = 0
⊢ x i = x i / a i * a i
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
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ SigmaFinite b.addHaar

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite

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
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite b.addHaar
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ Measure.map (⇑f) b.addHaar = (b.map ↑f).addHaar

Tactic:
rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable
    (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map,
    ← addHaar_self b, ← f.toEquiv.preimage_image (_root_.parallelepiped ⇑b)]
  have := image_parallelepiped f.toLinearMap (⇑b : ι → E)
  simp_all

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist x y = 0
⊢ x = y

Tactic:
rw [dist_pseudoMetricSpaceToPi] at h
    apply eq_of_dist_eq_zero at h
    exact WithLp.toLp_injective p 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
f : E →ₗ[ℝ] E := r • 1
⊢ ¬r ^ finrank ℝ E = 0

Tactic:
exact pow_ne_zero _ hr

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

Goal state before:
pp: case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite

Goal state after:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)
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✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
⊢ μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (fundamentalDomain b₀)

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (fundamentalDomain b₀)
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
⊢ fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite

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
⊢ fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b
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
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
⊢ False

Tactic:
rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩

Goal state after:
ι : 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
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ m, (J m).lower
hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[Box.Icc I] z
hU :
  ∀ 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
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case inl
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
⊢ (Set.Ioc (max (x i) (x i)) (min (J₁.upper i) (J₂.upper i))).Nonempty

Tactic:
sup_idem,

Goal state after:
case inl
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
i : ι
H : ∀ (x_1 : ι), J₁.lower x_1 = x x_1 ↔ J₂.lower x_1 = x x_1
hi₁ : J₁.lower i = x i
hi₂ : J₂.lower i = x i
H₁ : x i < J₁.upper i
H₂ : x i < J₂.upper i
⊢ (Set.Ioc (x i) (min (J₁.upper i) (J₂.upper i))).Nonempty
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

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

Tactic:
refine fun H => ⟨fun J hJ J' hJ' Hne => ?_, iUnion_mono H⟩

Goal state after:
case mp
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : (↑J ∩ ↑J').Nonempty
⊢ J ≤ J'
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ √(∑ x_1, x.ofLp x_1 ^ 2) = r ↔ ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2

Tactic:
Real.sqrt_eq_iff_eq_sq this hr

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

Goal state before:
pp: case e'_2.pq
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
x✝ : Box ι
⊢ (x✝ ∈ π.filter fun J ↦ ¬p J) ↔ x✝ ∈ ↑π.boxes \ ↑(π.filter p).boxes

pp: ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).PairwiseDisjoint Box.toSet

Tactic:
· simp +contextual

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).PairwiseDisjoint Box.toSet
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ ((Pi.orthonormalBasis B) ⟨i, j⟩).ofLp k = (PiLp.single 2 ⟨i, j⟩.fst ((B ⟨i, j⟩.fst) ⟨i, j⟩.snd)).ofLp k

Tactic:
simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]

Goal state after:
η : Type u_7
inst✝⁵ : Fintype η
inst✝⁴ : DecidableEq η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
k i : η
j : ι i
⊢ (B k).repr.symm (toLp 2 (Pi.single i (Pi.single j 1) k)) = Pi.single i ((B i) j) k
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case refine_2
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ J.upper i

Tactic:
· rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
    have := Hle hxs
    rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
    exact (Hle hy).2

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
⊢ span ℤ (Set.range ⇑(ofZLatticeBasis K L b)) = L

Tactic:
calc span ℤ (Set.range (b.ofZLatticeBasis K))
    _ = span ℤ (L.subtype '' Set.range b) := by congr; ext; simp
    _ = map L.subtype (span ℤ (Set.range b)) := by rw [Submodule.map_span]
    _ = L := by simp [b.span_eq]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ ↑I =ᵐ[volume] Box.Icc I

Tactic:
rw [coe_eq_pi]
  exact Measure.univ_pi_Ioc_ae_eq_Icc

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
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‖⌉₊
⊢ ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0

Tactic:
simp [N]

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

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x ↦ ↑⌈x⌉₊ / x) atTop (𝓝 1)

Tactic:
· exact tendsto_nat_ceil_div_atTop

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

Goal state before:
pp: case neg
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol

Tactic:
have : ¬Integrable I l (fun x => c • f x) vol := mt (fun h => h.of_smul hc) hf

Goal state after:
case neg
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
this : ¬Integrable I l (fun x ↦ c • f x) vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol
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 ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
rw [convergenceR, dif_pos h₀] at hπ

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 ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (⋯.choose c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x✝ : E
x y : E ⧸ K
r : 𝕜
⊢ ⟪K.quotientEquivOrthogonal (r • x), K.quotientEquivOrthogonal y⟫_𝕜 =
    (starRingEnd 𝕜) r * ⟪K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal y⟫_𝕜

Tactic:
by rw [map_smul, inner_smul_left]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
⊢ (fun n ↦ Real.log (f n)) ~[l] fun n ↦ Real.log (g n)

Tactic:
by
  have hg := g_tendsto.eventually_ne_atTop 0
  have hf := hfg.symm.tendsto_atTop g_tendsto |>.eventually_ne_atTop 0
  rw [isEquivalent_iff_tendsto_one hg] at hfg
  have := hfg.log (by norm_num) |>.congr' <| by
    filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
  exact IsLittleO.isEquivalent <| calc
    (fun n ↦ Real.log (f n) - Real.log (g n)) =o[l] fun _ ↦ (1 : ℝ) := by simpa
    _ =o[l] fun n ↦ Real.log (g n) := isLittleO_one_left_iff ℝ |>.mpr <|
      tendsto_norm_atTop_atTop.comp <| Real.tendsto_log_atTop.comp g_tendsto

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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ ENNReal.ofReal |LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun.symm.symm| * volume s =
    volume s / ENNReal.ofReal (covolume L volume)

Tactic:
LinearEquiv.symm_symm,

Goal state after:
ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ ENNReal.ofReal |LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun| * volume s =
    volume s / ENNReal.ofReal (covolume L volume)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range N, f i‖ + ∑ i ∈ Finset.Ico N n, ε / 2 * g i ≤
    ‖∑ i ∈ Finset.range N, f i‖ + ∑ i ∈ Finset.range n, ε / 2 * g i

Tactic:
gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl

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

Goal state before:
pp: case convert_3
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0

Tactic:
· rw [frontier_equivFun, volume_image_eq_volume_div_covolume', h₄, ENNReal.zero_div]
    exact NullMeasurableSet.of_null h₄

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∏ x ∈ ?m.37, (g x)!) * multinomial s f = (∏ x ∈ ?m.37, (g x)!) * multinomial t g

pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ Finset α

Tactic:
multinomial_spec,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ (∏ x ∈ t, (g x)!) * multinomial s f = (∑ i ∈ t, g i)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (∏ x ∈ ?m.17, (?m.26 x)!) * multinomial s (Pi.single a n) = ∏ x ∈ ?m.17, (?m.26 x)!

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Type ?u.20

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ Finset ?m.13

pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ ?m.13 → ℕ

Tactic:
multinomial_spec,

Goal state after:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (∑ i ∈ s, Pi.single a n i)! = ∏ x ∈ s, (Pi.single a n x)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) =
    (Function.update f a (f a).succ a + Function.update f a (f a).succ b).choose (Function.update f a (f a).succ a) *
      (f a).succ

Tactic:
Function.update_self,

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b).succ * (f a + f b).choose (f a) =
    ((f a).succ + Function.update f a (f a).succ b).choose (f a).succ * (f a).succ