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

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1} ∧ x ∉ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
Set.mem_ofPred_eq,

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ x ∉ fundamentalDomain b
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
this : (b.repr x) i = 1
⊢ ∑ x_1 ∈ Finset.univ.erase i, (b.repr x) x_1 • b x_1 +ᵥ b i ∈
    ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩

Goal state after:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i✝ : ι
hi✝ : 0 ≤ (b.repr x) i✝ → 1 ≤ (b.repr x) i✝
this : (b.repr x) i✝ = 1
i : ι
hi : i ∈ Finset.univ.erase i✝
⊢ b i ∈ ⇑b '' (Set.univ \ {i✝})
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    I.distortion * nndist (I.lower i) (I.upper i)

Tactic:
distortion,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    (Finset.univ.sup fun i ↦ nndist I.lower I.upper / nndist (I.lower i) (I.upper i)) * nndist (I.lower i) (I.upper i)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ x✝

Tactic:
exists_prop

Goal state after:
case e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ x✝ ∈ π ∧ x ∈ x✝
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Set.range b) = span ℤ (⇑L.subtype '' Set.range ⇑b₀)

Tactic:
Set.range_comp

Goal state after:
case e'_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝² : Module.Finite ℤ ↥L
this✝¹ : Module ℚ E
this✝ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this : LinearIndependent ℤ b
⊢ span ℤ (Subtype.val '' Set.range ⇑b₀) = span ℤ (⇑L.subtype '' Set.range ⇑b₀)
Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged

Goal state before:
pp: case e'_2
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ x✝

Tactic:
exists_prop

Goal state after:
case e'_2
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ x✝ ∈ π ∧ x ∈ 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 ι
inst✝ : DecidableEq ι
e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
x✝ : ι
⊢ EquivLike.coe e.symm (EuclideanSpace.single x✝ 1) = EquivLike.coe e.symm (EuclideanSpace.single x✝ 1)

Tactic:
congr!

Goal state after:
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 ι
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ EquivLike.coe b.repr.symm (EuclideanSpace.single i 1) = EquivLike.coe b.repr.symm (EuclideanSpace.single i 1)

Tactic:
congr!

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

Goal state before:
pp: case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ ¬x ≤ I.lower i

Tactic:
not_le

Goal state after:
case inr
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h✝ : I.lower i < x
⊢ I.lower 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 𝕜 ι
⊢ ∑ x_1, ((EuclideanSpace.basisFun ι 𝕜).repr x).ofLp x_1 • b ((Equiv.refl ι) x_1) = ∑ x_1, x.ofLp x_1 • b x_1

Tactic:
EuclideanSpace.basisFun_repr,

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, x.ofLp x_1 • b ((Equiv.refl ι) x_1) = ∑ x_1, x.ofLp x_1 • b x_1
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = Fintype.card ι

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

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 ι
i : Fin 2
⊢ ∀ (j : Fin 2), inner ℝ (basisOneI i) (basisOneI j) = if i = j then 1 else 0

Tactic:
fin_cases i <;> intro j <;> fin_cases j <;> simp [real_inner_eq_re_inner]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
r' : ℝ
hr' : ENNReal.ofReal r' ≤ r
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam n

Tactic:
← image_subset_iff.2 hr,

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
n : Set F
hn₁ : f ⁻¹' n ∈ 𝓝[D] x
hn₂ : ediam n < ε
r : ℝ≥0∞
r0 : r > 0
hr : eball x r ∩ D ⊆ f ⁻¹' n
r' : ℝ
hr' : ENNReal.ofReal r' ≤ r
⊢ ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ediam (f '' (eball x r ∩ D))
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ν ∈ {ν | ↑(box n ν) ⊆ ↑B} ↔ box n ν ≤ B

Tactic:
Set.mem_ofPred_eq,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ↑(box n ν) ⊆ ↑B ↔ box n ν ≤ B
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
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ k < i

Tactic:
simpa using hki'

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

Goal state before:
pp: case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ (prepartition n B).tag I ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]

Goal state after:
case refine_3
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
I : Box ι
hI : I ∈ (prepartition n B).boxes ∧ (prepartition n B).tag I ∈ s
⊢ tag n (index n ((prepartition n B).tag I)) ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Analysis.InnerProductSpace.Orientation

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

Tactic:
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]

Goal state after:
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = f.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

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

Tactic:
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = -f.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

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

Tactic:
simp only [add_fst, add_snd, inner_add_left]

Goal state after:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y z : WithLp 2 (E × F)
⊢ ⟪x.fst, z.fst⟫_𝕜 + ⟪y.fst, z.fst⟫_𝕜 + (⟪x.snd, z.snd⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜) =
    ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)
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 (fundamentalDomain ((Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map ↑e.symm))

Tactic:
congr!

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) ν μ
⊢ Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑↑e) (Basis.ofZLatticeComap ℝ L (↑e) (Free.chooseBasis ℤ ↥L)) =
    (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)).map ↑e.symm
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ c⁻¹ • x ∈ {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ c⁻¹ • x ∈ X ∧ F (c⁻¹ • x) ≤ 1 ↔ x ∈ X ∧ F x ≤ c ^ card ι
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
⊢ Bornology.IsBounded (range f) ↔ f =O[atTop] 1 ∧ f =O[atBot] 1

Tactic:
by
  rw [hf.isBounded_range_iff_isBigO, cocompact_eq_atBot_atTop, isBigO_sup, and_comm]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ ∑ i ∈ Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
by
      apply sum_le_sum_of_subset_of_nonneg
      · intro x hx
        simp only [mem_Ioo] at hx
        simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true, and_self_iff]
      · intro i _hi _hident
        positivity

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃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 {x | x ∈ X ∧ F x ≤ 1}) = 0
inst✝ : Nonempty ι
⊢ card (Free.ChooseBasisIndex ℤ ↥L) = card ι

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

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
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 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, (↑k + 1) ^ (d - 1) * (↑k + 1) ^ r =
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, ↑(k + 1) ^ (↑d - 1 + r)

Tactic:
congr with k
        rw [← Real.rpow_natCast, ← Real.rpow_add (by positivity), Nat.cast_sub hd]
        norm_cast

Goal state after:
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✝ : Zero V
f : R[G]
x : P → V
p : P
gh : G × P
⊢ gh.1 ∈ ↑f.coeff.support ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p

Tactic:
Finset.mem_coe,

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✝ : Zero V
f : R[G]
x : P → V
p : P
gh : G × P
⊢ gh.1 ∈ f.coeff.support ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
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)
x✝¹ : G × P
h₁ : x✝¹ ∈ s
x✝ : G × P
h₂ : x✝ ∈ s
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝

Tactic:
Finset.mem_coe,

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)
x✝¹ : G × P
h₁ : x✝¹ ∈ Finset.SMulAntidiagonal p hp
x✝ : G × P
h₂ : x✝ ∈ Finset.SMulAntidiagonal p hp
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r) ≤ (A⁻¹ * B) ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
rw [Real.mul_rpow (inv_pos.mpr hA).le hB.le, mul_assoc, mul_assoc]

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A * (B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)) ≤ A⁻¹ ^ r * (B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r))
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Nontrivial ↥L
H : IsClosed ↑L
t : ↥L
ht : t ∈ {x_1 | (fun i ↦ ‖‖↑i - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖↑t - x‖ = 0
this : 0 < finrank ℤ ↥L
⊢ (2⁻¹ * ‖t‖) ^ r < ‖↑t - x‖ ^ r

Tactic:
simpa [Real.mul_rpow, abs_eq_self.mpr (show 0 ≤ ‖t - x‖ ^ r by positivity)] using ht

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

Goal state before:
pp: case h₁.inl
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum ⇑s = n
⊢ False

Tactic:
apply hs'
      rw [← hs, sum_of_support_subset _ hs'' _ (by simp)]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Tactic:
Multiset.filter_eq_self.mpr

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a
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 [hr j h₁.1, if_neg h₁.2]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree

Tactic:
apply le_antisymm

Goal state after:
case neg.a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ Finsupp.degree (degLex.degree f) ≤ f.totalDegree

case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ f.totalDegree ≤ Finsupp.degree (degLex.degree f)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case pos
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree a < degree b
⊢ degree a < degree b ∨ degree a = degree b ∧ toLex a ≤ toLex b

Tactic:
exact Or.inl ha

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 g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f)

Tactic:
apply le_antisymm

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f)

case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (f + g))