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

Goal state before:
pp: case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
⊢ dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ

Tactic:
have hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ := fun J hJ => hgi.mono_set (π.le_of_mem' J hJ)

Goal state after:
case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi✝ : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ
⊢ dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |(Matrix.of (Subtype.val ∘ ⇑b₁)).det| / covolume L₂ volume =
    |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)).det⁻¹| * |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det|

Tactic:
covolume_eq_det _ b₂,

Goal state after:
ι : Type u_2
inst✝⁴ : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst✝³ : DiscreteTopology ↥L₁
inst✝² : IsZLattice ℝ L₁
inst✝¹ : DiscreteTopology ↥L₂
inst✝ : IsZLattice ℝ L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ |(Matrix.of (Subtype.val ∘ ⇑b₁)).det| / |(Matrix.of (Subtype.val ∘ ⇑b₂)).det| =
    |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₂ b₂)).det⁻¹| * |(Matrix.of ⇑(Basis.ofZLatticeBasis ℝ L₁ b₁)).det|
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ (fun n ↦ ∑ i ∈ Finset.range n, f i) =o[atTop] fun n ↦ ↑n

Tactic:
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
  simp only [sum_const, card_range, Nat.smul_one_eq_cast] at this
  exact this tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ∞
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞

Tactic:
replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
      ENNReal.coe_le_coe.2 (hf hm hmn)
    have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top
    simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict

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

Goal state before:
pp: case pos
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 : d = 0
this : IsEmpty ι
⊢ ∑ p ∈ Fintype.piFinset fun x ↦ Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
    2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
simp [hd, hr'.ne]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: case inj.a
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum

pp: case inj.g
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι

Tactic:
apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
⊢ ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
P

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α β : Type u_1
inst✝ : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ IsNilpotent P ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α : Type u_1
inst✝ : Fintype α
H : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
⊢ ∀ (x : MvPolynomial (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
P

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α : Type u_1
inst✝ : Fintype α
H : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial (Option α) R
⊢ IsNilpotent P ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i P)
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
s : Finset ι
f : ι → R
a : R
⊢ s.sup f * a = s.sup fun x ↦ f x * a

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : MvPolynomial σ R
r : R
⊢ (expand p) f = C r ↔ f = C r

Tactic:
by
  rw [← expand_C, expand_inj hp, expand_C]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
φ : MvPolynomial σ R
⊢ (map f) ((expand p) φ) = (expand p) ((map f) φ)

Tactic:
simp [expand, map_bind₁]

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

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

Tactic:
by
  induction n with
  | zero =>
    apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
    simpa [constantCoeff, coeff] using h 0 finZeroElim
  | succ n ih =>
    apply (finSuccEquiv R n).injective
    rw [map_zero]
    apply Polynomial.eq_zero_of_infinite_isRoot
    apply ((hs 0).image (C_injective ..).injOn).mono
    rintro _ ⟨r, hr, rfl⟩
    refine ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_
    rw [eval_polynomial_eval_finSuccEquiv]
    exact h _ fun i _ ↦ i.cases (by simpa [eval_C] using hr) (by simpa using hx)

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Tactic:
rw [multinomial, multinomial, ← mul_sum,
    ← Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum ..)]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ WellFounded (Function.swap (Function.swap WellOrderingRel))

Tactic:
simp +unfoldPartialApp only [Function.swap]
        exact IsWellFounded.wf

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
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c 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 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
⊢ ∑ J ∈ π.boxes, ε' * B J = B I * ε'

Tactic:
by rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬m i = 0
⊢ m = 0 ∨ m = Finsupp.single i 1

Tactic:
right
      ext j
      apply le_antisymm (hmn j)
      by_cases hj : j = i
      · simpa [hj, Nat.one_le_iff_ne_zero]
      · simp [Finsupp.single_eq_of_ne hj]

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
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.Monic (f + g)

Tactic:
by
  simp only [Monic, leadingCoeff_add_of_lt h, hf.leadingCoeff_eq_one]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
· rw [m.coeff_eq_zero_of_lt hf, zero_mul]

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

Goal state before:
pp: case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (∏ i ∈ insert a s, P i)) ≤ m.toSyn (∑ i ∈ insert a s, m.degree (P i))

Tactic:
Finset.prod_insert has,

Goal state after:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a * ∏ x ∈ s, P x)) ≤ m.toSyn (∑ i ∈ insert a s, m.degree (P i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
leadingTerm_eq_zero_iff

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : ¬g = 0
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + g) = m.degree f → ¬f + g = 0

Tactic:
intro h'

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : ¬g = 0
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
h' : m.degree (f + g) = m.degree f
⊢ ¬f + g = 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ (p ^ k).factorization p = p ^ k

Tactic:
hp.factorization_pow,

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ (Finsupp.single p k) p = p ^ k
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
rcases n with - | n

Goal state after:
case zero
⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a

case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · simp only [ArithmeticFunction.sigma_apply]
    aesop

Goal state after:
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 b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b

Tactic:
refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
apply subset_union_left

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 : K
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋₊

Tactic:
rw [div_eq_inv_mul]

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop

Tactic:
by
  rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]

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

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

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

Goal state before:
pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0} ⊆
    {a | (VAddAntidiagonal a ⋯).Nonempty}

Tactic:
intro a ha

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha : a ∈ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0}
⊢ a ∈ {a | (VAddAntidiagonal a ⋯).Nonempty}
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j

Tactic:
seed.coeff_baseEmbedding hf.symm

Goal state after:
case refine_1
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ (ofLex 0).coeff j = (seed.coeff j) (f j)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ∀ j < f.support.min' hsupport, (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j

pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (ofLex 0).coeff (f.support.min' hsupport) < (ofLex (↑seed.baseEmbedding x)).coeff (f.support.min' hsupport)

Tactic:
· intro j hj
    rw [seed.coeff_baseEmbedding hf.symm]
    rw [DFinsupp.notMem_support_iff.mp ?_]
    · simp
    contrapose! hj
    rw [← Subtype.coe_le_coe, Subtype.coe_mk]
    exact Finset.min'_le f.support _ hj

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (ofLex 0).coeff (f.support.min' hsupport) < (ofLex (↑seed.baseEmbedding x)).coeff (f.support.min' hsupport)