mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ∑ j, star U₂ i✝.2 j.2 * star U₁ i✝.1 j.1 * U₁ j.1 j✝.1 * U₂ j.2 j✝.2 = 1 i✝ j✝

Tactic:
simp_rw [mul_assoc _ (star U₁ _ _), ← Finset.univ_product_univ, Finset.sum_product]

Goal state after:
case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ∑ x, ∑ x_1, star U₂ i✝.2 x_1 * (star U₁ i✝.1 x * U₁ x j✝.1) * U₂ x_1 j✝.2 = 1 i✝ j✝
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing A
inst✝³ : StarRing B
inst✝² : StarRing R
inst✝¹ : StarModule R A
inst✝ : StarModule R B
U : A
V : B
hU : U ∈ unitary A
hV : V ∈ unitary B
⊢ U ⊗ₜ[R] V ∈ unitary (A ⊗[R] B)

Tactic:
by
  simp [Unitary.mem_iff, hU, hV, Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f

Tactic:
refine fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩ <;>
    simp only [LinearMap.range_eq_top, LinearMap.ker_eq_bot, f.coe_coe, h.1, h.2]

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ ∞)
__spread✝⁻⁰ : WithLp ∞ (α × β) ≃ WithLp ∞ (β × α) := WithLp.congr ∞ (Equiv.prodComm α β)
x✝¹ x✝ : WithLp ∞ (α × β)
⊢ edist ((WithLp.congr ∞ (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr ∞ (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝

Tactic:
simp [WithLp.prod_edist_eq_sup, max_comm]

Goal state after:
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)

Goal state after:
case inl
this : StieltjesFunction.id.measure.IsAddLeftInvariant
H : parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ) = Icc 0 1
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1

case inr
this : StieltjesFunction.id.measure.IsAddLeftInvariant
H : parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ) = Icc (-1) 0
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = (∑ x, t x • b.repr (b x)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1

Tactic:
Finset.sum_apply',

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t ∈ Icc 0 1, ∀ (i : ι), (b.repr x) i = ∑ k, (t k • b.repr (b k)) i) ↔ ∀ (i : ι), (b.repr x) i ∈ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
⊢ volume (closedEBall a ∞) = 2 * ∞

pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r

Tactic:
· rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]

Goal state after:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 < g a.1}})

Tactic:
refine
    MeasurableSet.inter ?_
      ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
        (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ x = ((c ^ n - c ^ m)⁻¹ * (c ^ n - c ^ m)) • x

Tactic:
inv_mul_cancel₀ H,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ x = 1 • x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ c • span ℤ (Set.range ⇑b) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
rw [smul_span, Set.smul_set_range]

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
c : K
hc : c ≠ 0
⊢ span ℤ (Set.range fun i ↦ c • b i) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : s.Nonempty
h : finrank ℝ E = 0
⊢ μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s

Tactic:
have : Subsingleton E := finrank_zero_iff.1 h
    simp only [h, one_mul, ENNReal.ofReal_one, abs_one, Subsingleton.eq_univ_of_nonempty hs,
      pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))]

Goal state after:
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
hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
⊢ False

Tactic:
replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (Eventually.of_forall hJu_mem)

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)
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
α : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ ∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J ↦ f J = y).boxes, g J = ∑ J ∈ π.boxes, g J

Tactic:
by
  convert! sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

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
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
⊢ -↑n + ↑m ≠ 0

Tactic:
rwa [Ne, add_eq_zero_iff_eq_neg.not, neg_inj, Rat.intCast_inj, ← Ne]

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

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : J ≤ I₀
j : Fin (n + 1)
x : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
⊢ f x { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ } -
        f (J.lower i)
          { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ } +
      (f (J.upper i)
          { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ } -
        f x
          { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ }) =
    f (J.upper i)
        { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ } -
      f (J.lower i)
        { lower := fun x ↦ J.lower (i.succAbove x), upper := fun x ↦ J.upper (i.succAbove x), lower_lt_upper := ⋯ }

Tactic:
abel

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ (∀ (i : ι), B.lower i ≤ ↑(⌈↑n * x i⌉ - 1) / ↑n) ∧ ∀ (i : ι), (↑(⌈↑n * x i⌉ - 1) + 1) / ↑n ≤ B.upper i

Tactic:
hl,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = ↑(l i)
hu : ∀ (i : ι), B.upper i = ↑(u i)
⊢ (∀ (i : ι), ↑(l i) ≤ ↑(⌈↑n * x i⌉ - 1) / ↑n) ∧ ∀ (i : ι), (↑(⌈↑n * x i⌉ - 1) + 1) / ↑n ≤ B.upper i
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc.refine_2
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ ↑I
hμt : μ t ≠ ∞
⊢ μ (s ∩ ↑I) - μ t ≤ ↑ε

Tactic:
refine le_measure_sdiff.trans ((measure_mono ?_).trans hμF.le)

Goal state after:
case hbc.refine_2
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ ↑I
hμt : μ t ≠ ∞
⊢ (s ∩ ↑I) \ t ⊆ (s ∩ Box.Icc I) \ F
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 ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
exact tag_mem_smul_span _ _

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' => ?_
  rw [π.tag_biUnionTagged hJ hJ']

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 ι
inst✝ : Fintype ι
l : IntegrationParams
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
s : Finset α
f : α → (ι → ℝ) → E
g : α → F
h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp [hasIntegral_zero]
  | insert a s ha ihs =>
    simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
    exact h.1.add (ihs h.2)

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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
have hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ := by
      refine hC.mono J le_rfl le_rfl fun x _ => ?_; exact min_le_right _ _

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
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : (ι → ℝ) ≃L[ℝ] E := (EuclideanSpace.equiv ι ℝ).symm.trans (↑((stdOrthonormalBasis ℝ E).reindex e).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = volume (⇑f ⁻¹' s) / ENNReal.ofReal (covolume L volume)

Tactic:
← (covolume_comap L volume volume hf),

Goal state after:
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : (ι → ℝ) ≃L[ℝ] E := (EuclideanSpace.equiv ι ℝ).symm.trans (↑((stdOrthonormalBasis ℝ E).reindex e).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
    volume (⇑f ⁻¹' s) / ENNReal.ofReal (covolume (ZLattice.comap ℝ L ↑↑f) volume)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k

Tactic:
by
      rw [sum_range_succ, ← sum_Ico_consecutive]
      exacts [add_le_add ihn this,
        (add_le_add_left (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
        add_le_add_left (hu n.le_succ) _]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
⊢ ∑' (b : ℕ), ↑(f b) = ∞

Tactic:
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)

Goal state after:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(f b) = ∞
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case hx
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
J : Box ι
hJ : J ∈ B ∧ (J ∈ B → ¬↑J ⊆ U)
x : ι → ℝ
xJ : x ∈ J
xnU : x ∉ U
hx : x ∈ Box.Icc I \ U
⊢ x ∈ Metric.closedBall (t₁ J) (r / 2)

Tactic:
exact h₁.isSubordinate.infPrepartition π₂.toPrepartition J hJ.1 (Box.coe_subset_Icc xJ)

Goal state after: