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
h : m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.degree (g + f) = m.degree g

Tactic:
exact degree_add_of_lt h

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val

Tactic:
← Finset.mem_def,

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val

Tactic:
rw [← Finset.mem_def, Finset.mem_powerset] at hx hy

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_2.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 : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
hamax : (g (σ a), f (σ a)).1 < (g a, f a).1
⊢ g (σ a) ≤ g a

Tactic:
exact hamax.le

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

Goal state before:
pp: case cons.inr.inr
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 (∏ i ∈ s, a i) < mk (a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ s.min' hs ≤ y

Tactic:
· exact Finset.min'_le _ _ hmem

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 b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : mk a ≤ mk b
⊢ (orderHom f) (mk a) ≤ (orderHom f) (mk b)

Tactic:
exact OrderHomClass.monotone _ h

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

Goal state before:
pp: case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I → ∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x

pp: case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ (∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x) → x ∈ I

Tactic:
· intro hx
    rcases hpwo.exists_le_minimal hx with ⟨z, hz, hz'⟩
    rw [le_iff_exists_mul'] at hz
    rcases hz with ⟨y, rfl⟩
    exact ⟨y, z, hz', rfl⟩

Goal state after:
case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ (∃ y z, Minimal (fun x ↦ x ∈ I) z ∧ y * z = x) → x ∈ I
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : N₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
· simp [WithZero.withZeroUnitsEquiv]

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 - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
by
  simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

Goal state after:
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}
b : α × α
hb : b ∈ mulAntidiagonal hs ht a
⊢ a ∈ s * t

Tactic:
by
  rw [mem_mulAntidiagonal] at hb
  exact ⟨b.1, hb.1, b.2, hb.2⟩

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ⊥ ∈ S
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl

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✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha : a ∈ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0}
⊢ a ∈ {a | (VAddAntidiagonal a ⋯).Nonempty}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha : a ∈ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0}
⊢ (VAddAntidiagonal a ⋯).Nonempty
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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x✝ = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c✝ c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
⊢ ↑x ∈ seed.baseDomain

Tactic:
apply Set.mem_of_mem_of_subset x.prop

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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x✝ = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c✝ c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
⊢ ↑(seed.stratum c) ⊆ ↑seed.baseDomain
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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ x = (DirectSum.coeAddMonoidHom seed.stratum') f'

Tactic:
apply Submodule.subtype_injective

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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := ⋯
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype ((DirectSum.coeAddMonoidHom seed.stratum') f')
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x✝ : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx : x ∈ ((of R).symm (x✝ • y)).support
⊢ x ∈ {a | (VAddAntidiagonal a ⋯).Nonempty}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x✝ : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx : x ∈ ((of R).symm (x✝ • y)).support
⊢ (VAddAntidiagonal x ⋯).Nonempty
Module: Mathlib.Algebra.Order.Ring.Archimedean

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

Tactic:
mk_mul

Goal state after:
case mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
⊢ mk y + mk x = mk y + mk x
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
hrest_le : f (∑ i ∈ s.erase k, l i) ≤ (s.erase k).sup' hNonempty fun i ↦ f (l i)
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)

Tactic:
simp only [Finset.le_sup'_iff, Finset.mem_erase, ne_eq] at hrest_le

Goal state after:
case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
hrest_le : ∃ b, (¬b = k ∧ b ∈ s) ∧ f (∑ i ∈ s.erase k, l i) ≤ f (l b)
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A B : RingPreordering R
h : ↑A = ↑B
⊢ A = B

Tactic:
ext; rw [h]

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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range

Tactic:
refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩

Goal state after:
case refine_1
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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ (f'.sum fun d x ↦ ↑x) ∈ seed.baseEmbedding.domain

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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ seed.baseEmbedding.toFun ⟨f'.sum fun d x ↦ ↑x, ?refine_1⟩ =
    toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x)))
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ 0 < mk ↑(z - x)

Tactic:
apply hy.trans_le (mk_antitoneOn _ _ _)

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ∈ Set.Ici 0

K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(y - x) ∈ Set.Ici 0

K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ≤ ↑(y - x)
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
⊢ ((monomial n) x).coeffList.length = (x :: List.replicate n 0).length

Tactic:
classical simp [hx]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
⊢ mapCoeffs X = 0

Tactic:
by simp [← monomial_one_one_eq_X]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case e'_3.e'_5
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ (aeval x) (mapCoeffs p) =
    (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap A R)) (deriv.mapCoeffs p))

pp: case convert_7
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A), (Algebra.linearMap A R) a′ = ((algebraMap A R) a)′

Tactic:
· simp [mapCoeffs]

Goal state after:
case convert_7
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A), (Algebra.linearMap A R) a′ = ((algebraMap A R) a)′
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h✝ : ¬p = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
exact pow_nonneg (Int.natCast_nonneg _) _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

Tactic:
rcases lt_trichotomy n 1 with hn | rfl | hn

Goal state after:
case inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : n < 1
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

case inr.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ f.coeff 1 = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff 1

case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ

Tactic:
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n

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

Goal state before:
pp: case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

pp: case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
· rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
      have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
      aesop

Goal state after:
case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (R a b → (R b c → R a b ∧ IsChain R (b :: destutter' R c l)) ∧ (¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))

Tactic:
imp_and

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
a : α
IH2 : ∀ (y a : α), R a y → IsChain R (a :: destutter' R y l)
⊢ (((R a b → R b c → R a b) ∧ (R a b → R b c → IsChain R (b :: destutter' R c l))) ∧
      (R a b → ¬R b c → IsChain R (a :: destutter' R b l))) ∧
    (¬R a b → R a c → IsChain R (a :: destutter' R c l))