mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
⊢ edist f h ≤ edist f g + edist g h

Tactic:
by
    rcases p.dichotomy with (rfl | hp)
    · simp only [edist_eq_iSup]
      cases isEmpty_or_nonempty ι
      · simp only [ciSup_of_empty, ENNReal.bot_eq_zero, add_zero, nonpos_iff_eq_zero]
      -- Porting note: `le_iSup` needed some help
      refine
        iSup_le fun i => (edist_triangle _ (g i) _).trans <| add_le_add
            (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)
    · simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
      calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ∞ (α × β)
⊢ max ‖x.fst‖ ‖x.snd‖ = max ‖idemFst x‖ ‖idemSnd x‖

Tactic:
← WithLp.norm_toLp_fst ∞ α β x.fst,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp ∞ (α × β)
⊢ max ‖toLp ∞ (x.fst, 0)‖ ‖x.snd‖ = max ‖idemFst x‖ ‖idemSnd x‖
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case mpr.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
h : Bijective ⇑f
⊢ (↑f).ker = ⊥

pp: case mpr.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
h : Bijective ⇑f
⊢ (↑f).range = ⊤

Tactic:
<;>

Goal state after:
case mpr.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
h : Bijective ⇑f
⊢ (↑f).ker = ⊥

case mpr.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
h : Bijective ⇑f
⊢ (↑f).range = ⊤
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (↑f).ker = ⊥

pp: case refine_2
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (↑f).range = ⊤

Tactic:
<;>

Goal state after:
case refine_1
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (↑f).ker = ⊥

case refine_2
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (↑f).range = ⊤
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

pp: case inr
this : StieltjesFunction.id.measure.IsAddLeftInvariant
H : parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ) = Icc (-1) 0
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1

Tactic:
<;>

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✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1

Tactic:
exact addHaarMeasure_self

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

pp: case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ MeasurableSet s

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.restrict s).prod volume) (regionBetween f g s)

Tactic:
Measure.restrict_prod_eq_prod_univ

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.prod volume).restrict (s ×ˢ univ)) (regionBetween f g s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)

Tactic:
Measure.restrict_prod_eq_prod_univ

Goal state after:
case e'_3
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s) =
    ((μ.prod volume).restrict (s ×ˢ univ)) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case e'_2
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ fundamentalDomain b = ⇑(b.equiv b₀ (Equiv.refl ι)) ⁻¹' fundamentalDomain b₀

pp: case e'_3
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ b₀.det ⇑b = LinearMap.det ↑(b.equiv b₀ (Equiv.refl ι)).symm

Tactic:
· rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]

Goal state after:
case e'_3
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ b₀.det ⇑b = LinearMap.det ↑(b.equiv b₀ (Equiv.refl ι)).symm
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
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ.real (closedBall x r) = μ.real (ball x r)

Tactic:
simp [measureReal_def, addHaar_closedBall_eq_addHaar_ball μ x r]

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

Goal state before:
pp: case bot
ι : Type u_1
⊢ ⋃ J, ⋃ (_ : ↑J = ⊥), ↑J = ↑⊥

pp: case coe
ι : Type u_1
a✝ : Box ι
⊢ ⋃ J, ⋃ (_ : ↑J = ↑a✝), ↑J = ↑↑a✝

Tactic:
<;>

Goal state after:
case bot
ι : Type u_1
⊢ ⋃ J, ⋃ (_ : ↑J = ⊥), ↑J = ↑⊥

case coe
ι : Type u_1
a✝ : Box ι
⊢ ⋃ J, ⋃ (_ : ↑J = ↑a✝), ↑J = ↑↑a✝
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑{ lower := l, upper := u, lower_lt_upper := h } = ⊥ ↔ ∃ i, u i ≤ l i

pp: case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑{ lower := l, upper := u, lower_lt_upper := h } = ⊥ ↔ ∃ i, u i ≤ l i

case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ⊥ ↔ ∃ i, u i ≤ l i
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = univ.pi fun i ↦ Ioc (l i) (u i)

