mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ π₂.tag J ∈ Box.Icc J
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ⟪x, b x✝⟫ * ⟪b x✝, y⟫ = ((innerSL 𝕜) x) ((b.repr y).ofLp x✝ • b x✝)

Tactic:
map_smul,

Goal state after:
case e'_2.a
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x y : E
this : ∑ x_1, ((innerSL 𝕜) x) ((b.repr y).ofLp x_1 • b x_1) = ((innerSL 𝕜) x) y
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ⟪x, b x✝⟫ * ⟪b x✝, y⟫ = (b.repr y).ofLp x✝ • ((innerSL 𝕜) x) (b x✝)
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.biUnionTagged πi).distortion = π.distortion

Tactic:
rw [distortion_biUnionTagged]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), (πi J).IsPartition
πiH : ∀ (J : Box ι), (πi J).IsHenstock
πir : ∀ (J : Box ι), (πi J).IsSubordinate r
h✝ : ∀ (J J_1 : Box ι), J_1 ∈ πi J → ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m
πid : ∀ (J : Box ι), (πi J).distortion = J.distortion
⊢ (π.boxes.sup fun J ↦ (πi J).distortion) = π.distortion
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(mk' I.lower (update I.upper i (min x (I.upper i)))) = ↑I ∩ {y | y i ≤ x}

Tactic:
coe_mk'

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) = ↑I ∩ {y | y i ≤ x}
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(mk' (update I.lower i (max x (I.lower i))) I.upper) = ↑I ∩ {y | x < y i}

Tactic:
coe_mk'

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 ↦ Ioc (update I.lower i (max x (I.lower i)) i_1) (I.upper i_1)) = ↑I ∩ {y | x < y i}
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
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ 0 < μ (vᶜ ∩ u) → μ (vᶜ ∩ u) < μ u → (μ u)⁻¹ ≠ ∞

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
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ (μ u - μ (vᶜ ∩ u)) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹

Tactic:
· simp only [uzero, ENNReal.inv_eq_top, imp_true_iff, Ne, not_false_iff]

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 : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
vmeas : MeasurableSet v
⊢ (μ u - μ (vᶜ ∩ u)) * (μ u)⁻¹ = μ (v ∩ u) * (μ u)⁻¹
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
⊢ ∑ x_1, (b.equiv b' e) ((b.repr x).ofLp x_1 • b x_1) = ∑ x_1, (b.repr x).ofLp x_1 • b' (e x_1)

Tactic:
map_smul,

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁶ : RCLike 𝕜
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
x : E
⊢ ∑ x_1, (b.repr x).ofLp x_1 • (b.equiv b' e) (b x_1) = ∑ x_1, (b.repr x).ofLp x_1 • b' (e x_1)
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case neg
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)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)

Goal state after:
case neg
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)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
r' : ℝ
hr' : 0 < r' ∧ r' < r.toReal
⊢ ∃ i, 0 < i ∧ x ∈ S i
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 ι
inst✝ : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ Orthonormal 𝕜 ⇑(basisSingleton ι h v ⋯)

Tactic:
by simpa

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
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,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε

Tactic:
set r : (ι → ℝ) → Ioi (0 : ℝ) := s.piecewise rs rs'

Goal state after:
ι : 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'
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inl
𝕜 : 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
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₁ : i < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
rw [inner_eq_zero_symm]
    exact ih a h₀ i hia₁

Goal state after:
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 ≠ ∞
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ ↑I
hxF : x ∈ F
⊢ x ∈ t

Tactic:
simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]

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 ≠ ∞
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ ↑I
hxF : x ∈ F
⊢ ∃ i, ∃ (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ ↑i
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case refine_2
ι : 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
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ (vol J) (f ((π₁.disjUnion π₂ h).tag J)) = (vol J) (f (π₂.tag J))

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orientation

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

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

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‖
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)

Tactic:
refine HasIntegral.of_mul (μ.real I + 1 + 1) fun ε ε0 => ?_

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 < ε
⊢ ∃ 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.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:
map_smul,

Goal state after:
𝕜 : 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 : 𝕜
⊢ ⟪r • K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal y⟫_𝕜 =
    (starRingEnd 𝕜) r * ⟪K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal y⟫_𝕜
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
this : Tendsto (fun n ↦ Real.log (f n) - Real.log (g n)) l (𝓝 (Real.log 1))
⊢ (fun n ↦ Real.log (f n) - Real.log (g n)) =o[l] fun x ↦ 1

Tactic:
by simpa

Goal state after:
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₂ := ⋯
⊢ covolume L₁ volume / covolume L₂ volume = |(Basis.ofZLatticeBasis ℝ L₂ b₂).det ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)|

Tactic:
rw [← Basis.det_mul_det _ (Pi.basisFun ℝ ι) _, abs_mul, Pi.basisFun_det_apply,
      ← Basis.det_inv, Units.val_inv_eq_inv_val, IsUnit.unit_spec, Pi.basisFun_det_apply,
      covolume_eq_det _ b₁, covolume_eq_det _ b₂, mul_comm, abs_inv]
    congr 3 <;> ext <;> simp

Goal state after:
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
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = volume s / ENNReal.ofReal (covolume L volume)

Tactic:
have hf : MeasurePreserving f :=
    ((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
      (PiLp.volume_preserving_toLp ι)

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 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.range n, ε / 2 * g i ≤
    ε / 2 * ‖∑ i ∈ Finset.range n, g i‖ + ε / 2 * ∑ i ∈ Finset.range n, g i

Tactic:
rw [← mul_sum]; gcongr

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ ↑k * (2 ^ (p * ↑k))⁻¹) ↔ 1 < p

Tactic:
rpow_mul zero_lt_two.le,

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ ↑k * ((2 ^ p) ^ ↑k)⁻¹) ↔ 1 < p
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
← summable_one_div_nat_rpow,

Goal state after:
a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ Summable fun n ↦ 1 / ↑n ^ s
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
ι : 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 : d = 0
⊢ ∑ p ∈ Fintype.piFinset fun x ↦ Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
have : IsEmpty ι := Fintype.card_eq_zero_iff.mp hd

Goal state after:
case pos
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 : d = 0
this : IsEmpty ι
⊢ ∑ p ∈ Fintype.piFinset fun x ↦ Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
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
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
ht₂ : ¬‖↑t - x‖ = 0
this : 0 < finrank ℤ ↥L
⊢ -↑(finrank ℤ ↥L) < 0

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ i ∈ s.support

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
    (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
r : R
hr : r ∈ s 0
x : Fin n → R
hx : x ∈ Set.univ.pi fun x ↦ s x.succ
i : Fin (n + 1)
x✝ : i ∈ Set.univ
⊢ Fin.cases ((eval x) (C r)) x 0 ∈ s 0

Tactic:
by simpa [eval_C] using hr

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

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, d i)! / ∏ i ∈ s, (d i)! = d.multinomial

Tactic:
Finsupp.multinomial,

Goal state after:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, d i)! / ∏ i ∈ s, (d i)! = (d.sum fun x ↦ id)! / d.prod fun x n ↦ n !
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
by
  induction ha generalizing b with | _ a _ iha
  induction hb with | _ b hb ihb
  refine Acc.intro _ fun s => ?_
  induction s with | _ c d
  rw [Sym2.GameAdd]
  dsimp
  rintro ((rc | rd) | (rd | rc))
  · exact iha c rc ⟨b, hb⟩
  · exact ihb d rd
  · rw [Sym2.eq_swap]
    exact iha d rd ⟨b, hb⟩
  · rw [Sym2.eq_swap]
    exact ihb c rc

Goal state after: