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

Goal state before:
pp: case mp
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] := ⋯
⊢ x ∈ Ideal.span (of' k A '' s) → x ∈ RHS

pp: case mpr
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] := ⋯
⊢ x ∈ RHS → x ∈ Ideal.span (of' k A '' s)

Tactic:
· suffices Ideal.span (of' k A '' s) ≤ RHS from @this x
    rw [Ideal.span_le]
    rintro _ ⟨i, hi, rfl⟩ m hm
    refine ⟨_, hi, 0, ?_⟩
    simpa using Finsupp.support_single_subset hm

Goal state after:
case mpr
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] := ⋯
⊢ x ∈ RHS → x ∈ Ideal.span (of' k A '' s)
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
    multinomial, mul_assoc, mul_left_comm _ (f a)!,
    Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
    Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
  positivity

Goal state after:
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:
by
  rw [← cons_eq_insert _ _ ha, multinomial_cons]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) ≠ n
⊢ coeff s ((linearCombination R X) a ^ n) = 0

Tactic:
simp only [sum, linearCombination_apply, Finset.sum_pow_eq_sum_piAntidiag, coeff_sum, ← map_pow,
    ← C_eq_coe_nat, coeff_C_mul, smul_eq_C_mul, mul_pow, Finset.prod_mul_distrib, ← map_prod,
    coeff_prod_X_pow, mul_ite, mul_one, mul_zero]
  apply Finset.sum_eq_zero (fun x hx ↦ ?_)
  rw [if_neg]
  rintro ⟨rfl⟩
  apply hs
  simp only [Finset.mem_piAntidiag] at hx
  rw [sum_of_support_subset _ (support_indicator_subset a.support _) _ (by simp), ← hx.1]
  congr
  ext i
  by_cases hi : i ∈ a.support
  · simp [Finsupp.indicator_of_mem hi]
  · grind [Finsupp.indicator_of_notMem hi]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
    (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ p = 0

Tactic:
| succ n ih =>

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ degreeOf j (C c * p) = degreeOf j p

Tactic:
classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul']
  · simp
  · have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
    simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]
    contrapose hp'
    ext m
    apply hc.1
    simpa using congr_arg (coeff m) hp'

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
n : ℕ
hf : m.Monic f
⊢ m.Monic (f ^ n)

Tactic:
nontriviality R
  rw [Monic, leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, hf.leadingCoeff_eq_one, one_pow]
  rw [hf.leadingCoeff_eq_one, one_pow]
  exact one_ne_zero

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.Monic (∏ i ∈ s, P i)

Tactic:
rw [Monic, leadingCoeff_prod_of_regular]
  · exact Finset.prod_eq_one H
  · intro i hi
    rw [(H i hi).leadingCoeff_eq_one]
    exact isRegular_one

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

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

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

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

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ p ∈ s

Tactic:
← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq

Goal state after:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ q ∈ s
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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

Tactic:
by
  by_cases hf : m.degree f = 0 ∧ m.degree g = 0
  · rcases hf with ⟨h₁, h₂⟩
    right
    suffices C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0 by simp_all [sPolynomial_def]
    nth_rewrite 1 [degree_eq_zero_iff.mp h₁]
    nth_rewrite 2 [degree_eq_zero_iff.mp h₂]
    ring
  · rw [or_iff_not_imp_right]
    intro hs
    apply (m.degree_sPolynomial_le f g).lt_of_ne
    apply m.toSyn.injective.ne
    contrapose hs
    rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero]

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

Goal state before:
pp: case neg
d n : ℕ
f : Fin d → ℕ
h : ¬0 < n
⊢ f ∈ ∅ ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
· simp only [not_lt, nonpos_iff_eq_zero] at h
    simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]

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

Goal state before:
pp: d n : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag n ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
by
  unfold finMulAntidiag
  split_ifs with h
  · 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]
    constructor
    · rintro ⟨a, ha_mem, rfl⟩
      exact ⟨ha_mem, h.ne.symm⟩
    · rintro ⟨rfl, _⟩
      refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
      apply Nat.pos_of_ne_zero
      exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)
  · simp only [not_lt, nonpos_iff_eq_zero] at h
    simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]

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

Goal state before:
pp: case neg.succ
m : ℕ
hm : ¬m = 0
n : ℕ
ih : Ω (m ^ n) = n * Ω m
⊢ Ω (m ^ (n + 1)) = (n + 1) * Ω m

Tactic:
| succ n ih =>

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

Goal state before:
pp: case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ x, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0

Tactic:
rw [← Finset.mul_prod_erase (h := mem_univ i),
      ← Finset.mul_prod_erase (a := i')]

Goal state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0

case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ f n * ∑ m ∈ Ioc 0 (N / n), ↑zeta m = f n * ↑(N / n)

Tactic:
simp_rw [natCoe_apply]

Goal state after:
R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ f n * ∑ m ∈ Ioc 0 (N / n), ↑(zeta m) = f n * ↑(N / n)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb :
  b ∈
    {x ∈ n.divisors ×ˢ n.divisors |
      match x with
      | (x, y) => x.lcm y = n}
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), f a ha = b

Tactic:
dsimp only at hb

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), f a ha = b
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₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) * m.sPolynomial p₁ p₂

Tactic:
by
  classical
  simp only [sPolynomial_def]
  wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  rcases H with ⟨hc1, hc2, hp1, hp2⟩
  have hm1 := (monomial_eq_zero (s := d₁)).not.mpr hc1
  have hm2 := (monomial_eq_zero (s := d₂)).not.mpr hc2
  simp_rw [m.degree_mul hm1 hp1, m.degree_mul hm2 hp2,
    mul_sub, ← mul_assoc _ _ p₁, ← mul_assoc _ _ p₂, monomial_mul,
    m.leadingCoeff_mul, m.leadingCoeff_monomial,
    degree_monomial, hc1, hc2, reduceIte, mul_right_comm, mul_comm c₂ c₁]
  rw [tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_eq_add_tsub le_sup_left, tsub_add_eq_add_tsub le_sup_right,
    add_comm d₁, add_comm d₂, add_tsub_add_eq_tsub_right, add_tsub_add_eq_tsub_right]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn f (g ∘ ⇑σ) ↑s

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
    hfg.sum_smul_comp_perm_le_sum_smul hσ]

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

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ = ⊤ ↔ r = ∞

Tactic:
cases r

Goal state after:
case top
⊢ ⌊∞⌋ₑ = ⊤ ↔ ∞ = ∞

case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ = ⊤ ↔ ↑x✝ = ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌈r⌉ₑ = ⊤ ↔ r = ∞

Tactic:
cases r

Goal state after:
case top
⊢ ⌈∞⌉ₑ = ⊤ ↔ ∞ = ∞

case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ = ⊤ ↔ ↑x✝ = ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ < ⊤ ↔ r < ∞

Tactic:
cases r

Goal state after:
case top
⊢ ⌊∞⌋ₑ < ⊤ ↔ ∞ < ∞

case coe
x✝ : ℝ≥0
⊢ ⌊↑x✝⌋ₑ < ⊤ ↔ ↑x✝ < ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌈r⌉ₑ < ⊤ ↔ r < ∞

Tactic:
cases r

Goal state after:
case top
⊢ ⌈∞⌉ₑ < ⊤ ↔ ∞ < ∞

case coe
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ < ⊤ ↔ ↑x✝ < ∞
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
⊢ n ≤ ⌊r⌋ₑ ↔ ↑n ≤ r

Tactic:
cases r

Goal state after:
case top
n : ℕ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ ↑n ≤ ∞

case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ n ≤ ⌊↑x✝⌋ₑ ↔ ↑n ≤ ↑x✝
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
⊢ ⌈r⌉ₑ ≤ n ↔ r ≤ ↑n

Tactic:
cases r

Goal state after:
case top
n : ℕ∞
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ ↑n

case coe
n : ℕ∞
x✝ : ℝ≥0
⊢ ⌈↑x✝⌉ₑ ≤ n ↔ ↑x✝ ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Extended

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

Tactic:
simp [← lt_add_one_iff hn]

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

Goal state before:
pp: r : ℝ≥0∞
n : ℕ
hn₀ : ↑n ≠ 0
⊢ ↑n ≤ ⌈r⌉ₑ ↔ ↑↑n - 1 < r

Tactic:
cases r

Goal state after:
case top
n : ℕ
hn₀ : ↑n ≠ 0
⊢ ↑n ≤ ⌈∞⌉ₑ ↔ ↑↑n - 1 < ∞

case coe
n : ℕ
hn₀ : ↑n ≠ 0
x✝ : ℝ≥0
⊢ ↑n ≤ ⌈↑x✝⌉ₑ ↔ ↑↑n - 1 < ↑x✝
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Goal state after:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd : d < a * b
⊢ d ≤ c
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) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
by
  classical rw [Ioc, Ioc, ← Finset.image_add_left_Ioc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ↑(⋯.min ⋯) ≤ ↑g

Tactic:
WithTop.coe_le_coe

Goal state after:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g
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

pp: case neg
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:
case neg
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
Module: Mathlib.RingTheory.HahnSeries.Addition

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

Tactic:
WithTop.coe_le_coe

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
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

pp: case neg
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:
case neg
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
Module: Mathlib.Algebra.Order.Module.PositiveLinearMap

Goal state before:
pp: case succ
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid E₁
inst✝⁸ : PartialOrder E₁
inst✝⁷ : AddCommMonoid E₂
inst✝⁶ : PartialOrder E₂
inst✝⁵ : AddCommMonoid E₃
inst✝⁴ : PartialOrder E₃
inst✝³ : Module R E₁
inst✝² : Module R E₂
inst✝¹ : Module R E₃
inst✝ : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
n : ℕ
ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
⊢ ((n + 1) • f.toLinearMap).toFun x ≤ ((n + 1) • f.toLinearMap).toFun y

Tactic:
| succ n ih =>

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

Goal state before:
pp: case mp.inl
Γ : 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⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
⊢ (∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b

Tactic:
refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩

Goal state after:
case mp.inl
Γ : 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⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
j : Γ
hjk : j < k
⊢ (ofLex a).coeff j = (ofLex b).coeff j
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : ¬(of R).symm (x • y) = 0
⊢ ↑(⋯.min ⋯) ≤ ↑(⋯.min ⋯)

Tactic:
WithTop.coe_le_coe

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : ¬(of R).symm (x • y) = 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
⊢ mk x + mk y + z = mk x + (mk y + z)

Tactic:
induction z with | mk z
   =>  _ 

Goal state after:
case mk.mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : R
⊢ mk x + mk y + mk z = mk x + (mk y + mk z)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal (⋯.min ⋯ + ⋯.min ⋯) ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (x.orderTop.untop ⋯) • ((of R).symm y).leadingCoeff

Tactic:
HahnSeries.leadingCoeff_of_ne_zero hy,

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ∑ ij ∈ VAddAntidiagonal (⋯.min ⋯ + ⋯.min ⋯) ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (x.orderTop.untop ⋯) • ((of R).symm y).coeff (((of R).symm y).orderTop.untop ⋯)
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
c : FiniteArchimedeanClass M
hc : c ∈ ↑f.support
d : FiniteArchimedeanClass M
hd : d ∈ ↑f.support
h : c < d
⊢ ↑(f d) ≠ 0

Tactic:
by simpa using! hd

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
hna : IsNonarchimedean f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Tactic:
by
  simpa [Finset.le_sup'_iff] using IsNonarchimedean.apply_sum_le_sup hna ht

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

pp: case neg
Γ : 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:
case neg
Γ : 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
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
hx' : mk x ≠ ⊤
⊢ mk x + mk x⁻¹ = mk x + mk y⁻¹

Tactic:
nth_rw 2 [h]

Goal state after:
case inr.inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
hx' : mk x ≠ ⊤
⊢ mk x + mk x⁻¹ = mk y + mk y⁻¹
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

pp: case neg
Γ : 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:
case neg
Γ : 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
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
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ (x * y).order

Tactic:
order_of_ne <| ne_zero_of_coeff_ne_zero hxy,

Goal state after:
Γ : 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.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ ⋯.min ⋯