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

Goal state before:
pp: case right
ι : 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
rw [← add_halves ε]

Goal state after:
case right
ι : 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
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}
h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε / 2 + ε / 2}
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ ↑l.val + ↑m = l

Tactic:
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Tactic:
by
  grw [← sum_condensed_le' hf n]
  simp [sum_range_succ', add_comm, pow_succ', mul_nsmul', sum_nsmul]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_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
⊢ 1 ≤ d

Tactic:
rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra

Tactic:
by
  apply_fun AddMonoidAlgebra.toDirectSum
  · simp
  · apply Function.LeftInverse.injective
    apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

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

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ 0! = ∏ x ∈ s, (Pi.single a n x)!

Tactic:
eq_comm,

Goal state after:
case neg
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∉ s
⊢ ∏ x ∈ s, (Pi.single a n x)! = 0!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ i ∈ f.support, (f i)! = ∏ i ∈ s, (f i)!

Tactic:
Finset.prod_subset h

Goal state after:
case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∏ x ∈ s, (f x)! = ∏ i ∈ s, (f i)!

case e_a
α : Type u_1
f : α →₀ ℕ
s : Finset α
h : f.support ⊆ s
⊢ ∀ x ∈ s, x ∉ f.support → (f x)! = 1
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
nth_rewrite 1 [← hp]
      nth_rewrite 1 [← hq]
      simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]
      simp only [← mul_assoc, mul_comm _ (X i)]
      simp only [mul_assoc, ← mul_add (X i)]
      apply dvd_mul_right

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:
by simp [expand, map_bind₁]

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

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ r ∣ (monomial (n - m)) 1 * q

Tactic:
apply dvd_mul_of_dvd_right hrq

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

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p

Tactic:
apply induction_on p

Goal state after:
case C
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (C a)) =
      eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (C a)

case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)
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 (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x

Tactic:
eq_comm,

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) * (x + m.sum).choose x =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      m.multinomial ^ (k + 1)

Tactic:
pow_succ'

Goal state after:
case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
Module: Mathlib.Data.DFinsupp.WellFounded

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

Tactic:
hr j h₂,

Goal state after:
case pos
ι : 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)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ x₁ j = if j ∈ p then x₁ j else x₂ j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : 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)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j

Tactic:
hr j h₂,

Goal state after:
case pos
ι : 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)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = if j ∈ p then x₁ j else x₂ j
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (p ^ n) = n * degreeOf i p

Tactic:
by
  rw [pow_eq_prod_const, degreeOf_prod_eq (range n) (fun _ ↦ p) (fun _ _ ↦ hp)]
  simp

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
k : ¬degree (ofDegLex x) < degree (ofDegLex 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:
simp only [h, k, false_or]

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

Goal state before:
pp: α : Type u_1
⊢ degLex.toSyn (single 1 1) < degLex.toSyn (single 0 1)

Tactic:
by
  rw [degLex_lt_iff, single_lt_iff]
  exact Nat.one_pos

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
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ 0 ≤ m.toSyn d ∧ ¬0 = m.toSyn d

Tactic:
eq_comm,

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ 0 ≤ m.toSyn d ∧ ¬m.toSyn d = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ Prime d

Tactic:
rw [h] at this

Goal state after:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp n.minSqFac
⊢ d * d ∣ n

Tactic:
rw [h] at this

Goal state after:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m

Tactic:
rw [h] at this

Goal state after:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m
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
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : f ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
rw [← m.leadingCoeff_ne_zero_iff, ← mem_nonZeroDivisors_iff_ne_zero] at hf

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : m.leadingCoeff f ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
⊢ r • 0 = 0

Tactic:
ext
    simp only [smul_apply, sum_const_zero, smul_zero, zero_apply]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ b.1 * (b.2 / g) = b.1 * b.2 / b.1.gcd b.2

Tactic:
Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ b.1 * (b.2 / g) = b.1 * (b.2 / b.1.gcd b.2)
Module: Mathlib.Algebra.Order.Archimedean.Hom

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : α →+*o α
x : α
⊢ f x = x

Tactic:
f.eq_id

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : α →+*o α
x : α
⊢ (OrderRingHom.id α) x = x
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun x ↦ a) k = Nat.card ↑s • a

Tactic:
have key : ∀ x ∈ hs.toFinset, s.indicator (fun _ ↦ a) x = a := by
    intro x hx
    rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]
  rw [Nat.card_eq_card_finite_toFinset hs, ← sum_eq_card_nsmul key, eventually_atTop]
  obtain ⟨m, hm⟩ := hs.bddAbove
  refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩ <;> intro x <;> rw [hs.mem_toFinset]
  · rw [Finset.mem_range]
    exact fun x_s ↦ ((mem_upperBounds.1 hm) x x_s).trans_lt (Nat.lt_of_succ_le n_m)
  · exact fun _ x_s ↦ indicator_of_notMem x_s (fun _ ↦ a)

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : ↑q < ↑q'
hqa' : ↑q' < a
⊢ ↑q * ↑q < a * a

Tactic:
exact mul_self_lt_mul_self (mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)

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

Goal state before:
pp: case e_a
σ : 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
⊢ ∀ x ∈ B, coeff (m.degree (g x)) (g x) = coeff (m.degree (g b)) (g x)

Tactic:
intro b' hb'

Goal state after:
case e_a
σ : 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
b' : ι
hb' : b' ∈ B
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')
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
⊢ ∀ x ∈ B, g x - (m.leadingCoeff (g x) * ↑isunit_gb.unit⁻¹) • g b = ↑isunit_gb.unit⁻¹ • m.sPolynomial (g x) (g b)

Tactic:
intro b' hb'

Goal state after:
σ : 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
b' : ι
hb' : b' ∈ B
⊢ g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b = ↑isunit_gb.unit⁻¹ • m.sPolynomial (g b') (g b)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i - C r)

Tactic:
rw [sub_eq_add_neg, ← map_neg]
  apply monic_X_add_C

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

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✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
  rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
  exact sum_le_card_nsmul _ _ _ fun n _ ↦
    hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

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 : M
⊢ ⊤ = mk a ↔ a = 1

Tactic:
eq_comm,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
⊢ mk a = ⊤ ↔ a = 1
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ mk ⊤.out = ⊤

Tactic:
mk_out

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ ⊤ = ⊤
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
h : ∃ i ∈ ↑s, ∃ j ∈ ↑s, (g ∘ ⇑σ) i < (g ∘ ⇑σ) j ∧ f j < f i
⊢ ¬∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i

Tactic:
obtain ⟨x, hx, y, hy, hgxy, hfxy⟩ := h

Goal state after:
ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
⊢ ¬∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case e'_7
ι : 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
⊢ g = g ∘ id

Tactic:
comp_id

Goal state after:
case e'_7
ι : 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
⊢ g = g
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case e'_6
ι : 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
⊢ f = f ∘ id

Tactic:
comp_id

Goal state after:
case e'_6
ι : 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
⊢ f = f
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ a', a' < a ∧ c < a' * b

Tactic:
by
  obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul.2 hc)
  exact ⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩

Goal state after: