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

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
r : ℝ≥0
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≤ ↑r ↔ ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i)) ≤ ↑r

Tactic:
have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _

Goal state after:
case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g : PiLp ∞ α
h✝ : Nonempty ι
r : ℝ≥0
this : BddAbove (range fun i ↦ dist (f.ofLp i) (g.ofLp i))
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≤ ↑r ↔ ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i)) ≤ ↑r
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (1 ≤ 0)
x1✝ x2✝ : WithLp 0 (α × β)
⊢ edist (WithLp.map 0 (Prod.map f g) x1✝) (WithLp.map 0 (Prod.map f g) x2✝) = edist x1✝ x2✝

Tactic:
absurd hp.elim

Goal state after:
case inl
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (1 ≤ 0)
x1✝ x2✝ : WithLp 0 (α × β)
⊢ ¬1 ≤ 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
absurd hp.elim

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ 0)
__spread✝⁻⁰ : WithLp 0 (α × β) ≃ WithLp 0 (β × α) := WithLp.congr 0 (Equiv.prodComm α β)
x✝¹ x✝ : WithLp 0 (α × β)
⊢ ¬1 ≤ 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ 0)
x✝¹ x✝ : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ edist ((fun x ↦ WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd))) x✝¹)
      ((fun x ↦ WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd))) x✝) =
    edist x✝¹ x✝

Tactic:
absurd hp.elim

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoEMetricSpace α'
inst✝ : PseudoEMetricSpace β'
hp : Fact (1 ≤ 0)
x✝¹ x✝ : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ ¬1 ≤ 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ 0)
__spread✝⁻⁰ : WithLp 0 (α × β) ≃ α := (WithLp.equiv 0 (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ edist x.fst y.fst = edist x y

Tactic:
absurd hp.elim

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ 0)
__spread✝⁻⁰ : WithLp 0 (α × β) ≃ α := (WithLp.equiv 0 (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ ¬1 ≤ 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
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 β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y

Tactic:
simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']

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

Tactic:
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

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

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

Tactic:
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ ↑(Pi.basisFun ℝ ι).parallelepiped = ↑(PositiveCompacts.piIcc01 ι)

Tactic:
by
    refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)
    · classical convert! parallelepiped_single (ι := ι) 1
    · exact zero_le_one

Goal state after:
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)
⊢ μ ↑s = 0

Tactic:
apply addHaar_eq_zero_of_disjoint_translates μ _ A _
    (Submodule.closed_of_finiteDimensional s).measurableSet

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)
⊢ Pairwise (Disjoint on fun n ↦ {c ^ n • x} + ↑s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
Cg : Continuous ⇑g
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑e.symm
this : (map (⇑e) μ).IsAddHaarMeasure
ecomp : ⇑e.symm ∘ ⇑e = id
⊢ map (⇑e.symm) (map (⇑g) (map (⇑e) μ)) = ENNReal.ofReal |(LinearMap.det g)⁻¹| • μ

Tactic:
rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul,
    map_map Cesymm.measurable Ce.measurable, ecomp, Measure.map_id]

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

Goal state before:
pp: case e'_3
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : LinearMap.det ↑f ≠ 0
⊢ LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹

Tactic:
simp only [LinearEquiv.det_coe_symm]

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Tactic:
by
  /- By second-countability, we cover `s` by countably many intervals `(a, b)` (except maybe for
    two endpoints, which don't matter since `μ` does not have any atom). -/
  let T : s × s → Set ℝ := fun p => Ioo p.1 p.2
  let u := ⋃ i : ↥s × ↥s, T i
  have hfinite : (s \ u).Finite := s.finite_sdiff_iUnion_Ioo'
  obtain ⟨A, A_count, hA⟩ :
    ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
    isOpen_iUnion_countable _ fun p => isOpen_Ioo
  have : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p := by
    intro x hx
    by_cases h'x : x ∈ ⋃ i : ↥s × ↥s, T i
    · rw [← hA] at h'x
      obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
        simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using h'x
      right
      exact mem_biUnion pA ⟨hx, xp⟩
    · exact Or.inl ⟨hx, h'x⟩
  apply ae_restrict_of_ae_restrict_of_subset this
  rw [ae_restrict_union_iff, ae_restrict_biUnion_iff _ A_count]
  constructor
  · have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
    simp only [this, ae_zero, eventually_bot]
  · rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
    dsimp [T]
    rcases le_or_gt b a with (hba | hab)
    · simp only [Ioo_eq_empty_of_le hba, inter_empty, restrict_empty, ae_zero, eventually_bot]
    · exact h a b as bs hab

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

Goal state before:
pp: case convert_2
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
h : Set.MapsTo ⇑b.equivFun ↑(span ℤ (Set.range ⇑b)) ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun) (↑(span ℤ (Set.range ⇑b))) (↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) h)

Tactic:
refine Subtype.map_injective _ (Basis.equivFun b).injective

Goal state after:
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₀.reindex (Equiv.refl ι).symm) = fundamentalDomain b₀

Tactic:
Equiv.refl_symm,

Goal state after:
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₀.reindex (Equiv.refl ι)) = fundamentalDomain b₀
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I J₁ J₂ : WithBot (Box ι)
h₁ : I ≤ J₁
h₂ : I ≤ J₂
⊢ I ≤ J₁ ⊓ J₂

Tactic:
simp only [← withBotCoe_subset_iff, coe_inf] at *
      exact subset_inter h₁ h₂

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

Goal state before:
pp: ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.boxes.biUnion fun J ↦ (πi J).boxes
⊢ J ≤ I

Tactic:
simp only [Finset.mem_biUnion, mem_boxes] at hJ
    rcases hJ with ⟨J', hJ', hJ⟩
    exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')

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

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ √(∑ x_1, x.ofLp x_1 ^ 2) < r ↔ ∑ x_1, x.ofLp x_1 ^ 2 < r ^ 2

Tactic:
sqrt_lt this hr

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
⊢ (∀ (x : ℤ), fract e (x • v) ∈ Metric.closedBall 0 (∑ i, ‖e i‖)) ∧ ∀ (x : ℤ), fract e (x • v) ∈ ↑L

Tactic:
refine ⟨fun _ ↦ mem_closedBall_zero_iff.mpr (norm_fract_le e _), fun _ => ?_⟩

Goal state after:
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
x✝ : ℤ
⊢ fract e (x✝ • v) ∈ ↑L
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 ι
b b' : OrthonormalBasis ι 𝕜 E
i : ι
k : 𝕜
this : k = k • 1
h : b.repr.symm (EuclideanSpace.single i 1) = b'.repr.symm (EuclideanSpace.single i 1)
⊢ k • b.repr.symm (PiLp.single 2 i 1) = k • b'.repr.symm (PiLp.single 2 i 1)

Tactic:
h

Goal state after:
ι : 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 ι
b b' : OrthonormalBasis ι 𝕜 E
i : ι
k : 𝕜
this : k = k • 1
h : b.repr.symm (EuclideanSpace.single i 1) = b'.repr.symm (EuclideanSpace.single i 1)
⊢ k • b'.repr.symm (EuclideanSpace.single i 1) = k • b'.repr.symm (PiLp.single 2 i 1)
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

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

Tactic:
not_lt,

Goal state after:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ ¬x < J.upper i
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
⊢ finrank K ↥(span K (Set.range b)) ≤ Fintype.card (Free.ChooseBasisIndex ℤ ↥L)

Tactic:
convert! finrank_span_le_card (R := K) (Set.range b)

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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) = v

Tactic:
_root_.Module.Basis.coe_toOrthonormalBasis,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : ⊤ ≤ span 𝕜 (range v)
⊢ ⇑(Basis.mk ⋯ hsp) = v
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ (fun π' ↦ π'.iUnion = ↑I \ π₁.iUnion) = fun π' ↦ π'.iUnion = ↑I \ π₂.iUnion

Tactic:
h

Goal state after:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ (fun π' ↦ π'.iUnion = ↑I \ π₂.iUnion) = fun π' ↦ π'.iUnion = ↑I \ π₂.iUnion
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hf : ContinuousWithinAt f D x
ε : ℝ≥0∞
hε : 0 < ε
⊢ 0 < ε / 2

Tactic:
by simp [ne_of_gt hε]

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
⊢ ENNReal.ofReal (a - (a - r) / 2) + ENNReal.ofReal ((a - r) / 2) = ENNReal.ofReal a

Tactic:
rw [← ofReal_add (by linarith) (by linarith), sub_add_cancel]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₁.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J

Tactic:
h

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
inst✝ : Finite ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
s : Finset (ι × ℝ)
h₁ : (π₁.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
h₂ : (π₂.biUnion fun J ↦ splitMany J s) = (splitMany I s).filter fun J ↦ ↑J ⊆ π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

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

Tactic:
intro J hJ j x

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : ↑J ≤ ↑I₀
j : Fin (n + 1)
x : ℝ
⊢ x ∈ Set.Ioo (J.lower j) (J.upper j) →
    Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower j x) +
        Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper j x) =
      f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ (∀ (i : ι), x i ∈ Set.Ioc (↑(ν i) / ↑n) ((↑(ν i) + 1) / ↑n)) ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n

Tactic:
Set.mem_Ioc

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
⊢ (fun ν ↦ box n ν) a₁✝ = (fun ν ↦ box n ν) a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
h : (fun ν ↦ box n ν) a₁✝ = (fun ν ↦ box n ν) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
⊢ Finset (ι → ℤ)

Tactic:
refine (setFinite_index n B.measurableSet_coe.nullMeasurableSet ?_).toFinset
  exact lt_top_iff_ne_top.mp (IsBounded.measure_lt_top B.isBounded)

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (prepartition n B).tag (box n ν) = tag n ν

Tactic:
dsimp only [prepartition]

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then tag n hI.choose else ⋯.choose) = tag n ν
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x y : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
hy : y ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
h : index n x = index n y
⊢ tag n (index n x) = tag n (index n y)

Tactic:
h

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x y : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
hy : y ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
h : index n x = index n y
⊢ tag n (index n y) = tag n (index n y)