mathlib-initiative/mathlib-tactics huggingface dataset:
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 + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ ≠ 0 ∧ (eval x) p = 0}) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
rw [← filter_filter, filter_piFinset_eq_map_consEquiv S (fun r ↦ eval r pₖ ≠ 0),
              filter_map, card_map, product_eq_biUnion_right, filter_biUnion]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ #({r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}.biUnion fun a ↦
        filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding) (image (fun a_1 ↦ (a_1, a)) (S 0))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))
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
⊢ n.factorization p = m.factorization p

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

Tactic:
· have h₁ := h _ hp
    rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff,
      hp.dvd_iff_one_le_factorization hm.ne_zero, not_le, lt_one_iff] at h₁
    have h₂ := hn.natFactorization_le_one p
    have h₃ := hm.natFactorization_le_one p
    lia

Goal state after:
case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ 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 g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
nontriviality R using Subsingleton.eq_zero (α := MvPolynomial σ R)
  by_cases! hf : f = 0
  · simp [hf]
  rw [← m.leadingCoeff_ne_zero_iff, ← mem_nonZeroDivisors_iff_ne_zero] at hf
  exact m.withBotDegree_mul_of_left_mem_nonZeroDivisors hf

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 : MvPolynomial σ R
h : f - m.leadingTerm f ≠ 0
⊢ m.degree f ≠ 0

Tactic:
by
  contrapose h
  rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_zero]

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 : MvPolynomial σ R
⊢ m.toSyn.symm ((-f).support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)

Tactic:
rw [support_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

Tactic:
ext
  simp only [pmul_apply, mul_assoc]

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

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k_1 ↦ (σ k) (p ^ k_1)) =
    ∏ p ∈ n.primeFactors, ∑ i ∈ range (n.factorization p + 1), p ^ (i * k)

Tactic:
exact prod_congr n.support_factorization fun _ h ↦
    sigma_apply_prime_pow <| prime_of_mem_primeFactors h

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

Goal state before:
pp: d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiag m = {f ∈ Fintype.piFinset fun x ↦ n.divisors | ∏ i, f i = m}

Tactic:
by
  ext f
  simp only [ne_eq,
    Fintype.mem_piFinset, mem_divisors, mem_filter]
  constructor
  · intro hf
    refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩
    exact fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩
  · rw [mem_finMulAntidiag]
    exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩

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

Goal state before:
pp: 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

Tactic:
exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩

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

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 2 = b 2

Tactic:
← mul_right_inj' <| mul_ne_zero (ne_zero_of_mem_finMulAntidiag ha 0)
      (ne_zero_of_mem_finMulAntidiag ha 1)

Goal state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
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 : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
obtain h | rfl | h := lt_trichotomy x 0

Goal state after:
case 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
x : α
h : x < 0
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

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

case inr.inr
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
x : α
h : 0 < x
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
⊢ a ≤ b ∨ b ≤ a

Tactic:
obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ

Goal state after:
case inl
M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
hab : |val a|ₘ ≤ |val b|ₘ
⊢ a ≤ b ∨ b ≤ a

case inr
M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
hab : |val b|ₘ ≤ |val a|ₘ
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ mk a ≤ mk 1

Tactic:
| mk a
     => 

Goal state after:
case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ mk a ≤ mk 1
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m

Tactic:
simpa using pow_nonneg hx _

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

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B

Tactic:
| mk a
     => 

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : 0 < a
⊢ GaloisConnection (fun x ↦ a • x) fun x ↦ x / a

Tactic:
simpa [mul_comm] using Nat.galoisConnection_mul_div ha

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

Goal state before:
pp: case refine_2.mk
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 : M
hA : MulArchimedeanClass.mk a ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ (MulArchimedeanClass.mk a) ≠ ⊤

Tactic:
| mk a
     => 

Goal state after:
case refine_2.mk
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 : M
hA : MulArchimedeanClass.mk a ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ (MulArchimedeanClass.mk a) ≠ ⊤
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((WithZero.map' (toLexMulEquiv (αˣ × βˣ)).toMonoidHom).comp (MonoidWithZeroHom.inl α β))).toFun

Tactic:
simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inl_mono

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 b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

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 b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_pred_right_eq_Ico h

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ∈
    lowerBounds (upperBounds x✝)

Tactic:
intro s ha
      split_ifs with h
      · exact bot_le
      obtain ⟨b, hs, hb⟩ := not_subset.1 h
      lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)
      exact
        Interval.coe_le_coe.2
          ⟨le_iInf₂ fun c hc => (WithBot.coe_le_coe.1 <| ha hc).1,
            iSup₂_le fun c hc => (WithBot.coe_le_coe.1 <| ha hc).2⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
⊢ x.orderTop = ↑g

Tactic:
rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
    x.isWF_support.min_eq_of_le hg hx]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
hy : y ≠ 0
hyg : ⋯.min ⋯ = g
hxyc : x.coeff g = y.coeff g
⊢ (x - y).coeff g = 0

Tactic:
coeff_sub,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : R⟦Γ⟧
g : Γ
hx : x ≠ 0
hxg : ⋯.min ⋯ = g
hy : y ≠ 0
hyg : ⋯.min ⋯ = g
hxyc : x.coeff g = y.coeff g
⊢ x.coeff g - y.coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
· exact (leadingCoeff_pos_iff.mpr hlt).le

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
have habs : ofLex |x| ≠ 0 := by simpa using hne

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
habs : ofLex |x| ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order
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 α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝ = swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝ ⊔ swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝

Tactic:
← sup_mul_distrib,

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝ = (n₂✝ ⊔ n₁✝) * m✝
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
· exact order_single one_ne_zero

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
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
⊢ 0 < ↑seed.baseEmbedding x

Tactic:
have hfpos : 0 < (f.sum fun _ x ↦ x.val) := by
    rw [hf]
    simpa using! hx

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
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
⊢ 0 < ↑seed.baseEmbedding x
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
y : S
hy : y ≠ 0
⊢ mk x ≤ mk (f y) + mk x

Tactic:
· rw [mk_map_of_archimedean' f hy, zero_add]

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
left✝ : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2

Tactic:
exact ⟨add_right_cancel h1, rfl⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
by
  simp_rw [← toOrderAddMonoidHom_apply, ← orderHom_mk]
  trans ArchimedeanClass.mk x = .mk y
  · exact Function.Injective.eq_iff <| orderHom_injective <| toOrderAddMonoidHom_injective _
  · simp_rw [mk_eq_mk]
    aesop

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✝⁴ : 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
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    x_1 ∉ antidiagonal ⋯ ⋯ (a + x.order) → z.coeff x_1.1 * x.coeff x_1.2 = 0

pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ 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
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    x_1 ∉ antidiagonal ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0

Tactic:
· simp +contextual [← or_and_right]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    x_1 ∉ antidiagonal ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ 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
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ antidiagonal ⋯ ⋯ (a + x.order),
    x_1 ∉ antidiagonal ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0

Tactic:
· simp +contextual [← or_and_right]

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

Goal state before:
pp: case refine_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h : ⟨A.ofPrime a.asIdeal, ⋯⟩ ≤ ⟨A.ofPrime b.asIdeal, ⋯⟩
this : A.idealOfLE ↑⟨A.ofPrime b.asIdeal, ⋯⟩ ?refine_2 ≤ A.idealOfLE ↑⟨A.ofPrime a.asIdeal, ⋯⟩ ?refine_1
⊢ b ≤ a

Tactic:
idealOfLE_ofPrime,

Goal state after:
case refine_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h : ⟨A.ofPrime a.asIdeal, ⋯⟩ ≤ ⟨A.ofPrime b.asIdeal, ⋯⟩
this : b.asIdeal ≤ A.idealOfLE ↑⟨A.ofPrime a.asIdeal, ⋯⟩ ?refine_1
⊢ b ≤ a
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
c : K
hc : c ≠ 0
hx : -(c • x) ∈ (↑f).domain
⊢ x ∈ (↑f).domain

Tactic:
neg_mem_iff,

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : K
hc : c ≠ 0
hx : c • x ∈ (↑f).domain
⊢ x ∈ (↑f).domain
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥

Tactic:
| _ a
   => 

Goal state after:
case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ ↑a ∈ ⊥
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
⊢ stdPart (-x) = -stdPart x

Tactic:
simp_rw [stdPart, ArchimedeanClass.mk_neg]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : x ≤ 0
⊢ stdPart x ≤ 0

Tactic:
by
  simpa using stdPart_nonneg (neg_nonneg.2 h)

Goal state after: