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

Goal state before:
pp: n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1

Tactic:
refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩
  rcases eq_or_ne n 0 with (rfl | -)
  · simp [zero_pow hk] at h
  refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩
  have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩
  apply hn (Nat.isUnit_iff.1 (h _ _))
  rw [← sq]
  exact pow_dvd_pow _ this

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

Goal state before:
pp: case neg
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
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))

Tactic:
have k0 : 0 < k := lt_of_lt_of_le (by decide) k2

Goal state after:
case neg
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
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
have hSne : S.Nonempty := by
    use 1
    have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
    simp [S, h1]

Goal state after:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
f : ℕ → R
⊢ f ∈ Set.range DFunLike.coe ↔ f ∈ {f | f 0 = 0}

Tactic:
exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

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

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
by
  rw [isPrimePow_nat_iff]
  refine exists₂_congr fun p k => ?_
  constructor
  · rintro ⟨hp, hk, hn⟩
    exact ⟨hk, by rw [← hn, Nat.Prime.factorization_pow hp]⟩
  · rintro ⟨hk, hn⟩
    have hn0 : n ≠ 0 := by
      rintro rfl
      simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
    rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
    exact ⟨Nat.prime_of_mem_primeFactors <|
      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩

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

Goal state before:
pp: k : ℕ
⊢ (σ k).IsMultiplicative

Tactic:
rw [← zeta_mul_pow_eq_sigma]
  apply isMultiplicative_zeta.mul isMultiplicative_pow

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

Goal state before:
pp: p a m n : ℕ
hp : Prime p
hn : n ≠ 0
h : p ^ m = a ^ n
⊢ ∃ k, a = p ^ k

Tactic:
by
  rcases exponent_dvd_of_prime_pow_eq_pow hp h with ⟨k, m_eq⟩
  rw [m_eq, pow_mul'] at h
  use k
  exact Nat.pow_left_injective hn h.symm

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply,
      Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
      toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
      PNat.coe_prod]

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i, ↑(x i) = n ∧ (fun i ↦ ↑(x i)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: ι : 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)
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hxy : x ≠ y
⊢ y ∈ ↑(cons a s ha)

Tactic:
simp [hy]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ i, ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = i, ↑p = n

Tactic:
rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]

Goal state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ x ∈ n.primeFactors, x = n

case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∑ k ∈ Finset.range n, s.indicator (fun x ↦ a) k = ∑ a_1 ∈ hs.toFinset, s.indicator (fun x ↦ a) a_1

Tactic:
eventually_atTop

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
⊢ ∃ a_1,
    ∀ (b : ℕ),
      a_1 ≤ b → ∑ k ∈ Finset.range b, s.indicator (fun x ↦ a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x ↦ a) a_3
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : mk a < mk b
⊢ |a|ₘ ≤ |a * b|ₘ ^ 2

Tactic:
rw [mk_lt_mk] at h

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
⊢ |a|ₘ ≤ |a * b|ₘ ^ 2
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

Tactic:
· exact s.upper h hb

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

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

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

Tactic:
intro s ha
      split_ifs with h
      · lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1
        -- Porting note: Lean failed to figure out the function `f` by itself,
        -- so I added it through manually
        let f := fun (s : NonemptyInterval α) (_ : ↑s ∈ s₁) => s.toProd.fst
        exact WithBot.coe_le_coe.2 ⟨le_iSup₂ (f := f) s ha, iInf₂_le s ha⟩
      · exact bot_le

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

Goal state before:
pp: case some.some
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ : Interval α
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹

Tactic:
exact congr_arg WithBot.some (mul_inv_rev _ _)

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

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
simp [hy]

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

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

Tactic:
simp [hy]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case mp
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ a * c ≤ x ∧ x < b * c → ∃ a_2, (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x

Tactic:
rintro ⟨h₁, h₂⟩
      obtain ⟨d, rfl⟩ := exists_mul_of_le h₁
      exact ⟨a * d, ⟨by simpa using h₁, by simpa [mul_right_comm a c d] using h₂⟩,
        by simp_rw [mul_assoc, mul_comm]⟩

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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simp_rw [ArchimedeanClass.mk_le_mk]
  obtain rfl | hy := eq_or_ne y 0
  · -- special case: both `x` and `y` are zero
    simp_all
  -- general case: `x` and `y` are not zero
  have hx : x ≠ 0 := by simpa using orderTop_ne_top.1 <| h ▸ orderTop_ne_top.2 (by simpa using hy)
  have h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop := by simpa using h
  constructor
  · -- `mk x ≤ mk y → mk x.leadingCoeff ≤ mk y.leadingCoeff`
    intro ⟨n, hn⟩
    refine ⟨n + 1, ?_⟩
    have hn' : |y| < (n + 1) • |x| :=
      lt_of_le_of_lt hn <| nsmul_lt_nsmul_left (by simpa using hx) (by simp)
    obtain ⟨j, hj, hi⟩ := (lt_iff _ _).mp hn'
    simp_rw [ofLex_smul, coeff_smul] at hj hi
    simp_rw [← leadingCoeff_abs]
    rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]
    simp_rw [← h']
    obtain hjlt | hjeq | hjgt := lt_trichotomy (WithTop.some j) (ofLex |x|).orderTop
    · -- impossible case: `x` and `y` differ before their leading coefficients
      have hjlt' : j < (ofLex |y|).orderTop := h'.symm ▸ hjlt
      simp [coeff_eq_zero_of_lt_orderTop hjlt, coeff_eq_zero_of_lt_orderTop hjlt'] at hi
    · convert! hi.le <;> exact (WithTop.untop_eq_iff _).mpr hjeq.symm
    · exact (hj _ ((WithTop.untop_lt_iff _).mpr hjgt)).le
  · -- `mk x.leadingCoeff ≤ mk y.leadingCoeff → mk x ≤ mk y`
    intro ⟨n, hn⟩
    refine ⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩
    refine ⟨(ofLex x).orderTop.untop (by simpa using hx), ?_, ?_⟩
    · -- all coefficients before the leading coefficient are zero
      intro j hj
      trans 0
      · apply coeff_eq_zero_of_lt_orderTop
        simpa [← h] using hj
      · suffices (ofLex |x|).coeff j = 0 by simp [this]
        apply coeff_eq_zero_of_lt_orderTop
        simpa using hj
    -- the leading coefficient determines the relation
    rw [ofLex_smul, coeff_smul]
    suffices |(ofLex y).leadingCoeff| < (n + 1) • |(ofLex x).leadingCoeff| by
      simp_rw [← leadingCoeff_abs] at this
      rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]
        at this
      convert! this using 3 <;> simp [h]
    refine lt_of_le_of_lt hn <| nsmul_lt_nsmul_left ?_ (by simp)
    rwa [abs_pos, leadingCoeff_ne_zero]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this✝ : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
this : ArchimedeanClass.mk a = ↑c
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support

Tactic:
rw [← val_mk h0, ← Subtype.ext_iff] at this

Goal state after:
case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this✝ : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
this : FiniteArchimedeanClass.mk a h0 = c
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support
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:
simp_rw [le_iff_lt_or_eq, 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 : α
hne : f x ≠ f y
⊢ f (x + y) = max (f x) (f y)

Tactic:
rcases hne.lt_or_gt with h_lt | h_lt
  · rw [add_eq_right_of_lt hna h_lt]
    exact (max_eq_right_of_lt h_lt).symm
  · rw [add_eq_left_of_lt hna h_lt]
    exact (max_eq_left_of_lt h_lt).symm

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

Goal state before:
pp: 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
y : S
⊢ mk x ≤ mk x + mk (f y)

Tactic:
by
  rw [add_comm]
  exact mk_le_mk_add_of_archimedean f x y

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hy]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hy]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
simp [hy]

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
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
simp_rw [mk_eq_mk]

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ((∃ m, |y| ≤ m • |x|) ∧ ∃ n, |x| ≤ n • |y|) ↔ (∃ m, |↑y| ≤ m • |↑x|) ∧ ∃ n, |↑x| ≤ n • |↑y|
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 : y ≠ z
⊢ x * y ≠ x * z

Tactic:
simp only [ne_eq, ← coeff_inj, funext_iff, not_forall] at ⊢ hyz

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
⊢ ∃ 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 : y ≠ z
⊢ y * x ≠ z * x

Tactic:
simp only [ne_eq, ← coeff_inj, funext_iff, not_forall] at ⊢ hyz

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
⊢ ∃ x_1, ¬(y * x).coeff x_1 = (z * x).coeff x_1
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx') *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ⋯) =
    1

Tactic:
by
        rw [← map_mul, this, map_one]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x + y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      if h : 0 ≤ mk y then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y h) else 0

Tactic:
dif_pos hy,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x + y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x * y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      if h : 0 ≤ mk y then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y h) else 0

Tactic:
dif_pos hy,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x * y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) h) else 0) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)
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
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ ∃ y, ((↑f).supSpanSingleton x (f.eval x) hx).toFun y = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))

Tactic:
refine ⟨⟨x, by simpa using Submodule.mem_sup_right (Submodule.mem_span_singleton_self x)⟩, ?_⟩

Goal state after:
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
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨x, ⋯⟩ = toLex ((truncLTLinearMap K c) (ofLex (f.eval x)))
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : R[X][Y]
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) p) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p))

Tactic:
induction p using Polynomial.induction_on' with
  | add p q _ _ => aesop
  | monomial n p =>
  induction p using Polynomial.induction_on' with
  | add p q _ _ => aesop
  | monomial m a =>
    simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
    simp [map_nsmul]

Goal state after: