mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
⊢ Tendsto (fun c ↦ ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) atTop
    (𝓝 (volume.real (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})))

Tactic:
refine Tendsto.congr' ?_ <| (tendsto_card_div_pow_atTop_volume'
      ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1}) ?_ ?_ h₄ fun x y hx hy ↦ ?_).comp
        (tendsto_rpow_atTop <| inv_pos.mpr
          (Nat.cast_pos.mpr card_pos) : Tendsto (fun x ↦ x ^ (card ι : ℝ)⁻¹) atTop atTop)
  · filter_upwards [eventually_gt_atTop 0] with c hc
    have aux₁ : (card ι : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr card_ne_zero
    have aux₂ : 0 < c ^ (card ι : ℝ)⁻¹ := Real.rpow_pos_of_pos hc _
    have aux₃ : (c ^ (card ι : ℝ)⁻¹)⁻¹ ≠ 0 := inv_ne_zero aux₂.ne'
    have aux₄ : c ^ (-(card ι : ℝ)⁻¹) ≠ 0 := (Real.rpow_pos_of_pos hc _).ne'
    obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc
    rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ aux₁, eq_comm]
    congr
    refine Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
          (Equiv.smulRight aux₄)) fun _ ↦ ?_
    rw [Set.mem_inter_iff, Set.mem_inter_iff, Equiv.trans_apply, LinearEquiv.coe_toEquiv,
      Equiv.smulRight_apply, Real.rpow_neg hc₁, Set.smul_mem_smul_set_iff₀ aux₃,
      ← Set.mem_smul_set_iff_inv_smul_mem₀ aux₂.ne', ← image_smul_set,
      tendsto_card_le_div''_aux hX h₁ aux₂, ← Real.rpow_natCast, ← Real.rpow_mul hc₁,
      inv_mul_cancel₀ aux₁, Real.rpow_one]
    simp_rw [SetLike.mem_coe, Set.mem_image, EmbeddingLike.apply_eq_iff_eq, exists_eq_right,
      and_congr_right_iff, ← b.ofZLatticeBasis_span ℝ, Basis.mem_span_iff_repr_mem,
      Pi.basisFun_repr, Basis.equivFun_apply, implies_true]
  · rw [← NormedSpace.isVonNBounded_iff ℝ] at h₂ ⊢
    exact Bornology.IsVonNBounded.image h₂ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr h₃
  · simp_rw [← image_smul_set]
    apply Set.image_mono
    rw [tendsto_card_le_div''_aux hX h₁ hx,
      tendsto_card_le_div''_aux hX h₁ (lt_of_lt_of_le hx hy)]
    exact fun a ⟨ha₁, ha₂⟩ ↦ ⟨ha₁, le_trans ha₂ <| pow_le_pow_left₀ (le_of_lt hx) hy _⟩

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

Goal state before:
pp: case h
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 : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
hk : k ∈ range n
v : ι → ℤ
hv : v ∈ s (k + 1) \ s k
⊢ ‖∑ i, v i • b i‖ ^ r ≤ ((↑k + ↑1) * ε) ^ r

Tactic:
← Nat.cast_add

Goal state after:
case h
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 : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
hk : k ∈ range n
v : ι → ℤ
hv : v ∈ s (k + 1) \ s k
⊢ ‖∑ i, v i • b i‖ ^ r ≤ (↑(k + 1) * ε) ^ r
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
sum_pi_single'

Goal state after:
α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
⊢ (if a ∈ s then n else 0)! = ∏ x ∈ s, (Pi.single a n x)!
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ coeff d ((∑ i, X i) ^ n) = ↑(if (d.sum fun x m ↦ m) = n then d.multinomial else 0)

Tactic:
by
  have : (∑ i, X i : MvPolynomial σ R) = ∑ i, (1 : σ → R) i • X i := by simp
  simp [this, coeff_linearCombination_X_pow_of_fintype]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (expand p) ((bind₁ f) φ) = (bind₁ fun i ↦ (expand p) (f i)) φ

Tactic:
rw [← AlgHom.comp_apply, expand_comp_bind₁]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
← Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum ..)

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
refine Acc.intro _ fun h => ?_

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
h : α × β
⊢ Prod.GameAdd rα rβ h (a, b) → Acc (Prod.GameAdd rα rβ) h
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)

Tactic:
| _ i _ ih
   => 

Goal state after:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ (f * r).totalDegree

Tactic:
rw [totalDegree_mul_of_isDomain (by aesop) (by aesop)]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ f.totalDegree + r.totalDegree
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
ext d
  simp only [leadingCoeff, hf]
  classical
  by_cases hd : d = 0
  · simp [hd]
  · rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩

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

Tactic:
by
  simp only [leadingCoeff, m.degree_add_of_lt h, coeff_add, coeff_eq_zero_of_lt h, add_zero]

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
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
← not_lt,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → ¬m.toSyn (m.degree f + m.degree g) < m.toSyn c
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
hf : m.leadingCoeff f ∈ R⁰
h0 : f ≠ 0 ∧ g ≠ 0
this : f * g ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
simp [withBotDegree_eq, m.degree_mul_of_left_mem_nonZeroDivisors hf, *]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
s : Finset α
f : α → MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s haA h =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans (m.withBotDegree_add_le _ _) (max_le_max le_rfl h)

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

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
hU : U ∈ F
⊢ U ∈ Filter.map (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite

Tactic:
refine ((((hf hU).image Prod.fst)).add ((hf hU).image Prod.snd)).subset ?_

Goal state after:
M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
hU : U ∈ F
⊢ ((fun a ↦ (antidiagonal a).sup' ⋯ f) ⁻¹' U)ᶜ ⊆ Prod.fst '' (f ⁻¹' U)ᶜ + Prod.snd '' (f ⁻¹' U)ᶜ
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ f a ha ∈
    {x ∈ n.divisors ×ˢ n.divisors |
      match x with
      | (x, y) => x.lcm y = n}

Tactic:
rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors]

Goal state after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (((f a ha).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match f a ha with
    | (x, y) => x.lcm y = n
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
div_le_iff₀' (by positivity)

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)
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
h✝ : mk a < mk b
hpos : 1 ≤ a
h : |a|ₘ⁻¹ < b ∧ b < |a|ₘ
⊢ b < a

Tactic:
mabs_eq_self.mpr hpos

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h✝ : mk a < mk b
hpos : 1 ≤ a
h : a⁻¹ < b ∧ b < a
⊢ b < a
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✝ : MulArchimedean M
ha : a ≠ 1
hb : b ≠ 1
⊢ mk a = mk b

Tactic:
by
  obtain hm := MulArchimedean.arch |b|ₘ (show 1 < |a|ₘ by simpa using ha)
  obtain hn := MulArchimedean.arch |a|ₘ (show 1 < |b|ₘ by simpa using hb)
  exact mk_eq_mk.mpr ⟨hm, hn⟩

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
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
⊢ 1 ∈ (subsemigroup s).carrier

Tactic:
rw [subsemigroup, Set.mem_preimage]

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
s : UpperSet (MulArchimedeanClass M)
hs : ¬s = ⊤
⊢ mk 1 ∈ ↑s
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
t : UpperSet (MulArchimedeanClass M)
hst : ⊤ ≤ t
⊢ subgroup t ≤ subgroup ⊤

pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
hs : s ≠ ⊤
⊢ subgroup t ≤ subgroup s

Tactic:
· rw [eq_top_iff.mpr hst]

Goal state after:
case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
hs : s ≠ ⊤
⊢ subgroup t ≤ subgroup s
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r, x

Tactic:
rw [← sum_inter_add_sum_sdiff r s _]
      gcongr
      refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_
      rw [mem_sdiff, mem_Ioc] at mx; exact mx.1.1.le

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : One α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : R⟦Γ⟧
⊢ (-x).leadingCoeff = -x.leadingCoeff

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> simp [leadingCoeff_of_ne_zero, *]

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

Goal state before:
pp: case mpr
Γ : 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
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
⊢ 0 < (ofLex x).leadingCoeff

Tactic:
have horder' : (ofLex x).orderTop.untop htop = i := (WithTop.untop_eq_iff _).mpr horder

Goal state after:
case mpr
Γ : 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
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
horder' : (ofLex x).orderTop.untop htop = i
⊢ 0 < (ofLex x).leadingCoeff
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
⊢ ArchimedeanClass.mk (f.sum fun x xi ↦ ↑xi) ≠ ArchimedeanClass.mk b

Tactic:
rw [← hab, DFinsupp.sum]

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
⊢ ArchimedeanClass.mk (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : ArchimedeanClass R
⊢ x ≠ ⊤ → IsAddLeftRegular x

Tactic:
induction x with | mk x => simp +contextual [isAddRegular_mk]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
⊢ f (∑ i ∈ s, l i) = f (l k)

Tactic:
rw [← Finset.add_sum_erase _ _ hk]

Goal state after:
case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)

Tactic:
have hrest_le := IsNonarchimedean.apply_sum_le_sup fna hNonempty (l := l)

Goal state after:
case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
hrest_le : f (∑ i ∈ s.erase k, l i) ≤ (s.erase k).sup' hNonempty fun i ↦ f (l i)
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc,
      seed.coeff_baseEmbedding hf.symm]

Goal state after:
case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = (seed.coeff d) (f d)
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ x * a ∈ P

Tactic:
by
  rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›
  simp [*]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ -(x * a) ∈ P

Tactic:
by
  rw [hasIdealSupport_iff] at ‹P.HasIdealSupport›
  simp [*]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
hx''mem : ↑x'' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
h0 : (seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩ ≠ 0
heq' :
  ((single (FiniteArchimedeanClass.mk (↑x) hx0'))
        ((seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩)).orderTop =
    (ofLex (↑↑f x)).orderTop
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
HahnSeries.orderTop_single h0

Goal state after:
case neg
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
hx''mem : ↑x'' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
h0 : (seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩ ≠ 0
heq' : ↑(FiniteArchimedeanClass.mk (↑x) hx0') = (ofLex (↑↑f x)).orderTop
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x