mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : p ∣ n ↔ p ∣ m
⊢ n.factorization p = m.factorization p

Tactic:
← not_iff_not,

Goal state after:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ¬p ∣ n ↔ ¬p ∣ m
⊢ n.factorization p = m.factorization p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
⊢ d * d ∣ n

Tactic:
by
  have := minSqFac_has_prop n
  rw [h] at this
  exact this.2.1

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ {d ∈ n.divisors | Squarefree d}.val = Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

n : ℕ
h0 : n ≠ 0
⊢ ∀ 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
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
con : 0 ∈ s.val
⊢ False

Tactic:
apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))

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 : MvPolynomial σ R
h : m.degree f = 0
⊢ f - m.leadingTerm f = 0

Tactic:
m.degree_eq_zero_iff.mp h,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f = 0
⊢ C (m.leadingCoeff f) - m.leadingTerm (C (m.leadingCoeff f)) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (↑(m * n).primeFactorsList).card = m.primeFactorsList.length + n.primeFactorsList.length

Tactic:
← factors_eq,

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
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).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∈ n.divisors) ∧
    match f a ha with
    | (x, y) => x.lcm y = n

Tactic:
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.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial ((m.degree p₁ + m.degree q₁) ⊔ (m.degree p₂ + m.degree q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

Tactic:
by
  simp [sPolynomial_monomial_mul, leadingTerm]

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

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

Tactic:
simp_rw [map_neg, neg_mul, mul_neg, neg_neg]

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

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

Tactic:
use a⁻¹, Left.inv_lt_one_iff.mpr ha1

Goal state after:
case right
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
⊢ Subgroup.zpowers a⁻¹ = H
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀
x : M₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inr.inl
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₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
⊢ 0 ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀
x : N₀ˣ
⊢ ↑x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inr.inl
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₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2

Tactic:
exact ⟨hb₁.trans <| s.fst_le_snd.trans hc₂, hc₁.trans <| s.fst_le_snd.trans hb₂⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).coeff a = r

Tactic:
classical exact Pi.single_eq_same (M := fun _ => R) a r

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

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ¬(⋂ s ∈ S, ↑s).Nonempty

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : x ∈ ⋂ s ∈ S, ↑s
⊢ False
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g

Tactic:
by_cases h : g = a <;> simp [h]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : PartialOrder Γ
inst✝² : Zero R
a b : Γ
r✝ : R
inst✝¹ : Nonempty Γ
inst✝ : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : (single default) r = (single default) s
⊢ r = s

Tactic:
← coeff_single_same (default : Γ) r,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : PartialOrder Γ
inst✝² : Zero R
a b : Γ
r✝ : R
inst✝¹ : Nonempty Γ
inst✝ : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : (single default) r = (single default) s
⊢ ((single default) r).coeff default = s
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
hy : y ≠ 0
⊢ (x - y).coeff g = 0

Tactic:
rw [orderTop_of_ne_zero hy, WithTop.coe_eq_coe] at hyg

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
hy : y ≠ 0
hyg : ⋯.min ⋯ = g
⊢ (x - y).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a = b
⊢ a ≤ b ∨ b ≤ a

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ a

Tactic:
· exact Or.inl hab.le

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Disjoint (u.stratum c) (⨆ j, ⨆ (_ : j ≠ c), u.stratum j)

Tactic:
rw [Submodule.disjoint_def']

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
⊢ ∀ x ∈ u.stratum c, ∀ y ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j, x = y → x = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: 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
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ |n • x| < |y|

Tactic:
have hgt' : (ofLex y).orderTop < (ofLex (n • x)).orderTop := by
    apply lt_of_lt_of_le hgt
    simpa using orderTop_smul_not_lt n (ofLex x)

Goal state after:
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
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
hgt' : (ofLex y).orderTop < (ofLex (n • x)).orderTop
⊢ |n • x| < |y|
Module: Mathlib.Algebra.Order.Quantale

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

Tactic:
rw [← sSup_empty, mul_sSup_distrib]

Goal state after:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, x * y = sSup ∅
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : 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 : Γ
⊢ ((of R).symm ((single b) r • x)).coeff (b +ᵥ a) = r • ((of R).symm x).coeff a

Tactic:
by
  by_cases hr : r = 0
  · simp_all only [map_zero, zero_smul, coeff_smul, HahnSeries.support_zero, HahnSeries.coeff_zero,
    sum_const_zero]
  simp only [hr, coeff_smul, coeff_smul, HahnSeries.support_single_of_ne, ne_eq, not_false_iff]
  by_cases hx : ((of R).symm x).coeff a = 0
  · simp only [hx, smul_zero]
    rw [sum_congr _ fun _ _ => rfl, sum_empty]
    ext ⟨a1, a2⟩
    simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_vaddAntidiagonal, iff_false]
    rintro rfl h2 h1
    rw [IsCancelVAdd.left_cancel a1 a2 a h1] at h2
    exact h2 hx
  trans ∑ ij ∈ {(b, a)},
    (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd
  · apply sum_congr _ fun _ _ => rfl
    ext ⟨a1, a2⟩
    simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_vaddAntidiagonal, mem_singleton]
    constructor
    · rintro ⟨rfl, _, h1⟩
      exact ⟨rfl, IsCancelVAdd.left_cancel a1 a2 a h1⟩
    · rintro ⟨rfl, rfl⟩
      exact ⟨rfl, by exact hx, rfl⟩
  · simp

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : ¬f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
· exact mul_eq_zero_of_right (f (x.coeff gh.1)) (hz h)

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
⊢ 0 ≤ mk ↑q

Tactic:
obtain rfl | hn := eq_or_ne q 0

Goal state after:
case inl
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
⊢ 0 ≤ mk ↑0

case inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
hn : q ≠ 0
⊢ 0 ≤ mk ↑q
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0
⊢ ((single g) r * x).order = g + x.order

Tactic:
rw [order_mul_of_ne_zero hrx, order_single <| IsRegular.ne_zero hr]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
⊢ ∃ x_1, ¬(x * y).coeff x_1 = (x * z).coeff x_1

Tactic:
have : Set.IsWF {a | y.coeff a ≠ z.coeff a} :=
      .mono (y.isWF_support.union z.isWF_support) (by intro; simp; grind)

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
⊢ ∃ x_1, ¬(x * y).coeff x_1 = (x * z).coeff x_1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
⊢ ∃ x_1, ¬(y * x).coeff x_1 = (z * x).coeff x_1

Tactic:
have : Set.IsWF {a | y.coeff a ≠ z.coeff a} :=
      .mono (y.isWF_support.union z.isWF_support) (by intro; simp; grind)

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
⊢ ∃ x_1, ¬(y * x).coeff x_1 = (z * x).coeff x_1
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
h' : ¬∃ y, ↑y - k • x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c

Tactic:
simp [f.evalCoeff_eq_zero h, f.evalCoeff_eq_zero h']

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

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

Tactic:
by_cases hr : x ∈ R

Goal state after:
case pos
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∈ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)

case neg
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
⊢ x ∈ R.ofPrime (R.idealOfLE S h)
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
y : ↥(↑f).domain
⊢ ∃ z, ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)

Tactic:
by
  set c := mk _ (val_sub_ne_zero f hx y)
  have hc : ArchimedeanClass.mk (y.val - x) = c := rfl
  by_contra!; apply hx
  have h := f.eval_eq_truncLT hc this
  obtain ⟨x', hx'⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range y c)
  rw [← hx'] at h
  contrapose! h
  exact f.eval_ne h _

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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
⊢ z < y

Tactic:
change z.val < y.val

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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
⊢ ↑z < ↑y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ IsUnit x ↔ mk ↑x = 0

Tactic:
← not_iff_not,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : FiniteElement K
⊢ ¬IsUnit x ↔ ¬mk ↑x = 0
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(upperClosure s) * t = ↑(upperClosure (s * t))

Tactic:
simp_rw [mul_comm _ t]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))

Tactic:
simp_rw [mul_comm _ t]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))