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

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

Tactic:
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
  · intro a
    simp only [Multiset.mem_filter, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
      mem_divisors]
    constructor
    · rintro ⟨⟨an, h0⟩, hsq⟩
      use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
      simp only [Finset.mem_powerset]
      rcases an with ⟨b, rfl⟩
      rw [mul_ne_zero_iff] at h0
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
      rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
        normalizedFactors_mul h0.1 h0.2]
      exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩
    · rintro ⟨s, hs, rfl⟩
      rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
      have hs0 : s.val.prod ≠ 0 := by
        rw [Ne, Multiset.prod_eq_zero_iff]
        intro con
        apply
          not_irreducible_zero
            (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
      rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]
      refine ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, ?_⟩
      have h :=
        UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
          (fun x hx =>
            irreducible_of_normalized_factor x
              (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
          (prod_normalizedFactors hs0)
      rw [associated_eq_eq, Multiset.rel_eq] at h
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
      apply s.nodup
  · intro x hx y hy h
    rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
    rw [← Finset.mem_def, Finset.mem_powerset] at hx hy
    apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
    · intro z hz
      apply irreducible_of_normalized_factor z
      · rw [← Multiset.mem_toFinset]
        apply hx hz
    · intro z hz
      apply irreducible_of_normalized_factor z
      · rw [← Multiset.mem_toFinset]
        apply hy hz

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ d ∈ n.divisors with Squarefree d, f d = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod

Tactic:
rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map,
    Finset.sum_eq_multiset_sum]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
obtain rfl | hs := S.eq_empty_or_nonempty
      · simp
      simp_rw [totalDegree, Nat.cast_finsetSup]
      rw [sup_div₀ (by positivity)]
      simp [← sum_div, Finsupp.sum_fintype]

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

Goal state before:
pp: k x✝ : ℕ
⊢ (ζ * pow k) x✝ = (σ k) x✝

Tactic:
rw [sigma, zeta_mul_apply]

Goal state after:
k x✝ : ℕ
⊢ ∑ i ∈ x✝.divisors, (pow k) i = { toFun := fun n ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
Multiset.coe_card

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ m.primeFactorsList.length + n.primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ ω n = 0 ↔ n ≤ 1

Tactic:
by
  simp [cardDistinctFactors_apply, le_one_iff_eq_zero_or_eq_one]

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

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)

Tactic:
induction s using cons_induction_on with
  | empty => simp
  | cons a s ha ih =>
    rw [prod_cons, sum_cons, cardDistinctFactors_mul, ih]
    · exact fun x hx y hy hxy => h (by simp [hx]) (by simp [hy]) hxy
    · exact Coprime.prod_right fun i hi =>
        h (by simp) (by simp [hi]) (ne_of_mem_of_not_mem hi ha).symm

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ #(m * n).divisors = #m.divisors * #n.divisors

Tactic:
by
  simp only [← sigma_zero_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

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

Goal state before:
pp: case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬p ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp✝, ↑p

Tactic:
rw [Prime.dvd_finsetProd_iff hp.1.prime]

Goal state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬∃ a ∈ {p_1 ∈ n.primeFactors.attach | g ↑p_1 ⋯ = f p hp✝}, p ∣ ↑a
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case pos.inl
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
s : Finset ι
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
x : ι
has : x ∉ s
hamax : ∀ x_1 ∈ s, toLex (g x_1, f x_1) ≤ toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := Equiv.trans σ (Equiv.swap x (σ x))
hτ : τ = Equiv.trans σ (Equiv.swap x (σ x))
h₁ : σ x = x
hx : ¬σ x = x
⊢ x ∈ ↑s

pp: case pos.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : σ x = a
hx : ¬σ a = x
hax : x ≠ a
⊢ x ∈ ↑s

Tactic:
· contradiction

Goal state after:
case pos.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : σ x = a
hx : ¬σ a = x
hax : x ≠ a
⊢ x ∈ ↑s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : y = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
simp only [hy, f.map_zero, mul_zero, lcm_zero_right, gcd_zero_right, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
by_cases h : m = 1

Goal state after:
case pos
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : m = 1
⊢ 1 (m * n) = 1 m * 1 n

case neg
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : ¬m = 1
⊢ 1 (m * n) = 1 m * 1 n
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inl
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
⊢ i = (Finset.cons i s hi).min' ⋯

Tactic:
apply le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ (by simp))

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
⊢ ∀ y ∈ Finset.cons i s hi, i ≤ y
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
⊢ (0 + a - 1) / a = 0

Tactic:
cases a <;> simp [Nat.div_eq_zero_iff]

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
⊢ (if h : a = 1 then ⊤ else ↑(f ⟨a, h⟩)) = if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)

Tactic:
split_ifs with ha hb hb
    · rfl
    · exact (hb (MulArchimedeanClass.mk_eq_top_iff.mp (ha ▸ h').symm)).elim
    · exact (ha (MulArchimedeanClass.mk_eq_top_iff.mp (by apply hb ▸ h'))).elim
    · rw [h ⟨a, ha⟩ ⟨b, hb⟩ (by simpa [mk] using h')]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a', a' > a ∧ a' * b < c
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∉ ⇑f '' x.support
⊢ g ∉ (embDomain f x).support

Tactic:
rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff (f g) = (embDomain f y).coeff (f g)
⊢ x.coeff g = y.coeff g

Tactic:
rwa [embDomain_coeff, embDomain_coeff] at xyg

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

Goal state before:
pp: case inr.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
this : ¬0 < a + b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ Covariant α α (fun x1 x2 ↦ x1 * x2) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by
    intro _ _ _; simp only; intro
    rwa [← left_eq_sup, ← mul_sup_distrib, sup_of_le_left]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℤ
⊢ f ↑n ≤ 1

Tactic:
obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑↑a ≤ 1

case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑(-↑a) ≤ 1
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
f_zero : f 0 = 0
f_nonneg : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
g : β → α
t : Finset β
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i)

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
f_zero : f 0 = 0
f_nonneg : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
g : β → α
⊢ ∃ i, (∅.Nonempty → i ∈ ∅) ∧ f (∅.sum g) ≤ f (g i)

case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
f_zero : f 0 = 0
f_nonneg : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ i, (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i)
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)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f ((f.support.erase (f.support.min' hsupport)).min' hsupport')) ≠ 0

Tactic:
by
      simpa using! (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2

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

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ ((single b) r * x).coeff a = r * x.coeff (a - b)

Tactic:
simpa using coeff_single_mul_add (a := a - b) (b := b)

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
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  apply orderTop_mul_of_ne_zero
  simp_all

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

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1 → 0 < (x - 1).orderTop

Tactic:
intro h
    refine lt_of_le_of_ne (le_of_eq_of_le (by simp_all)
      (min_orderTop_le_orderTop_sub (Γ := Γ) (R := R))) <| Ne.symm <|
      orderTop_sub_ne h.1 orderTop_one ?_
    rw [h.2, leadingCoeff_one]

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

Goal state before:
pp: case inr.refine_2
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.leadingCoeff = 1

Tactic:
simpa [this.2, y.val_inv] using (leadingCoeff_mul_of_ne_zero nz).symm

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case refine_1
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂

pp: case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂

Tactic:
· exact .trans (.single <| .inr (symm hx)) <| .trans h (.single <| .inr hy)

Goal state after:
case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this : HasMemOrNegMem P
⊢ P.IsOrdering

Tactic:
refine IsOrdering.mk' P (fun {x y} _ => ?_)

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
⊢ x ∈ P.support ∨ y ∈ P.support
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✝⁴ : PartialOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommSemiring R
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A⟦Γ⟧
x✝ : Γ
⊢ r • x.coeff x✝ = x.coeff x✝ * (algebraMap R A) r

Tactic:
rw [← Algebra.commutes, Algebra.smul_def]

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

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ↑b = 0
⊢ a * 0 = b ∨ b * 0 = a

Tactic:
left

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ↑b = 0
⊢ a * 0 = b
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : ↑b / ↑a ∈ A
⊢ a * ⟨↑b / ↑a, hh⟩ = b ∨ b * ⟨↑b / ↑a, hh⟩ = a

Tactic:
left

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : ↑b / ↑a ∈ A
⊢ a * ⟨↑b / ↑a, hh⟩ = b
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) = 1

Tactic:
rw [← π.map_one, ← sub_eq_zero, ← π.map_sub, Ideal.Quotient.eq_zero_iff_mem, valuation_lt_one_iff]

Goal state after:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ A.valuation ↑(↑(A.unitGroupMulEquiv x) - 1) < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ A.unitGroup.subtype x✝ ∈ A.principalUnitGroup

Tactic:
Subgroup.coe_subtype,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ ↑x✝ ∈ A.principalUnitGroup
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
hieq : i = FiniteArchimedeanClass.mk (↑y - x) hxy0
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

Tactic:
exact hieq ▸ hi

Goal state after:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ eval 1 p.mirror = eval 1 p

Tactic:
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x = ∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize n) = p

Tactic:
aeval_homogenize_of_eq_one

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (aeval (![X, 1] 0)) p = p

case hn
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p.natDegree ≤ n

case hg
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ![X, 1] 1 = 1
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
r s : R[X]
hr : (r * q).smeval x = r.smeval x * q.smeval x
hs : (s * q).smeval x = s.smeval x * q.smeval x
⊢ ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x

Tactic:
simp only [hr, hs, smeval_add, add_mul]

Goal state after: