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

Goal state before:
pp: case refine_1
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (↑n)⁻¹ ≤ ↑(r 0 0)

Tactic:
inv_le_comm₀ (mod_cast (Nat.pos_of_neZero n)) (r 0 0).prop

Goal state after:
case refine_1
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (↑(r 0 0))⁻¹ ≤ ↑n
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε

Tactic:
let μ' := μ.restrict (Box.Icc I)

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
⊢ ∃ r,
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (toLp 2) (Pi.basisFun ℝ ι).addHaar

Tactic:
← PiLp.coe_symm_continuousLinearEquiv 2 ℝ,

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (Pi.basisFun ℝ ι).addHaar
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ (fun x ↦ x ^ p / x ^ q) =ᶠ[atTop] fun x ↦ x ^ (↑p - ↑q)

Tactic:
apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), 0 < x → (fun x ↦ x ^ p / x ^ q) x = (fun x ↦ x ^ (↑p - ↑q)) x
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x ↦ x ^ p / x ^ q) atTop atTop

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x ↦ x ^ (↑p - ↑q)) atTop atTop
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x ↦ x ^ p / x ^ q) atTop (𝓝 0)

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x ↦ x ^ (↑p - ↑q)) atTop (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x ↦ ‖v x‖) l atTop

Tactic:
rw [IsBigOWith] at hcuv

Goal state after:
𝕜 : Type u_1
inst✝ : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x ↦ ‖v x‖) l atTop
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 : ℕ
⊢ ∑ k ∈ Ico 1 (2 ^ n), f k ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Tactic:
convert!
    le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n)
      (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2
  simp [pow_succ, mul_two]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (↑x)⁻¹ • ∑ i ∈ Finset.range x, (u i - l)) =ᶠ[atTop] fun x ↦ (↑x)⁻¹ • ∑ i ∈ Finset.range x, u i - l

Tactic:
filter_upwards [Ici_mem_atTop 1] with n npos
    have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
    simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
    rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_3 : DiscreteTopology ↥L] {ι : Type u_2} (b : Basis ι ℤ ↥L),
    IsZLattice ℝ L → ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ ↑L
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst : DiscreteTopology ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
⊢ Submodule.map E'.subtype (Submodule.span ℝ ↑L') = Submodule.map E'.subtype ⊤

Tactic:
simp [E', L']

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

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ⇑s ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
⊢ ↑(Nat.multinomial a.support ⇑s) * ∏ x ∈ a.support, a x ^ s x = 0

Tactic:
exfalso

Goal state after:
case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ⇑s ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((Finset.image (fun x ↦ p • x) f.support).sup fun m ↦ (Finsupp.toMultiset m).card) =
    (f.support.sup fun m ↦ (Finsupp.toMultiset m).card) * p

Tactic:
simp only [Finsupp.card_toMultiset, Finset.sup_image, Finset.sup_mul₀, Function.comp_def]

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ (f.support.sup fun x ↦ (p • x).sum fun x ↦ id) = f.support.sup fun x ↦ (x.sum fun x ↦ id) * p
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial (Fin 0) R
s : Fin 0 → Set R
hs : ∀ (i : Fin 0), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ (isEmptyRingEquiv R (Fin 0)) p = (isEmptyRingEquiv R (Fin 0)) 0

Tactic:
simpa [constantCoeff, coeff] using h 0 finZeroElim

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

Goal state before:
pp: x : ℕ
l : List ℕ
⊢ (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧

Tactic:
exact List.multinomial_cons x l

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
h : ¬r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
· exact ih _ ⟨h, hij⟩ _

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

Goal state before:
pp: case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ (if 0 = 0 then ⊤ else ↑0) < if b = 0 then ⊤ else ↑b

Tactic:
exfalso

Goal state after:
case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ False
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
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ coeff (m.degree (f * g)) (f * g) = coeff (m.degree f + m.degree g) (f * g)

Tactic:
degree_mul_of_mul_leadingCoeff_ne_zero hfg

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ coeff (m.degree f + m.degree g) (f * g) = coeff (m.degree f + m.degree g) (f * g)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:

Tactic:
#{x ∈ S ^^ (n + 1) | eval x p = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the first case, `pₖ` evaluates to `0`.
        = #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the second case, `pₖ` does not evaluate to `0`.
          + #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0) := by
        rw [← add_div, ← Nat.cast_add, ← card_union_add_card_inter, filter_union_right,
          ← filter_and]
        simp [← and_or_left, em, and_and_and_comm]
      _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S i.succ) : ℚ≥0)) + p.degreeOf 0 / #(S 0) := ?_
      _ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := ?_

Goal state after:
case calc_1
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})) / ∏ i, ↑(#(S i)) +
      ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0))

case calc_2
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
⊢ (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))
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 (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))

Tactic:
rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]

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
⊢ ↑(#(S 0) * #({r ∈ piFinset fun k ↦ S k.succ | (eval r) pₖ = 0})) / (↑(#(S 0)) * ∏ i, ↑(#(S i.succ))) =
    ↑(#(S 0)) * ↑(#({xₜ ∈ piFinset fun i ↦ (fun k ↦ S k.succ) i | (eval xₜ) pₖ = 0})) /
      (↑(#(S 0)) * ∏ i, ↑(#(S i.succ)))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ False

Tactic:
have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩

Goal state after:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ False
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
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

Tactic:
by_cases! h : f = 0 ∨ g = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
ext p

Goal state after:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ p ∈ (∏ p ∈ s, p).primeFactors ↔ p ∈ s
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2
n k : ℕ
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ ∏ p ∈ n.primeFactors, p ∣ k

Tactic:
grw [← k.prod_primeFactors_dvd, Finset.prod_dvd_prod_of_subset _ _ _ h]

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

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

Tactic:
ext p

Goal state after:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
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
⊢ ⊤ = mk a ↔ a = 1

Tactic:
by
  rw [eq_comm, mk_eq_top_iff]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ (x.lcm y).factorization x_1)) *
      ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ (x.gcd y).factorization x_1) =
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ x.factorization x_1)) *
      ∏ x ∈ x.primeFactors ∪ y.primeFactors, f (x ^ y.factorization x)

Tactic:
rw [← prod_mul_distrib, ← prod_mul_distrib]

Goal state after:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      f (x_1 ^ (x.lcm y).factorization x_1) * f (x_1 ^ (x.gcd y).factorization x_1) =
    ∏ x_1 ∈ x.primeFactors ∪ y.primeFactors, f (x_1 ^ x.factorization x_1) * f (x_1 ^ y.factorization x_1)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h✝ : mk a < mk b
hpos : 1 ≤ a
h : |b|ₘ ^ 1 < |a|ₘ
⊢ b < a

Tactic:
rw [pow_one, mabs_lt, mabs_eq_self.mpr hpos] at h

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h✝ : mk a < mk b
hpos : 1 ≤ a
h : a⁻¹ < b ∧ b < 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 b : M
inst✝ : MulArchimedean M
ha : a ≠ 1
hb : b ≠ 1
⊢ mk a = mk b

Tactic:
obtain hm := MulArchimedean.arch |b|ₘ (show 1 < |a|ₘ by simpa using ha)
  obtain hn := MulArchimedean.arch |a|ₘ (show 1 < |b|ₘ by simpa using hb)
  exact mk_eq_mk.mpr ⟨hm, hn⟩

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊

Tactic:
exact le_floor hba

Goal state after:
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 ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

Tactic:
by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Subgroup.zpowers g2 = ⊥
⊢ g1 = g2

pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ g1 = g2

Tactic:
· rw [h'] at h
    simp_all only [Subgroup.zpowers_eq_bot]

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ g1 = g2
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

pp: case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ↑⊥ = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

Tactic:
· simp only [coe_coe, NonemptyInterval.coe_def]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ↑⊥ = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑(a✝¹ * a✝) = ↑1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
Interval.coe_inj,

Goal state after:
case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ a✝¹ * a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2).IsPWO

Tactic:
refine Set.IsPWO.mono x.isPWO_support' ?_
      simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]
      exact fun _ ↦ ne_zero_of_coeff_ne_zero

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ f = coeff 0 ↔ f = 0

Tactic:
funext_iff,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ (∀ (x : Γ), f x = coeff 0 x) ↔ ∀ (x : Γ), f x = 0 x
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
· refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ x.orderTop < i ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0

Tactic:
rw [← not_le, le_orderTop_iff_forall]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ (¬∀ (j : Γ), ↑j < i → x.coeff j = 0) ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0
Module: Mathlib.Algebra.Order.Monoid.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CommMonoid α
inst✝⁴ : Preorder α
inst✝³ : MulLeftStrictMono α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
x✝¹ x✝ : Lex (α × β)
hxy✝ : x✝¹ ≤ x✝
z : Lex (α × β)
hxy : (ofLex x✝¹).1 = (ofLex x✝).1 ∧ (ofLex x✝¹).2 ≤ (ofLex x✝).2
⊢ (ofLex (x✝¹ * z)).1 = (ofLex (x✝ * z)).1

Tactic:
simp only [ofLex_mul, fst_mul, hxy.1]

Goal state after: