mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x ∈ range 0, f x + f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k ≤ f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k

Tactic:
sum_range_zero,

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ 0 + f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k ≤ f 0 + ∑ k ∈ Ico 1 (2 ^ n), f k
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 • x ∈ ↑(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))) ↔
      ↑n • ⇑((Basis.ofZLatticeBasis ℝ L b).repr x) ∈ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
← Finsupp.coe_smul,

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 →
    (↑n • x ∈ ↑(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))) ↔
      ⇑(↑n • (Basis.ofZLatticeBasis ℝ L b).repr x) ∈ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: 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
⊢ Tendsto (fun n ↦ ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι) atTop
    (𝓝 (volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))

Tactic:
refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
  · filter_upwards [eventually_gt_atTop 0] with n hn
    congr
    refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm
    simp_rw [Set.mem_inter_iff, ← b.ofZLatticeBasis_span ℝ, LinearEquiv.coe_toEquiv,
      Basis.equivFun_apply, Set.mem_image, DFunLike.coe_fn_eq, EmbeddingLike.apply_eq_iff_eq,
      exists_eq_right, and_congr_right_iff, Set.mem_inv_smul_set_iff₀
      (mod_cast hn.ne' : (n : ℝ) ≠ 0), ← Finsupp.coe_smul, ← map_smul, SetLike.mem_coe,
      Basis.mem_span_iff_repr_mem, Pi.basisFun_repr, implies_true]
  · rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢
    exact Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
have hnorm : Tendsto (fun n : ℕ ↦ ‖(n : ℝ)‖) atTop atTop :=
    tendsto_natCast_atTop_atTop.congr' (by simp)

Goal state after:
a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case neg
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝¹ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this✝ : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
this : |ε / 2| * (|‖x‖|⁻¹ * |↑((b.repr x) i)|) < 1
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖

Tactic:
mul_left_comm,

Goal state after:
case neg
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝¹ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this✝ : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
ε : ℝ
hε : ε > 0
hε' : Metric.ball 0 ε ⊆ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1
x : ↥L
i : ι
hx✝ : ¬x = 0
hx : ‖↑x‖ ≠ 0
this : |‖x‖|⁻¹ * (|ε / 2| * |↑((b.repr x) i)|) < 1
⊢ ε / 2 * ↑|(b.repr x) i| ≤ ‖x‖
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
s : Finset ↥L
⊢ ∑ z ∈ s, ‖z‖ ^ r ≤ 1 ^ r * ∑' (k : ℕ), ↑k ^ (↑(finrank ℤ ↥L) - 1 + r)

Tactic:
have hr : r ≠ 0 := by linarith

Goal state after:
case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
r : ℝ
hr✝ : r < -↑(finrank ℤ ↥L)
s : Finset ↥L
hr : r ≠ 0
⊢ ∑ z ∈ s, ‖z‖ ^ r ≤ 1 ^ r * ∑' (k : ℕ), ↑k ^ (↑(finrank ℤ ↥L) - 1 + r)
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
⊢ comap f x = x

Tactic:
by
  convert! comap_id_apply x
  ext1 φ
  simp [hf, AlgHom.id_apply]

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

Goal state before:
pp: case hnc.e_f
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ (fun x_1 ↦ (indicator a.support fun i x_2 ↦ x i) x_1) = x

Tactic:
ext i

Goal state after:
case hnc.e_f
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
i : σ
⊢ (indicator a.support fun i x_1 ↦ x i) i = x i
Module: Mathlib.Algebra.MvPolynomial.Coeff

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

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

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

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

Tactic:
simp only [← exists_prop, gt_iff_lt, Subtype.exists'] at H₁ H₂

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) * q -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
nth_rewrite 1 [← hq]

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) *
        (q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1)) -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
⊢ (Finsupp.single 0 x + Finsupp.embDomain succEmb l.toFinsupp).update 0 0 =
    (Finsupp.embDomain succEmb l.toFinsupp).update 0 0

Tactic:
ext i

Goal state after:
x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
i : ℕ
⊢ ((Finsupp.single 0 x + Finsupp.embDomain succEmb l.toFinsupp).update 0 0) i =
    ((Finsupp.embDomain succEmb l.toFinsupp).update 0 0) i
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : 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)
h₂ : r j i
⊢ x₂ j = x j

Tactic:
rw [hr j h₂, if_neg]
        simpa [h₂] using h₁

Goal state after:
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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ i ∈ x.support, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
generalize ht : x.support = t

Goal state after:
ι : 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)
x : Π₀ (i : ι), α i
t : Finset ι
ht : x.support = t
⊢ (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) < degree (ofDegLex b)
hbc : degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) < toLex (ofDegLex c)
⊢ degree (ofDegLex a) < degree (ofDegLex c) ∨
    degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

Tactic:
· left; exact lt_of_lt_of_eq hab hbc.1

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
⊢ x_zero ∈ s_zero ∧ tail (cons x_zero x_tail) ∈ piFinset (tail (cons s_zero s_tail)) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail

Tactic:
tail_cons

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.toSyn (m.degree ((monomial d) c)) ≤ m.toSyn d

Tactic:
simp only [degree, AddEquiv.apply_symm_apply]
  apply le_trans (Finset.sup_mono support_monomial_subset)
  simp only [Finset.sup_singleton, le_refl]

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

Goal state before:
pp: case h₀
σ : 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
⊢ ∀ b_1 ∈ Finset.antidiagonal (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0

Tactic:
rintro ⟨c, d⟩ hcd h

Goal state after:
case h₀
σ : 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 : σ →₀ ℕ
hcd : (c, d) ∈ Finset.antidiagonal (a + b)
h : (c, d) ≠ (a, b)
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : MvPolynomial (Fin 0) R
hp : p ≠ 0
S : Fin 0 → Finset R
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0})) / ∏ i, ↑(#(S i)) ≤ p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
rw [p.eq_C_of_isEmpty] at *

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : MvPolynomial (Fin 0) R
hp : C (coeff 0 p) ≠ 0
S : Fin 0 → Finset R
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) (C (coeff 0 p)) = 0})) / ∏ i, ↑(#(S i)) ≤
    (C (coeff 0 p)).support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
simp [leadingTerm, h, degree_monomial]

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 : MvPolynomial σ R
h : ¬f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
simp [leadingTerm, h, degree_monomial]

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
⊢ #(filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding)
        (S 0 ×ˢ {r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0})) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
product_eq_biUnion_right,

Goal state after:
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
⊢ #(filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding)
        ({r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}.biUnion fun b ↦ image (fun a ↦ (a, b)) (S 0))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))
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.leadingTerm p).support = {m.degree p}

Tactic:
simp [leadingTerm, support_monomial, hp]

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
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
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 => ?_

Goal state after:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
⊢ k + 2 ≤ m
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: x : ℕ
⊢ ζ x = 0 ↔ x = 0

Tactic:
simp [zeta]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
⊢ r • 0 = 0

Tactic:
by
    ext
    simp only [smul_apply, sum_const_zero, smul_zero, zero_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight a = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
Function.Embedding.arrowCongrRight_apply,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        ⇑(Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }) ∘ a = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Tendsto

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
⊢ Tendsto (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite F

Tactic:
intro U

Goal state after:
M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
⊢ U ∈ F → U ∈ Filter.map (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ

Tactic:
apply fun _ _ => mem_univ _

Goal state after:
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
· obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
    apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
    exact mod_cast hq

Goal state after:
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a = σ a
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g ((Equiv.trans σ (Equiv.swap a (σ a))) i)

Tactic:
← hσa,

Goal state after:
case insert.inl
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a = σ a
⊢ f a • g a + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g ((Equiv.trans σ (Equiv.swap a a)) i)
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (∑ i ∈ s, f i ^ 2) * (↑(#s) * ↑(#s))

Tactic:
mul_left_comm,

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ ↑(#s) * ((∑ i ∈ s, f i ^ 2) * ↑(#s))
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : mk a < mk b
⊢ b < a

Tactic:
mk_lt_mk

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ b < a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : mk b < mk a
⊢ b < a

Tactic:
mk_lt_mk

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
⊢ b < a