mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p ∈ {x | p ∣ x}

Tactic:
Set.mem_ofPred_eq

Goal state after:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p ∉ {x | p ∣ x}

Tactic:
Set.mem_ofPred_eq

Goal state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ¬p ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n

Tactic:
Finset.mem_range

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ s → x < n
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
i : ℕ
i_t : i ∈ t
⊢ i ∈ Finset.range (m + 1)

Tactic:
Finset.mem_range

Goal state after:
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
i : ℕ
i_t : i ∈ t
⊢ i < m + 1
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
rw [tendsto_congr' (sum_indicator_eventually_eq_card r hs), tendsto_atTop_atTop]

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬∀ (b : R), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ Nat.card ↑s • r
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ {a b : β}, (↑↑(inducedOrderRingHom β γ).toRingHom).toFun a ≤ (↑↑(inducedOrderRingHom β γ).toRingHom).toFun b ↔ a ≤ b

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

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i - C r)

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg]
  apply monic_X_add_C

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

Goal state before:
pp: case h
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 c : MulArchimedeanOrder M
m : ℕ
hm : |val b|ₘ ≤ |val a|ₘ ^ m
n : ℕ
hn : |val c|ₘ ≤ |val b|ₘ ^ n
⊢ |val c|ₘ ≤ |val a|ₘ ^ (m * n)

Tactic:
pow_mul

Goal state after:
case h
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 c : MulArchimedeanOrder M
m : ℕ
hm : |val b|ₘ ≤ |val a|ₘ ^ m
n : ℕ
hn : |val c|ₘ ≤ |val b|ₘ ^ n
⊢ |val c|ₘ ≤ (|val a|ₘ ^ m) ^ n
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_1.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 ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 < (g a, f a).1
⊢ f ((Equiv.symm σ) a) ≤ f a

Tactic:
exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 ∧ 0 < x ^ n

Tactic:
exact ⟨h0.trans h1, pow_pos h0 n⟩

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

Goal state before:
pp: case insert.inr.refine_3
ι : 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
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : 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
x : ι
hx : x ∈ s.erase ((Equiv.symm σ) a)
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))

Tactic:
rw [mem_erase, Ne, eq_symm_apply] at hx

Goal state after:
case insert.inr.refine_3
ι : 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
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : 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
x : ι
hx : ¬σ x = a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : 1 < x
⊢ ∃ n, x ≤ y ^ n

Tactic:
have hxy : mk x = mk y := h x hx.ne.symm y hy.ne.symm
      obtain ⟨_, ⟨m, hm⟩⟩ := mk_eq_mk.mp hxy
      rw [mabs_eq_self.mpr hx.le, mabs_eq_self.mpr hy.le] at hm
      exact ⟨m, hm⟩

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

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

Tactic:
_root_.mul_add_one,

Goal state after:
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * ↑⌊a⌋₊ + b ≤ ↑⌊a⌋₊
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : z ^ 2 ≤ y
⊢ z ^ (2 * (n + 1)) = (z ^ 2) ^ (n + 1)

Tactic:
pow_mul

Goal state after:
M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
n : ℕ
y : M
hy : 1 < y
hyx : y ^ (n + 1) < x
z : M
hz : 1 < z
hzy : z ^ 2 ≤ y
⊢ (z ^ 2) ^ (n + 1) = (z ^ 2) ^ (n + 1)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∀ a ∈ range #s, c + ↑a ∈ Ico c (c + ↑(#s))

Tactic:
intro x mx; rw [mem_Ico]; rw [mem_range] at mx; lia

Goal state after:
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
  simp

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

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

Tactic:
lift n to βˣ using isUnit_iff_ne_zero.mpr hn
  simp

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

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ mk (k • a) = mk a

Tactic:
simp_rw [mk_eq_mk, abs_smul]

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ (∃ m, |a| ≤ m • |k| • |a|) ∧ ∃ n, |k| • |a| ≤ n • |a|
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Interval α
⊢ ↑(dual s) = ⇑ofDual ⁻¹' ↑s

Tactic:
by
  cases s with
  | bot => rfl
  | coe s₀ => exact NonemptyInterval.coe_dual s₀

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
⊢ ↑(↑s ⊓ ↑t) = ↑↑s ∩ ↑↑t

Tactic:
simp only [coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, inf_coe]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
⊢ ↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ }
      else ⊥) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } ≤ s

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s

Tactic:
· lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1
        -- Porting note: Lean failed to figure out the function `f` by itself,
        -- so I added it through manually
        let f := fun (s : NonemptyInterval α) (_ : ↑s ∈ s₁) => s.toProd.fst
        exact WithBot.coe_le_coe.2 ⟨le_iSup₂ (f := f) s ha, iInf₂_le s ha⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s
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).leadingCoeff = r

