mathlib-initiative/mathlib-tactics huggingface dataset:
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) = ⊤
⊢ Function.Injective b

Tactic:
exact Subtype.coe_injective.comp (Basis.injective _)

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

Goal state before:
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 (π₂.tag J) ↑(r (π₂.tag J))

Tactic:
exact h₂ _ hJ

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

Goal state before:
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
⊢ π₂.tag J ∈ Box.Icc J

Tactic:
exact h₂ _ hJ

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

Tactic:
have : Fintype ι := Fintype.ofEquiv _ e

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
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ Basis ι K E
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ (π.boxes.sup fun J ↦ (πi J).distortion) ≤ c

Tactic:
Finset.sup_le_iff

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ ∀ b ∈ π.boxes, (πi b).distortion ≤ c
Module: Mathlib.Analysis.BoxIntegral.Partition.Additive

Goal state before:
pp: case refine_1
ι : 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 : ℝ
hx : x ∈ Set.Ioo (J.lower i) (J.upper i)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower i x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper i x) =
    f (J.upper i) (J.face i) - f (J.lower i) (J.face i)

Tactic:
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, update_self, ← WithBot.some_eq_coe,
          Option.elim', Box.face, Function.comp_def, update_of_ne (Fin.succAbove_ne _ _)]
        abel

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

Goal state before:
pp: ι : 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) ≠ ∞
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε

Tactic:
obtain ⟨F, hFs, hFc, hμF⟩ : ∃ F, F ⊆ s ∩ Box.Icc I ∧ IsClosed F ∧ μ ((s ∩ Box.Icc I) \ F) < ε :=
    (hs.inter I.measurableSet_Icc).exists_isClosed_sdiff_lt A (ENNReal.coe_pos.2 ε0).ne'

Goal state after:
ι : 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) < ↑ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
        l.MemBaseSet I c (r c) π →
          π.IsPartition →
            dist (integralSum (s.indicator fun x ↦ y) μ.toBoxAdditive.toSMul π) (μ.real (s ∩ ↑I) • y) ≤ ‖y‖ * ↑ε
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : 1 / ↑n ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x✝ : ι → ℝ
h : x✝ ∈ Box.Icc (box n ν)
⊢ Metric.diam (Box.Icc (box n ν)) ≤ ↑((fun x ↦ ⟨r, hr⟩) ((prepartition n B).tag (box n ν)))

Tactic:
exact le_trans (diam_boxIcc n ν) hn

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
· rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self]
      rwa [inner_self_ne_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ Ray.map (AlternatingMap.domLCongr R R ι R (LinearEquiv.refl R M)) = Equiv.refl (Orientation R M ι)

Tactic:
AlternatingMap.domLCongr_refl,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
⊢ Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)) = Equiv.refl (Orientation R M ι)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ m * ↑n ≤ δ n

Tactic:
←
    ENNReal.coe_le_coe,

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ ↑(m * ↑n) ≤ ↑(δ n)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ ↑(m * ↑n) ≤ ↑(δ n)

Tactic:
ENNReal.coe_mul,

Goal state after:
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hl : l.bRiemann = false
ε : ℝ≥0
ε0 : 0 < ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
this✝ : Fact (μ ↑I < ∞)
hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0
N : (ι → ℝ) → ℕ := fun x ↦ ⌈‖f x‖⌉₊
N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0
U : ℕ → Set (ι → ℝ)
hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n
hUo : ∀ (n : ℕ), IsOpen (U n)
hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n
r : (ι → ℝ) → ↑(Set.Ioi 0)
hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
x✝ : π.IsPartition
n : ℕ
m : ℝ≥0
this : ↑m < ↑(δ n) / ↑n
⊢ ↑m * ↑↑n ≤ ↑(δ n)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : 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
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖

Tactic:
← dist_eq_norm,

Goal state after:
ι : 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
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ dist ((f n) x) (g x) ≤ ‖(f m) x - g x‖
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : 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
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ dist ((f n) x) (g x) ≤ ‖(f m) x - g x‖

Tactic:
← dist_eq_norm,

Goal state after:
ι : 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
x : ι → ℝ
m n : ℕ
hmn : m ≤ n
⊢ dist ((f n) x) (g x) ≤ dist ((f m) x) (g x)
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ volume (parallelepiped ⇑b) = 1

Tactic:
by
  have : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
  let o := (stdOrthonormalBasis ℝ F).toBasis.orientation
  rw [← o.measure_eq_volume]
  exact o.measure_orthonormalBasis b

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

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∧ x ∈ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∧
      (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
← b.ofZLatticeBasis_span ℝ,

Goal state after:
case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∧ x ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))) ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∧
      (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
⊢ Bornology.IsBounded (range f)

Tactic:
rw [← Set.image_union_image_compl_eq_range (s := t)]

Goal state after:
case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
⊢ Bornology.IsBounded (f '' t ∪ f '' tᶜ)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑(-↑n)| ^ (-b)

Tactic:
simp_rw [Int.cast_neg, abs_neg]

Goal state after:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n ↦ |↑↑n| ^ (-b)
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} →
    (x✝ ∈ L ↔ (Basis.ofZLatticeBasis ℝ L b).equivFun x✝ ∈ span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
← b.ofZLatticeBasis_span ℝ,

Goal state after:
case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} →
    (x✝ ∈ span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)) ↔
      (Basis.ofZLatticeBasis ℝ L b).equivFun x✝ ∈ span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
m : G
hm : m ∈ (x • y).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d * m'

Tactic:
simp only [smul_eq_mul, mul_def, coeff_finsuppSum] at hm

Goal state after:
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x✝ x y : k[G]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}
m : G
hm : m ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support
⊢ ∃ m' ∈ s, ∃ d, m = d * m'
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
m : A
hm : m ∈ (x • y).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'

Tactic:
simp only [smul_eq_mul, mul_def, coeff_finsuppSum] at hm

Goal state after:
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x✝ x y : k[A]
hy : y ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}
m : A
hm : m ∈ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i + i_1) (n * n_1)).coeff).support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (f.support.erase a) ⇑f = Nat.multinomial (f.support.erase a) ⇑(f.update a 0)

Tactic:
exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) *
        (q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1)) -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    X i * p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
      (p.modMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)) +
        X i * p.divMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)))
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : Finite σ
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
  · intro α β _ e h₁ P
    rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]
    simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]
  · simp [Unique.forall_iff, ← IsNilpotent.map_iff (isEmptyRingEquiv R PEmpty).injective,
      -isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero]
  · intro α _ H P
    obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
    simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]

Goal state after: