mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace

Goal state before:
pp: p : ℝ≥0∞
X✝ : Type u_1
inst✝⁵ : MeasurableSpace X✝
ι : Type u_2
X : ι → Type u_3
inst✝⁴ : Countable ι
inst✝³ : (i : ι) → MeasurableSpace (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), BorelSpace (X i)
inst✝ : ∀ (i : ι), SecondCountableTopology (X i)
⊢ WithLp.measurableSpace p ((i : ι) → X i) = borel (PiLp p X)

Tactic:
topologicalSpace,

Goal state after:
p : ℝ≥0∞
X✝ : Type u_1
inst✝⁵ : MeasurableSpace X✝
ι : Type u_2
X : ι → Type u_3
inst✝⁴ : Countable ι
inst✝³ : (i : ι) → MeasurableSpace (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), BorelSpace (X i)
inst✝ : ∀ (i : ι), SecondCountableTopology (X i)
⊢ WithLp.measurableSpace p ((i : ι) → X i) = borel (PiLp p X)
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
⊢ volume = map (fun x ↦ x • v) (map (fun x ↦ ‖v‖⁻¹ • x) volume)

Tactic:
let f : ℝ ≃ₗᵢ[ℝ] E := (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v)
      (by simp [norm_smul, hv])).trans (LinearIsometryEquiv.ofTop E _ hv')

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯).trans (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ volume = map (fun x ↦ x • v) (map (fun x ↦ ‖v‖⁻¹ • x) volume)
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun.symm ⁻¹' s) = volume s / ENNReal.ofReal (covolume L volume)

Tactic:
Measure.addHaar_preimage_linearEquiv,

Goal state after:
ι : Type u_2
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ ENNReal.ofReal |LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun.symm.symm| * volume s =
    volume s / ENNReal.ofReal (covolume L volume)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
by
  have hnorm : Tendsto (fun n : ℕ ↦ ‖(n : ℝ)‖) atTop atTop :=
    tendsto_natCast_atTop_atTop.congr' (by simp)
  have h_abs : (fun n : ℕ ↦ |n + a|) ~[atTop] (·) := by
    apply (IsEquivalent.refl.add_const_of_norm_tendsto_atTop hnorm).congr_left
    · filter_upwards [eventually_gt_atTop (Nat.ceil |a|)] with _ hn
      rw [abs_of_pos]
      linarith [lt_of_abs_lt ((abs_neg a).symm ▸ Nat.lt_of_ceil_lt hn)]
  rw [← summable_one_div_nat_rpow, Asymptotics.IsEquivalent.summable_iff_nat]
  simpa [one_div] using! (IsEquivalent.rpow (fun n ↦ by positivity) h_abs).inv

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
x : α
inst✝ : RCLike α
q k : ℕ
hq : 1 < q
⊢ Summable fun n ↦ ‖x / (↑n + ↑k) ^ q‖

Tactic:
by
  simp_rw [norm_div]
  apply Summable.const_div
  simpa [hq, Nat.cast_add, one_div, norm_inv, norm_pow, RCLike.norm_natCast,
    Real.summable_nat_pow_inv, iff_true]
      using summable_nat_add_iff (f := fun x => ‖1 / (x ^ q : α)‖) k

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
n : ℕ
h : l₁.length ≤ n
⊢ (l₁ ++ l₂).getD n 0 = l₁.getD n 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n

Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩

Goal state after:
case inr
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ (l₁ ++ l₂).getD (l₁.length + k) 0 =
    l₁.getD (l₁.length + k) 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) (l₁.length + 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
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
x : E
⊢ Summable fun z ↦ ‖↑z - x‖ ^ r

Tactic:
cases subsingleton_or_nontrivial L
  · exact .of_finite
  refine Summable.of_norm_bounded_eventually
    (.mul_left ((1 / 2) ^ r) (summable_norm_rpow L r hr)) ?_
  have H : IsClosed (X := E) L := @AddSubgroup.isClosed_of_discrete _ _ _ _ _
    L.toAddSubgroup (inferInstanceAs (DiscreteTopology L))
  refine ((Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
    (Metric.isBounded_closedBall (x := (0 : E)) (r := 2 * ‖x‖)) H).preimage_embedding
    (.subtype _)).subset ?_
  intro t ht
  by_cases ht₁ : ‖t‖ = 0
  · simp [show t = 0 by simpa using ht₁]
  by_cases ht₂ : ‖t - x‖ = 0
  · simpa [show t = x by simpa [sub_eq_zero] using ht₂, two_mul] using t.2
  have : 0 < Module.finrank ℤ L := Module.finrank_pos
  have : ‖t - x‖ < 2⁻¹ * ‖t‖ := by
    rw [← Real.rpow_lt_rpow_iff_of_neg (by positivity) (by positivity) (hr.trans (by simpa))]
    simpa [Real.mul_rpow, abs_eq_self.mpr (show 0 ≤ ‖t - x‖ ^ r by positivity)] using ht
  have := (norm_sub_norm_le _ _).trans_lt this
  rw [sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', AddSubgroupClass.coe_norm] at this
  simpa using show ‖t.1‖ ≤ 2 * ‖x‖ by linarith

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬s.support ⊆ a.support
⊢ 0 = ↑s.multinomial * s.prod fun r m ↦ a r ^ m

Tactic:
Finset.subset_iff

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬∀ ⦃x : σ⦄, x ∈ s.support → x ∈ a.support
⊢ 0 = ↑s.multinomial * s.prod fun r m ↦ a r ^ m
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case hb
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (Box.Icc I)
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ
hC : f '' Box.Icc I ⊆ C • Metric.closedBall 0 1
⊢ ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C

Tactic:
use ‖C‖, fun x hx ↦ by
      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H : ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i ((rename ⇑f) P))
i : Fin n →₀ ℕ
⊢ IsNilpotent (coeff i P)

Tactic:
by simpa using H (i.embDomain f)

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

Goal state before:
pp: case cons.e_a.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ f✝ t ^ (f t + if t = a then p.1 else 0) = f✝ t ^ f t

Tactic:
rw [if_neg, add_zero]

Goal state after:
case cons.e_a.e_a.hnc
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
t : α
ht : t ∈ s
⊢ ¬t = a
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.succ.refine_1.inl
σ : 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
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
hp✝ : p ∣ (monomial n') 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : p = (monomial m) 1 * r
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
exact ⟨m, r, le_trans hm hnn', hr, hp⟩

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p

pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p

Tactic:
· rw [hf, map_zero, totalDegree_zero, zero_mul]

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ (eval x) (Polynomial.eval q ((finSuccEquiv R n) f)) = (eval fun i ↦ Fin.cases ((eval x) q) x i) f

Tactic:
simp only [finSuccEquiv_apply, coe_eval₂Hom, polynomial_eval_eval₂, eval_eval₂]

Goal state after:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
⊢ eval₂ ((eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C)))
      (fun s ↦ (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) s))) f =
    (eval fun i ↦ Fin.cases ((eval x) q) x i) f
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
⊢ {n}.multinomial = 1

Tactic:
by
  simp [← cons_zero, multinomial_cons]

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

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k

Tactic:
by
  induction k with
  | zero => simp
  | succ k hk =>
    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring

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 : MvPolynomial σ R
hmn : m ≤ n
hr : ∃ b, b ∣ a ∧ r = C b
h : p = (monomial m) 1 * r
⊢ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

Tactic:
obtain ⟨b, hb, hr⟩ := hr

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
h : p = (monomial m) 1 * r
b : R
hb : b ∣ a
hr : r = C b
⊢ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b
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 1 = 0

Tactic:
degree_one

Goal state after:
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
⊢ 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
hp : p ≠ 0
⊢ (m.leadingTerm p).support = {m.degree p}

Tactic:
by
  classical
  simp [leadingTerm, support_monomial, hp]

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

Goal state before:
pp: case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors (a * b) ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
Multiset.toFinset_val,

Goal state after:
case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors (a * b) ∧ (normalizedFactors a).dedup.prod = a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f - g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
by
  rw [sub_eq_add_neg]
  apply le_of_le_of_eq m.degree_add_le
  rw [degree_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
by_cases hn0 : n = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ C (m.leadingCoeff g) * C (m.leadingCoeff f) - C (m.leadingCoeff f) * g = 0

Tactic:
degree_eq_zero_iff.mp h₂

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ C (m.leadingCoeff g) * C (m.leadingCoeff f) - C (m.leadingCoeff f) * C (m.leadingCoeff g) = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case succ
n a b : ℕ
h₁ : b ^ 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
exact ⟨a, b, h₁, h₂⟩

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

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

Tactic:
by_cases hn0 : n = 0

Goal state after:
case pos
k n : ℕ
hn0 : n = 0
⊢ (σ k) n = 1 ↔ n = 1

case neg
k n : ℕ
hn0 : ¬n = 0
⊢ (σ k) n = 1 ↔ n = 1
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 c : MulArchimedeanOrder M
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
intro ⟨m, hm⟩

Goal state after:
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 c : MulArchimedeanOrder M
m : ℕ
hm : |val b|ₘ ≤ |val a|ₘ ^ m
⊢ b ≤ c → a ≤ c
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 : ι → α
⊢ (∑ i ∈ s, f i) ^ 2 ≤ ↑(#s) * ∑ i ∈ s, f i ^ 2

Tactic:
simp_rw [sq]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ x ∈ s, f x * f x
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

Tactic:
rw [max_eq_right h, min_eq_right, mk_mabs]

Goal state after:
case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ mk z ≤ mk y
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_3
ι : 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)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : x ∈ s.erase ((Equiv.symm σ) a)
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))

Tactic:
rw [mem_erase, Ne, eq_symm_apply] at hx
    rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
    rintro rfl
    exact has hx.2

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
⊢ subgroup ⊤ = ⊥

Tactic:
ext; simp [subgroup, MulArchimedeanClass.subsemigroup, toUpperSetMulArchimedeanClass]

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

Goal state before:
pp: r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌈r⌉ₑ ≤ ⌈s⌉ₑ

Tactic:
by simpa using hrs.trans le_ceil_self

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

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

Tactic:
rw [Subgroup.zpowers_one_eq_bot] at ha

Goal state after:
case inr.inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
ha : ⊥ = H
⊢ ∃ a < 1, Subgroup.zpowers a = H
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: case refine_2
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
this : n • |a| = (n • 1) • |a|
⊢ |k| • |a| ≤ (n • 1) • |a|

Tactic:
exact smul_le_smul_of_nonneg_right hn (by simp)

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
s : UpperSet (FiniteArchimedeanClass M)
k : K
a : M
ha : a ∈ (addSubgroup s).carrier
ne : ArchimedeanClass.mk (k • a) ≠ ⊤
eq : ArchimedeanClass.mk a = ⊤
⊢ ArchimedeanClass.mk (k • a) = ⊤

Tactic:
simp [ArchimedeanClass.mk_eq_top_iff.mp eq]

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:
refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
    exact mul_inv_rev _ _

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
dif_pos (Set.mem_image_of_mem f ha)

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a
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 : R⟦Γ⟧
⊢ (embDomain f x).support ⊆ ⇑f '' x.support

Tactic:
intro g hg

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∈ (embDomain f x).support
⊢ g ∈ ⇑f '' x.support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'

Tactic:
intro g hg

Goal state after:
case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
g : Γ
hg : g ∈ (ofLex x).support
⊢ i ≤ g
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ x * ⊥ = ⊥

Tactic:
by
  rw [← sSup_empty, mul_sSup_distrib]
  simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔ A.valuation ↑a < 1

Tactic:
rw [valuation_eq_one_iff]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬A.valuation ↑a = 1 ↔ A.valuation ↑a < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Ideal.comap (A.inclusion ⊤ ⋯) (IsLocalRing.maximalIdeal ↥⊤) = ⊥

Tactic:
IsLocalRing.maximalIdeal_eq_bot,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Ideal.comap (A.inclusion ⊤ ⋯) ⊥ = ⊥
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a - f b ≤ f (a - b)

Tactic:
rw [tsub_le_iff_right, ← f.map_add]
  exact hf le_tsub_add

Goal state after: