mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: 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 ℝ ι)))

Tactic:
exact discreteTopology_pi_basisFun

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✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ¬∀ (i : ι), (b.repr x) i ∈ Set.Ico 0 1
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
Set.mem_Ico,

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
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ¬∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i < 1
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

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

Tactic:
simp only [← withBotCoe_subset_iff, coe_inf] at *

Goal state after:
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : ↑I ⊆ ↑J₁
h₂ : ↑I ⊆ ↑J₂
⊢ ↑I ⊆ ↑J₁ ∩ ↑J₂
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r
⊢ I.distortion = J.distortion

Tactic:
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]
  congr 1 with i
  have : 0 < r := by
    by_contra hr
    have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
    rw [← h] at this
    exact this.not_gt (sub_pos.2 <| I.lower_lt_upper i)
  have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
  simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right₀ hn0]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Tactic:
by
  have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
    simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
  simpa [ofWithBot, le_def]

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'
⊢ ↑b.repr.symm = ↑b'.repr.symm

Tactic:
classical
        rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
        simp +instances only
        refine LinearMap.pi_ext fun i k => ?_
        have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
        rw [this, Pi.single_smul]
        replace h := congr_fun h i
        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
          coe_symm_linearEquiv, PiLp.toLp_single,
          LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
        rw [h]

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

Goal state before:
pp: case e'_1
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
x✝ : E
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

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

Goal state before:
pp: case e'_3
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

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

Goal state before:
pp: case e'_4
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

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₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
⊢ ∑ Ji ∈ π.boxes, f Ji = f I

Tactic:
rcases hπ.exists_splitMany_le with ⟨s, hs⟩

Goal state after:
ι : 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₀ → ∀ (s : Finset (ι × ℝ)), ∑ J ∈ (splitMany I s).boxes, f J = f I
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
Hle : ∀ J ∈ π, ↑J ≤ I₀
s : Finset (ι × ℝ)
hs : splitMany I s ≤ π
⊢ ∑ Ji ∈ π.boxes, f Ji = f I
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ (↑n)⁻¹ ^ Finset.univ.card = (↑n)⁻¹ ^ card ι

Tactic:
Finset.card_univ

Goal state after:
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
⊢ gramSchmidt 𝕜 f = f

Tactic:
ext i
  rw [gramSchmidt_def]
  trans f i - 0
  · congr
    apply Finset.sum_eq_zero
    intro j hj
    rw [Submodule.starProjection_apply, Submodule.coe_eq_zero]
    suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i by
      apply orthogonalProjectionOnto_apply_of_mem_orthogonal
      rw [mem_orthogonal_singleton_iff_inner_left, ← mem_orthogonal_singleton_iff_inner_right]
      exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
    rw [isOrtho_span]
    rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)
    apply hf
    exact (lt_of_le_of_lt hk (Finset.mem_Iio.mp hj)).ne
  · simp

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

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ ∀ᶠ (x : ℝ) in atTop,
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
      ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
    ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
⊢ (fun x ↦
      ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι *
        (↑⌊x⌋₊ / x) ^ card ι) =ᶠ[atTop]
    fun x ↦ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι * (↑⌊x⌋₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
⊢ (fun x ↦
      ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι *
        (↑⌈x⌉₊ / x) ^ card ι) =ᶠ[atTop]
    fun x ↦ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι * (↑⌈x⌉₊ / x) ^ card ι =
    ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
Module: Mathlib.Analysis.InnerProductSpace.Orientation

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

Tactic:
intro h
    rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
    simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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 ι
v : ι → M
⊢ |(e.adjustToOrientation x).det v| = |e.det v|

Tactic:
by
  rcases e.det_adjustToOrientation x with h | h <;> simp [h]

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

Goal state before:
pp: case e'_3
ι : 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‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
n : ℕ
hn : n ∈ Finset.image (fun J ↦ Nx (π.tag J)) π.boxes
hNxn : ∀ J ∈ π.filter fun J ↦ Nx (π.tag J) = n, Nx (π.tag J) = n
hrn : ∀ J ∈ π.filter fun J ↦ Nx (π.tag J) = n, r c (π.tag J) = ⋯.convergenceR (↑(δ n)) c (π.tag J)
this : l.MemBaseSet I c (⋯.convergenceR (↑(δ n)) c) (π.filter fun J ↦ Nx (π.tag J) = n)
⊢ ∑ J ∈ (π.filter fun J ↦ Nx (π.tag J) = n).boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J) =
    integralSum (⇑(f n)) μ.toBoxAdditive.toSMul (π.filter fun J ↦ Nx (π.tag J) = n)

Tactic:
refine sum_congr rfl fun J hJ => ?_
      simp [hNxn J hJ]

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

Goal state before:
pp: case e'_6
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : measureSpaceOfInnerProductSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) (EuclideanSpace.basisFun ι ℝ).toBasis.addHaar

Tactic:
MeasurableEquiv.coe_toEquiv_symm,

Goal state after:
case e'_6
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : measureSpaceOfInnerProductSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) (EuclideanSpace.basisFun ι ℝ).toBasis.addHaar
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this : MeasurableVAdd (↥L) E
⊢ covolume L μ = μ.real F

Tactic:
have : VAddInvariantMeasure L E μ := (inferInstance : VAddInvariantMeasure L.toAddSubgroup E μ)

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this✝ : MeasurableVAdd (↥L) E
this : VAddInvariantMeasure (↥L) E μ
⊢ covolume L μ = μ.real F
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : |f (max n N)| < |f n|
⊢ False

Tactic:
contrapose! hN

Goal state after:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : True
⊢ |f n| ≤ |f (max n N)|
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := ⋯
b₂ : Basis ι ℤ ↥L₂ := ⋯
⊢ |(Basis.ofZLatticeBasis ℝ L₂ b₂).det ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)| = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|

Tactic:
Basis.det_apply,

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |((Basis.ofZLatticeBasis ℝ L₂ b₂).toMatrix ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det| = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |((Basis.ofZLatticeBasis ℝ L₂ b₂).toMatrix ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det| = |↑(b₂.det fun i ↦ ⟨↑(b₁ i), ⋯⟩)|

Tactic:
Basis.det_apply,

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |((Basis.ofZLatticeBasis ℝ L₂ b₂).toMatrix ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det| =
    |↑(b₂.toMatrix fun i ↦ ⟨↑(b₁ i), ⋯⟩).det|
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
xm ym : G
hym : ym ∈ y.coeff.support
hm✝¹ : xm * ym ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support
hm✝ : xm * ym ∈ (y.coeff.sum fun i n ↦ (single (xm * i) (x.coeff xm * n)).coeff).support
hm : xm * ym ∈ (single (xm * ym) (x.coeff xm * y.coeff ym)).coeff.support
⊢ ∃ m' ∈ s, ∃ d, xm * ym = d * m'

Tactic:
refine (hy _ hym).imp fun sm p => And.imp_right ?_ p

Goal state after:
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
xm ym : G
hym : ym ∈ y.coeff.support
hm✝¹ : xm * ym ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support
hm✝ : xm * ym ∈ (y.coeff.sum fun i n ↦ (single (xm * i) (x.coeff xm * n)).coeff).support
hm : xm * ym ∈ (single (xm * ym) (x.coeff xm * y.coeff ym)).coeff.support
sm : G
p : sm ∈ s ∧ ∃ d, ym = d * sm
⊢ (∃ d, ym = d * sm) → ∃ d, xm * ym = d * sm
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
φ✝ : MvPolynomial σ R
⊢ ((↑f.symm).comp ↑f) φ✝ = φ✝

Tactic:
simp only [AlgHom.id_apply, AlgEquiv.symm_comp]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi : (if j = i then s else 0) = coeff i ((monomial i) r * x)
hj : s = coeff j ((monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
simp_rw [coeff_monomial_mul'] at hi hj

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hj : s = if i ≤ j then r * coeff (j - i) x else 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ expand 0 = (Algebra.ofId R (MvPolynomial σ R)).comp (aeval 1)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (expand 0) (X i) = ((Algebra.ofId R (MvPolynomial σ R)).comp (aeval 1)) (X i)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ expand 1 = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (expand 1) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p q : ℕ
⊢ expand (p * q) = (expand p).comp (expand q)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p q : ℕ
i : σ
⊢ (expand (p * q)) (X i) = ((expand p).comp (expand q)) (X i)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
⊢ (expand p).comp (bind₁ f) = bind₁ fun i ↦ (expand p) (f i)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i ↦ (expand p) (f i)) (X i)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case left
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
p' : MvPolynomial σ R
hp✝ : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n') 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m) 1 * r
⊢ m + Finsupp.single i 1 ≤ n

Tactic:
· simpa [← hn'] using hm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → τ
⊢ (rename f).comp (expand p) = (expand p).comp (rename f)

Tactic:
ext1 i

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → τ
i : σ
⊢ ((rename f).comp (expand p)) (X i) = ((expand p).comp (rename f)) (X i)
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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
hsne : s.Nonempty
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J ∈ s}
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ εs (π.tag J)

Tactic:
by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₁ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ (hεs0 _) _ (π.le_of_mem' _ hJ) ?_
        (hπδ.2 hlH J hJ) fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_pos hJs).symm

Goal state after: