mathlib-initiative/mathlib-tactics huggingface dataset:
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 ε'
⊢ ∀ (x : TaggedPrepartition I),
    (∃ c, l.MemBaseSet I c (δ c) x ∧ x.IsPartition) → integralSum f vol x ∈ Metric.closedBall (g I) ε

Tactic:
rintro π ⟨c, hπδ, hπp⟩

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥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
⊢ integralSum f vol π ∈ Metric.closedBall (g I) ε
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ (bind₁ fun i ↦ X i ^ p) ((monomial d) r) = (monomial (p • d)) r

Tactic:
bind₁_monomial,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ C r * ∏ i ∈ d.support, (X i ^ p) ^ d i = (monomial (p • d)) r
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
| ∑ k ∈ s.sym n, ↑(↑k).countPerms * (Multiset.map x ↑k).prod

Tactic:
← sum_coe_sort

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
| ∑ i, ↑(↑↑i).countPerms * (Multiset.map x ↑↑i).prod
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ ⊥ ↔ ∀ (x : σ), d x = 0

Tactic:
← eq_bot_iff,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = ⊥ ↔ ∀ (x : σ), d x = 0
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 = 0 ↔ f.totalDegree = 0

Tactic:
rw [← m.toSyn.injective.eq_iff]
  rw [map_zero, ← m.bot_eq_zero, eq_bot_iff, m.bot_eq_zero, ← m.toSyn.map_zero]
  rw [degree_le_iff]
  rw [totalDegree_eq_zero_iff]
  apply forall_congr'
  intro d
  apply imp_congr (rfl.to_iff)
  rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]
  simp only [EmbeddingLike.map_eq_zero_iff]
  exact Finsupp.ext_iff

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

Tactic:
rw [add_comm]
  exact degree_add_of_lt h

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

Tactic:
simp [withBotDegree_eq, h]

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

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

Tactic:
simp [withBotDegree_eq, h]

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
h : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
· simp [h, m.withBotDegree_eq]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ normalizedFactors ?m.423

Tactic:
← Multiset.mem_toFinset

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ (normalizedFactors ?m.423).toFinset
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors ?m.439

Tactic:
← Multiset.mem_toFinset

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ (normalizedFactors ?m.439).toFinset
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h

Goal state after:
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
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:
← k.prod_primeFactors_dvd,

Goal state after:
case refine_2
n k : ℕ
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ ∏ p ∈ n.primeFactors, p ∣ ∏ p ∈ k.primeFactors, p
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
inst✝¹ : Field α
inst✝ : LinearOrder α
a : α
⊢ cutMap α a = Iio a ∩ range Rat.cast

Tactic:
grind [mem_cutMap_iff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ #s • ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
exact hfg.card_smul_sum_le_sum_smul_sum

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
⊢ a ≤ b ∨ b ≤ a

Tactic:
obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
    · exact .inr ⟨1, by simpa using hab⟩
    · exact .inl ⟨1, by simpa using hab⟩

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

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

pp: case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
· have : i + 1 = i := by
      have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
      exact le_antisymm (hi h) h
    simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]
    apply le_trans (le_partialSups _ _) le_sup_right

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
h : mk (a i) = mk (a (s.min' hs))
⊢ False

Tactic:
obtain eq := hmono.injOn (by simp) hminmem h

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
h : mk (a i) = mk (a (s.min' hs))
eq : i = s.min' hs
⊢ False
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : 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
⊢ ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s

Tactic:
classical
  refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm <| by
    simpa using h.sum_smul_comp_perm_le_sum_smul ((set_support_symm_eq _).subset.trans hσ)⟩
  rw [MonovaryOn] at h
  push Not at h
  obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h
  set τ : Perm ι := (Equiv.swap x y).trans σ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    refine (set_support_mul_subset σ <| swap x y).trans (Set.union_subset hσ fun z hz ↦ ?_)
    obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption
  refine ((hfg.sum_smul_comp_perm_le_sum_smul hτs).trans_lt' ?_).ne
  obtain rfl | hxy := eq_or_ne x y
  · cases lt_irrefl _ hfxy
  simp only [τ, ← s.sum_erase_add _ hx,
    ← (s.erase x).sum_erase_add _ (mem_erase.2 ⟨hxy.symm, hy⟩),
    add_assoc, Equiv.coe_trans, Function.comp_apply, swap_apply_right, swap_apply_left]
  refine add_lt_add_of_le_of_lt (Finset.sum_congr rfl fun z hz ↦ ?_).le
    (smul_add_smul_lt_smul_add_smul hfxy hgxy)
  simp_rw [mem_erase] at hz
  rw [swap_apply_of_ne_of_ne hz.2.1 hz.1]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ mk (f a) = mk (f b) → mk a = mk b

Tactic:
mk_eq_mk,

Goal state after:
case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ ((∃ m, |f b|ₘ ≤ |f a|ₘ ^ m) ∧ ∃ n, |f a|ₘ ≤ |f b|ₘ ^ n) → (∃ m, |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ n, |a|ₘ ≤ |b|ₘ ^ n
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✝ : Nontrivial M
⊢ Nonempty (FiniteMulArchimedeanClass M)

Tactic:
by
  obtain ⟨x, hx⟩ := exists_ne (1 : M)
  exact ⟨mk x hx, by simpa using hx⟩

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
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ MulArchimedeanClass.mk a = ⊤

Tactic:
by apply hb ▸ h'

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

Goal state before:
pp: case top.top
⊢ ⊤ ≤ ⌊∞⌋ₑ ↔ ↑⊤ ≤ ∞

Tactic:
simp [Nat.le_floor_iff]

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

Goal state before:
pp: case top.coe
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊∞⌋ₑ ↔ ↑↑a✝ ≤ ∞

Tactic:
simp [Nat.le_floor_iff]

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

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
⊢ ⊤ ≤ ⌊↑x✝⌋ₑ ↔ ↑⊤ ≤ ↑x✝

Tactic:
simp [Nat.le_floor_iff]

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

Goal state before:
pp: case coe.coe
x✝ : ℝ≥0
a✝ : ℕ
⊢ ↑a✝ ≤ ⌊↑x✝⌋ₑ ↔ ↑↑a✝ ≤ ↑x✝

Tactic:
simp [Nat.le_floor_iff]

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

Goal state before:
pp: case coe
n : ℕ
hn₀ : ↑n ≠ 0
x✝ : ℝ≥0
⊢ ↑n ≤ ⌈↑x✝⌉ₑ ↔ ↑↑n - 1 < ↑x✝

Tactic:
simp only [ne_eq, Nat.cast_eq_zero, ceil_coe, Nat.cast_le, toENNReal_coe] at hn₀ ⊢
    norm_cast
    rw [← Nat.add_one_le_ceil_iff, Nat.sub_add_cancel]
    lia

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
x✝ : ℝ≥0∞
⊢ x✝ ≤ ↑(⨅ i, f i) ↔ x✝ ≤ ⨅ i, ↑(f i)

Tactic:
by simp [← ceil_le]

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 → c ≤ a' * b'
⊢ c ≤ a * b

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

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I ↔ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ I}) x}

Tactic:
simp only [mem_closure'', SetLike.setOfPred_mem_eq, SetLike.mem_coe, Set.mem_ofPred_eq]

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I ↔ ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ mk (k • a) = mk a

Tactic:
mk_eq_mk,

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ (∃ m, |a| ≤ m • |k • a|) ∧ ∃ n, |k • a| ≤ n • |a|
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b

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

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

Tactic:
by
    refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
    exact mul_inv_rev _ _

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

Goal state before:
pp: case inr.mpr.refine_2
Γ : 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
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ |(ofLex y).leadingCoeff| < (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
refine lt_of_le_of_lt hn <| nsmul_lt_nsmul_left ?_ (by simp)

Goal state after:
case inr.mpr.refine_2
Γ : 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
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ 0 < |(ofLex x).leadingCoeff|
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb : b ∈ VAddAntidiagonal a ⋯ \ VAddAntidiagonal a ⋯
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0

Tactic:
simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧ ((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (((of R).symm y).coeff b.2 ≠ 0 ∧ b.1 +ᵥ b.2 = a → x.coeff b.1 = 0)
⊢ x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
⊢ mk x + mk y = mk y + mk x

Tactic:
rw [← mk_mul, mul_comm, mk_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
f_zero : f 0 = 0
f_nonneg : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
g : β → α
t : Finset β
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i)

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht
  · simp [f_zero, f_nonneg]
  · exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <|
      IsNonarchimedean.finset_image_add_of_nonempty hna g ht

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✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ x * (y + z) = x * y + x * z

Tactic:
simp only [← of_symm_smul_of_eq_mul]
    exact HahnModule.smul_add x y z

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
⊢ ∃ t, t.card = s.card - m ∧ (∀ x ∈ t, x ∈ s) ∧ f (map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod

Tactic:
set g := fun t : Multiset α ↦ t.prod
  obtain ⟨b, hb_in, hb_le⟩ := hf_na.multiset_image_add g (powersetCard (card s - m) s)
  have hb : b ≤ s ∧ card b = card s - m := by
    rw [← mem_powersetCard]
    exact hb_in (card_pos.mp
      (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))
  exact ⟨b, hb.2, fun x hx ↦ mem_of_le hb.left hx, hb_le⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Finset β
b : β → α
m : ℕ
g : Finset β → α := fun t ↦ ∏ i ∈ t, -b i
⊢ ∃ u, f ((powersetCard (#s - m) s).sum g) ≤ f (∏ i ∈ ↑u, -b i)

Tactic:
obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add (by grind) (apply_nonneg f)
    g (powersetCard (s.card - m) s)

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Finset β
b✝ : β → α
m : ℕ
g : Finset β → α := fun t ↦ ∏ i ∈ t, -b✝ i
b : Finset β
hb_in : (powersetCard (#s - m) s).Nonempty → b ∈ powersetCard (#s - m) s
hb : f ((powersetCard (#s - m) s).sum g) ≤ f (g b)
⊢ ∃ u, f ((powersetCard (#s - m) s).sum g) ≤ f (∏ i ∈ ↑u, -b✝ i)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
⊢ 0 ≤ mk ↑n

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp
  · rw [mk_intCast hn]

Goal state after: