mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)

Tactic:
set s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)

Goal state after:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
⊢ (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (i⁻¹ • p)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
rw [← cons_eq_insert _ _ ha, multinomial_cons]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (monomial i) 1 ∣ (monomial j) 1 ↔ i ≤ j

Tactic:
rw [monomial_dvd_monomial]
  simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]

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

Goal state before:
pp: case e'_3.e'_6
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x ↦ a ≠ x) m) = (toFinsupp m).update a 0

Tactic:
· ext1 a
    rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
    split_ifs with h
    · rw [Function.update_of_ne h.symm, toFinsupp_apply]
    · rw [not_ne_iff.1 h, Function.update_self]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s) = ↑s

Tactic:
rw [coe_fill, coe_replicate, Multiset.filter_add]

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), (eval x) p = (eval x) q

Tactic:
by rintro rfl; simp only [forall_const]

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

Goal state before:
pp: case cons
x : ℕ
m : Multiset ℕ
h : 0 < m.multinomial
⊢ 0 < (x ::ₘ m).multinomial

Tactic:
simp only [multinomial_cons, h, mul_pos_iff_of_pos_right]

Goal state after:
case cons
x : ℕ
m : Multiset ℕ
h : 0 < m.multinomial
⊢ 0 < (x + m.sum).choose x
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a b c : DegLex (α →₀ ℕ)), a < b → b < c → a < c

Tactic:
intro a b c hab hbc
    simp only [lt_iff] at hab hbc ⊢
    rcases hab with (hab | hab)
    · rcases hbc with (hbc | hbc)
      · left; exact lt_trans hab hbc
      · left; exact lt_of_lt_of_eq hab hbc.1
    · rcases hbc with (hbc | hbc)
      · left; exact lt_of_eq_of_lt hab.1 hbc
      · right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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

Goal state before:
pp: case f
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 → (monomial m) b = C b

Tactic:
simp +contextual [smul_monomial, smul_eq_mul, mul_one]

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

Goal state before:
pp: case g
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = Finsupp.single i 1 → (monomial m) b = b • (monomial (Finsupp.single i 1)) 1

Tactic:
simp +contextual [smul_monomial, smul_eq_mul, 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
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
⊢ m.degree (g * f) = m.degree f + m.degree g

Tactic:
m.degree_mul_of_isRegular_left hg hf,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
⊢ m.degree g + m.degree f = m.degree f + m.degree g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
← coeff_mul_of_degree_add

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ coeff (m.degree f + m.degree g) (f * g) = coeff (m.degree f + m.degree g) (f * g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.withBotDegree f = ↑(m.degree f) ↔ f ≠ 0

Tactic:
by
  classical
  simp [withBotDegree_eq]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.withBotDegree f = ⊥ ↔ f = 0

Tactic:
by
  classical
  simp [withBotDegree_eq]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.withBotDegree (m.leadingTerm f) = m.withBotDegree f

Tactic:
by
  classical
  simp [withBotDegree_eq]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ m.withBotDegree 1 = 0

Tactic:
by
  classical
  simp [withBotDegree_eq]

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
⊢ ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f

Tactic:
intro f

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g f : MvPolynomial σ R
⊢ ∀ (g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
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.sPolynomial f g =
    (monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f -
      (monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g

Tactic:
by
  suffices ∀ f g, m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f by
    rw [sPolynomial, this, this, sup_comm]
  intro f g
  ext a
  obtain (h | h) := le_total (m.degree f a) (m.degree g a) <;> simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Tactic:
simp [one_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Tactic:
simp [one_apply]

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
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

Tactic:
by
  classical
  by_cases hl : f - m.leadingTerm f = 0
  · simpa [hl, toSyn_lt_iff_ne_zero]
  · apply lt_of_le_of_ne (m.degree_sub_leadingTerm_le f)
    by_contra! h'
    simp only [EmbeddingLike.apply_eq_iff_eq] at h'
    apply m.degree_mem_support at hl
    rw [h', mem_support_iff] at hl
    simp [leadingTerm, leadingCoeff] at hl

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨p, ⟨hp, hn⟩, hq⟩

Goal state after:
case mpr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ (ArithmeticFunction.prodPrimeFactors f) (x * y) =
    (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y

Tactic:
rw [prodPrimeFactors_apply hxy₀, prodPrimeFactors_apply hx, prodPrimeFactors_apply hy,
    primeFactors_mul hx hy, ← prod_union hxy.disjoint_primeFactors]

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

Goal state before:
pp: k n : ℕ
⊢ (pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
cases k <;> simp [pow]

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

Goal state before:
pp: case inr
k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
simp only [ArithmeticFunction.sigma_apply]
    aesop

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

Goal state before:
pp: k : ℕ
⊢ ζ * pow k = σ k

Tactic:
ext
  rw [sigma, zeta_mul_apply]
  apply sum_congr rfl
  aesop

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
⊢ ω (m * n) = ω m + ω n

Tactic:
by
  simp [cardDistinctFactors_apply, perm_primeFactorsList_mul_of_coprime h |>.dedup |>.length_eq,
    coprime_primeFactorsList_disjoint h |>.dedup_append]

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
· rw [← inducedMap_rat α] at h
    exact (inducedMap_mono α β).reflect_lt h

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : a ≤ b
⊢ mk b ≤ mk a

Tactic:
contrapose! hab

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Ici 1
b : M
hb : b ∈ Set.Ici 1
hab : mk a < mk b
⊢ b < a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : a ≤ b
⊢ mk a ≤ mk b

Tactic:
contrapose! hab

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : mk b < mk a
⊢ b < a
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn : n ≠ ⊤
⊢ n < ⌊r⌋ₑ ↔ ↑n + 1 ≤ r

Tactic:
by simp [← add_one_le_iff hn]

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
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
⊢ I.FG

Tactic:
refine ⟨_, (setOfPred_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOfPred_minimal_subset _)), ?_⟩

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
⊢ I = closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ I}) x}
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
⊢ ∀ (a : ℕ →o SemigroupIdeal M), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
intro f

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
n : β
hn : n ≠ 0
⊢ (inr α β) n = ↑((OrderMonoidHom.inrₗ αˣ βˣ) (Units.mk0 n hn))

Tactic:
by
  lift n to βˣ using isUnit_iff_ne_zero.mpr hn
  simp

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ |a| ≤ m • |k| • |a|

Tactic:
← smul_assoc

Goal state after:
case refine_1
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ |a| ≤ (m • |k|) • |a|
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
⊢ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ } =
    AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
      AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ }

Tactic:
apply AddOpposite.unop_injective
    ext
    simp

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).leadingCoeff = x.leadingCoeff

Tactic:
by
  rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact leadingCoeff_add_eq_left hxy

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

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

Tactic:
lt_iff

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff ↔
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
hpos : 0 < (ofLex x).leadingCoeff
⊢ ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i

Tactic:
have hne : (ofLex x) ≠ 0 := leadingCoeff_ne_zero.mp hpos.ne.symm

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
hpos : 0 < (ofLex x).leadingCoeff
hne : ofLex x ≠ 0
⊢ ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c < b + c

Tactic:
lt_iff

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : ∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i
⊢ ∃ i, (∀ j < i, (ofLex (a + c)).coeff j = (ofLex (b + c)).coeff j) ∧ (ofLex (a + c)).coeff i < (ofLex (b + c)).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a <
        { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ∨
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a =
        { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    a < b ∨ a = b

Tactic:
lt_iff

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ (∃ i,
        (∀ j < i,
            (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a)).coeff j =
              (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b)).coeff j) ∧
          (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a)).coeff i <
            (ofLex ({ toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b)).coeff i) ∨
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a =
        { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    (∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: 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 : α
h_lt : f y < f x
h : f (x + y) ≠ f x
h1 : f (x + y) ≤ f x
⊢ f x < f x

Tactic:
calc
    f x = f (x + y + -y) := by simp
    _   ≤ max (f (x + y)) (f (-y)) := hna (x + y) (-y)
    _   < max (f x) (f x) := by
      rw [max_self, map_neg_eq_map]
      apply max_lt (lt_of_le_of_ne h1 h) h_lt
    _   = f x := max_self (f x)

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

Goal state before:
pp: case refine_2
Γ : 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
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
by_cases h : f (x.coeff gh.1) = 0

Goal state after:
case pos
Γ : 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

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
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Tactic:
← add_right_cancel h1

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
a1 : Γ
hx : x.coeff a1 = 0
a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝ : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
⊢ ∀ (x : R) {a : R}, a ∈ P.supportAddSubgroup → x * a ∈ P.supportAddSubgroup

Tactic:
simpa [mem_supportAddSubgroup]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ -↑P

Tactic:
by simpa using mul_mem hx ha.2

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ ↑P

Tactic:
by simpa using mul_mem hx ha.2

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

Goal state before:
pp: Γ : 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
⊢ ¬r * x.leadingCoeff = 0

Tactic:
hr.left.mul_left_eq_zero_iff,

Goal state after:
Γ : 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
⊢ ¬x.leadingCoeff = 0
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
⊢ Submodule.toAddSubgroup P.support ≠ Submodule.toAddSubgroup ⊤

Tactic:
simpa using supportAddSubgroup_ne_top P

Goal state after: