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

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I) μ
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᵐ[μ.restrict ↑I] g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
⊢ HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)

Tactic:
refine BoxIntegral.HasIntegral.congr_ae ?_ hfg.symm hl

Goal state after:
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hf : IntegrableOn f (↑I) μ
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
hfg : f =ᵐ[μ.restrict ↑I] g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi : IntegrableOn g (↑I) μ
⊢ HasIntegral I l g μ.toBoxAdditive.toSMul (∫ (a : ι → ℝ) in ↑I, g a ∂μ)
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
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₀) (𝓝 (∑ J ∈ π₀.boxes, integral J l f vol))

Tactic:
refine ((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_
  refine ⟨h.convergenceR ε, h.convergenceR_cond ε, ?_⟩
  simp only [mem_ofPred_eq]
  rintro π ⟨c, hc, hU⟩
  exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
ENNReal.tsum_eq_iSup_nat' (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)

Goal state after:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ⨆ i, ∑ a ∈ range (2 ^ i), f a ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r : ℝ
hr : r < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
⊢ ∃ n, u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n

Tactic:
obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
r✝ : ℝ
hr✝ : r✝ < -↑d
e : (I → ℤ) ≃ₗ[ℤ] ↥L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I).symm
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : ↑u ⊆ Metric.closedBall 0 r
⊢ ∃ n, u ⊆ Fintype.piFinset fun x ↦ Finset.Icc (-↑n) ↑n
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
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
h✝ : Subsingleton ↥L
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r

Tactic:
exact .of_finite

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (g.comp f) = comap f ∘ comap g

Tactic:
by
  funext x
  exact comap_comp_apply _ _ _

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m ((monomial j) s) = coeff m ((monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩

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
⊢ HasIntegral I l f vol (g I)

Tactic:
refine ((l.hasBasis_toFilteriUnion_top _).tendsto_iff Metric.nhds_basis_closedBall).2 ?_

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
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
⊢ ∀ (ib : ℝ),
    0 < ib →
      ∃ ia,
        (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
          ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ib
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ C r * ∏ i ∈ d.support, (X i ^ p) ^ d i = C r * ∏ x ∈ d.support, X x ^ (p • d) x

pp: case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, X i ^ 0 = 1

Tactic:
· simp [pow_mul]

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, X i ^ 0 = 1
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos.refine_3
ι : 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)
⊢ (x₁.piecewise x {j | r j i}).piecewise x₂ {j | r j i → j ∈ p} = x

Tactic:
· ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₂, if_pos (h₁ h₂)]
      · rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]

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

Goal state before:
pp: case refine_1.inr.refine_2
ι : 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 : 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
hsne : s.Nonempty
this : ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s}, dist ((vol J) (f (π.tag J))) (g J) ≤ εs (π.tag J)
⊢ ↑({J ∈ π.boxes | π.tag J ∈ s}) ⊆ π.tag ⁻¹' s

Tactic:
exact fun J hJ => (Finset.mem_filter.1 hJ).2

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Trichotomous r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Function.onFun (Prod.Lex s (Finsupp.Lex r s)) fun x ↦ (degree x, x))

Tactic:
← Set.wellFoundedOn_range

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Trichotomous r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ (Set.range fun x ↦ (degree x, x)).WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ degreeOf j (C c * p) = degreeOf j p

Tactic:
simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul']
  · simp
  · have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
    simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
    contrapose hp'
    ext m
    apply hc.1
    simpa using congr_arg (coeff m) hp'

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ piFinset s_init

Tactic:
mem_piFinset_iff_last_init,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last (last n) ∈ snoc s_init s_last (last n) ∧
      init (snoc x_init x_last) ∈ piFinset (init (snoc s_init s_last)) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset s_init
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ {r ∈ piFinset S | P (tail r)} = map (consEquiv α).toEmbedding (S 0 ×ˢ {r ∈ piFinset (tail S) | P r})

Tactic:
simp [← map_consEquiv_filter_piFinset, map_map]

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 g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree f) = m.toSyn (m.degree g) ∨ m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
Classical.or_iff_not_imp_left,

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree f) = m.toSyn (m.degree g) → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
by_cases h : f = 0

Goal state after:
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

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
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : (n / k).MinSqFacProp none
⊢ n.MinSqFacProp none

Tactic:
rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢
    exact fun p pp dp => H p pp ((dvd_div_iff_mul_dvd dk).2 (this _ pp dp))

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 : MvPolynomial σ R
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

Tactic:
by_cases h : f = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = 0
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)
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) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

Tactic:
by_cases! hg : g = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
rcases eq_or_ne n 0 with (rfl | hn0)

Goal state after:
case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1

case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
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 =
    ∑ i ∈ (↑n.primeFactorsList).toFinset.powerset, f i.val.prod * g (n / i.val.prod)

Tactic:
apply sum_congr rfl

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors.powerset, (∏ i ∈ x, f i) * ∏ i ∈ n.primeFactors \ x, g i = f x.val.prod * g (n / x.val.prod)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k x✝ : ℕ
⊢ ∑ i ∈ x✝.divisors, (pow k) i = { toFun := fun n ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } x✝

Tactic:
apply sum_congr rfl

Goal state after:
k x✝ : ℕ
⊢ ∀ x ∈ x✝.divisors, (pow k) x = x ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = ∏ p ∈ n.primeFactors, ∑ i ∈ range (n.factorization p + 1), p ^ (i * k)

Tactic:
rw [isMultiplicative_sigma.multiplicative_factorization _ hn]
  exact prod_congr n.support_factorization fun _ h ↦
    sigma_apply_prime_pow <| prime_of_mem_primeFactors h

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✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
q : ℚ
hb : q ∈ {t | ↑t < a * a}
q' : ℚ
hq' : 0 < q'
hqq' : ↑q < ↑q' ^ 2
hqa : ↑q' ^ 2 < a * a
⊢ ↑q ≤ ↑q' ^ 2

Tactic:
exact mod_cast hqq'.le

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

Goal state before:
pp: case insert
ι : 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)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i

Tactic:
set τ : Perm ι := σ.trans (swap a (σ a)) with hτ

Goal state after:
case insert
ι : 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)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0
hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d
⊢ ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

Tactic:
by
  refine m.sPolynomial_decomposition ?_ hfd
  simpa [and_or_right, em']

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

Goal state before:
pp: case e'_8
ι : 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ ↑s = ⇑(Equiv.symm σ) ⁻¹' ↑s

Tactic:
· rw [σ.symm.eq_preimage_iff_image_eq]
      exact Set.image_perm hσinv

Goal state after:
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
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a = mk b
⊢ mk (f a) = mk (f b)

Tactic:
← orderHom_mk,

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a = mk b
⊢ (orderHom f) (mk a) = mk (f b)
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
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a = mk b
⊢ (orderHom f) (mk a) = mk (f b)

Tactic:
← orderHom_mk,

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a = mk b
⊢ (orderHom f) (mk a) = (orderHom f) (mk b)
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
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a ≤ mk b
⊢ mk (f a) ≤ mk (f b)

Tactic:
← orderHom_mk,

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a ≤ mk b
⊢ (orderHom f) (mk a) ≤ mk (f b)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌈r⌉ₑ = 0 ↔ r = 0

Tactic:
by simpa using ceil_le (n := 0)

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

Goal state before:
pp: r : ℝ≥0
⊢ ⌈↑r⌉ₑ ≤ ⌊↑r⌋ₑ + 1

Tactic:
simpa using mod_cast Nat.ceil_le_floor_add_one r

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b

Tactic:
simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
  exact hd.le.trans (h a' ha' b' hb')

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊓ y = ⅟2 • 2 • (x ⊓ y)

Tactic:
two_smul,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊓ y = ⅟2 • (x ⊓ y + x ⊓ y)
Module: Mathlib.Algebra.Order.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • 2 • (x ⊔ y)

Tactic:
two_smul,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • (x ⊔ y + x ⊔ y)