mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Tactic:
dsimp only

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff d f * coeff e g = 0
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2

Tactic:
have (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b ∨ b ≠ a) :
      {z ∈ s.offDiag | Sym2.mk.uncurry z = s(a, b)} = .cons (a, b) {(b, a)}
        (by simpa [eq_comm] using hab) := by aesop

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this :
  ∀ (a b : α),
    a ∈ s → b ∈ s → ∀ (hab : a ≠ b ∨ b ≠ a), {z ∈ s.offDiag | uncurry Sym2.mk z = s(a, b)} = cons (a, b) {(b, a)} ⋯
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : { P // (P.sum fun x ↦ id) = n }
⊢ ((↑f).extendDomain.sum fun x x_1 ↦ x_1) = n

Tactic:
by simpa [sum] using f.2

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

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ¬p ∣ n ↔ ¬p ∣ m
⊢ n.factorization p = m.factorization p

Tactic:
hp.dvd_iff_one_le_factorization hn.ne_zero,

Goal state after:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ¬1 ≤ n.factorization p ↔ ¬p ∣ m
⊢ n.factorization p = m.factorization p
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toWithBotSyn ↑d ≤ m.toWithBotSyn (m.withBotDegree f)

Tactic:
classical
  simp [withBotDegree_eq, toWithBotSyn_apply, ne_zero_iff.mpr ⟨d, by simpa using hd⟩, le_degree hd]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ ↑ζ i.1 • f i.2 = f i.2

Tactic:
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]

Goal state after:
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
⊢ max (m.toSyn (m.degree f)) (m.toSyn (m.degree (-g))) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
rw [degree_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 0 = ↑ζ

Tactic:
by rw [ppow, dif_pos rfl]

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

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero

Goal state after:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
⊢ (∏ p ∈ s, p).primeFactors = s
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ a.factorization p = 0 ∨ b.factorization p = 0

Tactic:
← Finsupp.notMem_support_iff,

Goal state after:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ∉ a.factorization.support ∨ b.factorization p = 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ∉ a.factorization.support ∨ b.factorization p = 0

Tactic:
← Finsupp.notMem_support_iff,

Goal state after:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left✝ : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ∉ a.factorization.support ∨ p ∉ b.factorization.support
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : { n // IsPrimePow n }
⊢ ↑((fun pk ↦ ⟨↑pk.1 ^ (pk.2 + 1), ⋯⟩) ((fun n ↦ (⟨(↑n).minFac, ⋯⟩, (↑n).factorization (↑n).minFac - 1)) n)) = ↑n

Tactic:
dsimp only

Goal state after:
n : { n // IsPrimePow n }
⊢ (↑n).minFac ^ ((↑n).factorization (↑n).minFac - 1 + 1) = ↑n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case cons
ι : 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)
⊢ (f a).Coprime (∏ x ∈ s, f x)

Tactic:
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.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1

pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i

Tactic:
· rw [Nat.primeFactorsPiBij, ← prod_filter]
    congr
    grind

Goal state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if ↑p ∣ t i then ↑p else 1) = t i
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2

Tactic:
dsimp only

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

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

Tactic:
by
  have key : ∀ x ∈ hs.toFinset, s.indicator (fun _ ↦ a) x = a := by
    intro x hx
    rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]
  rw [Nat.card_eq_card_finite_toFinset hs, ← sum_eq_card_nsmul key, eventually_atTop]
  obtain ⟨m, hm⟩ := hs.bddAbove
  refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩ <;> intro x <;> rw [hs.mem_toFinset]
  · rw [Finset.mem_range]
    exact fun x_s ↦ ((mem_upperBounds.1 hm) x x_s).trans_lt (Nat.lt_of_succ_le n_m)
  · exact fun _ x_s ↦ indicator_of_notMem x_s (fun _ ↦ a)

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)

Tactic:
rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 < a * a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
· rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd

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

Goal state before:
pp: 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 : ℚ
⊢ ∀ {a b : β}, (↑↑(inducedOrderRingHom β γ).toRingHom).toFun a ≤ (↑↑(inducedOrderRingHom β γ).toRingHom).toFun b ↔ a ≤ b

Tactic:
by
      dsimp
      refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
      convert! inducedMap_mono γ β h <;>
      · rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
        dsimp
        rw [inducedMap_inv_self β γ _]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1 + 1) = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i

Tactic:
rw [pow_succ]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i) ≤ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
gcongr _ * ?_

Goal state after:
case hbc
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Tactic:
rw [div_pow, div_le_div_iff₀ (by positivity) (by positivity), sq (#s : α), mul_left_comm,
    ← mul_assoc]

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (↑(#s) * ∑ i ∈ s, f i ^ 2) * ↑(#s)
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
ha : a ≠ 1
x✝ : mk a ≤ mk b
n : ℕ
hn : |MulArchimedeanOrder.val (MulArchimedeanOrder.of b)|ₘ ≤ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n
⊢ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n < |a|ₘ ^ (n + 1)

Tactic:
rw [pow_succ]

Goal state after:
case refine_1
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : a ≠ 1
x✝ : mk a ≤ mk b
n : ℕ
hn : |MulArchimedeanOrder.val (MulArchimedeanOrder.of b)|ₘ ≤ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n
⊢ |MulArchimedeanOrder.val (MulArchimedeanOrder.of a)|ₘ ^ n < |a|ₘ ^ n * |a|ₘ
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ max |y|ₘ |z|ₘ
⊢ min (mk y) (mk z) ≤ mk x

Tactic:
← mabs_of_one_le (le_max_of_le_left (one_le_mabs y))

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
⊢ min (mk y) (mk z) ≤ mk x
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → 1 (m * n) = 1 m * 1 n

Tactic:
intro m n hm hn hmn
    by_cases h : m = 1 <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hk : (f ^ k).IsMultiplicative
⊢ (f ^ (k + 1)).IsMultiplicative

Tactic:
rw [pow_succ]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hk : (f ^ k).IsMultiplicative
⊢ (f ^ k * f).IsMultiplicative
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
inst✝ : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ mk a ha = mk b hb

Tactic:
simpa [mk] using MulArchimedeanClass.mk_eq_mk_of_mulArchimedean ha hb

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

Goal state before:
pp: K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a : K
n : ℕ
⊢ ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos
  · simp
  nth_rw 2 [← div_mul_cancel₀ (a := a) (b := ↑n) (by positivity)]
  rw [mul_cast_floor_div_cancel (Nat.ne_zero_of_lt hn)]

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑↑n⌋ₑ = ⌊↑r⌋ₑ + ↑n

Tactic:
by
    -- FIXME: Why does `norm_cast` not use `ENNReal.ofNNReal_add_natCast`?
    norm_cast; rw [← ENNReal.ofNNReal_add_natCast]; norm_cast; exact n.floor_add_natCast zero_le

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)

Tactic:
← two_nsmul_sup_eq_add_add_abs_sub x y,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • 2 • (x ⊔ y)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred h

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
by
  simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

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 : R⟦Γ⟧
a : Γ
⊢ { coeff := fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a

Tactic:
dsimp only

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (fun x ↦ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ })
      ((fun x ↦ { coeff := fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x) =
    x

Tactic:
apply AddOpposite.unop_injective

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ AddOpposite.unop
      ((fun x ↦ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ })
        ((fun x ↦ { coeff := fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x)) =
    AddOpposite.unop x
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
⊢ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ } =
    AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
      AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ }

Tactic:
apply AddOpposite.unop_injective

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
⊢ AddOpposite.unop (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ }) =
    AddOpposite.unop
      (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
        AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ })
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff

Tactic:
apply AddOpposite.unop_injective

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ AddOpposite.unop (addOppositeEquiv.symm x).leadingCoeff =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₁.h
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
order : Γ
coeff : FiniteArchimedeanClass R
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R)) (toLex (order, coeff)) =
    OrderHom.id (toLex (order, coeff))

Tactic:
induction coeff using FiniteArchimedeanClass.ind with | mk a ha
     =>  _ 

Goal state after:
case h₁.h.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
order : Γ
a : R
ha : a ≠ 0
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R))
      (toLex (order, FiniteArchimedeanClass.mk a ha)) =
    OrderHom.id (toLex (order, FiniteArchimedeanClass.mk a ha))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
⊢ (finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R) = OrderHom.id

Tactic:
· ext x
    induction x using FiniteArchimedeanClass.ind with | mk a ha
    simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex,
      archimedeanClassMk_eq_archimedeanClassMk_iff, ha]

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
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : y + x = z + x
⊢ y = z

Tactic:
simp_rw [← add_comm x] at h

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z
Module: Mathlib.RingTheory.HahnSeries.Multiplication

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

Tactic:
· rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
      exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
⊢ ↑↑f x = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))

Tactic:
rw [← f.prop.baseEmbedding_le.2 heq]

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
⊢ ↑seed.baseEmbedding ⟨↑x, hx'⟩ = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ'
hg : (embDomain f x * embDomain f y).coeff g ≠ 0
⊢ g ∈ Set.range ⇑f

Tactic:
obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset ((mem_support _ _).2 hg)

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
w✝¹ : Γ'
hi : w✝¹ ∈ (embDomain f x).support
w✝ : Γ'
hj : w✝ ∈ (embDomain f y).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 ↦ x1 + x2) w✝¹ w✝) ≠ 0
⊢ (fun x1 x2 ↦ x1 + x2) w✝¹ w✝ ∈ Set.range ⇑f