mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖Int.fract ((b.repr m) i)‖ * ‖b i‖ ≤ ‖b i‖

Tactic:
convert! mul_le_mul_of_nonneg_right this (norm_nonneg _ : 0 ≤ ‖b i‖)
    exact (one_mul _).symm

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (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
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ μ.restrict (s \ u) = 0

Tactic:
simp only [restrict_eq_zero, hfinite.measure_zero]

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

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ (quotientEquiv b).symm x = Submodule.Quotient.mk ↑x

Tactic:
rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fractRestrict_apply]

Goal state after:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ↑x = fract b ↑x
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 u : Set E
h'u : μ u ≠ 0
t_bound : t ⊆ closedBall 0 1
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
apply
      tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h
        (Eventually.of_forall fun b => zero_le)

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) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
t_bound : t ⊆ closedBall 0 1
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ (closedBall x b) ≤ μ (s ∩ closedBall x b) / μ (closedBall x b)
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
⊢ ⊤ ≤ span K (Set.range Subtype.val)

Tactic:
by simp [ht_span, h_spanE]

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 u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
⊢ (r * R) • t' = r • t

Tactic:
ht',

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) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
r : ℝ
⊢ (r * R) • R⁻¹ • t = r • t
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:

Tactic:
μ (s ∩ ({x} + r • t)) ≤ μ ({x} + r • t) := measure_mono inter_subset_right
      _ = 0 := by
        simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add,
          mul_zero]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ ⟪v, single i a⟫ = a * (starRingEnd ((fun x ↦ 𝕜) i)) (v.ofLp i)

Tactic:
simp [PiLp.inner_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x ↦ -↑C, upper := fun x ↦ ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), |x i| < ↑⌈R⌉₊
⊢ x ∈ ↑I

Tactic:
abs_lt

Goal state after:
ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun x ↦ -↑C, upper := fun x ↦ ↑C, lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), -↑⌈R⌉₊ < x i ∧ x i < ↑⌈R⌉₊
⊢ x ∈ ↑I
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      if (prepartition n B).tag x ∈ s then volume.real ↑x * F ((prepartition n B).tag x) else 0

Tactic:
Finset.sum_ite,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s, volume.real ↑x * F ((prepartition n B).tag x) +
      ∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∉ s, 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inr
𝕜 : 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
i : ι
hi : i ∈ Iio b
hia : i ≠ a
hia₂ : a < i
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0

Tactic:
exact ih i (mem_Iio.1 hi) a hia₂

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

Goal state before:
pp: case refine_4
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
x✝ : ι → ℝ
hx : x✝ ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset
⊢ F x✝ / ↑n ^ card ι = volume.real ↑(box n (index n x✝)) * F ((prepartition n B).tag (box n (index n x✝)))

Tactic:
· rw [Set.mem_toFinset] at hx
    rw [measureReal_def, volume_box,
      prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div,
      ENNReal.toReal_one, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]

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

Goal state before:
pp: ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
⊢ ∃ N,
    ∀ n ≥ N,
      dist ((∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι)
          (∫ (x : ι → ℝ) in s, F x) <
        ε

Tactic:
have h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖Set.indicator s F x‖ ≤ C := by
    obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn
    refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
    rw [Set.indicator]
    split_ifs with hs
    · exact le_max_of_le_right (h₀ x hx)
    · exact norm_zero.trans_le <| le_max_left 0 _

Goal state after:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
⊢ ∃ N,
    ∀ n ≥ N,
      dist ((∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι)
          (∫ (x : ι → ℝ) in s, F x) <
        ε
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_1
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate (r 0)

Tactic:
show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)

Goal state after:
case refine_1
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate fun x ↦ r 0 0
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 ι
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
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f) k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0

Tactic:
have : k ≠ i := by
    rintro rfl
    exact hk hi

Goal state after:
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 ι
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
hk : ¬gramSchmidtNormed 𝕜 f k = 0
this : k ≠ i
⊢ ⟪(gramSchmidtOrthonormalBasis h f) k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f = -1

Tactic:
contrapose! h
  simp [e.toBasis.orientation_eq_iff_det_pos,
    (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]

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

Goal state before:
pp: case pos
ι : 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
c : ℝ
hc : c ≠ 0
hf : Integrable I l f vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol

pp: case neg
ι : 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
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol

Tactic:
· exact (hf.hasIntegral.smul c).integral_eq

Goal state after:
case neg
ι : 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
c : ℝ
hc : c ≠ 0
hf : ¬Integrable I l f vol
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: 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 : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ (map ι f) x = x ↔ 0 < LinearMap.det ↑f

Tactic:
by
  cases isEmpty_or_nonempty ι
  · have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
    simp [LinearMap.det_eq_one_of_finrank_eq_zero H]
  rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]

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

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
r : 𝕜
⊢ ⟪(r • x).fst, y.fst⟫_𝕜 + ⟪(r • x).snd, y.snd⟫_𝕜 = (starRingEnd 𝕜) r * (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)

Tactic:
simp only [smul_fst, inner_smul_left, smul_snd]

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
r : 𝕜
⊢ (starRingEnd 𝕜) r * ⟪x.fst, y.fst⟫_𝕜 + (starRingEnd 𝕜) r * ⟪x.snd, y.snd⟫_𝕜 =
    (starRingEnd 𝕜) r * (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case neg.e_f
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⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖

pp: case neg.e_f
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⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)

Tactic:
· field

Goal state after:
case neg.e_f
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⟫
h : ∀ (i : Fin (n + 1)), v i ≠ 0
i : Fin n.succ
hb : b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range N, f i‖ + ∑ i ∈ Finset.Ico N n, ε / 2 * g i ≤
    ‖∑ i ∈ Finset.range N, f i‖ + ∑ i ∈ Finset.range n, ε / 2 * g i

Tactic:
by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ↑|(b.repr x) i| ≤ (normBound b)⁻¹ * ‖x‖

Tactic:
rw [le_inv_mul_iff₀ (normBound_pos b)]
  exact normBound_spec b x i

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

Goal state before:
pp: case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
⊢ 2 * ↑d * (3 * (↑k + 1)) ^ (d - 1) * ((↑k + 1) * ε) ^ r =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ((↑k + 1) ^ (d - 1) * (↑k + 1) ^ r)

Tactic:
Real.mul_rpow (by positivity) (by positivity),

Goal state after:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
⊢ 2 * ↑d * (3 * (↑k + 1)) ^ (d - 1) * ((↑k + 1) ^ r * ε ^ r) =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ((↑k + 1) ^ (d - 1) * (↑k + 1) ^ r)
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
inst✝ : Inhabited α
n : ℕ
⊢ l.getI n = l[n]?.getD default

Tactic:
by
  rw [← getD_default_eq_getI, getD_eq_getElem?_getD]

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬s.support ⊆ a.support
⊢ 0 = ↑s.multinomial * s.prod fun r m ↦ a r ^ m

Tactic:
rw [Finset.subset_iff] at hs'
      simp only [Finsupp.mem_support_iff, ne_eq, not_forall, Decidable.not_not] at hs'
      obtain ⟨i, hsi, hai⟩ := hs'
      rw [← mul_prod_erase _ i _ (by simpa), hai, zero_pow hsi, zero_mul, mul_zero]

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

Goal state before:
pp: case hnc
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hx : x ∈ a.support.piAntidiag n
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
⊢ ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) = n

Tactic:
simp only [Finset.mem_piAntidiag] at hx

Goal state after:
case hnc
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) = n
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
this : p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = 0
h : (p * q).modMonomial (Finsupp.single i 1) = 0
⊢ p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0

Tactic:
mul_eq_zero

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
this : p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
h : (p * q).modMonomial (Finsupp.single i 1) = 0
⊢ p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 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:
induction φ using induction_on'

Goal state after:
case monomial
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m u✝ : σ →₀ ℕ
a✝ : R
⊢ coeff (p • m) ((expand p) ((monomial u✝) a✝)) = coeff m ((monomial u✝) a✝)

case add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
m : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (p • m) ((expand p) p✝) = coeff m p✝
a✝ : coeff (p • m) ((expand p) q✝) = coeff m q✝
⊢ coeff (p • m) ((expand p) (p✝ + q✝)) = coeff m (p✝ + q✝)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ m i
⊢ coeff m ((expand p) φ) = 0

Tactic:
by
  classical
  contrapose! h
  grw [← mem_support_iff, support_expand_subset, Finset.mem_image] at h
  rcases h with ⟨a, -, rfl⟩
  exact ⟨a i, by simp⟩

Goal state after: