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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
⊢ edist x.fst y.fst = edist x y

Tactic:
by
    rcases p.trichotomy with rfl | rfl | hp
    · absurd hp.elim; simp
    · simp_rw [WithLp.prod_edist_eq_sup, Unique.eq_default, edist_self, max_zero]
    · simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
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
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
g : (E × ↥G) ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(↑f).range

Tactic:
rw [range_eq_map_coprodSubtypeLEquivOfIsCompl f h hker]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
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
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
g : (E × ↥G) ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ↑(Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥))
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x ↦ 𝕜)
A : Matrix ι ι 𝕜
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j ↦ (b.repr (toLp p (Aᵀ j))) i

Tactic:
have := basis_toMatrix_basisFun_mul (b.map (WithLp.linearEquiv _ 𝕜 _)) A
  simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply,
    WithLp.linearEquiv_symm_apply, Basis.toMatrix_map, Function.comp_def, Basis.map_apply,
    LinearEquiv.symm_apply_apply] at this
  exact this

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)

Tactic:
dsimp only [regionBetween, Ioo, mem_ofPred_eq, ofPred_and]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 < g a.1}})
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
R : ℝ
⊢ Pairwise (Disjoint on fun n ↦ {u n} + s ∩ closedBall 0 R)

Tactic:
refine pairwise_disjoint_mono hs fun n => ?_

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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
R : ℝ
n : ℕ
⊢ {u n} + s ∩ closedBall 0 R ⊆ {u n} + s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : x ∈ ⋃ i, T i
⊢ p x

Tactic:
rw [← hA] at Hx
    obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
      simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
    apply h'x p pA ⟨xs, xp⟩

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

Goal state before:
pp: case coe.coe
ι : Type u_1
a✝¹ a✝ : Box ι
⊢ ↑↑a✝¹ ⊆ ↑↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp [le_def]

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

Goal state before:
pp: case ha
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ ↑c * (I.upper i - I.lower i)
x : ι → ℝ
hx : x ∈ Box.Icc I
y : ι → ℝ
hy : y ∈ Box.Icc I
⊢ 0 ≤ I.upper i - I.lower i

Tactic:
exact sub_nonneg.2 (I.lower_le_upper i)

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

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

Tactic:
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i, x.ofLp i ^ 2 < r ^ 2}
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.sphere 0 r ↔ x ∈ {x | ∑ i, x.ofLp i ^ 2 = r ^ 2}

Tactic:
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i, x.ofLp i ^ 2 = r ^ 2}
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 : ℝ
⊢ μ ({x} + r • t) = 0

Tactic:
simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add,
          mul_zero]

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 πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
this : ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂
⊢ (↑(π₁.boxes ∪ π₂.boxes)).Pairwise (Disjoint on Box.toSet)

Tactic:
simpa [pairwise_union_of_symm, pairwiseDisjoint]

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
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ (s ∩ ({x} + r • (t \ closedBall 0 ↑n))) ≤
    μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))

Tactic:
gcongr; apply inter_subset_right

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Tactic:
classical
  rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]

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
⊢ span ℤ (Set.range ⇑(ofZLatticeBasis K L b)) = span ℤ (⇑L.subtype '' Set.range ⇑b)

Tactic:
congr; ext; simp

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

Goal state before:
pp: F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v : OrthonormalBasis (Fin 2) ℝ F
z : ℂ
⊢ (isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1

Tactic:
by
  simp [Complex.isometryOfOrthonormal, ← v.sum_repr_symm]

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 : 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
⊢ finrank 𝕜 V - finrank 𝕜 ↥LS = finrank 𝕜 V - finrank 𝕜 ↥S

Tactic:
by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]

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

Goal state before:
pp: case pos
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then tag n hI.choose else ⋯.choose) ∈ Box.Icc B

Tactic:
simp_rw [dif_pos hI]

Goal state after:
case pos
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ tag n hI.choose ∈ Box.Icc B
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 ι
f : ι → E
b : ι
⊢ ∀ (x : ι),
    (∀ y < x, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0) →
      ∀ a < x, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 = 0

Tactic:
intro b

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 ι
f : ι → E
b✝ b : ι
⊢ (∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0) →
    ∀ a < b, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case neg
ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hgi : ¬Integrable I l g μ.toBoxAdditive.toSMul
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
rw [integral, dif_neg hgi]

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

Goal state before:
pp: ι : Type u
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
g : (ι → ℝ) → ℝ
hg : ∀ x ∈ Box.Icc I, 0 ≤ g x
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ 0 ≤ integral I l g μ.toBoxAdditive.toSMul

Tactic:
by
  by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
  · refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_
    exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)
  · rw [integral, dif_neg hgi]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]

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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε

Tactic:
refine le_of_forall_pos_le_add fun δ δ0 => ?_

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 ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace

Goal state before:
pp: p : ℝ≥0∞
X : Type u_1
inst✝ : MeasurableSpace X
t : Set X
ht : MeasurableSet t
⊢ MeasurableSet (toLp p ⁻¹' ofLp ⁻¹' t)

Tactic:
simpa [Set.preimage_preimage]

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

Goal state after:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
⊢ m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
a✝ : ℕ
hn : ⌈|a|⌉₊ < a✝
⊢ ↑a✝ + ?m.78 = |↑a✝ + a|

Tactic:
abs_of_pos

Goal state after:
a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
a✝ : ℕ
hn : ⌈|a|⌉₊ < a✝
⊢ ↑a✝ + ?m.78 = ↑a✝ + a

a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
a✝ : ℕ
hn : ⌈|a|⌉₊ < a✝
⊢ 0 < ↑a✝ + a
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : m ∈ ((of k G) i).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d * m'

Tactic:
refine ⟨_, hi, 1, ?_⟩

Goal state after:
case mp
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : G
hi : i ∈ s
m : G
hm : m ∈ ((of k G) i).coeff.support
⊢ m = 1 * i
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
⊢ (Function.Surjective fun x ↦ l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l

Tactic:
apply forall_congr'

Goal state after:
α : Type u
l : List α
d : α
⊢ ∀ (a : α), (∃ a_1, (fun x ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.f
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
this : X i ∣ p ∨ X i ∣ X i * r
hp : X i * (p * r) = p * (X i * r)
⊢ p ∣ p * r

Tactic:
exact dvd_mul_right p r

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
⊢ n.support.Nonempty

Tactic:
rw [Finsupp.support_nonempty_iff]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
⊢ n ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff (p • m) ((expand p) φ) = coeff m φ

Tactic:
by
  classical
  induction φ using induction_on' <;> simp [*, nsmul_right_inj hp]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
h : ¬r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
exact ih _ ⟨h, hij⟩ _

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ ∀ b ∈ f.support, (b.sum fun x e ↦ e) ≤ Finsupp.degree (degLex.degree f)

Tactic:
intro b

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
b : σ →₀ ℕ
⊢ b ∈ f.support → (b.sum fun x e ↦ e) ≤ Finsupp.degree (degLex.degree f)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ ∀ (a : R),
    (∃ a_1 ≤ Finsupp.single i 1, a ∣ r ∧ p = (monomial a_1) a) ↔
      a ∣ r ∧ (p = C a ∨ p = a • (monomial (Finsupp.single i 1)) 1)

Tactic:
intro b

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) ↔ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0

Tactic:
apply forall_congr'

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), a ∈ f.support → m.toSyn a ≤ m.toSyn 0 ↔ a ∈ f.support → ∀ (x : σ), a x = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.degree f) ∨ m.toSyn c ≤ m.toSyn (m.degree g)

Tactic:
intro b

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
⊢ b ∈ (f + g).support → m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
rw [degree_le_iff]
  intro c
  rw [← not_lt, mem_support_iff, not_imp_not]
  intro hc
  rw [coeff_mul]
  apply Finset.sum_eq_zero
  rintro ⟨d, e⟩ hde
  simp only [Finset.mem_antidiagonal] at hde
  dsimp only
  by_cases hd : m.degree f ≺[m] d
  · rw [m.coeff_eq_zero_of_lt hd, zero_mul]
  · suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2

Tactic:
convert! card_image_offDiag (univ : Finset α)

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = #(image (uncurry Sym2.mk) univ.offDiag)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
· simp [hg]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g