mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : I.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
rw [← Prepartition.distortion_top] at hc
  have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp
  simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r

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 : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E

Tactic:
let b := Classical.choose (Classical.choose_spec <| exists_orthonormalBasis 𝕜 E)

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 : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis (↥(Classical.choose ⋯)) 𝕜 E := Classical.choose ⋯
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E
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✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
⊢ {a | subordinateOrthonormalBasisIndex hn hV a hV' = i}.card = finrank 𝕜 ↥(V i)

Tactic:
by
  apply Finset.card_eq_of_equiv_fin
  simpa using hV.subordinateOrthonormalBasisIndexFiberEquiv hn hV' i

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
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
⊢ V →ₗᵢ[𝕜] V

Tactic:
let M := L.toLinearMap.comp p1 + L3.toLinearMap.comp p2

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ᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this✝ : CompleteSpace ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := ↑S.orthogonalProjectionOnto
p2 : V →ₗ[𝕜] ↥Sᗮ := ↑Sᗮ.orthogonalProjectionOnto
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
⊢ V →ₗᵢ[𝕜] V
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < (↑(ν x✝) + 1) / ↑n ∧ (↑(ν x✝) + 1) / ↑n ≤ (↑(ν x✝) + 1) / ↑n

Tactic:
add_div

Goal state after:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < ↑(ν x✝) / ↑n + 1 / ↑n ∧ ↑(ν x✝) / ↑n + 1 / ↑n ≤ ↑(ν x✝) / ↑n + 1 / ↑n
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
⊢ x ≤ ↑a ↔ (↑⌈↑n * x⌉ - 1 + 1) / ↑n ≤ ↑a

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]

Goal state after:
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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
RCLike.ofReal_pow,

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 ι
f : ι → E
b✝ b : ι
ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ↑‖gramSchmidt 𝕜 f a‖ ^ 2 * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
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
⊢ ‖integralSum f μ.toBoxAdditive.toSMul π‖ ≤ ↑ε

Tactic:
← integralSum_fiberwise fun J => N (π.tag J)

Goal state after:
ι : 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
⊢ ‖∑ y ∈ Finset.image (fun J ↦ N (π.tag J)) π.boxes,
        integralSum f μ.toBoxAdditive.toSMul (π.filter fun x ↦ N (π.tag x) = y)‖ ≤
    ↑ε
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 : ι
this : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ (gramSchmidtOrthonormalBasis h f) i
⊢ f j ∈ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)

Tactic:
span_gramSchmidtNormed

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 : ι
this : span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ (gramSchmidtOrthonormalBasis h f) i
⊢ f j ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
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
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
π : TaggedPrepartition I
⊢ ↑π.boxes ⊆ Set.Iic I

Tactic:
intro J hJ

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
π : TaggedPrepartition I
J : Box ι
hJ : J ∈ ↑π.boxes
⊢ J ∈ Set.Iic I
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ

Tactic:
by
  classical
    cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det

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
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
⊢ ∀ J ∈ π₀,
    ∃ πi,
      πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
intro J hJ

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 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) π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 ι
π : 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 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi

Tactic:
rcases l.exists_memBaseSet_isPartition J hJd r with ⟨πJ, hC, hp⟩

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 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
J : Box ι
hJ : J ∈ π₀
Hle : J ≤ I
HJi : Integrable J l f vol
r : (ι → ℝ) → ↑(Set.Ioi 0) := fun x ↦ min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
hJd : J.distortion ≤ C
πJ : TaggedPrepartition J
hC : l.MemBaseSet J C r πJ
hp : πJ.IsPartition
⊢ ∃ πi,
    πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ (fun x ↦ x ^ p / x ^ q) =ᶠ[atBot] fun x ↦ x ^ (↑p - ↑q)

Tactic:
by
  apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _
  intro x hx
  simp [zpow_sub₀ hx.ne]

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)
  exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: 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

Tactic:
rcases h_mono with ⟨m, hm⟩

Goal state after:
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ (Summable fun k ↦ 2 ^ k * f (2 ^ k)) ↔ Summable f
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e'_3
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x✝ : ℕ
⊢ finrank ℝ E = Fintype.card (Free.ChooseBasisIndex ℤ ↥L)

pp: case e'_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume.real s / covolume L volume = volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)

pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0

Tactic:
· rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]

Goal state after:
case e'_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume.real s / covolume L volume = volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)

E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
inst✝ : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume =
    volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})

Tactic:
simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Ring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
⊢ (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra

Tactic:
ext : 1; exact DFinsupp.toFinsupp_neg ..

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : ¬s ≤ s'
⊢ ¬∃ d, s' = s + d

Tactic:
rintro ⟨d, rfl⟩; exact h le_self_add

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

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

Tactic:
← Finsupp.card_toMultiset,

Goal state after:
case e'_3.e'_5.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.card = (Finsupp.toMultiset (toFinsupp m)).card
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ (f.support.sup fun x ↦ (p • x).sum fun x ↦ id) = f.support.sup fun x ↦ (x.sum fun x ↦ id) * p

Tactic:
congr! 2 with d

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
⊢ ((p • d).sum fun x ↦ id) = (d.sum fun x ↦ id) * p
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
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 : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j

Tactic:
rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]

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

Goal state before:
pp: case pos
ι : 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)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
refine Lex.acc_of_single hbot x fun j hj ↦ ?_

Goal state after:
case pos
ι : 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
⊢ Acc (DFinsupp.Lex r s) (single j (x j))
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)

Tactic:
let : ∀ i, Zero (α i) := fun i => ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case inl
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
nontrivial : Subsingleton (MvPolynomial σ R)
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
simp [Subsingleton.eq_zero (α := MvPolynomial σ R)]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ degreeOf s (p * q) = degreeOf s p + degreeOf s q

Tactic:
degreeOf_mul_eq hp hq

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
c : R
⊢ m.leadingCoeff (C c) = c

Tactic:
simp [leadingCoeff]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
⊢ m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)

Tactic:
by
  induction n with
  | zero => simp [m.degree_one]
  | succ n hrec =>
      simp only [pow_add, pow_one, add_smul, one_smul]
      apply le_trans m.degree_mul_le
      simp only [map_add, add_le_add_iff_right]
      exact hrec

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ Squarefree n

Tactic:
squarefree_iff_nodup_primeFactorsList hn,

Goal state after:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ n.primeFactorsList.Nodup