mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(b, a₂)

Tactic:
rw [Sym2.eq_swap]
  exact GameAdd.snd h

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset S | P (init r)}) = S (last n) ×ˢ {r ∈ piFinset (init S) | P r}

Tactic:
by
  unfold init; ext; simp [Fin.forall_iff_castSucc, and_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Goal state before:
pp: x y : ℤ
⊢ |x| < |y| ↔ x.natAbs < y.natAbs

Tactic:
abs_eq_natAbs,

Goal state after:
x y : ℤ
⊢ ↑x.natAbs < |y| ↔ x.natAbs < y.natAbs
Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Goal state before:
pp: x y : ℤ
⊢ ↑x.natAbs < |y| ↔ x.natAbs < y.natAbs

Tactic:
abs_eq_natAbs,

Goal state after:
x y : ℤ
⊢ ↑x.natAbs < ↑y.natAbs ↔ x.natAbs < y.natAbs
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ n) = 0

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
dk : k ∣ n
⊢ k ≤ k.minFac

Tactic:
exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)

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

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
prod_insert has,

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝ * ∏ x ∈ s✝, g x) = ∏ i ∈ insert a✝ s✝, f (g i)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝ * ∏ x ∈ s✝, g x) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
prod_insert has,

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝ * ∏ x ∈ s✝, g x) = f (g a✝) * ∏ x ∈ s✝, f (g x)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiag 0 n ↔ a✝ ∈ ∅

Tactic:
simp [hn.symm]

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

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

Tactic:
simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hb0 : ¬g b = 0
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < d
hd :
  (m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b))) ∧
    ∀ a ∈ B, m.toSyn (m.degree (g a)) = d ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ ∃ c, ∑ b ∈ insert b B, g b = ∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
⊢ f n = g n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f n = g n

case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ f n = g n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f n = g n

pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ f n = g n

Tactic:
· rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ f n = g n
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case pos
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : x ≤ 1
⊢ ∃ n, x ≤ y ^ n

pp: case neg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : 1 < x
⊢ ∃ n, x ≤ y ^ n

Tactic:
· use 0
      simpa using hx

Goal state after:
case neg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : 1 < x
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
· rw [← sub_pos] at hb
    calc
      ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d < 1

Tactic:
exact lt_of_le_of_lt (by simp [mul_nonneg]) one_pos

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

Goal state before:
pp: 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
⊢ n • |a| = (n • 1) • |a|

Tactic:
rw [smul_assoc, one_smul]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
by
  simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } ≤ s

Tactic:
lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
h : ⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
s : NonemptyInterval α
ha : ↑s ∈ s₁
⊢ ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } ≤ ↑s
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → x.coeff j = 0
h : x ≠ 0
⊢ i ≤ x.orderTop

Tactic:
· by_contra! hi
      exact x.isWF_support.min_mem (support_nonempty_iff.2 h) (H _ (orderTop_of_ne_zero h ▸ hi))

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  by_cases hxy : x + y = 0; · simp [hxy]
  rw [orderTop_of_ne_zero hx, orderTop_of_ne_zero hy, orderTop_of_ne_zero hxy, ← WithTop.coe_min,
    WithTop.coe_le_coe]
  exact HahnSeries.min_le_min_add hx hy hxy

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

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

Tactic:
by
  have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
  have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy
  by_cases h : x + y = 0
  · rw [h, orderTop_zero] at ho
    rw [h, orderTop_eq_top.mp ho.symm]
  · simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]
    rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]

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

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid E₁
inst✝⁴ : PartialOrder E₁
inst✝³ : AddCommMonoid E₂
inst✝² : PartialOrder E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
x✝¹ x✝ : E₁ →ₚ[R] E₂
h : x✝¹.toLinearMap = x✝.toLinearMap
⊢ x✝¹ = x✝

Tactic:
ext x; congrm($h x)

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
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : i ∈ v
⊢ i ∈ u

Tactic:
Set.mem_union,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : i ∈ v
⊢ i ∈ {i | (ofLex a).coeff i ≠ 0} ∨ i ∈ {i | (ofLex b).coeff i ≠ 0}
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
⊢ ArchimedeanClass.mk (f.sum fun x xi ↦ ↑xi) ≠ ArchimedeanClass.mk a

Tactic:
DFinsupp.sum

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
⊢ ArchimedeanClass.mk (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a
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✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
by
  classical
  rw [coeff_smul]
  apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right _ _ _ hys) _ fun _ _ => rfl
  intro b hb
  simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
  rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]

Goal state after:
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 ↔
    a ≤ b

Tactic:
le_iff_lt_or_eq,

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⟦Γ⟧
⊢ { 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
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (x ^ n * x) = mk (y ^ n * y)

Tactic:
mk_mul,

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (x ^ n) + mk x = mk (y ^ n) + mk y
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ n * x) = n • mk x + mk x

Tactic:
mk_mul,

Goal state after:
case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ n) + mk x = n • mk x + mk x
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
⊢ IsAddRegular (mk x)

Tactic:
← isAddLeftRegular_iff_isAddRegular

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
⊢ IsAddLeftRegular (mk x)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case hpos
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ 0 ≤ f y

Tactic:
simpa using f.monotone' hy.le

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

Goal state before:
pp: case hneg
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y ≤ 0

Tactic:
simpa using f.monotone' hy.le

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

Goal state before:
pp: case mk.inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
hx : x ≠ 0
⊢ mk (x ^ ↑n * x) = ↑n • mk x + mk x

Tactic:
mk_mul,

Goal state after:
case mk.inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
hx : x ≠ 0
⊢ mk (x ^ ↑n) + mk x = ↑n • mk x + mk x
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ -mk (x ^ n * x) = -(↑n • mk x + mk x)

Tactic:
mk_mul,

Goal state after:
case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ -(mk (x ^ n) + mk x) = -(↑n • mk x + mk x)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk (x * y⁻¹) = mk x - mk y

Tactic:
mk_mul,

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x + mk y⁻¹ = mk x - mk y
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ((of R).symm ((x * y) • z)).coeff b = ((of R).symm (x • y • z)).coeff b

Tactic:
coeff_smul_left (x.isPWO_support.add y.isPWO_support)
    HahnSeries.support_mul_subset,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ ij ∈ VAddAntidiagonal b ⋯, (x * y).coeff ij.1 • ((of R).symm z).coeff ij.2 = ((of R).symm (x • y • z)).coeff b
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.inl.inl
α : 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⟧

Tactic:
exact congrArg _ (h₁.antisymm 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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (↑z - x)
⊢ (ofLex (f.eval x)).coeff c = (ofLex (↑↑f z)).coeff c

Tactic:
simp_rw [eval, 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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (↑z - x)
⊢ f.evalCoeff x c = (ofLex (↑↑f z)).coeff c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
⊢ v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring

Tactic:
by
  constructor
  · intro h; ext x; specialize h x 1; simpa using h
  · intro h; apply isEquiv_of_val_le_one
    intro x
    have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]
    simpa using this

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

Goal state before:
pp: case a
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
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj✝ : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hlt : FiniteArchimedeanClass.mk (↑y - x) hxy0 < i
hj : True
⊢ (ofLex (↑↑f (z - y))).coeff (FiniteArchimedeanClass.mk (↑z - ↑y) hzyne) ≠ 0

Tactic:
apply f.coeff_ne_zero

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ ↑(FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯) = ↑1

Tactic:
apply inv_mul_cancel₀

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ x ≠ 0