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

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s / covolume L volume = volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)

pp: ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0

Tactic:
· simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume (frontier s) / ENNReal.ofReal (covolume L volume) = 0

Tactic:
hs₃,

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ 0 / ENNReal.ofReal (covolume L volume) = 0
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 ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume =
    volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})

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 ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0

Tactic:
· simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Goal state after:
ι : 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 ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := (Free.chooseBasis ℤ ↥L).reindex e
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
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 < ε
⊢ ∑ k ∈ range n, ∑ p ∈ s (k + 1) \ s k, ((↑k + 1) * ε) ^ r ≤
    ∑ k ∈ range n, ↑(2 * d * (3 * (k + 1)) ^ (d - 1)) * ((↑k + 1) * ε) ^ r

Tactic:
simp only [sum_const, nsmul_eq_mul]

Goal state after:
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 < ε
⊢ ∑ x ∈ range n, ↑(#(s (x + 1) \ s x)) * ((↑x + 1) * ε) ^ r ≤
    ∑ k ∈ range n, ↑(2 * d * (3 * (k + 1)) ^ (d - 1)) * ((↑k + 1) * ε) ^ r
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 ι
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real {x | x ∈ X ∧ F x ≤ 1} / covolume L volume))

Tactic:
by
  let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := by
    refine Fintype.equivOfCardEq ?_
    rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
  let b := (Module.Free.chooseBasis ℤ L).reindex e
  convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
  · simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, ENNReal.zero_div]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ volume (frontier s) / ENNReal.ofReal (covolume L volume) = 0

pp: case hs
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet (frontier s) volume

Tactic:
hs₃,

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ 0 / ENNReal.ofReal (covolume L volume) = 0

case hs
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
L : Submodule ℤ E
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet (frontier s) volume
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
⊢ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp

Goal state after:
case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : q = p.divMonomial (Finsupp.single i 1) * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
⊢ p.divMonomial (Finsupp.single i 1) ∣ q
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) (1 * 1) * r ∣ (monomial (m + (n - m))) (1 * 1) * q

Tactic:
← monomial_mul,

Goal state after:
case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) (1 * 1) * r ∣ (monomial m) 1 * (monomial (n - m)) 1 * q
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
    (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ ⇑C '' s 0 ⊆ {x | ((finSuccEquiv R n) p).IsRoot x}

Tactic:
rintro _ ⟨r, hr, rfl⟩

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
    (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
r : R
hr : r ∈ s 0
⊢ C r ∈ {x | ((finSuccEquiv R n) p).IsRoot x}
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e_a.e_a
x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.sum fun x ↦ id) = x + l.sum

Tactic:
exact List.toFinsupp_sum (x :: l)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
    · convert! emptyWf.wf
    let : ∀ i, Zero (α i) := fun i => ⟨(hw i).wf.min ⊤ ⟨x i, trivial⟩⟩
    have := Fintype.ofFinite ι
    refine InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => ?_).wf
    exact (hw i).wf.not_lt_min ⊤ trivial

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.degree 0 = 0

Tactic:
by
  simp [degree]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
s : Finset α
f : α → MvPolynomial σ R
⊢ m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
induction s using Finset.cons_induction_on with

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
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ 1 * m.leadingCoeff g = 1

Tactic:
hg.leadingCoeff_eq_one,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
⊢ 1 * 1 = 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Tactic:
exact this.1

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
s : Finset α
f : α → MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
induction s using Finset.cons_induction_on with

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

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
⊢ x = 1

Tactic:
by_contra hx

Goal state after:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

Tactic:
· apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)
    by_contra! h'
    simp only [EmbeddingLike.apply_eq_iff_eq] at h'
    apply m.degree_mem_support at hl
    rw [h', mem_support_iff] at hl
    simp [leadingTerm, leadingCoeff] at hl

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

Goal state before:
pp: n : ℕ
⊢ ∃ a b, b ^ 2 * a = n ∧ Squarefree a

Tactic:
rcases n with - | n
  · exact ⟨1, 0, by simp, squarefree_one⟩
  · obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
    exact ⟨a, b, h₁, h₂⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i =
    ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2

Tactic:
sum_divisorsAntidiagonal (f · * g ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = ∑ i ∈ n.divisors, f i * g (n / i)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ g b + ∑ b ∈ B, g b = ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)

Tactic:
by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]

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 (τ i)

pp: case insert.inr
ι : 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 (τ i)

Tactic:
· rw [hτ, ← hσa, swap_self, trans_refl]

Goal state after:
case insert.inr
ι : 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 (τ i)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r, x

Tactic:
← sum_inter_add_sum_sdiff r s _

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r ∩ s, x + ∑ x ∈ r \ s, x
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = (Finset.Ioo (c + a) (c + b)).val

Tactic:
← Finset.image_add_left_Ioo,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = (Finset.image (fun x ↦ c + x) (Finset.Ioo a b)).val
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s : NonemptyInterval α
⊢ ↑(↑s ⊓ ⊥) = ↑↑s ∩ ↑⊥

Tactic:
rw [inf_bot_eq]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s : NonemptyInterval α
⊢ ↑⊥ = ↑↑s ∩ ↑⊥
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : NonemptyInterval α
a : α
⊢ ↑s = Interval.pure a ↔ s = pure a

Tactic:
by
  rw [← Interval.coe_inj, coe_pure_interval]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun b ↦ b) s = s

Tactic:
← Function.id_def,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map id s = s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun x ↦ x) s = s

Tactic:
← Function.id_def,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map id s = s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : Interval α
⊢ ∀ (x : Interval α), x⁻¹⁻¹ = x

Tactic:
rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (inv_inv _)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ∀ (a : Γ), {y | toLex (a, y) ∈ Function.support fun g ↦ (x.coeff g.1).coeff g.2}.IsPWO

Tactic:
exact fun a => by simpa [Function.mem_support, ne_eq] using! (x.coeff a).isPWO_support'

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
⊢ 0 < (ofLex x).leadingCoeff

Tactic:
have htop : (ofLex x).orderTop ≠ ⊤ := WithTop.ne_top_iff_exists.mpr ⟨i, horder.symm⟩

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
⊢ 0 < (ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
obtain rfl | hlt := h.eq_or_lt
    · simp
    · exact (leadingCoeff_pos_iff.mpr hlt).le

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
simpa using orderTop_ne_top.1 <| h ▸ orderTop_ne_top.2 (by simpa using hy)

Goal state after: