mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ (L ⊓ (span ℤ s).mkQ.ker).FG

Tactic:
· -- `span ℤ s` is finitely generated because `s` is finite
    rw [ker_mkQ, inf_of_le_right (span_le.mpr h_incl)]
    exact fg_span (LinearIndependent.setFinite h_lind)

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

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
classical
  refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
  rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
  rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
  exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Orthonormal 𝕜 fun i ↦ single i 1

Tactic:
simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
    PiLp.single_apply]

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ∀ (i j : ι), True
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 ι
b : OrthonormalBasis ι 𝕜 E
x y : E
⊢ ∑ i, ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, y⟫

Tactic:
have := congr_arg (innerSL 𝕜 x) (b.sum_repr y)
  rw [map_sum] at this
  convert! this
  rw [map_smul, b.repr_apply_apply, mul_comm]
  simp

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

Goal state before:
pp: case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.splitLower i x ≠ ⊥

Tactic:
rwa [Ne, splitLower_eq_bot, not_le]

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

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ Set.finrank ℝ s = Set.finrank ℤ s

Tactic:
Set.finrank,

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ finrank ℝ ↥(span ℝ s) = Set.finrank ℤ s
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ finrank ℝ ↥(span ℝ s) = Set.finrank ℤ s

Tactic:
Set.finrank,

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : DiscreteTopology ↥(span ℤ s)
F : Submodule ℝ E := span ℝ s
L : Submodule ℤ ↥(span ℝ s) := comap (Submodule.restrictScalars ℤ F).subtype (span ℤ s)
f : ↥(comap (Submodule.restrictScalars ℤ (span ℝ s)).subtype (span ℤ s)) ≃ₗ[ℤ] ↥(span ℤ s) := comapSubtypeEquivOfLe ⋯
this✝ : DiscreteTopology ↥L
this : IsZLattice ℝ L
⊢ finrank ℝ ↥(span ℝ s) = finrank ℤ ↥(span ℤ 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
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
r : ℝ
⊢ μ (toMeasurable μ s ∩ closedBall x r) / μ (closedBall x r) ≤ 1

Tactic:
apply ENNReal.div_le_of_le_mul

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 : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
r : ℝ
⊢ μ (toMeasurable μ s ∩ closedBall x r) ≤ 1 * μ (closedBall x r)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX : Orthonormal 𝕜 Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.domRestrict v)
hsv : Injective (s.domRestrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝¹⁰ : RCLike 𝕜
E : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
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
⊢ V →ₗᵢ[𝕜] V

Tactic:
have E : Sᗮ ≃ₗᵢ[𝕜] LSᗮ := by
    have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
    exact
      (stdOrthonormalBasis 𝕜 Sᗮ).repr.trans
        ((stdOrthonormalBasis 𝕜 LSᗮ).reindex <| finCongr dim_LS_perp).repr.symm

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ᗮ
⊢ V →ₗᵢ[𝕜] V
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν ↦ tag n ν) x✝¹ = (fun ν ↦ tag n ν) x✝
i : ι
this : x✝¹ i = x✝ i
⊢ x✝¹ i = x✝ i

Tactic:
exact this

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
⊢ ∀ ⦃u : E⦄,
    u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {(gramSchmidtOrthonormalBasis h f) i} → ⟪u, v⟫_𝕜 = 0

Tactic:
rintro u ⟨k, _, rfl⟩ v (rfl : v = _)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left✝ : k ∈ Set.Iic j
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : 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
y : F
a : ℝ
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ r,
        (∀ (c : ℝ≥0), l.RCond (r c)) ∧
          ∀ (c : ℝ≥0) (π : TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f vol π) y ≤ a * ε
⊢ HasIntegral I l f vol y

Tactic:
by
  refine hasIntegral_iff.2 fun ε hε => ?_
  rcases exists_pos_mul_lt hε a with ⟨ε', hε', ha⟩
  rcases h ε' hε' with ⟨r, hr, H⟩
  exact ⟨r, hr, fun c π hπ hπp => (H c π hπ hπp).trans ha.le⟩

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
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hf : f =ᵐ[μ.restrict ↑I] 0
hl : l.bRiemann = false
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul 0

Tactic:
refine hasIntegral_iff.2 fun ε ε0 => ?_
  lift ε to ℝ≥0 using ε0.lt.le; rw [gt_iff_lt, NNReal.coe_pos] at ε0
  rcases NNReal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩
  have := Fact.mk (I.measure_coe_lt_top μ)
  change μ.restrict I {x | f x ≠ 0} = 0 at hf
  set N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊
  have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp [N]
  have : ∀ n, ∃ U, N ⁻¹' {n} ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦ by
    refine (N ⁻¹' {n}).exists_isOpen_lt_of_lt _ ?_
    rcases n with - | n
    · simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
    · refine (measure_mono_null ?_ hf).le.trans_lt ?_
      · exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
      · simp [(δ0 _).ne']
  choose U hNU hUo hμU using this
  have : ∀ x, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U (N x) := fun x => by
    obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))
    exact ⟨⟨r, hr₀⟩, hr⟩
  choose r hrU using this
  refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩
  rw [dist_eq_norm, sub_zero, ← integralSum_fiberwise fun J => N (π.tag J)]
  grw [← hcε, ← sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc)]
  apply norm_sum_le_of_le
  rintro n -
  dsimp [integralSum]
  have : ∀ J ∈ π.filter fun J => N (π.tag J) = n,
      ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real J * n := fun J hJ ↦ by
    rw [TaggedPrepartition.mem_filter] at hJ
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
    gcongr
    exact hJ.2 ▸ Nat.le_ceil _
  refine (norm_sum_le_of_le _ this).trans ?_; clear this
  rw [← sum_mul, ← Prepartition.measure_iUnion_toReal]
  let m := μ (π.filter fun J => N (π.tag J) = n).iUnion
  change m.toReal * ↑n ≤ ↑(δ n)
  have : m < δ n / n := by
    simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
    refine (measure_mono ?_).trans_lt (hμU _)
    simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
    rintro x ⟨J, ⟨hJ, rfl⟩, hx⟩
    exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
  clear_value m
  lift m to ℝ≥0 using ne_top_of_lt this
  grw [ENNReal.coe_toReal, ← NNReal.coe_natCast, ← NNReal.coe_mul, NNReal.coe_le_coe, ←
    ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_natCast, mul_comm, this, ENNReal.mul_div_le]

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

Goal state before:
pp: ι : 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
⊢ HasIntegral I l f vol (integral I l f vol)

Tactic:
rw [integral, dif_pos h]

Goal state after:
ι : 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
⊢ HasIntegral I l f vol (Exists.choose h)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case insert
ι : 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)

Tactic:
Finset.forall_mem_insert

Goal state after:
case insert
ι : 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : HasIntegral I l (f a) vol (g a) ∧ ∀ x ∈ s, HasIntegral I l (f x) vol (g x)
⊢ HasIntegral I l (fun x ↦ f a x + ∑ i ∈ s, f i x) vol (g a + ∑ i ∈ s, g i)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : 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
⊢ Tendsto (fun π ↦ (integralSum f vol π.1, integralSum f vol π.2))
    (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π | π.1.iUnion = π.2.iUnion}) (𝓤 F)

Tactic:
by
  refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
    uniformity_basis_dist_le).2 fun ε ε0 => ?_
  replace ε0 := half_pos ε0
  use h.convergenceR (ε / 2), h.convergenceR_cond (ε / 2); rintro ⟨π₁, π₂⟩ ⟨⟨h₁, h₂⟩, hU⟩
  rw [← add_halves ε]
  exact h.dist_integralSum_le_of_memBaseSet ε0 ε0 h₁.choose_spec h₂.choose_spec hU

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

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
c c₁ c₂ : ℝ≥0
ε ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
inst✝ : CompleteSpace F
h : Integrable I l f vol
J : Box ι
hJ : ↑J ≤ ↑I
π : Prepartition J
hπ : π.iUnion = ⊤.iUnion
⊢ ∑ Ji ∈ π.boxes, integral Ji l f vol = integral J l f vol

Tactic:
(h.to_subbox (WithTop.coe_le_coe.1 hJ)).sum_integral_congr hπ,

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J✝ : Box ι
π✝ : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
c c₁ c₂ : ℝ≥0
ε ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
inst✝ : CompleteSpace F
h : Integrable I l f vol
J : Box ι
hJ : ↑J ≤ ↑I
π : Prepartition J
hπ : π.iUnion = ⊤.iUnion
⊢ ∑ J ∈ ⊤.boxes, integral J l f vol = integral J l f vol
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝⁶ : SeminormedAddCommGroup E
β : Type u_3
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder β
inst✝³ : OrderClosedTopology β
inst✝² : CompactIccSpace β
inst✝¹ : NoMaxOrder β
inst✝ : NoMinOrder β
f : β → E
hf : Continuous[inst✝⁵, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ f =O[atBot ⊔ atTop] 1 ↔ f =O[atTop] 1 ∧ f =O[atBot] 1

Tactic:
isBigO_sup,

Goal state after:
E : Type u_1
inst✝⁶ : SeminormedAddCommGroup E
β : Type u_3
inst✝⁵ : TopologicalSpace β
inst✝⁴ : LinearOrder β
inst✝³ : OrderClosedTopology β
inst✝² : CompactIccSpace β
inst✝¹ : NoMaxOrder β
inst✝ : NoMinOrder β
f : β → E
hf : Continuous[inst✝⁵, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ f =O[atBot] 1 ∧ f =O[atTop] 1 ↔ f =O[atTop] 1 ∧ f =O[atBot] 1
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : f a = 0
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x ↦ id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

Tactic:
intro p

Goal state after:
case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)

Tactic:
intro p

Goal state after:
case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
⊢ ∀ (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)
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
⊢ ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0

Tactic:
intro p

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
p : MvPolynomial σ R
⊢ (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) (↑s + Multiset.replicate (↑m) x) = ↑s

Tactic:
Multiset.filter_add

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
hα : rα a₁✝ a₂✝
hβ : rβ b₁✝ b₂✝
⊢ Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)

Tactic:
exact Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ)

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inl.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(a, d)

Tactic:
exact ihb d rd

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn (a + b)

Tactic:
exact m.toSyn_monotone le_self_add

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree b

Tactic:
← add_tsub_cancel_of_le h,

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree (a + (b - a))
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree (a + (b - a))

Tactic:
map_add

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree a + degree (b - a)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.degree f)

Tactic:
unfold degree
  simp only [AddEquiv.apply_symm_apply, Finset.le_sup hd]

Goal state after: