mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖

Tactic:
refine ⟨(ε / 2)⁻¹ * ‖c‖ * 2 * n, by positivity, fun y => ?_⟩

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
rcases Metric.mem_closure_iff.1 (H this) _ δpos with ⟨z₁, z₁im, h₁⟩

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomIsometric σ
inst✝¹ : RingHomIsometric σ'
inst✝ : CompleteSpace F
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ‖d‖ * ‖y‖ / 4
δpos : 0 < δ
this : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
h₁ : dist (a + d • y) z₁ < δ
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Tactic:
let v : K₁ := orthogonalProjectionOnto K₁ x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst✝ : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := K₁.orthogonalProjectionOnto x
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearEquiv.det K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
ext
  rw [LinearEquiv.coe_det, Units.val_pow_eq_pow_val]
  exact K.det_reflection

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
⊢ p.IsSymmetricProjection ↔ ∃ (x : p.range.HasOrthogonalProjection), p = ↑p.range.starProjection

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection _⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
⊢ ∃ (x : p.range.HasOrthogonalProjection), p = ↑p.range.starProjection
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
⊢ 2 * C + 1 > 0

Tactic:
linarith

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
⊢ 0 ≤ dist f g

Tactic:
rcases p.dichotomy with (rfl | h)
      · simp [prod_dist_eq_sup]
      · simp only [dist, one_div, dite_eq_ite]
        split_ifs with hp' <;> positivity

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ edist x y ≤ ↑(2 ^ (1 / ∞).toReal) * edist x.ofLp y.ofLp

Tactic:
simp [edist]

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

Goal state before:
pp: case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x.ofLp y.ofLp

Tactic:
simp [edist]

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

Goal state before:
pp: case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ edist x.ofLp y.ofLp

Tactic:
simp [edist]

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

Goal state before:
pp: case pos
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : p = 0
⊢ 0 ≤ ↑⋯.toFinset.card

Tactic:
linarith

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
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ 0
hp : p = ∞
⊢ False

Tactic:
linarith

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

Goal state before:
pp: a : ℝ
h : a ≠ 0
| 1 • Measure.map (fun x ↦ a * x) volume

Tactic:
one_smul

Goal state after:
a : ℝ
h : a ≠ 0
| Measure.map (fun x ↦ a * x) volume
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = 1 • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume

Tactic:
one_smul

Goal state after:
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = Measure.map (⇑(toLin' (Matrix.diagonal D))) volume
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ ‖single p i (b₁ - b₂)‖₊ = ‖b₁ - b₂‖₊

Tactic:
nnnorm_single

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ ‖b₁ - b₂‖₊ = ‖b₁ - b₂‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case refine_1
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x : R
y z : (i : ι) → α i
⊢ dist (x • y) (x • z) ≤ dist x 0 * dist y z

pp: case refine_2
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x y : R
z : (i : ι) → α i
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0

Tactic:
· simpa [dist_pseudoMetricSpaceToPi] using dist_smul_pair x (toLp p y) (toLp p z)

Goal state after:
case refine_2
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst✝² : SeminormedRing R
inst✝¹ : (i : ι) → Module R (α i)
inst✝ : ∀ (i : ι), IsBoundedSMul R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
x y : R
z : (i : ι) → α i
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0
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 = 1 • x

Tactic:
one_smul

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 = 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
⊢ span ℤ (c • Set.range ⇑b) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
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.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self,
    mem_fundamentalDomain, Set.mem_Ico]

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

Goal state before:
pp: case refine_1
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
⊢ E ⧸ span ℤ (Set.range ⇑b) → ↑(fundamentalDomain b)

Tactic:
refine fun q => Quotient.liftOn q (fractRestrict b) (fun _ _ h => ?_)
    rw [Subtype.mk.injEq, fractRestrict_apply, fractRestrict_apply, fract_eq_fract]
    exact QuotientAddGroup.leftRel_apply.mp h

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

Goal state before:
pp: case e_f
ι : 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 : ι
this : 0 < r
hn0 : Real.nnabs r ≠ 0
⊢ ↑(Finset.univ.sup fun a ↦
        Real.nnabs (J.upper a - J.lower a) / Real.nnabs r / (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) =
    ↑(Finset.univ.sup fun a ↦ Real.nnabs (J.upper a - J.lower a) / Real.nnabs (J.upper i - J.lower i))

Tactic:
div_div_div_cancel_right₀ hn0

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J
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
⊢ p I

Tactic:
by
  by_contra hpI
  -- First we use `H_ind` to construct a decreasing sequence of boxes such that `∀ m, ¬p (J m)`.
  replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
  simp only [not_forall] at H_ind
  choose! s hs using H_ind
  set J : ℕ → Box ι := fun m ↦ (fun J ↦ splitCenterBox J (s J))^[m] I
  have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) :=
    fun m ↦ iterate_succ_apply' _ _ _
  -- Now we prove some properties of `J`
  have hJmono : Antitone J :=
    antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
  have hJle (m) : J m ≤ I := hJmono zero_le
  have hJp (m) : ¬p (J m) := Nat.recOn m hpI fun m ↦ by simpa only [J_succ] using hs (J m) (hJle m)
  have hJsub (m i) : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m := by
    induction m with
    | zero => simp [J]
    | succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
  have h0 : J 0 = I := rfl
  clear_value J
  clear hpI hs J_succ s
  -- Let `z` be the unique common point of all `(J m).Icc`. Then `H_nhds` proves `p (J m)` for
  -- sufficiently large `m`. This contradicts `hJp`.
  set z : ι → ℝ := ⨆ m, (J m).lower
  have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
    mem_iInter.1 (ciSup_mem_iInter_Icc_of_antitone_Icc
      ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
  have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
  have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
  have hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z) :=
    tendsto_atTop_ciSup (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ ↦ hm ▸ (hJl_mem m).2⟩
  have hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z) := by
    suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
    refine tendsto_pi_nhds.2 fun i ↦ ?_
    simpa [hJsub] using
      tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
  replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z) :=
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (Eventually.of_forall hJl_mem)
  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)
  rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩
  rcases (tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩
  exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))

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

Goal state before:
pp: ι : Type u_1
I : Box ι
⊢ Injective boxes

Tactic:
rintro ⟨s₁, h₁, h₁'⟩ ⟨s₂, h₂, h₂'⟩ (rfl : s₁ = s₂)

Goal state after:
ι : Type u_1
I : Box ι
s₁ : Finset (Box ι)
h₁ : ∀ J ∈ s₁, J ≤ I
h₁' : (↑s₁).Pairwise (Disjoint on Box.toSet)
h₂ : ∀ J ∈ s₁, J ≤ I
h₂' : (↑s₁).Pairwise (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }
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:
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

Goal state after:
ι : 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'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ ⟪v, single i a⟫ = a * (starRingEnd ((fun x ↦ 𝕜) i)) (v.ofLp i)

Tactic:
by simp [PiLp.inner_apply]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ⟪b i, x⟫_𝕜 • b i = x

Tactic:
nth_rw 2 [← (b.sum_repr x)]

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
⊢ ∑ i, ⟪b i, x⟫_𝕜 • b i = ∑ i, (b.repr x).ofLp i • b i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
cases h

Goal state after:
case inl
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

case inr
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case insert
ι : 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₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
⊢ ∑ J ∈ ((splitMany I s).biUnion fun J ↦ split J a.1 a.2).boxes, f J = f I

Tactic:
← ihs,

Goal state after:
case insert
ι : 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₀ →
      ∀ {i : ι} {x : ℝ},
        x ∈ Set.Ioo (I.lower i) (I.upper i) →
          Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I
I : Box ι
hI : ↑I ≤ I₀
a : ι × ℝ
s : Finset (ι × ℝ)
a✝ : a ∉ s
ihs : ∑ J ∈ (splitMany I s).boxes, f J = f I
⊢ ∑ J ∈ ((splitMany I s).biUnion fun J ↦ split J a.1 a.2).boxes, f J = ∑ J ∈ (splitMany I s).boxes, f J
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ∞
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
h' : μ (s ∩ ({x} + r • t')) = 0
⊢ False

Tactic:
simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
hf : ContinuousAt f x
⊢ oscillation f x = 0

Tactic:
by
  rw [← continuousWithinAt_univ f x] at hf
  exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: 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)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
⊢ a - (a - r) / 2 > r

Tactic:
linarith

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: 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)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ 0 ≤ a - (a - r) / 2

Tactic:
linarith

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: 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)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
y : E
hy : y ∈ eball x (ENNReal.ofReal ((a - r) / 2))
z : E
hz : z ∈ eball y (ENNReal.ofReal (a - (a - r) / 2)) ∩ D
⊢ 0 ≤ (a - r) / 2

Tactic:
linarith

Goal state after: