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

Goal state before:
pp: case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
⊢ ∃ A > 0, ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
obtain ⟨A, hA, B, hB, H⟩ : ∃ A > (0 : ℝ), ∃ B > (0 : ℝ), ∀ r < (-d : ℝ), ∀ s : Finset L,
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' k : ℕ, (k : ℝ) ^ (d - 1 + r) := by
    refine ⟨2 * d * 3 ^ (d - 1), by positivity, ε, normBound_pos b, fun r hr u ↦ ?_⟩
    let e : (I → ℤ) ≃ₗ[ℤ] L := (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite _ _ _).symm
    obtain ⟨u, rfl⟩ : ∃ u' : Finset _, u = u'.image e.toEmbedding :=
      ⟨u.image e.symm.toEmbedding, Finset.coe_injective
        (by simpa using (e.image_symm_image _).symm)⟩
    dsimp
    simp only [EmbeddingLike.apply_eq_iff_eq, implies_true, Set.injOn_of_eq_iff_eq,
      Finset.sum_image, ge_iff_le]
    obtain ⟨n, hn⟩ : ∃ n : ℕ, u ⊆ Fintype.piFinset fun _ : I ↦ Finset.Icc (-n : ℤ) n := by
      obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0
      refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
      have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; positivity
      have := hr' hx
      simp only [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg hr.le,
        Int.norm_eq_abs, ← Int.cast_abs, ← Int.le_floor] at this
      simpa only [Int.ofNat_toNat, Fintype.mem_piFinset, Finset.mem_Icc, ← abs_le, hr'']
    refine (Finset.sum_le_sum_of_subset_of_nonneg hn (by intros; positivity)).trans ?_
    simp only [Submodule.norm_coe]
    convert! sum_piFinset_Icc_rpow_le b rfl n r hr with x
    simp [e, Finsupp.linearCombination]

Goal state after:
case inr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
⊢ ∃ A > 0, ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∈ s
⊢ ∀ b ∈ s, b ≠ a → (Pi.single a n b)! = 1

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
n : ℕ
inst✝ : DecidableEq α
ha : a ∈ s
⊢ a ∉ s → (Pi.single a n a)! = 1

Tactic:
by simp_all

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ ((expand p) (∑ v ∈ φ.support, (monomial v) (coeff v φ))).support ⊆ Finset.image (fun x ↦ p • x) φ.support

Tactic:
simp only [map_sum, expand_monomial]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (∑ x ∈ φ.support, (monomial (p • x)) (coeff x φ)).support ⊆ Finset.image (fun x ↦ p • x) φ.support
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ x_1 ∈ univ.sigma fun a ↦ univ,
      x a ^ ↑x_1.fst * (↑(↑↑x_1.snd).countPerms * (Multiset.map x ↑↑x_1.snd).noncommProd ⋯) * ↑(n.choose ↑x_1.fst) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
univ_sigma_univ

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ x_1, x a ^ ↑x_1.fst * (↑(↑↑x_1.snd).countPerms * (Multiset.map x ↑↑x_1.snd).noncommProd ⋯) * ↑(n.choose ↑x_1.fst) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝³ : LinearOrder α
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedCancelAddMonoid N
a b : Lex (α →₀ N)
h : a ≤ b
c : Lex (α →₀ N)
⊢ a + c ≤ b + c

Tactic:
by simpa using h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f g : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
h : degLex.toSyn (degLex.degree f) ≤ degLex.toSyn (degLex.degree g)
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
simp only [← MvPolynomial.degree_degLexDegree]
  exact DegLex.monotone_degree h

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
h : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
⊢ (rename ⇑?m.78) p = (rename ⇑?m.78) 0

Tactic:
by simpa using h

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

Goal state before:
pp: case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤ p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
refine le_sup_of_le (mem_support_coeff_finSuccEquiv.mp hi) ?_

Goal state after:
case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1) / ↑(#(S i_1))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
h : x = 0
⊢ False

Tactic:
by simp_all

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

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ Squarefree (m / m.gcd n * m.gcd n)

Tactic:
simpa [Nat.div_mul_cancel, gcd_dvd_left]

Goal state after:
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 (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

Tactic:
by_cases hf : m.degree f = 0 ∧ m.degree g = 0
  · rcases hf with ⟨h₁, h₂⟩
    right
    suffices C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0 by simp_all [sPolynomial_def]
    nth_rewrite 1 [degree_eq_zero_iff.mp h₁]
    nth_rewrite 2 [degree_eq_zero_iff.mp h₂]
    ring
  · rw [or_iff_not_imp_right]
    intro hs
    apply (m.degree_sPolynomial_le f g).lt_of_ne
    apply m.toSyn.injective.ne
    contrapose hs
    rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ ∏ a ∈ l.primeFactors, f a = f l

Tactic:
← h_mult.map_prod_of_subset_primeFactors l _ Subset.rfl,

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ f (∏ a ∈ l.primeFactors, a) = f l
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ #n.divisors = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Tactic:
← sigma_zero_apply,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (σ 0) n = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
x✝¹ : ℕ × ℕ
x✝ : x✝¹ ∈ Ioc 0 N ×ˢ Ioc 0 N
⊢ (∑ x ∈ Ioc 0 N, if x✝¹.1 * x✝¹.2 = x then f x✝¹.1 * g x✝¹.2 else 0) =
    if x✝¹.1 * x✝¹.2 ≤ N then f x✝¹.1 * g x✝¹.2 else 0

Tactic:
by simp_all

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

Goal state before:
pp: d n : ℕ
hn : Squarefree n
⊢ #univ ^ #n.primeFactors = d ^ #n.primeFactorsList.toFinset

Tactic:
toFinset_factors,

Goal state after:
d n : ℕ
hn : Squarefree n
⊢ #univ ^ #n.primeFactors = d ^ #n.primeFactors
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case h
σ : 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))
h :
  (∀ b_1 ∈ B, m.toSyn (m.degree (g b_1)) = m.toSyn (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₂)
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
hd : ∀ a ∈ B, m.toSyn (m.degree (g a)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, ↑isunit_gb.unit⁻¹ • m.sPolynomial (g x) (g b)

Tactic:
simp only [m.toSyn.injective.eq_iff] at *

Goal state after:
case h
σ : 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
⊢ g b + ∑ b ∈ B, g b = ∑ x ∈ B, ↑isunit_gb.unit⁻¹ • m.sPolynomial (g x) (g b)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) (-x * -x)

Tactic:
rw [neg_mul, mul_neg, neg_neg]

Goal state after:
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✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i

Tactic:
induction s using induction_on_max_value fun i ↦ toLex (g i, f i) generalizing σ with
  | empty => simp only [le_rfl, Finset.sum_empty]
  | insert a s has hamax hind => ?_

Goal state after:
case insert
ι : 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)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
⊢ ∑ i ∈ insert a s, f i • g (σ i) ≤ ∑ i ∈ insert a s, f i • g i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
h✝ : ∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ
h : |val b|ₘ ^ 1 ≤ |val a|ₘ
⊢ |val b|ₘ ≤ |val a|ₘ ^ 1

Tactic:
by simpa using h

Goal state after:
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:
exact pow_sum_le_card_mul_sum_pow hf _

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
ha : a ≠ 1
⊢ mk a ≤ mk b ↔ ∃ n, |b|ₘ < |a|ₘ ^ n

Tactic:
refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
  · rw [pow_succ]
    exact lt_mul_of_one_lt_right' _ (one_lt_mabs.mpr ha)
  · exact ⟨n, hn.le⟩

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
⊢ a = 1 → mk a = ⊤

Tactic:
by simp_all

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

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ^ n < (1 - x)⁻¹ * (1 - x)

pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x

Tactic:
inv_mul_cancel₀,

Goal state after:
K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ^ n < 1

K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0

K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x
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 ∘ ⇑(Equiv.symm σ) ∘ ⇑σ

Tactic:
symm_comp_self,

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 ∘ id
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
grw [← sum_inter_add_sum_sdiff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : x ∈ r \ s
⊢ x ≤ c + ↑(#s)
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero M₀
inst✝¹ : GroupWithZero N₀
inst✝ : Preorder N₀
⊢ Monotone ⇑(fst M₀ N₀)

Tactic:
refine WithZero.forall.mpr ?_

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero M₀
inst✝¹ : GroupWithZero N₀
inst✝ : Preorder N₀
⊢ (∀ ⦃b : WithZero (M₀ˣ × N₀ˣ)⦄, 0 ≤ b → (fst M₀ N₀) 0 ≤ (fst M₀ N₀) b) ∧
    ∀ (a : M₀ˣ × N₀ˣ) ⦃b : WithZero (M₀ˣ × N₀ˣ)⦄, ↑a ≤ b → (fst M₀ N₀) ↑a ≤ (fst M₀ N₀) b
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝² : GroupWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : LinearOrderedCommGroupWithZero N₀
⊢ Monotone ⇑(snd M₀ N₀)

Tactic:
refine WithZero.forall.mpr ?_

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝² : GroupWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : LinearOrderedCommGroupWithZero N₀
⊢ (∀ ⦃b : WithZero (M₀ˣ × N₀ˣ)⦄, 0 ≤ b → (snd M₀ N₀) 0 ≤ (snd M₀ N₀) b) ∧
    ∀ (a : M₀ˣ × N₀ˣ) ⦃b : WithZero (M₀ˣ × N₀ˣ)⦄, ↑a ≤ b → (snd M₀ N₀) ↑a ≤ (snd M₀ N₀) b
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = (Finset.Ioc (c + a) (c + b)).val

Tactic:
← Finset.image_add_left_Ioc,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = (Finset.image (fun x ↦ c + x) (Finset.Ioc a b)).val
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
y : Γ'
hy : y ∈ (embDomain f x).support
⊢ f (x.orderTop.untop ⋯) ≤ y

Tactic:
obtain ⟨z, hz, rfl⟩ :=
    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy

Goal state after:
case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ f (x.orderTop.untop ⋯) ≤ f z
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ ((truncLT c) x).support ⊆ x.support

Tactic:
by
  rw [support_truncLT]
  exact Set.sep_subset ..

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
x : G
hx : (orderAddMonoidHom G).toAddMonoidHom x = 1
a : ℤ
⊢ (orderAddMonoidHom G) (a • x) = a

Tactic:
by simp_all

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

Goal state before:
pp: case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ (ofLex (toLex ((single ao) a))).orderTop < (ofLex (toLex ((single bo) b))).orderTop ∨
    (ofLex (toLex ((single ao) a))).orderTop = (ofLex (toLex ((single bo) b))).orderTop ∧
      ArchimedeanClass.mk (ofLex (toLex ((single ao) a))).leadingCoeff ≤
        ArchimedeanClass.mk (ofLex (toLex ((single bo) b))).leadingCoeff

Tactic:
exact .inl (by simpa [ha, hb] using! h)

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

Goal state before:
pp: case mp
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ a1 = b ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = b +ᵥ a → a1 = b ∧ a2 = a

Tactic:
rintro ⟨rfl, _, h1⟩

Goal state after:
case mp
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
left✝ : a2 ∈ ((of R).symm x).support
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ a1 = a1 ∧ a2 = a
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
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < y - x

Tactic:
by simpa using h

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 0 = min x.orderTop (orderTop 1)

Tactic:
by simp_all

Goal state after:
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
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 : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
⊢ y < z → ↑(f.extendFun hx) y < ↑(f.extendFun hx) z

Tactic:
hyz

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
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 : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : y < z
⊢ ↑(f.extendFun hx) y < ↑(f.extendFun hx) z