mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ (gramSchmidtOrthonormalBasis h f) i

Tactic:
rw [isOrtho_span]

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 : ι
⊢ ∀ ⦃u : E⦄,
    u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {(gramSchmidtOrthonormalBasis h f) i} → ⟪u, v⟫_𝕜 = 0
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 k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ k ≠ i

Tactic:
rintro rfl

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
j k : ι
left✝ : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
hi : gramSchmidtNormed 𝕜 f k = 0
⊢ False
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2.refine_1
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x ↦ ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι) atTop
    (𝓝 (volume.real s))

Tactic:
exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_ceil_atTop

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

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ o = positiveOrientation → (-o).volumeForm = -o.volumeForm

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (-positiveOrientation).volumeForm = -positiveOrientation.volumeForm
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ o = -positiveOrientation → (-o).volumeForm = -o.volumeForm

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (- -positiveOrientation).volumeForm = -(-positiveOrientation).volumeForm
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ o = positiveOrientation → |o.volumeForm v| = |b.toBasis.det v|

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |positiveOrientation.volumeForm v| = |b.toBasis.det v|
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ o = -positiveOrientation → |o.volumeForm v| = |b.toBasis.det v|

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |(-positiveOrientation).volumeForm v| = |b.toBasis.det v|
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ o = positiveOrientation → |o.volumeForm v| ≤ ∏ i, ‖v i‖

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
⊢ |positiveOrientation.volumeForm v| ≤ ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ o = -positiveOrientation → |o.volumeForm v| ≤ ∏ i, ‖v i‖

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
⊢ |(-positiveOrientation).volumeForm v| ≤ ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ o = positiveOrientation → |o.volumeForm v| = ∏ i, ‖v i‖

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ |positiveOrientation.volumeForm v| = ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ o = -positiveOrientation → |o.volumeForm v| = ∏ i, ‖v i‖

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ |(-positiveOrientation).volumeForm v| = ∏ i, ‖v i‖
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ o = positiveOrientation → ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) positiveOrientation).volumeForm x = positiveOrientation.volumeForm (⇑φ.symm ∘ x)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ o = -positiveOrientation → ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) (-positiveOrientation)).volumeForm x = (-positiveOrientation).volumeForm (⇑φ.symm ∘ x)
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o = positiveOrientation → o.volumeForm (⇑φ ∘ x) = o.volumeForm x

Tactic:
rintro rfl

Goal state after:
case zero.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
x : Fin 0 → E
⊢ positiveOrientation.volumeForm (⇑φ ∘ x) = positiveOrientation.volumeForm x
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o = -positiveOrientation → o.volumeForm (⇑φ ∘ x) = o.volumeForm x

Tactic:
rintro rfl

Goal state after:
case zero.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
x : Fin 0 → E
⊢ (-positiveOrientation).volumeForm (⇑φ ∘ x) = (-positiveOrientation).volumeForm x
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
n : ℕ
hn : n ∈ Finset.image (fun J ↦ Nx (π.tag J)) π.boxes
hNxn : ∀ J ∈ π.filter fun J ↦ Nx (π.tag J) = n, Nx (π.tag J) = n
J : Box ι
hJ : J ∈ π.filter fun J ↦ Nx (π.tag J) = n
⊢ r c (π.tag J) = ⋯.convergenceR (↑(δ n)) c (π.tag J)

Tactic:
by
      obtain rfl := hNxn J hJ
      rfl

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

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
L : Submodule ℤ E
inst✝⁸ : DiscreteTopology ↥L
inst✝⁷ : IsZLattice ℝ L
μ : Measure E
inst✝⁶ : μ.IsAddHaarMeasure
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ ν.real
      (fundamentalDomain
        (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑↑e) (Basis.ofZLatticeComap ℝ L (↑e) (Free.chooseBasis ℤ ↥L)))) =
    ν.real (⇑e.symm '' fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)))

Tactic:
← e.symm.coe_toLinearEquiv,

Goal state after:
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
L : Submodule ℤ E
inst✝⁸ : DiscreteTopology ↥L
inst✝⁷ : IsZLattice ℝ L
μ : Measure E
inst✝⁶ : μ.IsAddHaarMeasure
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e) ν μ
⊢ ν.real
      (fundamentalDomain
        (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑↑e) (Basis.ofZLatticeComap ℝ L (↑e) (Free.chooseBasis ℤ ↥L)))) =
    ν.real (⇑↑e.symm '' fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)))
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

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

Tactic:
cocompact_eq_atBot_atTop,

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ (↑k)⁻¹ - (↑n)⁻¹ + (↑(n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹

Tactic:
push_cast

Goal state after:
case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ (↑k)⁻¹ - (↑n)⁻¹ + ((↑n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n + 1)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ {n | ↑n = k}.indicator (fun n ↦ 1 / ↑n) (n + 1)

Tactic:
indicator_apply,

Goal state after:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ if n + 1 ∈ {n | ↑n = k} then 1 / ↑(n + 1) else 0
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : SMul G P
s : Set G
t : Set P
a : P
h : (s.smulAntidiagonal t a).Finite
x : G × P
⊢ x ∈ SMulAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

Tactic:
by
  simp only [SMulAntidiagonal, Set.Finite.mem_toFinset]
  exact Set.mem_sep_iff

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:
push_cast

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 =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ((↑k + 1) ^ (d - 1) * (↑k + 1) ^ r)
Module: Mathlib.Algebra.MvPolynomial.Coeff

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

Tactic:
by
  split_ifs with hs
  · exact coeff_linearCombination_X_pow_of_eq a hs
  · exact coeff_linearCombination_X_pow_of_ne a hs

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

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε

Tactic:
have ε0' := half_pos ε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 ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p q : ℕ
⊢ expand (p * q) = (expand p).comp (expand q)

Tactic:
by
  ext1 i
  simp [pow_mul]

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

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
hc : (↑(insert a s)).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
| insert a s ha ih =>

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on x)) (n : ℕ),
    s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
hc : (↑(insert a s)).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), (insert a s).sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), (eval x) p = (eval x) q

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), (eval x) p = (eval x) p
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c ≤ lex.toSyn d ↔ c default ≤ d default

Tactic:
simp only [MonomialOrder.lex_le_iff, Finsupp.Lex.le_iff_of_unique, ofLex_toLex]

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : C c * ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0

Tactic:
ext m

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : C c * ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
m : { b // b ≠ j } →₀ ℕ
⊢ coeff m ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = coeff m 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : m.degree f ≠ 0
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
h : m.degree 0 ≠ 0
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
f : MvPolynomial σ R
hf : m.Monic f
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : m.Monic 0
⊢ False
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
hf : IsRegular (m.leadingCoeff f)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hg : g = 0
  · simp [hg]
  · simp only [leadingCoeff, degree_mul_of_isRegular_left hf hg, coeff_mul_of_degree_add]

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

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

Tactic:
simp only [leadingCoeff, degree_mul_of_isRegular_right hf hg, coeff_mul_of_degree_add]

Goal state after: