mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ⟨x, hxu⟩ ∉ Subtype.val ⁻¹' v
⊢ ∃ l ∈ supported 𝕜 𝕜 (Subtype.val ⁻¹' v), (linearCombination 𝕜 Subtype.val) l = y

Tactic:
by
      rw [← Finsupp.mem_span_image_iff_linearCombination]
      simp [huv, inter_eq_self_of_subset_right, hy]

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

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≠ ∞

Tactic:
by
  cases nonempty_fintype ι
  obtain ⟨M, hM⟩ := Finite.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)
  refine ne_of_lt ((iSup_le fun i => ?_).trans_lt (@ENNReal.coe_lt_top M))
  simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]
  exact mod_cast hM i

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α✝ : Type u_2
β✝ : Type u_3
hp : Fact (1 ≤ p)
inst✝³ : SeminormedAddCommGroup α✝
inst✝² : SeminormedAddCommGroup β✝
α : Type u_4
β : Type u_5
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedAddCommGroup β
x y : α × β
h : dist x y = 0
⊢ x = y

Tactic:
by
    rw [dist_pseudoMetricSpaceToProd] at h
    exact toLp_injective p (eq_of_dist_eq_zero h)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : 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✝
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
inst✝ : CompleteSpace ↥G
hker : (↑f).ker = ⊥
⊢ (↑(f.coprod G.subtypeL)).ker = ⊥

Tactic:
ker_coprod_of_disjoint_range

Goal state after:
𝕜 : 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✝
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
inst✝ : CompleteSpace ↥G
hker : (↑f).ker = ⊥
⊢ (↑f).ker.prod (↑G.subtypeL).ker = ⊥

𝕜 : 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✝
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
inst✝ : CompleteSpace ↥G
hker : (↑f).ker = ⊥
⊢ Disjoint (↑f).range (↑G.subtypeL).range
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i, ‖x.ofLp i‖₊ ^ 2

Tactic:
rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) '' ⇑K '' Icc 0 1

Tactic:
← image_comp

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) ∘ ⇑K '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, ((∀ (i : ι), 0 i ≤ t i) ∧ ∀ (i : ι), t i ≤ 1 i) ∧ x = ∑ i, t i • Pi.single i (a i)) ↔
    (∀ (i : ι), (0 ⊓ a) i ≤ x i) ∧ ∀ (i : ι), x i ≤ (0 ⊔ a) i

Tactic:
← forall_and,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t, (∀ (x : ι), 0 x ≤ t x ∧ t x ≤ 1 x) ∧ x = ∑ i, t i • Pi.single i (a i)) ↔
    ∀ (x_1 : ι), (0 ⊓ a) x_1 ≤ x x_1 ∧ x x_1 ≤ (0 ⊔ a) x_1
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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
⊢ ⇑f '' fundamentalDomain b = fundamentalDomain (b.map f)

Tactic:
ext x
  rw [mem_fundamentalDomain, Basis.map_repr, LinearEquiv.trans_apply, ← mem_fundamentalDomain,
    show f.symm x = f.toEquiv.symm x by rfl, ← Set.mem_image_equiv]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by
  refine NullMeasurableSet.inter
          (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)
  · change NullMeasurableSet {p : α × ℝ | f p.fst ≤ p.snd} (μ.prod volume)
    rw [show {p : α × ℝ | f p.fst ≤ p.snd} = {p : α × ℝ | p.snd < f p.fst}ᶜ by
          ext p
          simp]
    exact (nullMeasurableSet_lt measurable_snd.aemeasurable (by fun_prop)).compl
  · change NullMeasurableSet {p : α × ℝ | p.snd ≤ g p.fst} (μ.prod volume)
    rw [show {p : α × ℝ | p.snd ≤ g p.fst} = {p : α × ℝ | g p.fst < p.snd}ᶜ by
          ext p
          simp]
    exact (nullMeasurableSet_lt (by fun_prop) measurable_snd.aemeasurable).compl

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
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)

Tactic:
rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]

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
⊢ L.FG

Tactic:
obtain ⟨s, ⟨h_incl, ⟨h_span, h_lind⟩⟩⟩ := exists_linearIndependent K (L : Set 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
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ L.FG
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Tactic:
by
  have : FiniteDimensional ℝ G := b.finiteDimensional_of_finite
  have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by
    rw [image_parallelepiped]
    exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm
  rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
⊢ ⋃ s, ↑(I.splitCenterBox s) = ↑I

Tactic:
ext x
  simp

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 J' : Box ι
hJ' : J' ∈ π
hJ : J ∈ πi J'
⊢ J ≤ I

Tactic:
exact ((πi J').le_of_mem hJ).trans (π.le_of_mem hJ')

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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
H : μ (s ∩ ({x} + r • t)) = 0
⊢ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε

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

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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ E

Tactic:
exact b.repr.symm (EuclideanSpace.single i (1 : 𝕜))

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ (↑(Finset.map I.splitCenterBoxEmb Finset.univ)).Pairwise (Function.onFun Disjoint Box.toSet)

Tactic:
rw [Finset.coe_map, Finset.coe_univ, image_univ]
    rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ Hne
    exact I.disjoint_splitCenterBox (mt (congr_arg _) Hne)

Goal state after:
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
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
by
  classical
  refine ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1,
    fun hD => (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩
  rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
  set π₂ := π.filter fun J => ¬p J
  have : Disjoint π₁.iUnion π₂.iUnion := by
    simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
  refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
  · suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
    have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
    ext x
    fconstructor
    · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
      exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
    · rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
  · have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
    simpa [hc]

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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
have : ∀ r', (ENNReal.ofReal r') ≤ r →
        ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε := by
      intro r' hr'
      grw [← hn₂, ← image_subset_iff.2 hr, hr']

Goal state after:
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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
⊢ ∃ i, 0 < i ∧ x ∈ S i
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν ν' : ι → ℤ
⊢ ν ≠ ν' ↔ Disjoint ↑(box n ν) ↑(box n ν')

Tactic:
rw [not_iff_comm, Set.not_disjoint_iff]
  refine ⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩
  rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']

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
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 < ↑ε
this : Tendsto (fun n ↦ ∫⁻ (x : ι → ℝ) in ↑I, ↑‖(f n) x - g x‖₊ ∂μ) atTop (𝓝 0)
N : ℕ
hN : ∫⁻ (x : ι → ℝ) in ↑I, ↑‖(f N) x - g x‖₊ ∂μ ≤ ↑ε
⊢ ∫ (x : ι → ℝ) in ↑I, ‖(f N) x - g x‖ ∂μ ≤ ↑ε

Tactic:
exact integral_coe_le_of_lintegral_coe_le hN

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

Goal state before:
pp: case right
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
← add_halves ε

Goal state after:
case right
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε / 2 + ε / 2}
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ ∏ x, |⟪b x, v x⟫| = ∏ i, ‖v i‖

Tactic:
Finset.prod_eq_zero (Finset.mem_univ i),

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ 0 = ∏ i, ‖v i‖

case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪b i, v i⟫| = 0
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
⊢ covolume L μ = μ.real F

Tactic:
by
  have : MeasurableVAdd L E := (inferInstance : MeasurableVAdd L.toAddSubgroup E)
  have : VAddInvariantMeasure L E μ := (inferInstance : VAddInvariantMeasure L.toAddSubgroup E μ)
  exact congr_arg ENNReal.toReal (h.covolume_eq_volume μ)

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
⊢ Summable ({n | ↑n = k}.indicator f) ↔ Summable f

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩
  rw [Finset.sum_indicator_mod m f]
  convert!
    summable_sum (s := Finset.univ) fun a _ ↦
      summable_indicator_mod_iff_summable_indicator_mod hf a H
  simp only [Finset.sum_apply]

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
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ContinuousOn f (Box.Icc I)
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := BoxIntegral.integrable_of_continuousOn l hc μ
  convert! hy
  have : IntegrableOn f I μ :=
    IntegrableOn.mono_set (hc.integrableOn_compact I.isCompact_Icc) Box.coe_subset_Icc
  exact HasIntegral.unique (IntegrableOn.hasBoxIntegral this ⊥ rfl) (HasIntegral.mono hy bot_le)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case h
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 : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ ∀ᶠ (x : D) in cocompact D, ‖f x‖ ≤ c * ‖1 x‖

Tactic:
apply Eventually.of_forall

Goal state after:
case h
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 : ℝ
hc : ∀ (a : D), ‖f a‖ ≤ c
⊢ ∀ (x : D), ‖f x‖ ≤ c * ‖1 x‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
intro m n hm hmn

Goal state after:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
⊢ (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ⋯.min ⋯ = hs.min hsn • ht.min htn

Tactic:
refine le_antisymm (IsWF.min_le _ _ (mem_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn • ht.min htn ≤ ⋯.min ⋯
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
by simp [sup_assoc]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ f.multinomial = Nat.multinomial s ⇑f

Tactic:
by
  simp only [Finsupp.multinomial_eq, Nat.multinomial]
  congr 1
  · simp [Finset.sum_subset h]
  · rw [Finset.prod_subset h]
    grind [Nat.factorial_eq_one]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e'_3.e'_5.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.card = (toFinsupp m).sum fun x ↦ id

pp: case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x ↦ a ≠ x) m) = (toFinsupp m).update a 0

Tactic:
· rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]

Goal state after:
case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x ↦ a ≠ x) m) = (toFinsupp m).update a 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (⇑(toFinsupp m)) a✝ 0 a

Tactic:
rw [Function.update_of_ne h.symm, toFinsupp_apply]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ IsUnit P ↔ ∃ r, IsUnit r ∧ P = C r

Tactic:
by
  rw [isUnit_iff_totalDegree_of_isReduced, totalDegree_eq_zero_iff_eq_C]
  refine ⟨fun H ↦ ⟨_, H⟩, ?_⟩
  rintro ⟨r, hr, rfl⟩
  simpa

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * ∏ i ∈ s, f i ^ k i

Tactic:
simp_rw [← noncommProd_eq_prod]
  rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
⊢ (eval x) p = 0

Tactic:
choose g hg using fun i ↦ (hs i).nonempty

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
⊢ (eval x) p = 0