mathlib-initiative/mathlib-tactics huggingface dataset:
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 ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖

Tactic:
have J : ‖f (σ' d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖ :=
      calc
        ‖f (σ' d⁻¹ • x) - y‖ = ‖d⁻¹ • f x - (d⁻¹ * d) • y‖ := by
          rwa [f.map_smulₛₗ _, inv_mul_cancel₀, one_smul, map_inv₀, map_inv₀,
            RingHomCompTriple.comp_apply, RingHom.id_apply]
        _ = ‖d⁻¹ • (f x - d • y)‖ := by rw [mul_smul, smul_sub]
        _ = ‖d‖⁻¹ * ‖f x - d • y‖ := by rw [norm_smul, norm_inv]
        _ ≤ ‖d‖⁻¹ * (2 * δ) := by gcongr
        _ = 1 / 2 * ‖y‖ := by simp [δ, field]; norm_num

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
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := x₁ - x₂
I : ‖f x - d • y‖ ≤ 2 * δ
J : ‖f (σ' d⁻¹ • x) - y‖ ≤ 1 / 2 * ‖y‖
⊢ ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖y‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := ⋯
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ⋯
ρ : F ≃ₗᵢ[ℝ] F := ⋯
V : Submodule ℝ F := ⋯
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
⊢ ρ (φ ↑v) = ↑v

Tactic:
have : ρ v = φ v := reflection_sub (φ.norm_map v).symm

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
this✝ : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
this : ρ ↑v = φ ↑v
⊢ ρ (φ ↑v) = ↑v
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ⇑b = Subtype.val) → span 𝕜 v = ⊤

Tactic:
rintro ⟨h, coe_h⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
h : Basis (↑v) 𝕜 E
coe_h : ⇑h = Subtype.val
⊢ span 𝕜 v = ⊤
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2)

Tactic:
simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
x✝¹ x✝ : WithLp p (α × β)
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝¹) ((WithLp.congr p (Equiv.prodComm α β)).toFun x✝) =
    edist x✝¹ x✝

Tactic:
rcases p.trichotomy with rfl | rfl | hp
    · absurd hp.elim; simp
    · simp [WithLp.prod_edist_eq_sup, max_comm]
    · simp [WithLp.prod_edist_eq_add hp, add_comm]

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ _i, edist x.ofLp y.ofLp ^ p.toReal) ^ (1 / p.toReal) = ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) * edist x.ofLp y.ofLp

Tactic:
simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
          ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]
        have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
          (ENNReal.coe_natCast (Fintype.card ι)).symm
        rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]

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

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
· have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
      have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
      rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one,
        Finset.mul_sum]
      simp_rw [← NNReal.mul_rpow, smul_apply]
      gcongr
      apply nnnorm_smul_le

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

Goal state before:
pp: a : ℝ
⊢ volume (Ici a) = ∞

Tactic:
rw [← measure_congr Ioi_ae_eq_Ici]

Goal state after:
a : ℝ
⊢ volume (Ioi a) = ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (t : TransvectionStruct ι ℝ), Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume

Tactic:
intro t

Goal state after:
case htransvec
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
t : TransvectionStruct ι ℝ
⊢ Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
⊢ (v.prod w).parallelepiped = v.parallelepiped ×ˢ w.parallelepiped

Tactic:
ext x
  simp only [Basis.coe_parallelepiped, TopologicalSpace.PositiveCompacts.coe_prod, Set.mem_prod,
    mem_parallelepiped_iff]
  constructor
  · intro h
    rcases h with ⟨t, ht1, ht2⟩
    constructor
    · use t ∘ Sum.inl
      constructor
      · exact ⟨(ht1.1 <| Sum.inl ·), (ht1.2 <| Sum.inl ·)⟩
      simp [ht2, Prod.fst_sum]
    · use t ∘ Sum.inr
      constructor
      · exact ⟨(ht1.1 <| Sum.inr ·), (ht1.2 <| Sum.inr ·)⟩
      simp [ht2, Prod.snd_sum]
  intro h
  rcases h with ⟨⟨t, ht1, ht2⟩, ⟨s, hs1, hs2⟩⟩
  use Sum.elim t s
  constructor
  · constructor
    · change ∀ x : ι ⊕ ι', 0 ≤ Sum.elim t s x
      aesop
    · change ∀ x : ι ⊕ ι', Sum.elim t s x ≤ 1
      aesop
  ext
  · simp [ht2, Prod.fst_sum]
  · simp [hs2, Prod.snd_sum]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ (basisFun p 𝕜 ι) i = single p i 1

Tactic:
by
  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]

Goal state after:
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 ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
i : ι
z : ℤ
hz : (algebraMap ℤ K) z = (b.repr m) i
⊢ ↑⌊(b.repr m) i⌋ = (b.repr m) i

Tactic:
← hz

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
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
i : ι
z : ℤ
hz : (algebraMap ℤ K) z = (b.repr m) i
⊢ ↑⌊(algebraMap ℤ K) z⌋ = (algebraMap ℤ K) z
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 ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
i : ι
z : ℤ
hz : (algebraMap ℤ K) z = (b.repr m) i
⊢ ↑⌈(b.repr m) i⌉ = (b.repr m) i

Tactic:
← hz

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
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
i : ι
z : ℤ
hz : (algebraMap ℤ K) z = (b.repr m) i
⊢ ↑⌈(algebraMap ℤ K) z⌉ = (algebraMap ℤ K) z
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✝ : Finite ι
x : E
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b

Tactic:
by
  cases nonempty_fintype ι
  refine ⟨-floor b x, ?_, fun y h => ?_⟩
  · exact (vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl
  · exact (vadd_mem_fundamentalDomain b y x).mp h

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
hpI : ¬p I
⊢ False

Tactic:
replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)

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
hpI : ¬p I
H_ind : ∀ J ≤ I, ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
⊢ ∃ π,
    π.IsPartition ∧
      π.IsHenstock ∧
        π.IsSubordinate r ∧
          (∀ J ∈ π, ∃ m, ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) ∧
            π.distortion = I.distortion

Tactic:
refine subbox_induction_on I (fun J _ hJ => ?_) fun z _ => ?_
  · choose! πi hP hHen hr Hn _ using hJ
    choose! n hn using Hn
    have hP : ((splitCenter J).biUnionTagged πi).IsPartition :=
      (isPartition_splitCenter _).biUnionTagged hP
    have hsub : ∀ J' ∈ (splitCenter J).biUnionTagged πi, ∃ n : ℕ, ∀ i,
        (J' :).upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n := by
      intro J' hJ'
      rcases (splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
      refine ⟨n J₁ J' + 1, fun i => ?_⟩
      simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ', div_div]
    refine ⟨_, hP, isHenstock_biUnionTagged.2 hHen, isSubordinate_biUnionTagged.2 hr, hsub, ?_⟩
    refine TaggedPrepartition.distortion_of_const _ hP.nonempty_boxes fun J' h' => ?_
    rcases hsub J' h' with ⟨n, hn⟩
    exact Box.distortion_eq_of_sub_eq_div hn
  · refine ⟨Box.Icc I ∩ closedBall z (r z),
      inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), ?_⟩
    intro J _ n Hmem HIcc Hsub
    rw [Set.subset_inter_iff] at HIcc
    refine ⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _,
      (isSubordinate_single _ _).2 HIcc.2, ?_, distortion_single _ _⟩
    simp only [TaggedPrepartition.mem_single, forall_eq]
    refine ⟨0, fun i => ?_⟩
    simp

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Tactic:
rw [← Box.mem_coe, H] at h₂

Goal state after:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False

Tactic:
rw [← Box.mem_coe, H] at h₂

Goal state after:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case refine_1
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.lower i)
Hle : ↑Js ⊆ ↑Jl
this : x ∈ Jl
⊢ J.lower i < y i

Tactic:
coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1

Goal state after:
case refine_1
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.lower i)
Hle : ↑Js ⊆ ↑I ∩ {y | J.lower i < y i}
this : x ∈ Jl
⊢ J.lower i < y 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
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
i : ι
⊢ (b.equiv b' e) (b i) = b' (e i)

Tactic:
simp only [OrthonormalBasis.equiv, LinearIsometryEquiv.trans_apply, OrthonormalBasis.repr_self]

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 : ι ≃ ι'
i : ι
⊢ b'.repr.symm ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (EuclideanSpace.single i 1)) = b' (e i)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ index n x = ν'

Tactic:
← mem_box_iff_index.mp hx'

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
x✝ : ∃ x ∈ ↑(box n ν), x ∈ ↑(box n ν')
x : ι → ℝ
hx : x ∈ ↑(box n ν)
hx' : x ∈ ↑(box n ν')
⊢ index n x = index n x
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc.refine_1
ι : 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
x : ι → ℝ
hx : x ∈ (U ∩ ↑I) \ (s ∩ ↑I)
⊢ x ∈ U \ (s ∩ Box.Icc I)

Tactic:
exact ⟨hx.1.1, fun hx' => hx.2 ⟨hx'.1, hx.1.2⟩⟩

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

Goal state before:
pp: case refine_4
ι : 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 ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ F x✝ / ↑n ^ card ι = 1 / (↑n).toReal ^ card ι * F x✝

Tactic:
ENNReal.toReal_natCast,

Goal state after:
case refine_4
ι : 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 ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ F x✝ / ↑n ^ card ι = 1 / ↑n ^ card ι * F x✝
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯
          (-positiveOrientation))
      ⋯ =
    -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
Or.by_cases,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        if hp : -positiveOrientation = positiveOrientation then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯
          (-positiveOrientation))
      ⋯ =
    -AlternatingMap.constLinearEquivOfIsEmpty 1
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation = o
this : o = positiveOrientation
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    b.toBasis.det

Tactic:
Or.by_cases,

Goal state after:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation = o
this : o = positiveOrientation
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        if h : o = positiveOrientation then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    b.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        ⋯.by_cases (fun x ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x ↦
          -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    -b.toBasis.det

Tactic:
Or.by_cases,

Goal state after:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
⊢ Nat.casesAuxOn (motive := fun a ↦ 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h ↦
        if h : o = positiveOrientation then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n h ↦
        Eq.rec (motive := fun x x_1 ↦ [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o ↦ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    -b.toBasis.det