mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
⊢ y ∈ toSubmodule S → ∀ n ∈ toSubmodule T, y * n ∈ toSubmodule (S ⊔ T)

Tactic:
hy

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
⊢ ∀ n ∈ toSubmodule T, y * n ∈ toSubmodule (S ⊔ T)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I

Tactic:
suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∀ m ∈ p.support, (monomial m) (coeff m p) ∈ I
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑b

Tactic:
← Nat.sub_add_cancel hle,

Goal state after:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑(b - a + a)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a = b + c ↔ a + c = b

Tactic:
rw [← eq_sub_iff_add_eq, sub_eq_add]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
⊢ r₁ • a₁ ≈ r₂ • a₂

Tactic:
have := h (p.quotientRel_def.mp hr)

Goal state after:
R✝ : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : r₁ - r₂ ∈ comap (algebraMap R A) P
⊢ r₁ • a₁ ≈ r₂ • a₂
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ (map (Quotient.mk I) p).IsPrime

Tactic:
by
  apply Ideal.map_isPrime_of_surjective
  · exact Quotient.mk_surjective
  · simpa

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
is : List α
⊢ [].permutationsAux is = []

Tactic:
permutationsAux,

Goal state after:
α : Type u_1
is : List α
⊢ permutationsAux.rec (fun x ↦ [])
      (fun t ts is IH1 IH2 ↦ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) [] is =
    []
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ (t :: ts).permutationsAux is =
    foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations

Tactic:
permutationsAux,

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ permutationsAux.rec (fun x ↦ [])
      (fun t ts is IH1 IH2 ↦ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) (t :: ts) is =
    foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem.add
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.add
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r : R
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ ((algebraMap R A) r) hx✝ ⋯
h₂ : p y✝ ((algebraMap R A) r) hy✝ ⋯
⊢ p (x✝ + y✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))

Tactic:
apply Perm.swap'

Goal state after:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: zs ++ [x]).nextOr x d = d
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
takeWhile

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (match decide (x = y) with
        | true => y :: takeWhile (fun x_1 ↦ decide (x = x_1)) l
        | false => []).length +
      1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
⊢ ys ∈ l.permutations' → (permutations'Aux x ys).Nodup

Tactic:
hy

Goal state after:
case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ∈ l.permutations'
⊢ (permutations'Aux x ys).Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
this : x ∈ bs
⊢ False

Tactic:
by exact h x (hb.subset this) rfl

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂

Tactic:
rw [eq_of_heq hxy]; simpa [eq_of_heq hxy] using h.mem_iff

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

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1

case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H * H.index = Nat.card G

Tactic:
← relIndex_bot_left,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = Nat.card G
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h] }

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ ↑a = ↑0

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = a % ↑n

Tactic:
refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_

Goal state after:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val % ↑n = a % ↑n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : x < 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
· exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1

Goal state after:
case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
this : if Even n.succ.succ then ∑ i ∈ range n.succ.succ, x ^ i < 0 else 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
⊢ y ∈ ↑n.divisors → n / x = n / y → x = y

Tactic:
hy

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
hy : y ∈ ↑n.divisors
⊢ n / x = n / y → x = y
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n.choose r) ≤ ↑n ^ r / ↑r !

Tactic:
le_div_iff₀'

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r / ↑r ! ≤ ↑(n.choose r)

Tactic:
div_le_iff₀'

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
if_neg h

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ n + 1 ∣ n.centralBinom

Tactic:
have h_s : (n + 1).Coprime (2 * n + 1) := by
    rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
    exact coprime_one_left n

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ n.centralBinom
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y

Tactic:
obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂

Goal state after:
case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
a : ℕ
ha : n = k + a
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Tactic:
simp only [digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

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

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n ≤ n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · exact Nat.le_of_lt <| padicValNat_lt_self hn

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inl.«0»
b n : ℕ
hn : n ≠ 0
hb : 0 ≤ 1
⊢ (digits 0 n).length ≤ (digits 0 (n + 1)).length

Tactic:
simp +arith [digits_zero_succ', hn]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inl.«1»
b n : ℕ
hn : n ≠ 0
hb : 1 ≤ 1
⊢ (digits 1 n).length ≤ (digits 1 (n + 1)).length

Tactic:
simp +arith [digits_zero_succ', hn]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b * m % b :: b.digits (b * m / b) = 0 :: b.digits m

Tactic:
simp [mul_div_right m (by positivity)]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (if h : ∃ n, ¬↑a ^ (n + 1) ∣ ↑b then ↑(Nat.find h) else ⊤) = if h : ∃ n, ¬a ^ (n + 1) ∣ b then ↑(Nat.find h) else ⊤

Tactic:
congr! <;> norm_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b = min (emultiplicity p a) (emultiplicity p b)

Tactic:
min_eq_right

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b = emultiplicity p b

case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b = min (multiplicity p a) (multiplicity p b)

Tactic:
min_eq_right

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b = multiplicity p b

case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
tsub_add_cancel_of_le (succ_le_of_lt hm0)

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1 + 1)) * s * p

Tactic:
tsub_add_cancel_of_le (succ_le_of_lt hm0)

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
· simpa using ha.ne_zero

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x * x ^ (orderOf x - 1) = 1

Tactic:
rw [← _root_.pow_succ', tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / n)) = n

Tactic:
orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn),

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / (orderOf x / n) = n

G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / p ^ n.factorization p

Tactic:
by
  if hn0 : n = 0 then simp [hn0] else
  if hd0 : d = 0 then simp [hd0] at hpd else
  rw [← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne', factorization_ordCompl]
  intro q
  if hqp : q = p then
    simp [factorization_eq_zero_iff, hqp, hpd]
  else
    simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

Tactic:
refine ⟨factorization_div, ?_⟩
  rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n); · simp
  have h1 : n / d ≠ 0 := by simp [*]
  intro h
  rw [dvd_iff_le_div_mul n d]
  by_contra h2
  obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)
  rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
    lt_self_iff_false] at hp

Goal state after: