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

Goal state before:
pp: case inl
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
exact False.elim (hp h)

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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
⊢ ∑' (n : ℕ), μ (s ∩ closedBall 0 ↑n) = 0

Tactic:
simp only [H, tsum_zero]

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

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ↑⊥ = 0

Tactic:
rw [AffineSubspace.bot_coe, measure_empty]

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'
ι : Type u_7
inst✝² : Fintype ι
f : ι → Type u_8
inst✝¹ : (i : ι) → NormedAddCommGroup (f i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (f i)
x : PiLp 2 f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [PiLp.norm_sq_eq_of_L2, map_sum, ← norm_sq_eq_re_inner]

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
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ √(∑ x_1, ‖x.ofLp x_1‖ ^ 2) < r ↔ ∑ x_1, x.ofLp x_1 ^ 2 < r ^ 2

Tactic:
norm_eq_abs,

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_1, |x.ofLp x_1| ^ 2) < r ↔ ∑ x_1, x.ofLp x_1 ^ 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, ‖x✝.ofLp x‖ ^ 2) ≤ r ↔ ∑ x, x✝.ofLp x ^ 2 ≤ r ^ 2

Tactic:
norm_eq_abs,

Goal state after:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ √(∑ x, |x✝.ofLp x| ^ 2) ≤ r ↔ ∑ x, x✝.ofLp x ^ 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
this : 0 ≤ ∑ i, x.ofLp i ^ 2
⊢ √(∑ x_1, ‖x.ofLp x_1‖ ^ 2) = r ↔ ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2

Tactic:
norm_eq_abs,

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_1, |x.ofLp x_1| ^ 2) = r ↔ ∑ x_1, x.ofLp x_1 ^ 2 = r ^ 2
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

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

Tactic:
refine ofWithBot_mono fun J₁ hJ₁ hne => ?_

Goal state after:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : J₁ ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₁.boxes
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'

Tactic:
rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩

Goal state after:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' ↦ ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).IsPartition ↔ J = I

Tactic:
by
  simp [isPartition_iff_iUnion_eq]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
h : π.IsPartition
hx : x ∈ I
⊢ ∃! J, J ∈ π ∧ x ∈ J

Tactic:
rcases h x hx with ⟨J, h, hx⟩
  exact ExistsUnique.intro J ⟨h, hx⟩ fun J' ⟨h', hx'⟩ => π.eq_of_mem_of_mem h' h hx' hx

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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint ↑(I.splitLower i x) ↑(I.splitUpper i x)

Tactic:
coe_splitLower,

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) ↑(I.splitUpper i x)
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 : EuclideanSpace 𝕜 ι
⊢ ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ x_1, x.ofLp x_1 • b x_1

Tactic:
equiv_apply,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : EuclideanSpace 𝕜 ι
⊢ ∑ x_1, ((EuclideanSpace.basisFun ι 𝕜).repr x).ofLp x_1 • b ((Equiv.refl ι) x_1) = ∑ x_1, x.ofLp x_1 • b x_1
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 ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
by
  have := (Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)).2
  rw [star_def, RCLike.mul_conj] at this
  norm_cast at this
  rwa [pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at this

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val

Tactic:
obtain ⟨u₀, hu₀s, hu₀, hu₀_max⟩ := exists_maximal_orthonormal hv

Goal state after:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : ∀ u ⊇ u₀, Orthonormal 𝕜 Subtype.val → u = u₀
⊢ ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
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
Y : Finset E
b₀ : OrthonormalBasis (↥Y) 𝕜 E
hX : range (s.domRestrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_domRestrict])

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
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ ∃ b, ∀ i ∈ s, b i = v i
Module: Mathlib.Analysis.BoxIntegral.Integrability

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

Tactic:
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 _

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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).fst‖ ^ 2 +
      ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).snd‖ ^ 2 =
    ‖x✝‖ ^ 2

Tactic:
K.norm_sq_eq_add_norm_sq_projection

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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x x✝ : E
⊢ ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).fst‖ ^ 2 +
      ‖(((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)).symm) x✝).snd‖ ^ 2 =
    ‖K.orthogonalProjectionOnto x✝‖ ^ 2 + ‖Kᗮ.orthogonalProjectionOnto x✝‖ ^ 2
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
p q : ℕ
hpq : p < q
⊢ (fun x ↦ x ^ p) =o[cobounded R] fun x ↦ x ^ (p + (q - p))

Tactic:
simpa [pow_add] using (isBigO_refl (· ^ p) (cobounded R)).mul_isLittleO
    ((isLittleO_const_id_cobounded 1).pow (Nat.sub_pos_of_lt hpq))

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ (fun x ↦ x ^ p) =o[atTop] fun x ↦ x ^ q

Tactic:
refine (isLittleO_iff_tendsto' ?_).mpr (tendsto_pow_div_pow_atTop_zero hpq)

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
x : α
hφ_pos : 0 < φ x
⊢ u x = (φ * v) x → (u ^ r) x = φ x ^ r * v x ^ r

Tactic:
huv'

Goal state after:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
x : α
hφ_pos : 0 < φ x
huv' : u x = (φ * v) x
⊢ (u ^ r) x = φ x ^ r * v x ^ r
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |(Matrix.of (Subtype.val ∘ ⇑b₁)).det| / |(Matrix.of (Subtype.val ∘ ⇑b₂)).det| =
    |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det| * |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)).det|⁻¹

Tactic:
congr 3

Goal state after:
case e_a
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ Matrix.of (Subtype.val ∘ ⇑b₁) = Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)

case e_a
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ Matrix.of (Subtype.val ∘ ⇑b₂) = Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case right
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
this✝ : IsFiniteMeasure (μ.restrict (Box.Icc I))
this : IsFiniteMeasure (μ.restrict ↑I)
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
⊢ ∃ v ∈ ae (μ.restrict ↑I), ∀ y ∈ v, ‖f y‖ ≤ C

Tactic:
use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)

Goal state after:
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
⊢ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖ + ε / 2 * ∑ i ∈ Finset.range n, g i = ε * ‖∑ i ∈ Finset.range n, g i‖

Tactic:
simp only [B]
      ring

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι) atTop
    (𝓝 (volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))

Tactic:
by
  refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
  · filter_upwards [eventually_gt_atTop 0] with n hn
    congr
    refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm
    simp_rw [Set.mem_inter_iff, ← b.ofZLatticeBasis_span ℝ, LinearEquiv.coe_toEquiv,
      Basis.equivFun_apply, Set.mem_image, DFunLike.coe_fn_eq, EmbeddingLike.apply_eq_iff_eq,
      exists_eq_right, and_congr_right_iff, Set.mem_inv_smul_set_iff₀
      (mod_cast hn.ne' : (n : ℝ) ≠ 0), ← Finsupp.coe_smul, ← map_smul, SetLike.mem_coe,
      Basis.mem_span_iff_repr_mem, Pi.basisFun_repr, implies_true]
  · rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢
    exact Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
h_nonneg : ∃ a, ∀ (b : ℕ), a ≤ b → 0 b ≤ f b
h_mono : ∃ a, ∀ (b : ℕ), a ≤ b → f (b + 1) ≤ f b
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
rcases h_nonneg with ⟨n, hn⟩

Goal state after:
f : ℕ → ℝ
h_mono : ∃ a, ∀ (b : ℕ), a ≤ b → f (b + 1) ≤ f b
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ (1 - p)‖ < 1 ↔ 1 < p

Tactic:
norm_eq_abs,

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ |2 ^ (1 - p)| < 1 ↔ 1 < p
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: case mp
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

pp: case mpr
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt

Tactic:
· rintro ⟨has, hat, hst⟩
    obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
    exact ⟨rfl, IsCancelSMul.left_cancel _ _ _ hst⟩

Goal state after:
case mpr
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a : G
b : P
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a • b = hs.min hns • ht.min hnt
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
h₃ : ∀ g ∈ f.coeff.support, g ∉ Prod.fst '' s → f.coeff g • x (g⁻¹ • p) = 0
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)

Tactic:
smul_eq,

Goal state after:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s ↑f.coeff.support
h₃ : ∀ g ∈ f.coeff.support, g ∉ Prod.fst '' s → f.coeff g • x (g⁻¹ • p) = 0
⊢ ∑ gh ∈ Finset.SMulAntidiagonal p ⋯, f.coeff gh.1 • x gh.2 = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
⊢ toAddMonoidAlgebra 0 = 0

Tactic:
by simp [toAddMonoidAlgebra]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: k : ℕ
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼

Tactic:
by
    rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼,
      mul_assoc]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
a : σ → R
s : σ →₀ ℕ
n : ℕ
⊢ coeff s ((∑ i, a i • X i) ^ n) = if (s.sum fun x m ↦ m) = n then ↑s.multinomial * s.prod fun r m ↦ a r ^ m else 0

Tactic:
rw [← ofSupportFinite_coe (f := a) (hf := Set.toFinite _),
    prod_congr (fun r _ ↦ rfl), ← coeff_linearCombination_X_pow]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
a : σ → R
s : σ →₀ ℕ
n : ℕ
⊢ coeff s ((∑ i, (ofSupportFinite a ⋯) i • X i) ^ n) = coeff s ((linearCombination R X) (ofSupportFinite a ⋯) ^ n)
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 ≠ 0

Tactic:
intro hn'

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
hn' : n = 0
⊢ False
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case h₁
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)!

Tactic:
exact Nat.factorial_two_mul_le _

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

Goal state before:
pp: case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ ((k + 1) • m).multinomial = (Nat.multinomial (Finset.range (k + 1)) fun x ↦ m.sum) * m.multinomial ^ (k + 1)

Tactic:
rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring

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

Goal state before:
pp: case pos.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ (x₁.piecewise x {j | r j i}).piecewise x₂ {j | r j i → j ∈ p} = x

Tactic:
ext1 j

Goal state after:
case pos.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
⊢ ((x₁.piecewise x {j | r j i}).piecewise x₂ {j | r j i → j ∈ p}) j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
⊢ x₁.piecewise (x₂.piecewise x {j | r j i}) {j | r j i ∧ j ∈ p} = x

Tactic:
ext1 j

Goal state after:
case neg.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
⊢ (x₁.piecewise (x₂.piecewise x {j | r j i}) {j | r j i ∧ j ∈ p}) j = x j