mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inr
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 : n < m
⊢ 0 ≤ x ^ m / (1 - x)

Tactic:
apply div_nonneg (pow_nonneg hx _)

Goal state after:
case inr
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 : n < m
⊢ 0 ≤ 1 - x
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
inst✝ : Nontrivial M
⊢ Nonempty (FiniteMulArchimedeanClass M)

Tactic:
obtain ⟨x, hx⟩ := exists_ne (1 : M)

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a b : M
inst✝ : Nontrivial M
x : M
hx : x ≠ 1
⊢ Nonempty (FiniteMulArchimedeanClass M)
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
by
  obtain ha | ha := le_or_gt a 0
  · simp [ha]
  · exact le_of_smul_le_smul_left ((smul_floorDiv_le ha).trans <| le_smul_ceilDiv ha) ha

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ ∃ x_1 < #s, c - ↑x_1 = x

Tactic:
rw [mem_coe, mem_Ioc] at mx

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - ↑(#s) < x ∧ x ≤ c
⊢ ∃ x_1 < #s, c - ↑x_1 = x
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.SurjOn (fun x ↦ c + ↑x) ↑(range #s) ↑(Ico c (c + ↑(#s)))

Tactic:
intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
    rw [mem_coe, mem_Ico] at mx
    use (x - c).toNat; grind

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Lattice

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
⊢ v (x j) ≤ ⨆ i, v (x ↑i)

Tactic:
rcases eq_or_ne (x j) 0 with h | h

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
h : x j = 0
⊢ v (x j) ≤ ⨆ i, v (x ↑i)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
h : x j ≠ 0
⊢ v (x j) ≤ ⨆ i, v (x ↑i)
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : α
hm : m ≠ 0
⊢ (inl α β) m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 m hm))

Tactic:
lift m to αˣ using isUnit_iff_ne_zero.mpr hm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : αˣ
hm : ↑m ≠ 0
⊢ (inl α β) ↑m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 (↑m) hm))
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
by
  simp [mul_comm, and_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
by
  simp [mul_comm, and_left_comm]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h
    have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
    refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]
    · nth_rw 2 [this.1]
    · nth_rw 2 [this.2]
  · rintro ⟨b, c, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]

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

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

Tactic:
simp only [hr, map_zero, orderTop_zero, le_top]

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

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

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  simp only [ne_eq, AddOpposite.unop_eq_zero_iff, EmbeddingLike.map_eq_zero_iff, hx,
    not_false_eq_true, leadingCoeff_of_ne_zero, addOppositeEquiv_orderTop]
  simp [addOppositeEquiv]

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d < b

Tactic:
by simpa [mul_right_comm a c d] using h₂

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ a * c - a * b

Tactic:
rw [← mul_sub, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ (ofLex a).leadingCoeff * (ofLex (c - b)).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
⊢ { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a ≤
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    a ≤ b

Tactic:
simp_rw [le_iff_lt_or_eq, lt_iff]
    simp only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]
    constructor
    · rintro (⟨i, hj, hi⟩ | heq)
      · have himem : i ∈ Set.range f := by
          contrapose hi
          simp [embDomain_of_notMem_range hi]
        obtain ⟨k, rfl⟩ := himem
        refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
        simpa using hj (f j) (f.lt_iff_lt.mpr hjk)
      · exact Or.inr <| embDomain_injective.comp (ofLex.injective) heq
    · rintro (⟨i, hj, hi⟩ | rfl)
      · refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
        by_cases hkmem : k ∈ Set.range f
        · obtain ⟨j', rfl⟩ := hkmem
          simpa using hj _ <| f.lt_iff_lt.mp hki
        · simp_rw [embDomain_of_notMem_range hkmem]
      · simp

Goal state after:
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
⊢ ((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support

Tactic:
refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
    fun a ↦ Set.VAddAntidiagonal.finite_of_isPWO x.isPWO_support ((of R).symm y).isPWO_support a)

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
⊢ x ∈ {a | (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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ f.support.min' hsupport ≤ j

Tactic:
rw [← Subtype.coe_le_coe, Subtype.coe_mk]

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
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ ↑(f.support.min' hsupport) ≤ ↑j
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f x < f y
h : f (x + y) ≠ f y
h1 : f (x + y) ≤ f y
⊢ max (f (-x)) (f (x + y)) < max (f y) (f y)

Tactic:
max_self,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f x < f y
h : f (x + y) ≠ f y
h1 : f (x + y) ≤ f y
⊢ max (f (-x)) (f (x + y)) < f y
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
h : f (x + y) ≠ f x
h1 : f (x + y) ≤ f x
⊢ max (f (x + y)) (f (-y)) < max (f x) (f x)

Tactic:
max_self,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
h : f (x + y) ≠ f x
h1 : f (x + y) ≤ f x
⊢ max (f (x + y)) (f (-y)) < f x
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case cons
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
a : β
s : Multiset β
h : ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)
b : β
hb1 : b ∈ a ::ₘ s
hb2 : f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)
⊢ ∃ b, (a ::ₘ s ≠ 0 → b ∈ a ::ₘ s) ∧ f (Multiset.map g (a ::ₘ s)).sum ≤ f (g b)

Tactic:
exact ⟨b, fun _ ↦ hb1, hb2⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).support ⊆ x.support +ᵥ y.support

Tactic:
exact HahnModule.support_smul_subset_vadd_support

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.h
α : Type u_1
s : Setoid α
inst✝ : LE α
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
z : α
h₂ : ⟦y⟧ ≤ ⟦z⟧
⊢ ⟦x⟧ ≤ ⟦z⟧

Tactic:
exact Relation.TransGen.trans h₁ h₂

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ (fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) ((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) P) = P

Tactic:
ext1

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) ((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) P)).asIdeal = P.asIdeal
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
S : { S // A ≤ S }
⊢ (fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) S) = S

Tactic:
ext1

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
S : { S // A ≤ S }
⊢ ↑((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) S)) = ↑S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx✝¹ : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
hx✝ : ¬A.valuation (x⁻¹ + 1 - 1) < 1
hx : Units.mk0 (x⁻¹ + 1) h_2 ∉ A.principalUnitGroup
⊢ Units.mk0 (x⁻¹ + 1) h_2 ∉ B.principalUnitGroup

Tactic:
simpa only [hx] using @h (Units.mk0 (x⁻¹ + 1) h_2)

Goal state after:
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 : Quotient (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))),
    (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {x}).OrdConnected

Tactic:
refine fun x ↦ ⟨?_⟩
  rintro x rfl y hy z ⟨hxz, hzy⟩
  have := hxz.trans hzy
  rw [Set.mem_preimage, Set.mem_singleton_iff, Quotient.eq, Submodule.quotientRel_def,
    IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, FiniteElement.not_isUnit_iff_mk_pos] at hy ⊢
  apply hy.trans_le (mk_antitoneOn _ _ _) <;> simpa

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

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

Tactic:
induction a using QuotientGroup.induction_on with | _ 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 y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart (x * y) = stdPart x * stdPart y

Tactic:
by
  unfold stdPart
  rw [dif_pos hx, dif_pos hy, dif_pos]
  exact map_mul _ (FiniteElement.mk x hx) (.mk y hy)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (C p) = eval x p

Tactic:
evalEval,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval x (eval (C y) (C p)) = eval x p
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (map C p) = eval y p

Tactic:
evalEval,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval x (eval (C y) (map C p)) = eval y p
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y Y = y

Tactic:
evalEval,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ eval x (eval (C y) Y) = y
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ eval₂ (evalRingHom x) = evalEval x

Tactic:
ext1

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = evalEval x x✝
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)

Tactic:
evalEval,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ eval (f x) (eval (C (f y)) (map (mapRingHom f) p)) = f (evalEval x y p)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ C 1 * X ^ n + p.eraseLead = X ^ n + p.eraseLead

Tactic:
map_one,

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ 1 * X ^ n + p.eraseLead = X ^ n + p.eraseLead
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ (evalEval h) ((mk p) g) = Polynomial.evalEval x y g

Tactic:
evalEval,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ (lift (evalRingHom x) y ⋯) ((mk p) g) = Polynomial.evalEval x y g
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : m + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n

Tactic:
exact (Nat.add_left_cancel this.symm).symm

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Subsingleton R
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢
    exact .inl hp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
rw [← hp.natDegree_eq, ← hq.natDegree_eq]

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ a) → IsUnit a

Tactic:
apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 1 x = 1 • x ^ 0

Tactic:
rw [← C_1, smeval_C]
  simp only [one_smul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
i : Fin n
⊢ (rs₂ i).degree < g.degree

Tactic:
by simpa using hr₂ i.castSucc

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ (aeval r) ((⇑derivative)^[q] p) = q ! • eval r p'

Tactic:
have h (x) (h : 1 ≤ x) (h' : x ≤ q) :
      (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rwa [tsub_tsub_cancel_of_le h']

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ (aeval r) ((⇑derivative)^[q] p) = q ! • eval r p'