Tactic:
exact coe_eq_pi _

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

Goal state before:
pp: case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (I.lower i + I.upper i) / 2 < I.upper i

pp: case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ I.lower i < (I.lower i + I.upper i) / 2

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (I.lower i + I.upper i) / 2 < I.upper i

case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ I.lower i < (I.lower i + I.upper i) / 2
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i)
        (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
split_ifs with hs

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

pp: case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)

case neg
ι : Type u_1
I : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∉ s
⊢ y i ∈ Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔
    y i ∈ Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: ι : Type u_1
I : Box ι
s : Set ι
i : ι
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
by_cases i ∈ s

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

case neg
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case pos
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

pp: case neg
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2

case neg
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2
Module: Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

Goal state before:
pp: case pos
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ I.upper i * 2 - (I.lower i + I.upper i) = I.upper i - I.lower i

pp: case neg
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ I.lower i + I.upper i - I.lower i * 2 = I.upper i - I.lower i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ I.upper i * 2 - (I.lower i + I.upper i) = I.upper i - I.lower i

case neg
ι : Type u_1
I : Box ι
s : Set ι
i : ι
h✝ : i ∉ s
⊢ I.lower i + I.upper i - I.lower i * 2 = I.upper i - I.lower i
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'

pp: case mpr
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'

Tactic:
<;>

Goal state after:
case mp
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₁ J') → ∃ J' ∈ π₁, J ∈ πi₂ J'

case mpr
ι : Type u_1
I : Box ι
π₁ : Prepartition I
πi₁ πi₂ : (J : Box ι) → Prepartition J
hi : ∀ J ∈ π₁, πi₁ J = πi₂ J
J : Box ι
⊢ (∃ J' ∈ π₁, J ∈ πi₂ J') → ∃ J' ∈ π₁, J ∈ πi₁ J'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case e'_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J = ⋯.choose

pp: case e'_3
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose

pp: case e'_4
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J = ⋯.choose

case e'_3
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose

case e'_4
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict J

pp: case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (∀ J ∈ π, πi J ≤ π'.restrict J) → π.biUnion πi ≤ π'

Tactic:
<;>

Goal state after:
case mp
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π.biUnion πi ≤ π' → ∀ J ∈ π, πi J ≤ π'.restrict J

case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (∀ J ∈ π, πi J ≤ π'.restrict J) → π.biUnion πi ≤ π'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ ∃ I' ∈ π', J ≤ I'

Tactic:
mem_biUnion

Goal state after:
case mpr
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ J ∈ π, πi J ≤ π'.restrict J
J : Box ι
hJ : ∃ J' ∈ π, J ∈ πi J'
⊢ ∃ I' ∈ π', J ≤ 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
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ 0 / μ ({x} + r • t) < ε

Tactic:
simpa only [ENNReal.zero_div] using εpos

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

Goal state before:
pp: case e_a.e_s
ι : 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✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp 2 fun i ↦ ↥(V i)
⊢ Finset.univ = (↑⟨Finset.univ.val, ⋯⟩).toFinset

pp: case e_a.e_s
ι : 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✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp 2 fun i ↦ ↥(V i)
⊢ Finset.univ = (↑⟨Finset.univ.val, ⋯⟩).toFinset

Tactic:
<;>

Goal state after:
case e_a.e_s
ι : 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✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp 2 fun i ↦ ↥(V i)
⊢ Finset.univ = (↑⟨Finset.univ.val, ⋯⟩).toFinset

case e_a.e_s
ι : 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✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
v w : PiLp 2 fun i ↦ ↥(V i)
⊢ Finset.univ = (↑⟨Finset.univ.val, ⋯⟩).toFinset
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
i j : ι
⊢ ⟪b i, b j⟫ = if i = j then 1 else 0

Tactic:
← b.repr.inner_map_map (b i) (b j),

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
i j : ι
⊢ ⟪b.repr (b i), b.repr (b j)⟫ = if i = j then 1 else 0