Tactic:
by_cases h : r = 0 <;> simp [leadingCoeff, h]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → x.coeff j = 0
⊢ i ≤ x.orderTop

Tactic:
obtain rfl | h := eq_or_ne x 0

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → coeff 0 j = 0
⊢ i ≤ orderTop 0

case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → x.coeff j = 0
h : x ≠ 0
⊢ i ≤ x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : i ∈ v
⊢ (ofLex a).coeff i ≠ 0 ∨ i ∈ {i | (ofLex b).coeff i ≠ 0}

Tactic:
Set.mem_ofPred_eq

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : i ∈ v
⊢ (ofLex a).coeff i ≠ 0 ∨ (ofLex b).coeff i ≠ 0
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z

Tactic:
simp_all only [leftMulResiduation, sSup_mul_distrib, Set.mem_ofPred_eq,
      iSup_le_iff, implies_true]

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
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk x) =
    (ofLex x).orderTop

Tactic:
obtain rfl | h := eq_or_ne x 0

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk 0) =
    (ofLex 0).orderTop

case inr
Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk x) =
    (ofLex x).orderTop
Module: Mathlib.Algebra.Order.Ring.Archimedean

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

Tactic:
obtain rfl | h := eq_or_ne x 0

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

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 = ⊤
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
h : q ≠ 0
⊢ mk ↑q = 0

Tactic:
simpa using mk_map_of_archimedean ⟨(Rat.castHom R).toAddMonoidHom, fun _ ↦ by simp⟩ 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f).domain
hx : ↑x ∈ ball K c
d : FiniteArchimedeanClass M
hd : ↑d ≤ ↑c
⊢ (ofLex (↑↑f x)).coeff d = 0

Tactic:
obtain rfl | ne := eq_or_ne x 0

Goal state after:
case inl
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
c d : FiniteArchimedeanClass M
hd : ↑d ≤ ↑c
hx : ↑0 ∈ ball K c
⊢ (ofLex (↑↑f 0)).coeff d = 0

case inr
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
c : FiniteArchimedeanClass M
x : ↥(↑f).domain
hx : ↑x ∈ ball K c
d : FiniteArchimedeanClass M
hd : ↑d ≤ ↑c
ne : x ≠ 0
⊢ (ofLex (↑↑f x)).coeff d = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (↑z - ↑y)

Tactic:
have h1 (c : FiniteArchimedeanClass M) (hc : c.val < .mk (x - z.val)) :
      (ofLex (f.eval x)).coeff c = (ofLex (f.val z)).coeff c := by
    rw [ArchimedeanClass.mk_sub_comm] at hc
    simp_rw [eval, ofLex_toLex]
    apply evalCoeff_eq
    simpa [c.prop] using! fun _ ↦ hc

Goal state after:
case neg
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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M),
    ↑c < ArchimedeanClass.mk (x - ↑z) → (ofLex (f.eval x)).coeff c = (ofLex (↑↑f z)).coeff c
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (↑z - ↑y)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation ((↑a⁻¹ - 1) * ↑a) < 1

Tactic:
sub_mul,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation (↑a⁻¹ * ↑a - 1 * ↑a) < 1
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 : FiniteElement K
⊢ x ≤ y ∨ x ≈ y ↔ x ≤ y ∨ mk x = mk y

Tactic:
rw [← Quotient.eq_iff_equiv]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
⊢ x ≤ y ∨ ⟦x⟧ = ⟦y⟧ ↔ x ≤ y ∨ mk x = mk 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 : FiniteElement K
⊢ x < y ∧ ¬x ≈ y ↔ x < y ∧ mk x ≠ mk y

Tactic:
rw [← Quotient.eq_iff_equiv]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
⊢ x < y ∧ ¬⟦x⟧ = ⟦y⟧ ↔ x < y ∧ mk x ≠ mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: 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
r : ℝ
hr : r ∈ {r | x < f r}
hra : r < ↑a
⊢ (↑↑f.toRingHom).toFun ↑a < (↑↑f.toRingHom).toFun r

Tactic:
by simpa using ha.trans hr

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

Goal state before:
pp: 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 : ℕ
x : A
⊢ d.mapCoeffs ((monomial n) x) = PolynomialModule.single A n (d x)

Tactic:
ext; simp [coeff_monomial, apply_ite d, Finsupp.single_apply]

Goal state after:
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]
q : R[X]
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

Tactic:
rw [eval_map, ← coe_mapRingHom, eval₂_hom]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v)

Tactic:
rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]

Goal state after: