mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : (ι → ℝ) ≃L[ℝ] E := (EuclideanSpace.equiv ι ℝ).symm.trans (↑((stdOrthonormalBasis ℝ E).reindex e).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
    volume (⇑f ⁻¹' s) / ENNReal.ofReal (covolume (ZLattice.comap ℝ L ↑↑f) volume)

Tactic:
← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
    (b.ofZLatticeComap ℝ L f.toLinearEquiv),

Goal state after:
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s volume
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : (ι → ℝ) ≃L[ℝ] E := (EuclideanSpace.equiv ι ℝ).symm.trans (↑((stdOrthonormalBasis ℝ E).reindex e).repr).symm
hf : MeasurePreserving (⇑f) volume volume
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
    volume (⇑(Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L ↑↑f) (Basis.ofZLatticeComap ℝ L (↑f) b)).equivFun '' ⇑f ⁻¹' s)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹

Tactic:
by
  refine Nat.le_induction ?_ ?_ n h
  · simp only [Ioc_self, sum_empty, sub_self, le_refl]
  intro n hn IH
  rw [sum_Ioc_succ_top hn]
  grw [IH]
  push_cast
  have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
  field_simp
  linarith

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

Goal state before:
pp: σ R : Type u
inst✝ : CommSemiring R
⊢ max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀

Tactic:
rw [lift_id, lift_id]

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = ↑s.multinomial * (a i ^ s i * (erase i s).prod fun r m ↦ a r ^ m)

Tactic:
hai,

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
i : σ
hsi : ¬s i = 0
hai : a i = 0
⊢ 0 = ↑s.multinomial * (0 ^ s i * (erase i s).prod fun r m ↦ a r ^ m)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (⇑(toFinsupp m)) a✝ 0 a

Tactic:
not_ne_iff.1 h,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (⇑(toFinsupp m)) a 0 a
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.f
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
⊢ X i ∣ r → p ∣ q

Tactic:
rintro ⟨r, rfl⟩

Goal state after:
case mp.f
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
⊢ p ∣ q
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k

Tactic:
induction k with
  | zero => simp
  | succ k hk =>
    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
    ring

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : i = k
hs : s k (x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
subst hik

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
⊢ Acc (DFinsupp.Lex r s) x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
refine Lex.acc_of_single hbot x fun j hj ↦ ?_
    obtain rfl | hij := eq_or_ne j i
    · exact ha _ hs
    by_cases h : r j i
    · rw [hr j h, single_eq_of_ne hij, single_zero]
      exact Lex.acc_zero hbot
    · exact ih _ ⟨h, hij⟩ _

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : C (coeff 0 f) ∣ C a
this : f = C (coeff 0 f)
⊢ coeff 0 f ∣ a

Tactic:
C_dvd_iff_dvd_coeff

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : ∀ (i : σ →₀ ℕ), coeff 0 f ∣ coeff i (C a)
this : f = C (coeff 0 f)
⊢ coeff 0 f ∣ a
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
n✝ n k : ℕ
s : { s // 0 ∉ s }
v : Fin (n.succ + 1)
hv : v ∈ ↑s
⊢ (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v

Tactic:
exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ Irreducible x

Tactic:
Nat.irreducible_iff_prime,

Goal state after:
n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ _root_.Prime x
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
hlts : 0 < s
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
rw [hsb] at hsa hn hlts

Goal state after:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : IsPrimePow n
⊢ n.minFac ^ n.factorization n.minFac = n

Tactic:
by
  obtain ⟨p, k, hp, hk, rfl⟩ := hn
  rw [← Nat.prime_iff] at hp
  rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit (f 1) → IsUnit f

Tactic:
suffices Invertible (f 1) → Invertible f by simpa using Nonempty.map this

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ Invertible (f 1) → Invertible f
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.fst.fst
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).1.1 = ((c1, c2), d1, d2).1.1

Tactic:
trans gcd (a1 * a2) (a1 * b1)
      · rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]

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

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

Tactic:
rw [cutMap_coe] at h

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr.inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
⊢ (inducedAddHom α β) (0 * 0) = (inducedAddHom α β) 0 * (inducedAddHom α β) 0

Tactic:
simp only [mul_zero, map_zero]

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

Goal state before:
pp: case empty
ι : 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 : ι → β
σ : Perm ι
hfg : MonovaryOn f g ↑∅
hσ : {x | σ x ≠ x} ⊆ ↑∅
⊢ ∑ i ∈ ∅, f i • g (σ i) ≤ ∑ i ∈ ∅, f i • g i

Tactic:
simp only [le_rfl, Finset.sum_empty]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : |a|ₘ ^ 1 < |b|ₘ
⊢ b < a

Tactic:
rw [mabs_eq_inv_self.mpr ha, mabs_eq_inv_self.mpr hb] at h

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : a⁻¹ ^ 1 < b⁻¹
⊢ b < a
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈1⌉ₑ = 1

Tactic:
simpa using ceil_natCast 1

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
⊢ mk (k • a) = mk a

Tactic:
have : Nontrivial K := nontrivial_iff.mpr ⟨k, 0, h⟩
  obtain ⟨m, hm⟩ := Archimedean.arch 1 (show 0 < |k| by simpa using h)
  obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)
  simp_rw [mk_eq_mk, abs_smul]
  refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩
  · rw [← smul_assoc]
    exact le_smul_of_one_le_left (by simp) hm
  · have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
    rw [this]
    exact smul_le_smul_of_nonneg_right hn (by simp)

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩ <;> apply NonemptyInterval.ext

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (pure s.toProd.1).toProd

case refine_1.refine_2
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ t.toProd = (pure t.toProd.1).toProd
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : ¬r = 0
⊢ ↑a ≤ ((single a) r).orderTop

Tactic:
rw [orderTop_single hr]

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg
    simp

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg
    simp

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

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

Tactic:
· intro ⟨i, hj, hi⟩
    have horder : (ofLex x).orderTop = WithTop.some i := by
      apply orderTop_eq_of_le
      · simpa using hi.ne.symm
      · intro g hg
        contrapose! hg
        simpa using (hj g hg).symm
    have htop : (ofLex x).orderTop ≠ ⊤ := WithTop.ne_top_iff_exists.mpr ⟨i, horder.symm⟩
    have hne : ofLex x ≠ 0 := orderTop_ne_top.1 htop
    have horder' : (ofLex x).orderTop.untop htop = i := (WithTop.untop_eq_iff _).mpr horder
    rw [leadingCoeff_of_ne_zero hne, horder']
    simpa using hi

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

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

Tactic:
mk_map_of_archimedean' f hy.ne'

Goal state after:
case h
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 < 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
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
r s : S
hr : f r ≤ x
hs : x ≤ f s
⊢ 0 ≤ min (mk (f r)) (mk (f s))

Tactic:
simp [mk_map_nonneg_of_archimedean]

Goal state after:
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✝ : NonAssocSemiring R
x : R⟦Γ⟧
⊢ 1 * x = x

Tactic:
ext
    exact coeff_single_zero_mul.trans (one_mul _)

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

Goal state before:
pp: case inr
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 y : ↥(↑f).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
rw [← archimedeanClassMk_eq_iff]

Goal state after:
case inr
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 y : ↥(↑f).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case hfg
Γ : 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
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ j ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    j ≠ (a, x.order) → y.coeff j.1 * x.coeff j.2 = z.coeff j.1 * x.coeff j.2

Tactic:
simp +contextual only [mem_union, mem_antidiagonal, mul_eq_mul_right_iff, Prod.mk.injEq,
        ne_eq, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]

Goal state after:
case hfg
Γ : 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
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ (a_1 b : Γ),
    ¬y.coeff a_1 = 0 ∨ ¬z.coeff a_1 = 0 →
      ¬x.coeff b = 0 → a_1 + b = a + x.order → (a_1 = a → ¬b = x.order) → y.coeff a_1 = z.coeff a_1
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy x : (i : ι) → A i
⊢ (x ∈ Set.range fun s ↦ star s * s) ↔ x ∈ Set.univ.pi fun i ↦ Set.range fun s ↦ star s * s

Tactic:
simp only [Set.mem_range, funext_iff, mul_apply, star_apply, Set.mem_pi,
        Set.mem_univ, forall_const]

Goal state after:
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy x : (i : ι) → A i
⊢ (∃ y, ∀ (x_1 : ι), star (y x_1) * y x_1 = x x_1) ↔ ∀ (i : ι), ∃ y, star y * y = x 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
⊢ f.eval x ≠ ↑↑f y

Tactic:
have := val_sub_ne_zero f hx y
  rw [sub_ne_zero, ne_comm, ← sub_ne_zero] at this
  let xy := mk _ this
  have hxy : x - y.val ∈ closedBall K xy := fun _ ↦ by simp; rfl
  rw [← seed.ball_sup_stratum_eq xy, Submodule.mem_sup] at hxy
  obtain ⟨u, hu, v, hv, huv⟩ := hxy
  have huv' : x - y.val - v = u := by simp [← huv]
  rw [mem_ball_iff K] at hu
  -- `z = x - u = y + v` is also in the domain.
  -- Assuming `f.eval x = f.val y` allows us to use `archimedeanClassMk_le_of_eval_eq` on `z`
  have hyv : y.val + v ∈ f.val.domain := Submodule.add_mem _ (by simp) (f.mem_domain hv)
  by_contra! h
  obtain h := f.archimedeanClassMk_le_of_eval_eq h ⟨y.val + v, hyv⟩
  contrapose! h
  simp_rw [← sub_sub, huv']
  obtain rfl | ne := eq_or_ne u 0
  exacts [Ne.lt_top (by simpa), (mk_lt_mk ..).mp (hu ne)]

Goal state after: