mathlib-initiative/mathlib-tactics huggingface dataset:
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 (ι → ℝ) := ⋯
μ' : Measure (ι → ℝ) := ⋯
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this✝ : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := ⋯
t₂ : Box ι → ι → ℝ := ⋯
B : Finset (Box ι) := ⋯
B' : Finset (Box ι) := ⋯
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
this : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C)
⊢ ∑ J ∈ B', μ ↑J ≤ μ' (⋃ J ∈ B', ↑J)

Tactic:
simp only [μ', μ.restrict_eq_self <| (un _ hB').trans I.coe_subset_Icc]

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)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this✝ : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
this : ∀ J ∈ B', ‖μ.toBoxAdditive J • (f (t₁ J) - f (t₂ J))‖ ≤ μ.toBoxAdditive J * (2 * C)
⊢ ∑ J ∈ B', μ ↑J ≤ μ (⋃ J ∈ B', ↑J)
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ coeff d ((X 0 + X 1) ^ n) = ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)

Tactic:
← Fin.sum_univ_two,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
d : Fin 2 →₀ ℕ
n : ℕ
⊢ coeff d ((∑ i, X i) ^ n) = ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: a b : ℕ
⊢ (![a, b] 0 + ![a, b] 1)! / ((![a, b] 0)! * (![a, b] 1)!) = (a + b)! / (a ! * b !)

Tactic:
dsimp only [Matrix.cons_val]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ (if h : ∃ a, f a = i then x (Classical.choose h) else g i) ∈ s i

Tactic:
dif_neg nex,

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ g i ∈ s i
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x

Tactic:
← Nat.choose_symm (Nat.le_add_right _ _),

Goal state after:
case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i ↦ { zero := ⋯.min ⊤ ⋯ }
this : Fintype ι
i : ι
a : α i
⊢ ¬a < 0

Tactic:
exact (hw i).wf.not_lt_min ⊤ trivial

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
· by_cases k : (ofDegLex x).degree < (ofDegLex y).degree
    · simp [k]
    · simp only [h, k, false_or]

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

Goal state before:
pp: case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) → ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

Tactic:
rintro ⟨r, hmn, hr, h⟩

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : r ∣ C a
h : p = (monomial m) 1 * r
⊢ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : DegLex (α →₀ ℕ)
⊢ toDegLex 0 ≤ x

Tactic:
by
    simp only [le_iff, ofDegLex_toDegLex, toLex_zero, map_zero]
    rcases eq_zero_or_pos (ofDegLex x).degree with (h | h)
    · simp only [h, lt_self_iff_false, true_and, false_or]
      exact bot_le
    · simp [h]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hf : ((↑f).sum fun x x_1 ↦ x_1) = n ∧ (↑f).support ⊆ s
⊢ ((subtypeDomain (fun x ↦ x ∈ s) ↑f).sum fun x ↦ id) = n

Tactic:
simpa [sum, filter_mem_eq_inter, inter_eq_left.mpr hf.2] using hf.1

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

Goal state before:
pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if n✝ + 1 = 0 then ⊤ else ↑(n✝ + 1)

Tactic:
simp only [succ_ne_zero, cast_lt, if_false]

Goal state after:
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
h1 : a + 1 ∣ n✝ + 1
h2 : ¬n✝ + 1 ∣ a + 1
⊢ a + 1 < n✝ + 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
apply m.toSyn.injective
  apply le_antisymm (m.degree_pow_le n)
  apply le_degree
  rw [mem_support_iff, coeff_pow_nsmul_degree]
  exact hf

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
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
rw [hn, pow_zero, degree_one]

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
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
zero_pow hn,

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
simp only [leadingTerm, monomial_eq_zero, leadingCoeff_eq_zero_iff]

Goal state after:
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
⊢ ∀ x_1 ∈ x.val, Irreducible x_1

Tactic:
intro z

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 : ℕ
⊢ z ∈ x.val → Irreducible z
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
⊢ ∀ x ∈ y.val, Irreducible x

Tactic:
intro z

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 : ℕ
⊢ z ∈ y.val → Irreducible z
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
have hs : s ∈ S := Finset.max'_mem S hSne

Goal state after:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
hs : s ∈ S
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ (∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then 0 • f x.2 else f x.2) = ∑ i ∈ x.divisors, f i

Tactic:
simp [← coe_zeta_smul_apply (R := R)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ f.pmul g = g.pmul f

Tactic:
by
  ext
  simp [mul_comm]

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

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

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

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

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

Tactic:
sum_divisors_filter_squarefree hn.ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i =
    ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod * g (n / i.val.prod)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
mem_map,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a ∈ finAntidiagonal d (Additive.ofMul ⟨n, h⟩),
      (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight a = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
⊢ #(n.primeFactors.pi fun x ↦ univ) = #(d.finMulAntidiag n)

Tactic:
by
  apply Finset.card_bij (Nat.primeFactorsPiBij d n) (primeFactorsPiBij_img d n hn)
    (primeFactorsPiBij_inj d n) (primeFactorsPiBij_surj d n hn)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
⊢ #(d.finMulAntidiag n) = d ^ ω n

Tactic:
← card_finMulAntidiag_pi d n hn,

Goal state after:
d n : ℕ
hn : Squarefree n
⊢ #(n.primeFactors.pi fun x ↦ univ) = d ^ ω n
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
⊢ s.Infinite → Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
rw [h_mono.tendsto_atTop_atTop_iff]

Goal state after:
case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
⊢ s.Infinite → ∀ (b : R), ∃ a, b ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

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

Goal state after:
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i

Tactic:
have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _

Goal state after:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε✝ : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
hε : 0 < Finset.univ.inf' ⋯ ε
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
⊢ ∃ y, 1 < y ∧ y ^ (n + 2) < x

Tactic:
by
    obtain ⟨y, hy, hyx⟩ := exists_pow_lt_of_one_lt hx (n + 1)
    obtain ⟨z, hz, hzy⟩ := exists_pow_two_le_of_one_lt hy
    refine ⟨z, hz, hyx.trans_le' ?_⟩
    calc z ^ (n + 2)
      _ ≤ z ^ (2 * (n + 1)) := pow_right_monotone hz.le (by lia)
      _ = (z ^ 2) ^ (n + 1) := by rw [pow_mul]
      _ ≤ y ^ (n + 1) := pow_le_pow_left' hzy (n + 1)

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

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
use a⁻¹, Left.inv_lt_one_iff.mpr ha1
    rw [Subgroup.zpowers_inv, ha]

Goal state after:
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
⊢ mk a ≤ mk (k • a)

Tactic:
obtain rfl | h := eq_or_ne k 0

Goal state after:
case inl
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
⊢ mk a ≤ mk (0 • a)

case inr
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
⊢ mk a ≤ mk (k • a)
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 * (↑x).2

Tactic:
← h

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑x).1 * (↑x).2
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑y).2

Tactic:
← h

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑x).2
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r s : R
rs : (single a) r = (single a) s
⊢ ((single a) r).coeff a = ((single a) s).coeff a

Tactic:
rs

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r s : R
rs : (single a) r = (single a) s
⊢ ((single a) s).coeff a = ((single a) s).coeff a
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
⊢ ((single a) r).map f = (single a) (f r)

Tactic:
ext g

Goal state after:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : embDomain f x = embDomain f y
⊢ x = y

Tactic:
ext g

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : embDomain f x = embDomain f y
g : Γ
⊢ x.coeff g = y.coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
⊢ embDomain f (x + y) = embDomain f x + embDomain f y

Tactic:
ext g

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
⊢ embDomain f (r • x) = r • embDomain f x

Tactic:
ext g

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x ∈ Ico 0 ↑b ↔ x ∈ {0}

Tactic:
simp only [mem_Ico, mem_singleton]

Goal state after:
case h
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ 0 ≤ x ∧ x < ↑b ↔ x = 0