mathlib-initiative/mathlib-tactics huggingface dataset:
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 : E
⊢ √(∑ i, ‖⟪b i, x⟫‖ ^ 2) ≤ √(∑ x_1, (⨆ j, ‖⟪b j, x⟫‖) ^ 2)

Tactic:
gcongr with i

Goal state after:
case hab
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
a✝ : i ∈ Finset.univ
⊢ ‖⟪b i, x⟫‖ ≤ ⨆ j, ‖⟪b j, x⟫‖
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ J ∈ {I.splitLower i x, I.splitUpper i x}, J ≤ ↑I

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Goal state after:
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)), J = I.splitLower i x ∨ J = I.splitUpper i x → J ≤ ↑I
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ (fun π' ↦ π'.iUnion = ↑I \ π₁.iUnion) = fun π' ↦ π'.iUnion = ↑I \ π₂.iUnion

Tactic:
rw [h]

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

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ (π.biUnionTagged πi).distortion ≤ c

Tactic:
Prepartition.distortion_biUnionTagged,

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
hD : l.bDistortion = true
⊢ (π.boxes.sup fun J ↦ (πi J).distortion) ≤ c
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
F' : Type u_6
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f

Tactic:
by
  simp only [isometryOfOrthonormal, OrthonormalBasis.map, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm]
  -- Porting note: `LinearIsometryEquiv.trans_assoc` doesn't trigger in the `simp` above
  rw [LinearIsometryEquiv.trans_assoc]

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

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

Tactic:
by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
    · simp_rw [dif_pos hI]
      exact Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)
    · simp_rw [dif_neg hI]
      exact Box.coe_subset_Icc B.exists_mem.choose_spec

Goal state after:
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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j, v i⟫_𝕜 = 0

Tactic:
rw [gramSchmidt_def'' 𝕜 v]

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 ι
v : ι → E
i j : ι
hij : i < j
⊢ ⟪gramSchmidt 𝕜 v j,
      gramSchmidt 𝕜 v i +
        ∑ i_1 < i, (⟪gramSchmidt 𝕜 v i_1, v i⟫_𝕜 / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1⟫_𝕜 =
    0
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_1
ι : 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
⊢ box n (index n x✝) ∈ (prepartition n B).boxes ∧ (prepartition n B).tag (box n (index n x✝)) ∈ s

Tactic:
rw [Set.mem_toFinset] at hx

Goal state after:
case refine_1
ι : 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 ℝ ι)))
⊢ box n (index n x✝) ∈ (prepartition n B).boxes ∧ (prepartition n B).tag (box n (index n x✝)) ∈ s
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

Goal state after:
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 ℝ ι)))
⊢ F x✝ / ↑n ^ card ι = volume.real ↑(box n (index n x✝)) * F ((prepartition n B).tag (box n (index n x✝)))
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
hf : Pairwise fun x1 x2 ↦ ⟪f x1, f x2⟫_𝕜 = 0
i j : ι
hj : j ∈ Finset.Iio i
this : span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
⊢ (𝕜 ∙ gramSchmidt 𝕜 f j).orthogonalProjectionOnto (f i) = 0

Tactic:
apply orthogonalProjectionOnto_apply_of_mem_orthogonal
      rw [mem_orthogonal_singleton_iff_inner_left, ← mem_orthogonal_singleton_iff_inner_right]
      exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det ((∏ i, w i)⁻¹ • e.det ⇑(e.unitsSMul w) • (e.unitsSMul w).det)

Tactic:
det_unitsSMul_self,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det ((∏ i, w i)⁻¹ • (∏ i, ↑(w i)) • (e.unitsSMul w).det)
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
c : ℝ
⊢ integral I l (fun x ↦ c • f x) vol = c • integral I l f vol

Tactic:
by
  rcases eq_or_ne c 0 with (rfl | hc); · simp only [zero_smul, integral_zero]
  by_cases hf : Integrable I l f vol
  · exact (hf.hasIntegral.smul c).integral_eq
  · have : ¬Integrable I l (fun x => c • f x) vol := mt (fun h => h.of_smul hc) hf
    rw [integral, integral, dif_neg hf, dif_neg this, smul_zero]

Goal state after:
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)
b : OrthonormalBasis (Fin n) ℝ E
hb : b.toBasis.orientation = o
⊢ o.volumeForm = b.toBasis.det

Tactic:
cases n
  · classical
      have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
      simp_rw [volumeForm, Or.by_cases, dif_pos this, Nat.rec_zero, Basis.det_isEmpty]
  · simp_rw [volumeForm]
    rw [same_orientation_iff_det_eq_det, hb]
    exact o.finOrthonormalBasis_orientation _ _

Goal state after:
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, ∫ (x : ι → ℝ) in ↑I, ‖(f N) x - g x‖ ∂μ ≤ ↑ε

Tactic:
by
    have : Tendsto (fun n => ∫⁻ x in I, ‖f n x - g x‖₊ ∂μ) atTop (𝓝 0) :=
      SimpleFunc.tendsto_approxOn_range_L1_enorm hg.measurable hgi
    refine (this.eventually (ge_mem_nhds ε0')).exists.imp fun N hN => ?_
    exact integral_coe_le_of_lintegral_coe_le hN

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

Tactic:
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, Module.Ray.ne_neg_self x]
  have H : 0 < finrank R M := by
    rw [← h]
    exact Fintype.card_pos
  have : FiniteDimensional R M := of_finrank_pos H
  rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]

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

Goal state before:
pp: case e'_2.e'_1
𝕜 : 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 : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ y = Quotient.mk ↑(f y)

pp: case e'_3
𝕜 : 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 : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑x‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)

Tactic:
· simp [f]

Goal state after:
case e'_3
𝕜 : 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 : E
y : E ⧸ K
f : (E ⧸ K) ≃ₗ[𝕜] ↥Kᗮ := K.quotientEquivOfIsCompl Kᗮ ⋯
h : ‖Quotient.mk ↑(f y)‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
⊢ ⨅ x, ‖↑(f y) - ↑x‖ = sInf ((fun x ↦ ‖↑(f y) + x‖) '' ↑K.toAddSubgroup)
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
hx : x ∈ Kᗮ
⊢ K.quotientEquivOrthogonal (Quotient.mk x) = ⟨x, hx⟩

Tactic:
simp [← K.quotientEquivOfIsCompl_apply_mk_right K.isCompl_orthogonal ⟨x, hx⟩]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x y : E
hx : x ∈ Kᗮ
hy : y ∈ Kᗮ
⊢ ⟪mk x, mk y⟫_𝕜 = ⟪x, y⟫_𝕜

Tactic:
by
  simp [K.quotientEquivOrthogonal_mk x hx, K.quotientEquivOrthogonal_mk y hy]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ volume ↑b.toBasis.parallelepiped = 1

Tactic:
exact b.volume_parallelepiped

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n ↦ f (m * n + k)

Tactic:
let g : ℕ → ℕ := fun n ↦ m * n + k

Goal state after:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n ↦ f (m * n + k)
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₂
i j : ι
⊢ (Basis.ofZLatticeBasis ℝ L₂ b₂).toMatrix (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)) i j =
    (b₂.toMatrix fun i ↦ ⟨↑(b₁ i), ⋯⟩).map (fun x ↦ ↑x) i j

Tactic:
Matrix.map_apply,

Goal state after:
ι : 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₂
i j : ι
⊢ (Basis.ofZLatticeBasis ℝ L₂ b₂).toMatrix (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)) i j =
    ↑(b₂.toMatrix (fun i ↦ ⟨↑(b₁ i), ⋯⟩) i j)
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
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ Finset.range x, f i‖ ≤ ε * ‖∑ i ∈ Finset.range x, g i‖

Tactic:
intro ε εpos

Goal state after:
α : 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 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ Finset.range x, f i‖ ≤ ε * ‖∑ i ∈ Finset.range x, g i‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case h₂
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

Tactic:
simp only [nsmul_eq_mul, this]

Goal state after:
case h₂
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n : ℕ
this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)
⊢ ∑ x ∈ range n, ↑(u (x + 1) - u x) * f (u x) ≤ ∑' (k : ℕ), ↑(u (k + 1) - u k) * f (u k)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
this : ↑(u k) ≤ ↑(u k.succ)
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))

Tactic:
simp [NNReal.coe_sub this]

Goal state after:
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[atBot] 1 ∧ f =O[atTop] 1 ↔ f =O[atTop] 1 ∧ f =O[atBot] 1

Tactic:
and_comm

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[atTop] 1 ∧ f =O[atBot] 1 ↔ f =O[atTop] 1 ∧ f =O[atBot] 1
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: ⊢ ¬Summable fun n ↦ (↑n)⁻¹

Tactic:
have : ¬Summable (fun n => ((n : ℝ) ^ 1)⁻¹ : ℕ → ℝ) :=
    mt (summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)
  simpa

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

Goal state before:
pp: case refine_4
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
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ x • ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ⊆
    y • ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1}

Tactic:
simp_rw [← image_smul_set]
    apply Set.image_mono
    rw [tendsto_card_le_div''_aux hX h₁ hx,
      tendsto_card_le_div''_aux hX h₁ (lt_of_lt_of_le hx hy)]
    exact fun a ⟨ha₁, ha₂⟩ ↦ ⟨ha₁, le_trans ha₂ <| pow_le_pow_left₀ (le_of_lt hx) hy _⟩

Goal state after:
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)
f g : ⨁ (x : ι), M
⊢ (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra

Tactic:
ext; simp [toAddMonoidAlgebra]

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
l : List α
d : α
i : Fin l.length
⊢ l.getD (↑i) d = l[i]?.get ⋯

Tactic:
simp only [getD_eq_getElem?_getD, Fin.is_lt, getElem?_pos, Option.getD_some, Fin.getElem_fin,
    Option.get_some]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (aeval x) ((aeval fun i ↦ g (X i)) (f (X i))) = comap f (comap g x) i

Tactic:
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom]

Goal state after:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (eval₂Hom ((eval₂Hom (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R))) fun i ↦
        (eval₂Hom (algebraMap R R) x) (g (X i)))
      (f (X i)) =
    (eval₂Hom (algebraMap R R) (comap g x)) (f (X i))
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
h₁ : f a = 1
⊢ multinomial {a, b} f = (f b).succ

Tactic:
by
  simp [h, h₁]

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : σ
p r : MvPolynomial σ R
h✝ : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : n i ≠ 0
⊢ n ∉ r.support

Tactic:
rw [h, notMem_support_iff]

Goal state after:
case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : σ
p r : MvPolynomial σ R
h✝ : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : n i ≠ 0
⊢ coeff n (p.modMonomial (Finsupp.single i 1)) = 0
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hp : p ∣ q
⊢ p ∣ X i * q

Tactic:
exact dvd_mul_of_dvd_right hp (X i)

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

Goal state before:
pp: case cons
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x ::ₘ m + m').multinomial = (x ::ₘ m + m').sum.choose (x ::ₘ m).sum * (x ::ₘ m).multinomial * m'.multinomial

Tactic:
| cons x m hind =>

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

Goal state before:
pp: case pos.inl
ι : 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 : ι
x : Π₀ (i : ι), α i
j : ι
hj : j ∈ x.support
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y j → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y j → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α j
ha : ∀ (y : α j), s j y a → Acc (DFinsupp.Lex r s) (single j y)
hr : ∀ (j_1 : ι), r j_1 j → x j_1 = (single j a) j_1
hs : s j (x j) (Eq.recOn ⋯ a)
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
exact ha _ hs

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

Goal state before:
pp: case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ 0 ≤ Finsupp.single i 1 ∧ b ∣ r ∧ p = (monomial 0) b

Tactic:
simp [hb, hp]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = c

Tactic:
classical
  simp only [leadingCoeff, degree_monomial]
  split_ifs with hc <;> simp [hc]

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

Goal state before:
pp: case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

Tactic:
not_imp_not

Goal state after:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → m.leadingCoeff f = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ coeff c (f * g) ≠ 0 → ¬m.toSyn (m.degree f + m.degree g) < m.toSyn c

Tactic:
not_imp_not

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0