mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

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

Tactic:
· rintro ⟨b, hmn, hb, h⟩
    use C b, hmn, map_dvd C hb
    rwa [mul_comm, C_mul_monomial, mul_one]

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieAdmissibleRing L
inst✝ : LieAdmissibleAlgebra R L
r : R
x y : L
⊢ ⁅x, r • y⁆ = r • ⁅x, y⁆

Tactic:
by
    simp [Ring.lie_def, mul_smul_comm, smul_mul_assoc, ← smul_sub]

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

Goal state before:
pp: n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x

Tactic:
intro x

Goal state after:
n x : ℕ
⊢ x ∈ ↑(n + 1).primeFactorsList → Irreducible x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' (B \ {0}) = m.leadingTerm '' B \ {0}

Tactic:
by
  aesop

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
B : Set (MvPolynomial σ R)
⊢ m.leadingTerm '' insert 0 B = insert 0 (m.leadingTerm '' B)

Tactic:
by
  aesop

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Tactic:
intro x

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
⊢ x ∈ (normalizedFactors n).toFinset.powerset.val →
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Tactic:
intro x hx y hy h

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ x = y
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
by
  ext n
  by_cases hn0 : n = 0
  · simp [hn0]
  by_cases hn1 : n = 1
  · simp [hn1]
  rw [dirichletInverse, mul_apply, coe_mk,
    Nat.sum_divisorsAntidiagonal' fun x y ↦ f x * dirichletInverseFun f hf y,
    ← Nat.cons_self_properDivisors hn0]
  simp [hn0, hn1, pos_of_ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
⊢ ∀ {m n : ℕ},
    ¬m = 0 →
      ¬n = 0 →
        m.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (m * n) =
            (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x : ℕ
⊢ ∀ {n : ℕ},
    ¬x = 0 →
      ¬n = 0 →
        x.Coprime n →
          (ArithmeticFunction.prodPrimeFactors f) (x * n) =
            (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : Finsupp.single p m = n • a.factorization
⊢ m = n * a.factorization p

Tactic:
simpa using congr($this p)

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

Goal state before:
pp: n : ℕ
⊢ 0 < n.primeFactorsList.length ↔ 1 < n

Tactic:
List.length_pos_iff,

Goal state after:
n : ℕ
⊢ n.primeFactorsList ≠ [] ↔ 1 < n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case inl
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0

pp: case inr
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d ≠ 0
⊢ 2 ≤ d

Tactic:
· exact i.elim0

Goal state after:
case inr
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d ≠ 0
⊢ 2 ≤ d
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
⊢ ∀ (x : M), (antidiagonal x).sup' ⋯ f ∉ U → x ∈ Prod.fst '' (f ⁻¹' U)ᶜ + Prod.snd '' (f ⁻¹' U)ᶜ

Tactic:
intro x

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
x : M
⊢ (antidiagonal x).sup' ⋯ f ∉ U → x ∈ Prod.fst '' (f ⁻¹' U)ᶜ + Prod.snd '' (f ⁻¹' U)ᶜ
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
⊢ x ∈ hs.toFinset → s.indicator (fun x ↦ a) x = a
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ hs.toFinset ⊆ Finset.range n

Tactic:
intro x

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ hs.toFinset → x ∈ Finset.range n
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
⊢ ∀ x ∈ Finset.range n, x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0

Tactic:
intro x

Goal state after:
case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
x y : α
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

Tactic:
by
  rw [inducedMap, cutMap_add]
  exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y)
    (cutMap_bddAbove β y)

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

Goal state before:
pp: 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 : α), (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
intro x

Goal state after:
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 : α
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: 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

Tactic:
| 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.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 α β
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)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
⊢ {x | τ x ≠ x} ⊆ ↑s

Tactic:
intro x

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✝ : 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)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
⊢ x ∈ {x | τ x ≠ x} → x ∈ ↑s
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (single i 1) ≠ 0

Tactic:
← map_zero m.toSyn

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (single i 1) ≠ m.toSyn 0
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋₊

Tactic:
div_eq_inv_mul

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋₊
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
⊢ ∀ x ∈ s, ∃ i, x ∈ f i

Tactic:
intro x

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
x : M
⊢ x ∈ s → ∃ i, x ∈ f i
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∀ a ∈ range #s, c - ↑a ∈ Ioc (c - ↑(#s)) c

Tactic:
intro x

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
⊢ x ∈ range #s → c - ↑x ∈ Ioc (c - ↑(#s)) c
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
hn : s.sup g ≤ n
⊢ iSup ⇑f ≤ f (s.sup g)

Tactic:
intro x

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
hn : s.sup g ≤ n
x : M
⊢ x ∈ iSup ⇑f → x ∈ f (s.sup g)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.InjOn (fun x ↦ c - ↑x) ↑(range #s)

Tactic:
intro x

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
⊢ x ∈ ↑(range #s) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c - ↑x) x = (fun x ↦ c - ↑x) x₂ → x = x₂
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.SurjOn (fun x ↦ c - ↑x) ↑(range #s) ↑(Ioc (c - ↑(#s)) c)

Tactic:
intro x

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
⊢ x ∈ ↑(Ioc (c - ↑(#s)) c) → x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∀ a ∈ range #s, c + ↑a ∈ Ico c (c + ↑(#s))

Tactic:
intro x

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
⊢ x ∈ range #s → c + ↑x ∈ Ico c (c + ↑(#s))
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.InjOn (fun x ↦ c + ↑x) ↑(range #s)

Tactic:
intro x

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
⊢ x ∈ ↑(range #s) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range #s) → (fun x ↦ c + ↑x) x = (fun x ↦ c + ↑x) x₂ → x = x₂
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.SurjOn (fun x ↦ c + ↑x) ↑(range #s) ↑(Ico c (c + ↑(#s)))

Tactic:
intro x

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
⊢ x ∈ ↑(Ico c (c + ↑(#s))) → x ∈ (fun x ↦ c + ↑x) '' ↑(range #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₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(ofClass WithZero.withZeroUnitsEquiv.symm)

Tactic:
intro x

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀
⊢ ∀ ⦃b : M₀⦄, x ≤ b → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 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₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(ofClass WithZero.withZeroUnitsEquiv.symm)

Tactic:
intro x

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : N₀
⊢ ∀ ⦃b : N₀⦄, x ≤ b → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) b
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
x : WithZero (Lex (αˣ × βˣ))
⊢ ∀ ⦃b : WithZero (Lex (αˣ × βˣ))⦄,
    x ≤ b →
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun x ≤
        (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Icc_pred_right_eq_Icc h

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

Goal state before:
pp: case neg
Γ : 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
⊢ 0 = x.coeff a

pp: case neg.hnc
Γ : 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
⊢ f a ∉ ⇑f '' x.support

Tactic:
Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)

Goal state after:
case neg
Γ : 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
⊢ 0 = 0

case neg.hnc
Γ : 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
⊢ f a ∉ ⇑f '' x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ (x + y).order

Tactic:
order_of_ne hxy

Goal state after:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g

Tactic:
rw [← hxy]

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

Goal state before:
pp: case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
exact (leadingCoeff_pos_iff.mp hlt).le

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Archimedean ↥(u.stratum c)

Tactic:
apply ArchimedeanClass.archimedean_of_mk_eq_mk

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ ∀ (a : ↥(u.stratum c)), a ≠ 0 → ∀ (b : ↥(u.stratum c)), b ≠ 0 → ArchimedeanClass.mk a = ArchimedeanClass.mk b
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
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
⊢ StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support

Tactic:
intro x

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
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
⊢ x ∈ ↑f.support →
    ∀ ⦃b : FiniteArchimedeanClass M⦄,
      b ∈ ↑f.support → x < b → (fun i ↦ ArchimedeanClass.mk ↑(f i)) x < (fun i ↦ ArchimedeanClass.mk ↑(f i)) b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : 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 : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bc : FiniteArchimedeanClass R
h : toLex (ao, ac) ≤ toLex ((ofLex (toLex (ao, ac))).1, bc)
hle : (ofLex (toLex (ao, ac))).2 ≤ (ofLex (toLex ((ofLex (toLex (ao, ac))).1, bc))).2
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex ((ofLex (toLex (ao, ac))).1, bc))

Tactic:
exact OrderHom.monotone _ hle

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
⊢ mk x ≤ mk y → ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
⊢ (∃ q, 0 < f q ∧ f q * |y| ≤ |x|) → mk x ≤ mk y

Tactic:
· rintro ⟨(_ | n), hn⟩
    · simp_all [exists_zero_lt]
    · obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
      refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
      simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
⊢ (∃ q, 0 < f q ∧ f q * |y| ≤ |x|) → mk x ≤ mk y