mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a

Tactic:
exact (ceil_lt_mul hb hba).le

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ⋯.min ⋯ = hs.min hsn * ht.min htn

Tactic:
refine le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_
  rw [IsWF.le_min_iff]
  rintro _ ⟨x, hx, y, hy, rfl⟩
  exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ (∀ (x : Γ), f x = 0) ↔ ∀ (x : Γ), f x = 0 x

Tactic:
Pi.zero_apply

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).coeff a = r

Tactic:
exact Pi.single_eq_same (M := fun _ => R) a r

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
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
simp_all

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

Goal state before:
pp: case inr
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = WithTop.map (⇑f) x.orderTop

Tactic:
← WithTop.coe_untop x.orderTop (by simpa using hx),

Goal state after:
case inr
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = WithTop.map ⇑f ↑(x.orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x✝ : Γ
⊢ ¬n ≤ x✝ → x✝ ∉ Function.support f

Tactic:
simp_all

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)).orderTop = x.orderTop

Tactic:
simp only [orderTop,
    addOppositeEquiv_support]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
⊢ (-f).order = f.order

Tactic:
by
  classical
  by_cases hf : f = 0
  · simp only [hf, neg_zero]
  simp only [order, support_neg, neg_eq_zero]

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

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

Tactic:
· obtain rfl | hlt := h.eq_or_lt
    · simp
    · exact (leadingCoeff_pos_iff.mpr hlt).le

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 : M
ha : 1 ≤ a
hb : 1 ≤ b
⊢ Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)

Tactic:
simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex 0).orderTop
⊢ (∃ n, |0| ≤ n • |x|) ↔ ∃ n, |(ofLex 0).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

Tactic:
simp_all

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

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
x : G
hx : (orderAddMonoidHom G).toAddMonoidHom x = 1
a : ℤ
⊢ (orderAddMonoidHom G) (a • x) = a

Tactic:
simp_all

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✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
le_antisymm_iff,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ∧ ArchimedeanClass.mk y ≤ ArchimedeanClass.mk x ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : x = 0
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
simp_all

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

Goal state before:
pp: case pos
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : y = 0
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
simp_all

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

Goal state before:
pp: case mk.inl
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
⊢ mk 0 = 0 ∨ mk 0 = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case mk.inr
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
x : S
h : x ≠ 0
⊢ mk x = 0 ∨ mk x = ⊤

Tactic:
simp_all

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 : x + y = x + z
⊢ y = z

Tactic:
simp_all

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 : x + y = x + z
⊢ y = z

Tactic:
by
  simp_all

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
y : R
h : mk 0 = mk y
⊢ mk 0⁻¹ = mk y⁻¹

Tactic:
simp_all

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

Goal state before:
pp: case inr.inl
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x : R
hx : x ≠ 0
h : mk x = mk 0
⊢ mk x⁻¹ = mk 0⁻¹

Tactic:
simp_all

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ x.leadingCoeff * y.leadingCoeff ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 0 = min x.orderTop (orderTop 1)

Tactic:
simp_all

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

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

Tactic:
by
  constructor
  · intro hx
    constructor
    · rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
      exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
    · rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
      exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
  · intro h
    refine lt_of_le_of_ne (le_of_eq_of_le (by simp_all)
      (min_orderTop_le_orderTop_sub (Γ := Γ) (R := R))) <| Ne.symm <|
      orderTop_sub_ne h.1 orderTop_one ?_
    rw [h.2, leadingCoeff_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
a : Rˣ
ha : ↑a ∈ P
this : ↑a * (↑a⁻¹ * ↑a⁻¹) ∈ P
⊢ ↑a⁻¹ ∈ P

Tactic:
simp_all

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
a : F
ha : a ∈ P
mem : 1 / a ∈ P
⊢ a⁻¹ ∈ P

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)

Tactic:
revert x y

Goal state after:
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
⊢ ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ (R.mapOfLE S h) (R.valuation ↑((A.inclusion R hR) x))
⊢ False

Tactic:
mapOfLE_valuation_apply

Goal state after:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv (A.primeSpectrumEquiv.symm ⟨B, hle⟩) = A.primeSpectrumEquiv ⊥
⊢ A = B ∨ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv (A.primeSpectrumEquiv.symm ⟨B, hle⟩) = A.primeSpectrumEquiv ⊤
⊢ A = B ∨ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : A = B
⊢ A = B

Tactic:
simp_all

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

Goal state before:
pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : B = ⊤
⊢ A = B

Tactic:
simp_all

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

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : A = B
⊢ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : B = ⊤
⊢ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : A = B
⊢ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : B = ⊤
⊢ B = ⊤

Tactic:
simp_all

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

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
⊢ x ∈ B

Tactic:
have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)

Goal state after:
case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
this : Units.mk0 x h_1 ∈ B.unitGroup
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
⊢ x ∈ B

Tactic:
have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
      exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
b : WithTop α
a : α
h : (↑a).untop₀ ≤ b.untop₀
hb : b = ⊤
⊢ ↑a ≤ b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a b : α
h : (↑a).untop₀ ≤ (↑b).untop₀
⊢ ↑a ≤ ↑b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a : WithTop α
b : α
h : a ≤ ↑b
ha : a = ⊤
⊢ a.untop₀ ≤ (↑b).untop₀

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
b a : α
h : ↑a ≤ ↑b
⊢ (↑a).untop₀ ≤ (↑b).untop₀

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ a • s = s

Tactic:
Set.ext_iff,

Goal state after:
case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : ∀ (b : α), a • b ∈ s ↔ b ∈ s
⊢ ∀ (x : α), x ∈ a • s ↔ x ∈ s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b * a ∈ s

Tactic:
by rwa [← smul_eq_mul, mem_stabilizer_set.1 hb]

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

Goal state before:
pp: case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk (↑(↑n / ↑d) * ↑d) ⋯) = ↑(↑n / ↑d) * mk (FiniteElement.mk ↑d ⋯)

Tactic:
simp_all

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 : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) =
    f (FiniteResidueField.mk (FiniteElement.mk x h))

Tactic:
dif_pos h,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) =
    f (FiniteResidueField.mk (FiniteElement.mk x h))
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
hx : mk x = 0
⊢ 0 ≤ mk x⁻¹

Tactic:
simp_all

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (if h : 0 ≤ mk x⁻¹ then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ h) else 0) =
    (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0)⁻¹

Tactic:
rw [dif_pos hx.ge, dif_pos hx']

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx') =
    ((Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 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
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (if h : 0 ≤ mk (x + y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) h) else 0) =
    (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) +
      if h : 0 ≤ mk y then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y h) else 0

Tactic:
rw [dif_pos hx, dif_pos hy, dif_pos]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x + y)
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
⊢ (if h : 0 ≤ mk (x * y) then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) h) else 0) =
    (if h : 0 ≤ mk x then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h) else 0) *
      if h : 0 ≤ mk y then (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y h) else 0

Tactic:
rw [dif_pos hx, dif_pos hy, dif_pos]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x * y)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl.hr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
hr : r > sInf {r | x < f r}
⊢ x ≤ f r

Tactic:
obtain ⟨s, hs, hs'⟩ := (csInf_lt_iff hb hn).1 hr

Goal state after:
case inl.hr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
hr : r > sInf {r | x < f r}
s : ℝ
hs : s ∈ {r | x < f r}
hs' : s < r
⊢ x ≤ f r
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
h₁✝ : 0 < ((monomial n) x).coeffList.length
h₁ : 0 < (x :: List.replicate n 0).length
⊢ ∀ (w : List R),
    ((monomial n) x).coeffList = ((monomial n) x).leadingCoeff :: w →
      ((monomial n) x).coeffList.get ⟨0, h₁✝⟩ = (x :: List.replicate n 0).get ⟨0, h₁⟩

Tactic:
simp_all

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

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Semiring R
P : R[X]
h✝ : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
w : List R
h : P.coeffList = P.leadingCoeff :: w
⊢ P.coeffList[0]? = (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList))[0]?

Tactic:
simp_all

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
q p✝ q✝ : A[X]
a✝¹ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p✝ * q)) =
    p✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm p✝)
a✝ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (q✝ * q)) =
    q✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q✝)
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((p✝ + q✝) * q)) =
    (p✝ + q✝) • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p✝ + q✝))

Tactic:
| add =>

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

Goal state before:
pp: case monomial.add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
a : A
p✝ q✝ : A[X]
a✝¹ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * p✝)) =
    (monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm p✝) +
      p✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))
a✝ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * q✝)) =
    (monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q✝) +
      q✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * (p✝ + q✝))) =
    (monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p✝ + q✝)) +
      (p✝ + q✝) • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))

Tactic:
| add =>

Goal state after: