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

Goal state before:
pp: case refine_1
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
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
x✝ : ℤ
⊢ x✝ • v ∈ span ℤ (Set.range b)

Tactic:
exact zsmul_mem (subset_span (Set.sdiff_subset hv)) _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
⊢ μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u

Tactic:
utop

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
u v : Set E
uzero : μ u ≠ 0
utop : μ u ≠ ∞
⊢ MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
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 ι
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
⊢ ⇑(v.toOrthonormalBasis hv) = ⇑(v.toOrthonormalBasis hv).toBasis

Tactic:
by
      rw [OrthonormalBasis.coe_toBasis]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case neg
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
this : ∀ (r' : ℝ), ENNReal.ofReal r' ≤ r → ediam (f '' (eball x (ENNReal.ofReal r') ∩ D)) ≤ ε
r_top : ¬r = ∞
⊢ ∃ i, 0 < i ∧ x ∈ S i

Tactic:
obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
      use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : Box.Icc J ⊆ Set.univ.pi fun i ↦ Set.Icc (I₀.lower i) (I₀.upper i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : ↑(J.face i) ≤ ↑(I₀.face i)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    (fb ⟨J.upper i, ⋯⟩) (J.face i) - f (J.lower i) (J.face i)

Tactic:
hf _ (hJ J.lower_mem_Icc _ trivial),

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
I₀✝ : WithTop (Box ι)
I : Box ι
i✝ : ι
G : Type u
inst✝ : AddCommGroup G
I₀ : Box (Fin (n + 1))
i : Fin (n + 1)
f : ℝ → Box (Fin n) → G
fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G
hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J
J : Box (Fin (n + 1))
hJ : Box.Icc J ⊆ Set.univ.pi fun i ↦ Set.Icc (I₀.lower i) (I₀.upper i)
j✝ : Fin (n + 1)
x : ℝ
j : Fin n
hx : x ∈ Set.Ioo (J.lower (i.succAbove j)) (J.upper (i.succAbove j))
this : ↑(J.face i) ≤ ↑(I₀.face i)
⊢ Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower (i.succAbove j) x) +
      Option.elim' 0 (fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper (i.succAbove j) x) =
    (fb ⟨J.upper i, ⋯⟩) (J.face i) - (fb ⟨J.lower i, ⋯⟩) (J.face i)
Module: Mathlib.Analysis.BoxIntegral.Integrability

Goal state before:
pp: case hbc.refine_2
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ ↑I
hμt : μ t ≠ ∞
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ ↑I
hxF : x ∈ F
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
⊢ ∃ i, ∃ (_ : i ∈ π ∧ π.tag i ∈ s), x ∈ ↑i

Tactic:
refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩

Goal state after:
case hbc.refine_2
ι : Type u
E : Type v
inst✝³ : Fintype ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
l : IntegrationParams
hl : l.bRiemann = false
s : Set (ι → ℝ)
hs : MeasurableSet s
I : Box ι
y : E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
ε : ℝ≥0
ε0 : 0 < ε
A : μ (s ∩ Box.Icc I) ≠ ∞
B : μ (s ∩ ↑I) ≠ ∞
F : Set (ι → ℝ)
hFs : F ⊆ s ∩ Box.Icc I
hFc : IsClosed F
hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε
U : Set (ι → ℝ)
hsU : s ∩ Box.Icc I ⊆ U
hUo : IsOpen U
hUt : μ U < ∞
hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε
rs : (ι → ℝ) → ↑(Set.Ioi 0)
hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U
rs' : (ι → ℝ) → ↑(Set.Ioi 0)
hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ
r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c ((fun x ↦ r) c) π
hπp : π.IsPartition
t : Set (ι → ℝ) := (π.filter fun x ↦ π.tag x ∈ s).iUnion
htU : t ⊆ U ∩ ↑I
hμt : μ t ≠ ∞
x : ι → ℝ
hxt : x ∉ t
hxs : x ∈ s
hxI : x ∈ ↑I
hxF : x ∈ F
J : Box ι
hJπ : J ∈ π.toPrepartition
hxJ : x ∈ J
⊢ π.tag J ∈ s
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
⊢ span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (Set.range (gramSchmidt 𝕜 f))

Tactic:
simpa only [image_univ.symm] using span_gramSchmidtNormed f univ

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
v : Fin n → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
cases n
  · refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
  · rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
      b.abs_det_adjustToOrientation]

Goal state after:
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
inst✝¹ : Fintype ι₁
inst✝ : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ Orthonormal 𝕜 ⇑((v.toBasis.prod w.toBasis).map (WithLp.linearEquiv 2 𝕜 (E × F)).symm)

Tactic:
constructor
    · simp
    · unfold Pairwise
      simp only [ne_eq, Basis.map_apply, Basis.prod_apply, LinearMap.coe_inl,
        OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.coe_symm_linearEquiv,
        WithLp.prod_inner_apply, Sum.forall, Sum.elim_inl, Function.comp_apply, inner_zero_right,
        add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq, reduceCtorEq, not_false_eq_true,
        inner_zero_left, imp_self, implies_true, and_true, Sum.inr.injEq, true_and]
      exact ⟨v.orthonormal.2, w.orthonormal.2⟩

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
⊢ volume = dirac 0

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]

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

Goal state before:
pp: U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving
    (⇑(((MeasurableEquiv.toLp 2 (Fin (finrank ℝ U) → ℝ)).trans
            (stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv).prodCongr
        ((MeasurableEquiv.toLp 2 (Fin (finrank ℝ V) → ℝ)).trans (stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv)))
    ((Measure.pi fun i ↦ volume).prod (Measure.pi fun i ↦ volume)) volume

Tactic:
refine MeasurePreserving.prod ?_ ?_

Goal state after:
case refine_1
U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving
    (⇑((MeasurableEquiv.toLp 2 (Fin (finrank ℝ U) → ℝ)).trans
          (stdOrthonormalBasis ℝ U).repr.symm.toMeasurableEquiv).toEquiv)
    (Measure.pi fun i ↦ volume) volume

case refine_2
U : Type u_4
V : Type u_5
inst✝⁹ : NormedAddCommGroup U
inst✝⁸ : InnerProductSpace ℝ U
inst✝⁷ : MeasurableSpace U
inst✝⁶ : BorelSpace U
inst✝⁵ : FiniteDimensional ℝ U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ MeasurePreserving
    (⇑((MeasurableEquiv.toLp 2 (Fin (finrank ℝ V) → ℝ)).trans
          (stdOrthonormalBasis ℝ V).repr.symm.toMeasurableEquiv).toEquiv)
    (Measure.pi fun i ↦ volume) volume
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
⊢ map (fun x ↦ x • v) (map (fun x ↦ ‖v‖⁻¹ • x) volume) = ‖v‖ₑ • map (fun x ↦ x • v) volume

Tactic:
rw [map_addHaar_smul _ (by simpa using hv)]
    simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
⊢ (fun n ↦ Real.log (f n)) ~[l] fun n ↦ Real.log (g n)

Tactic:
have hg := g_tendsto.eventually_ne_atTop 0

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
⊢ (fun n ↦ Real.log (f n)) ~[l] fun n ↦ Real.log (g n)
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
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

Tactic:
obtain ⟨y, hy⟩ := integrable_of_bounded_and_ae_continuous l hb μ hc

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
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
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
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n
⊢ ∑ i ∈ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n, ‖↑(e i)‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
simp only [Submodule.norm_coe]

Goal state after:
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
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
n : ℕ
hn : u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n
⊢ ∑ x ∈ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n, ‖e x‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
by
  simp [binomial_eq h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]

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

Goal state before:
pp: a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ∏ i, (![a, b, c] i)! = (a + b + c)! / (a ! * b ! * c !)

Tactic:
Fin.prod_univ_three

Goal state after:
a b c : ℕ
⊢ (![a, b, c] 0 + ![a, b, c] 1 + ![a, b, c] 2)! / ((![a, b, c] 0)! * (![a, b, c] 1)! * (![a, b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
a : R
⊢ (monomial d) a = C a * X 0 ^ d 0 * X 1 ^ d 1

Tactic:
by
  rw [monomial_eq, mul_assoc, d.prod_fintype _ fun _ ↦ pow_zero _, Fin.prod_univ_two]

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

Goal state before:
pp: case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (x + (y + l.sum)).choose (x + l.sum) * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
Nat.choose_mul (Nat.le_add_right _ _),

Goal state after:
case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (x + (y + l.sum)).choose x * (x + (y + l.sum) - x).choose (x + l.sum - x) * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
Nat.choose_mul (Nat.le_add_right _ _),

Goal state after:
case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose x * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : 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 : ι
hi : Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) i
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)

Tactic:
by
  induction hi with | _ i _ ih
  refine fun a => WellFounded.induction (hs i)
    (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_
  refine Acc.intro _ fun x ↦ ?_
  rintro ⟨k, hr, hs⟩
  rw [single_apply] at hs
  split_ifs at hs with hik
  swap
  · exact (hbot hs).elim
  subst hik
  classical
    refine Lex.acc_of_single hbot x fun j hj ↦ ?_
    obtain rfl | hij := eq_or_ne j i
    · exact ha _ hs
    by_cases h : r j i
    · rw [hr j h, single_eq_of_ne hij, single_zero]
      exact Lex.acc_zero hbot
    · exact ih _ ⟨h, hij⟩ _

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
⊢ a < b → b < c → a < c

Tactic:
hab

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : a < b
⊢ b < c → a < c
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ C (m.leadingCoeff p) * (monomial (m.degree p)) 1 = m.leadingTerm p

Tactic:
rw [MvPolynomial.C_mul_monomial, mul_one, leadingTerm]

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (k + 1)

Tactic:
rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1),
      ← card_sym_fin_eq_multichoose (n + 2) k, add_comm (Fintype.card _), ← card_sum]

Goal state after:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
⊢ (fun f ↦ ⟨(↑f).extendDomain, ⋯⟩) ((fun f ↦ ⟨subtypeDomain (fun x ↦ x ∈ s) ↑f, ⋯⟩) f) = f

Tactic:
by
    obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop
    ext1
    exact extendDomain_subtypeDomain _ hs

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
⊢ a + 1 < n✝ + 1

Tactic:
refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_

Goal state after:
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
con : a + 1 = n✝ + 1
⊢ n✝ + 1 ∣ a + 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
apply degree_pow_of_pow_leadingCoeff_ne_zero

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.leadingCoeff f ^ n ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
⊢ m.degree (r • f) = m.degree f

Tactic:
by_cases hf : f = 0
  · simp [hf]
  apply m.toSyn.injective
  apply le_antisymm degree_smul_le
  apply le_degree
  simp only [mem_support_iff, smul_eq_C_mul]
  rw [← zero_add (degree m f), ← degree_C r, coeff_mul_of_degree_add]
  simp [not_imp_not.mpr ((mem_nonZeroDivisors_iff.mp hr).1 _) <| m.leadingCoeff_ne_zero_iff.mpr hf]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0}) =
    #({x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ ≠ 0 ∧ (eval x) p = 0})

Tactic:
simp_rw [and_comm]

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

Goal state before:
pp: case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
rw [squarefree_iff_emultiplicity_le_one] at hn

Goal state after:
case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1
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
inst✝ : NoZeroDivisors R
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
nontriviality R using Subsingleton.eq_zero (α := MvPolynomial σ R)

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
rw [dirichletInverse, mul_apply, coe_mk,
    Nat.sum_divisorsAntidiagonal' fun x y ↦ f x * dirichletInverseFun f hf y,
    ← Nat.cons_self_properDivisors hn0]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ ∑ i ∈ cons n n.properDivisors ⋯, f (n / i) * dirichletInverseFun (⇑f) hf i = 1 n
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)

Tactic:
exact ⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).le⟩

Goal state after: