mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ span ℤ (⇑↑(LinearEquiv.restrictScalars ℤ f) '' Set.range ⇑b) = span ℤ (Set.range ⇑(b.map f))

Tactic:
LinearEquiv.coe_coe,

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
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ span ℤ ((fun a ↦ (LinearEquiv.restrictScalars ℤ f) a) '' Set.range ⇑b) = span ℤ (Set.range ⇑(b.map f))
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
hf : LinearMap.det f ≠ 0
⊢ ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

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
r : ℝ
hr : r ≠ 0
⊢ ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

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✝ : Finite ι
x : E
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b

Tactic:
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.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ Box.Icc J}

Tactic:
rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : { i | J₁.lower i = x i } = { i | J₂.lower i = x i })

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
J₁ : Box ι
h₁ : J₁ ∈ π
hx₁ : x ∈ Box.Icc J₁
J₂ : Box ι
h₂ : J₂ ∈ π
hx₂ : x ∈ Box.Icc J₂
H : {i | J₁.lower i = x i} = {i | J₂.lower i = x i}
⊢ J₁ = J₂
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ ↑x✝

Tactic:
Box.mem_coe,

Goal state after:
case e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ x✝
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ ∑ x, x✝.ofLp x ^ 2 ≤ r ^ 2

Tactic:
mem_closedBall_zero_iff,

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ ‖x✝‖ ≤ r ↔ ∑ x, x✝.ofLp x ^ 2 ≤ r ^ 2
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
⊢ finrank ℤ ↥L = finrank K E

Tactic:
rw [finrank_eq_card_chooseBasisIndex]

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
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = finrank K E
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)
⊢ (Set.range b \ Set.range ⇑e).Nonempty

Tactic:
by
      rw [Basis.coe_mk, Subtype.range_coe_subtype, Set.ofPred_mem_eq, ← Set.toFinset_nonempty]
      contrapose! h
      rw [Set.toFinset_sdiff, Finset.sdiff_eq_empty_iff_subset] at h
      replace h := Finset.card_le_card h
      rwa [h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card ht_lin]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
hp : ∀ J ∈ π, p J
⊢ π.filter p = π

Tactic:
ext J
  simpa using hp J

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

Goal state before:
pp: case e'_2
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π.toPrepartition), x ∈ ↑x✝

Tactic:
Box.mem_coe,

Goal state after:
case e'_2
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π.toPrepartition), x ∈ x✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
⊢ J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition

Tactic:
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]

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

Goal state before:
pp: case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))

pp: case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))

Tactic:
· rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
inst✝ : Fintype ι
h₁ : π₁.IsSubordinate r
h₂ : π₂.IsSubordinate r
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

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

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

Tactic:
· rw [disjUnion_tag_of_mem_left _ hJ]
    exact h₁ _ hJ

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

Goal state before:
pp: ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ J ∈ (split J i x).boxes

Tactic:
rw [mem_boxes, mem_split_iff]

Goal state after:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ Basis ι K E

Tactic:
have : Module.Finite ℤ L := ZLattice.module_finite K L

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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
this : Module.Finite ℤ ↥L
⊢ Basis ι K E
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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ Fintype.card ι = finrank K E

Tactic:
rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank K L]

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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i✝ i : ι
⊢ ↑(ofZLatticeBasis K L b).repr (L.subtype (b i)) = (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K)) (↑b.repr (b i))

Tactic:
LinearEquiv.coe_coe,

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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
x : ↥L
i✝ i : ι
⊢ (ofZLatticeBasis K L b).repr (L.subtype (b i)) = (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K)) (b.repr (b i))
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun J ↦ ¬p J
this✝ : Disjoint π₁.iUnion π₂.iUnion
this : ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion
⊢ (π₁.disjUnion π₂.toPrepartition this✝).iUnion = ↑I \ (π.filter p).iUnion

Tactic:
by
      simp [π₂, *]

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : NormedField K
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace K F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
⊢ span K (⇑↑↑e ⁻¹' ↑L) = ⊤

Tactic:
LinearEquiv.coe_coe,

Goal state after:
K : Type u_1
inst✝⁶ : NormedField K
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace K F
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice K L
e : F ≃L[K] E
⊢ span K (⇑↑e ⁻¹' ↑L) = ⊤
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: case e'_2
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι' 𝕜 E
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ ((a.toBasis.toMatrix ⇑b)ᴴ * a.toBasis.toMatrix ⇑b) i j = ⟪a.repr (b i), a.repr (b j)⟫

Tactic:
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, star_def, PiLp.inner_apply,
      inner_apply']
    congr

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ toFilteriUnion I π₁ = toFilteriUnion I π₂

Tactic:
simp only [toFilteriUnion, toFilterDistortioniUnion, h]

Goal state after:
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 ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
⊢ LeftInverse (fun b ↦ ⟨(sigmaOrthonormalBasisIndexEquiv hn hV hV') ⟨i, b⟩, ⋯⟩) fun a ↦
    Fin.cast ⋯ ((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm ↑a).snd

Tactic:
by grind [subordinateOrthonormalBasisIndex_def, Fin.cast_eq_self]

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
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillation f x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' eball x (ENNReal.ofReal δ)) ≤ ε

Tactic:
simp only [← oscillationWithin_univ_eq_oscillation] at hK

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
comp : IsCompact K
f : E → F
ε : ℝ≥0∞
hK : ∀ x ∈ K, oscillationWithin f univ x < ε
⊢ ∃ δ > 0, ∀ x ∈ K, ediam (f '' eball x (ENNReal.ofReal δ)) ≤ ε
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 ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp : M x = L (p1 x) + L3 (p2 x)
Mx_orth : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖M x‖ = ‖x‖

Tactic:
← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _),

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 ι
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L✝ L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp : M x = L (p1 x) + L3 (p2 x)
Mx_orth : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖M x‖ ^ 2 = ‖x‖ ^ 2
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case e'_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this✝ : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
n : ℕ
hn : n ∈ Finset.image (fun J ↦ Nx (π.tag J)) π.boxes
hNxn : ∀ J ∈ π.filter fun J ↦ Nx (π.tag J) = n, Nx (π.tag J) = n
hrn : ∀ J ∈ π.filter fun J ↦ Nx (π.tag J) = n, r c (π.tag J) = ⋯.convergenceR (↑(δ n)) c (π.tag J)
this : l.MemBaseSet I c (⋯.convergenceR (↑(δ n)) c) (π.filter fun J ↦ Nx (π.tag J) = n)
J : Box ι
hJ : J ∈ (π.filter fun J ↦ Nx (π.tag J) = n).boxes
⊢ μ.real ↑J • (f (Nx (π.tag J))) (π.tag J) =
    (μ.toBoxAdditive.toSMul J) ((f n) ((π.filter fun J ↦ Nx (π.tag J) = n).tag J))

Tactic:
simp [hNxn J hJ]

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

Goal state before:
pp: case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi✝ : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ
hfgi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (fun x ↦ ‖(f n) x - g x‖) (↑J) μ
J : Box ι
hJ : J ∈ π.boxes
⊢ ‖∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ - ∫ (x : ι → ℝ) in ↑J, g x ∂μ‖ ≤
    ∫ (x : ι → ℝ) in ↑J, ‖(f N₀) x - g x‖ ∂μ

Tactic:
← integral_sub (hfi _ J hJ) (hgi J hJ)

Goal state after:
case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi✝ : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ
hfgi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (fun x ↦ ‖(f n) x - g x‖) (↑J) μ
J : Box ι
hJ : J ∈ π.boxes
⊢ ‖∫ (a : ι → ℝ) in ↑J, (f (Nx (π.tag J))) a - g a ∂μ‖ ≤ ∫ (x : ι → ℝ) in ↑J, ‖(f N₀) x - g x‖ ∂μ
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))

Tactic:
have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le

Goal state after:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
this : ↑(u k) ≤ ↑(u k.succ)
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
refine ⟨fun h ↦ summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
    fun h ↦ .of_nat_of_neg (summable_one_div_nat_pow.mpr h)
      (((summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n ↦ ?_)⟩

Goal state after:
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / ↑(-↑n) ^ p