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

Goal state before:
pp: 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
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
⊢ span ℤ (Set.range ⇑(ofZLatticeBasis K L b)) = span ℤ (⇑L.subtype '' Set.range ⇑b)

Tactic:
by congr; ext; simp

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
refine ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1,
    fun hD => (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
⊢ ∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: case inr
𝕜 : 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
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
rw [inner_eq_zero_symm]
      exact this _ _ hb

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

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
c✝ : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
⊢ x ∈ s ∩ c⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ↔
    (Equiv.smulRight hc) x ∈ c • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Set.mem_inter_iff,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
c✝ : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
⊢ x ∈ s ∧ x ∈ c⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ↔
    (Equiv.smulRight hc) x ∈ c • s ∧ (Equiv.smulRight hc) x ∈ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
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 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
exact mem_span_gramSchmidt 𝕜 f le_rfl

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

Goal state before:
pp: case zero
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
hb : b.toBasis.orientation = o
⊢ o.volumeForm = b.toBasis.det

Tactic:
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty

Goal state after:
case zero
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
hb : b.toBasis.orientation = o
this : o = positiveOrientation
⊢ o.volumeForm = b.toBasis.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
h : Integrable I l f vol
⊢ Tendsto (fun π ↦ (integralSum f vol π.1, integralSum f vol π.2))
    (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π | π.1.iUnion = π.2.iUnion}) (𝓤 F)

Tactic:
refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
    uniformity_basis_dist_le).2 fun ε ε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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀
        x ∈
          {π | ∃ c, l.MemBaseSet I c (ia c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (ia c) π} ∩ {π | π.1.iUnion = π.2.iUnion},
        (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : ⇑b = Subtype.val
⊢ map (⇑f) volume = volume

Tactic:
erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f),
    Basis.map_addHaar _ f.toContinuousLinearEquiv]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : ⇑b = Subtype.val
⊢ (b.toBasis.map ↑↑f).addHaar = (b.map f).toBasis.addHaar
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯).trans (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ volume = map ((fun x ↦ x • v) ∘ fun x ↦ ‖v‖⁻¹ • x) volume

Tactic:
convert! f.measurePreserving.map_eq.symm

Goal state after:
case e'_5
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯).trans (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ ((fun x ↦ x • v) ∘ fun x ↦ ‖v‖⁻¹ • x) = ⇑f
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ ‖v‖⁻¹ ≠ 0

Tactic:
by simpa using hv

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
⊢ f = ∑ a, {n | ↑n = a}.indicator f

Tactic:
ext n
  simp only [Finset.sum_apply, Set.indicator_apply, Set.mem_ofPred_eq, Finset.sum_ite_eq,
    Finset.mem_univ, ↓reduceIte]

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

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∩ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Set.mem_inter_iff,

Goal state after:
case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s ∧ x ∈ (↑n)⁻¹ • ↑L ↔
    (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s ∧
      (Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv x ∈ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case e'_1
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
h_pow : Filter.Tendsto (fun n ↦ 2 ^ n) Filter.atTop Filter.atTop
⊢ (fun k ↦ 2 ^ k * f (2 ^ k)) =ᶠ[Filter.atTop] fun k ↦ 2 ^ k * f (max (2 ^ k) (n + m))

Tactic:
filter_upwards [h_pow.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]

Goal state after:
Module: Mathlib.Analysis.PSeries

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

Tactic:
← division_def,

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ 1 / 2 ^ p‖ < 1 ↔ 1 < p
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} ∩ ↑L ↔
    ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv.trans (Equiv.smulRight aux₄)) x✝ ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Set.mem_inter_iff,

Goal state after:
case e_a
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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} ∧ x✝ ∈ ↑L ↔
    ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv.trans (Equiv.smulRight aux₄)) x✝ ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} ∧ x✝ ∈ ↑L ↔
    ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv.trans (Equiv.smulRight aux₄)) x✝ ∈
      ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∩
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Set.mem_inter_iff,

Goal state after:
case e_a
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
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} ∧ x✝ ∈ ↑L ↔
    ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv.trans (Equiv.smulRight aux₄)) x✝ ∈
        ⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1} ∧
      ((Basis.ofZLatticeBasis ℝ L b).equivFun.toEquiv.trans (Equiv.smulRight aux₄)) x✝ ∈
        (c ^ (↑(card ι))⁻¹)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
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 - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n

Tactic:
summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)

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 ↦ 1 / ↑(n + 1)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n ↦ ‖x / (↑n + ↑k) ^ q‖

Tactic:
norm_div

Goal state after:
α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n ↦ ‖x‖ / ‖(↑n + ↑k) ^ q‖
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ x ∈ Ideal.span (⇑(of k G) '' s) ↔ ∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'

Tactic:
change _ ↔ x ∈ RHS

Goal state after:
k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
RHS : Ideal k[G] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ x ∈ Ideal.span (⇑(of k G) '' s) ↔ x ∈ RHS
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ x ∈ Ideal.span (of' k A '' s) ↔ ∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'

Tactic:
change _ ↔ x ∈ RHS

Goal state after:
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ x ∈ Ideal.span (of' k A '' s) ↔ x ∈ RHS
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)!

Tactic:
rw [factorial_eq_mul_doubleFactorial]

Goal state after:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)‼ * n‼
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 0 ^ 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
rw [_root_.pow_zero, Fintype.sum_subsingleton]
      swap
      · exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
      convert! (@one_mul R _ _).symm
      convert! @Nat.cast_one R _
      simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ((Finsupp.single 0 x + Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).sum fun x a ↦ a) = x + l.sum

Tactic:
Finsupp.sum_add_index (by simp) (by simp)

Goal state after:
α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ (((Finsupp.single 0 x).sum fun x a ↦ a) + (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).sum fun x a ↦ a) =
    x + l.sum
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case insert
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
⊢ ∀ (x : Π₀ (i : ι), α i),
    x.support = insert b t → (∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
| insert b t hb ih =>

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ f ∣ C a ↔ ∃ b, b ∣ a ∧ f = C b

Tactic:
by
  constructor
  · intro hf
    use coeff 0 f
    suffices f.totalDegree = 0 by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0
    apply Nat.eq_zero_of_le_zero
    simpa using totalDegree_le_of_dvd_of_isDomain hf (by simp [ha])
  · rintro ⟨b, hab, rfl⟩
    exact map_dvd C hab

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (init r)}) = #(S (last n) ×ˢ {r ∈ piFinset (init S) | P r})

Tactic:
← map_snocEquiv_filter_piFinset,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (init r)}) = #(map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset S | P (init r)}))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : m.toSyn 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
simp only [map_zero] at hd

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ m.degree p ∈ p.support

Tactic:
by
  rwa [MvPolynomial.mem_support_iff, coeff_degree_ne_zero_iff]

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
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Tactic:
simp only [le_of_lt (h' h)]

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
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
hf' : m.toSyn d ≤ m.toSyn (m.degree g)
⊢ m.toSyn (a + b) ≤ m.toSyn c + m.toSyn b

Tactic:
← hcd,

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
hf' : m.toSyn d ≤ m.toSyn (m.degree g)
⊢ m.toSyn (c + d) ≤ m.toSyn c + m.toSyn b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply degree_mul_of_mul_leadingCoeff_ne_zero
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero_iff, not_or]
  tauto

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

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ n.MinSqFacProp (n.minSqFacAux k)

Tactic:
by
  rw [minSqFacAux]
  by_cases h : n < k * k <;> simp only [h, ↓reduceDIte]
  · refine squarefree_iff_prime_squarefree.2 fun p pp d => ?_
    have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
    have := Nat.mul_le_mul this this
    exact not_le_of_gt h (le_trans this (le_of_dvd n0 d))
  have k2 : 2 ≤ k := by lia
  have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
  have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) := by
    intro n' nd' nk
    have hn' := le_of_dvd n0 nd'
    refine
      have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
        lt_of_le_of_lt (by gcongr) (Nat.minFac_lemma n k h)
      @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1)
        (by simp [e, left_distrib]) fun m m2 d => ?_
    rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with rfl | ml
    · contradiction
    apply (Nat.eq_or_lt_of_le ml).resolve_left
    intro me
    rw [← me, e] at d
    change 2 * (i + 2) ∣ n' at d
    have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
    rw [e] at this
    exact absurd this (by lia)
  have pk : k ∣ n → Prime k := by
    refine fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩
    exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
  split_ifs with dk dkk
  · exact ⟨pk dk, (Nat.dvd_div_iff_mul_dvd dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
  · specialize IH (n / k) (div_dvd_of_dvd dk) dkk
    exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff_mul_dvd dk).2 dkk) IH
  · exact IH n (dvd_refl _) dk

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

Goal state before:
pp: case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
simp [h0]

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

Goal state before:
pp: case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
simp [h0]

Goal state after: