mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0

Tactic:
rintro i ⟨a⟩
        apply hbot

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

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ toDegLex (single a 1) ≤ toDegLex (single b 1) ↔ b ≤ a

Tactic:
DegLex.single_le_iff

Goal state after:
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
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
⊢ p = (monomial m) b

Tactic:
rw [h, mul_comm, hr, C_mul_monomial, mul_one]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.degree ((monomial d) c) = if c = 0 then 0 else d

Tactic:
simp only [degree, support_monomial]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.toSyn.symm ((if c = 0 then ∅ else {d}).sup ⇑m.toSyn) = if c = 0 then 0 else d
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LeftPreLieRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
have assoc_xyz := LeftPreLieRing.assoc_symm' x y z

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ n.factorization a ≤ 1

Tactic:
apply hn'

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

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
hn : 0 ≠ 1
h : Squarefree (0 ^ k)
⊢ Squarefree 0 ∧ k = 1

pp: case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Tactic:
· simp [zero_pow hk] at h

Goal state after:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : Squarefree (n / k)
⊢ Squarefree n

Tactic:
squarefree_iff_prime_squarefree

Goal state after:
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
⊢ ∀ (x : ℕ), Prime x → ¬x * x ∣ n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

Tactic:
· simp [m.withBotDegree_eq, h, m.toWithBotSyn_apply]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i

Tactic:
trans ∑ i ∈ divisorsAntidiagonal x, f i.snd

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' : m.toSyn (m.degree (f - m.leadingTerm f)) = m.toSyn (m.degree f)
⊢ False

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at h'

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ IsUnit (↑f 1)

Tactic:
refine ⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩

Goal state after:
case mp.refine_1
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ ↑f 1 * ↑f⁻¹ 1 = 1

case mp.refine_2
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ ↑f⁻¹ 1 * ↑f 1 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f (l / d) = f l / f d

Tactic:
apply (div_eq_of_eq_mul hd ..).symm
  rw [← hf.right hl, Nat.div_mul_cancel hdl]

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

Goal state before:
pp: n : ℕ
⊢ (σ 1) n = ∑ d ∈ n.divisors, d

Tactic:
by simp [sigma_apply]

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

Goal state before:
pp: n : ℕ
⊢ (σ 0) n = #n.divisors

Tactic:
by simp [sigma_apply]

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

Goal state before:
pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ cons a s ha, f i) = ∑ i ∈ cons a s ha, ω (f i)

Tactic:
| cons a s ha ih =>

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

Goal state before:
pp: case e_s
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
a✝ : ℕ
⊢ a✝ ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a✝ ∈ Ioc 0 (N / n)

Tactic:
simp only [mem_filter, mem_Ioc, and_assoc, and_congr_right_iff] at hn ⊢

Goal state after:
case e_s
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝ : ℕ
hn : 0 < n ∧ n ≤ N
⊢ 0 < a✝ → (a✝ ≤ N ∧ n * a✝ ≤ N ↔ a✝ ≤ N / n)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N ∧ n * a✝¹ ≤ N → a✝¹ ≤ N / n

Tactic:
intro ⟨_, h⟩

Goal state after:
case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
left✝ : a✝¹ ≤ N
h : n * a✝¹ ≤ N
⊢ a✝¹ ≤ N / n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ a ∈ n.primeFactors.attach, if f ↑a ⋯ = f p hp then ↑a else 1

Tactic:
convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)

Goal state after:
case e'_3
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p = if f ↑⟨p, hp⟩ ⋯ = f p hp then ↑⟨p, hp⟩ else 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ coeff (m.degree (g b)) (g b) + coeff (m.degree (g b)) (∑ x ∈ B, g x) = 0

Tactic:
← coeff_add,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ coeff (m.degree (g b)) (g b + ∑ x ∈ B, g x) = 0
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⟩ ⟨n, hn⟩

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
n : ℕ
hn : |val c|ₘ ≤ |val b|ₘ ^ n
⊢ a ≤ c
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
z : ι
hz : z ∈ {x_1 | (Equiv.swap x y) x_1 ≠ x_1}
⊢ z ∈ ↑s

Tactic:
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz

Goal state after:
case inl
ι : 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
y : ι
hy : y ∈ ↑s
z : ι
hx : z ∈ ↑s
hgxy : (g ∘ ⇑σ) z < (g ∘ ⇑σ) y
hfxy : f y < f z
τ : Perm ι := Equiv.trans (Equiv.swap z y) σ
hz : z ∈ {x | (Equiv.swap z y) x ≠ x}
left✝ : z ≠ y
⊢ z ∈ ↑s

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
z : ι
hy : z ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) z
hfxy : f z < f x
τ : Perm ι := Equiv.trans (Equiv.swap x z) σ
hz : z ∈ {x_1 | (Equiv.swap x z) x_1 ≠ x_1}
left✝ : x ≠ z
⊢ z ∈ ↑s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ (orderHom f) (mk a) = (orderHom f) (mk b) → mk a = mk b

Tactic:
| mk b
   => 

Goal state after:
case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ (orderHom f) (mk a) = (orderHom f) (mk b) → mk a = mk b
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈1⌉ₑ = 1

Tactic:
by simpa using ceil_natCast 1

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
⊢ Subgroup.genLTOne H ∈ H

Tactic:
nth_rewrite 1 [← H.genLTOne_zpowers_eq_top]
  exact Subgroup.mem_zpowers (Subgroup.genLTOne H)

Goal state after:
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)
⊢ ∀ (m : ℕ), s.sup g ≤ m → f (s.sup g) = f m

Tactic:
intro n hn

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
⊢ f (s.sup g) = f n
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
by
  set r := Ico c (c + #s)
  calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_sdiff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_sdiff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
⊢ |a • b| = |a| • |b|

Tactic:
by
  obtain ha | ha := le_total a 0 <;> obtain hb | hb := le_total b 0 <;>
    simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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✝ : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : NonemptyInterval α
h : s + t = 0
⊢ -s = t

Tactic:
by
    obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
    rw [neg_pure, neg_eq_of_add_eq_zero_right hab]

Goal state after:
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:
← hxy

Goal state after:
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 = x.coeff g
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjlt : ↑j < (ofLex |x|).orderTop
hjlt' : ↑j < (ofLex |y|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
simp [coeff_eq_zero_of_lt_orderTop hjlt, coeff_eq_zero_of_lt_orderTop hjlt'] at hi

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
obtain hlt | heq | hgt := lt_trichotomy (ofLex x).orderTop (ofLex y).orderTop

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
heq : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
hne : f x ≠ f y
h_lt : f y < f x
⊢ f (x + y) = max (f x) (f y)

Tactic:
· rw [add_eq_left_of_lt hna h_lt]
    exact (max_eq_left_of_lt h_lt).symm

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝ : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
⊢ ⟦x⟧ ≤ z

Tactic:
induction y using Quotient.inductionOn with | h y
     =>  _ 

Goal state after:
case h.h
α : Type u_1
s : Setoid α
inst✝ : LE α
z : Quotient s
x y : α
h₂ : ⟦y⟧ ≤ z
h₁ : ⟦x⟧ ≤ ⟦y⟧
⊢ ⟦x⟧ ≤ z
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : Quotient s
x : α
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧

Tactic:
induction y using Quotient.inductionOn with | h y
     =>  _ 

Goal state after:
case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ∨ ⟦y⟧ ≤ ⟦x⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
y : Quotient s
x : α
h₁ : ⟦x⟧ ≤ y
h₂ : y ≤ ⟦x⟧
⊢ ⟦x⟧ = y

Tactic:
induction y using Quotient.inductionOn with | h y
     =>  _ 

Goal state after:
case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
h₂ : ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ = ⟦y⟧
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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = ofLex (toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩)))

Tactic:
rw [ofLex_toLex]

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = (single c) ((seed.coeff c) ⟨↑x, hx⟩)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
⊢ (C a).map f = C (f a)

Tactic:
by
  ext g
  by_cases h : g = 0 <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ f = conjneg 0 ↔ f = 0

Tactic:
conjneg_zero

Goal state after:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ f = 0 ↔ f = 0
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), e (a + b) = e a + e b
a b : M
⊢ e (a - b) = e a - e b

Tactic:
let e_add : M ≃+ N := { e with map_add' := h_add }

Goal state after:
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), e (a + b) = e a + e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ e (a - b) = e a - e b