mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (φ f).natDegree = fu f.natDegree →
          (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
· intro f g fg _ fk gk
    rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]
    by_cases! FG : k ≤ f.natDegree
    · rw [natDegree_add_eq_right_of_natDegree_lt, gk]
      rw [fk, gk]
      exact fc FG fg
    · cases k
      · nomatch FG
      · rwa [φ_k FG, zero_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rw [hp.irreducible_iff_natDegree', and_iff_right hp1]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
rw [neg_sub, ← mul_neg, neg_sub] at this

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : 1 = 0
⊢ False

Tactic:
exact one_ne_zero this

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range MvPolynomial.X) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S ↑(Finset.image (FreeAlgebra.ι S) Finset.univ) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range (FreeAlgebra.ι S)) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊓ ((aeval f) q).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥

Tactic:
simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
    LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero S
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
hp : Nat.Prime 1
hchar✝ : CharP R 1
⊢ ExpChar (R × S) 1

Tactic:
exact (Nat.not_prime_one hp).elim

Goal state after:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ -x = x

Tactic:
rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
⊢ ((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) (Submodule.Quotient.mk ⟨y, hy⟩) ∈
    Submodule.restrictScalars R (map (Quotient.mk (I ^ (n + 1))) (I ^ n))

Tactic:
simp [Ideal.mem_sup_left hy]

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length + 1)

Tactic:
← Nat.succ_eq_add_one,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ (minimalPeriod f x = 1 ∨ minimalPeriod f x = p) ∧ ¬minimalPeriod f x = 1

Tactic:
or_and_right,

Goal state after:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔
    minimalPeriod f x = 1 ∧ ¬minimalPeriod f x = 1 ∨ minimalPeriod f x = p ∧ ¬minimalPeriod f x = 1
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
this : k + 1 = l.length
⊢ False

Tactic:
by simp [this] at hk

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
⊢ f = g

Tactic:
refine DFunLike.ext f g fun a =>
    adjoin_induction_subtype (p := fun y => f y = g y) a (fun x hx => ?_) (fun r => ?_)
    (fun x y hx hy => ?_) (fun x y hx hy => ?_) fun x hx => ?_
  · exact h ⟨x, subset_adjoin R s hx⟩ hx
  · simp only [AlgHomClass.commutes]
  · simp only [map_add, map_add, hx, hy]
  · simp only [map_mul, map_mul, hx, hy]
  · simp only [map_star, hx]

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

Goal state before:
pp: α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
refine ⟨?_, nodup_permutations s⟩

Goal state after:
α : Type u_1
s : List α
⊢ s.permutations.Nodup → s.Nodup
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
x : orbitRel.Quotient G α
⊢ ∀ (x_1 y : ↑x.orbit), ∃ g, g • x_1 = y

Tactic:
induction x using Quotient.inductionOn'
    rintro ⟨y, yh⟩ ⟨z, zh⟩
    rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh
    rcases yh with ⟨g, rfl⟩
    rcases zh with ⟨h, rfl⟩
    refine ⟨h * g⁻¹, ?_⟩
    ext
    simp [mul_smul]

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
bot_subgroupOf,

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

Goal state before:
pp: n : ℕ
x : ZMod n
⊢ (-x).cast = (↑(-x.cast)).cast

Tactic:
Int.cast_neg,

Goal state after:
n : ℕ
x : ZMod n
⊢ (-x).cast = (-↑x.cast).cast
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
⊢ K.index < H.index

Tactic:
have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).index_ne_zero

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index < H.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1

Tactic:
hk,

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (0 - 1).cast = ↑n - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1

pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
· rw [hk, zero_sub, ZMod.cast_neg_one]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a + b).val = (a.val + b.val) % n

Tactic:
cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.val_add

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a b : ℕ
c : a < b
d : ℕ × ℕ
h :
  (have y := n / a;
    if a * y = n then some (a, y) else none) =
    some d
ha : ℕ × ℕ
h' :
  (have y := n / b;
    if b * y = n then some (b, y) else none) =
    some ha
⊢ d.1 < ha.1

Tactic:
Option.ite_none_right_eq_some,

Goal state after:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ some (a, n / a) = some d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ some (b, n / b) = some ha
⊢ d.1 < ha.1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
← hx.le

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Tactic:
refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : ∑ i ∈ range n, x ^ i = 0
⊢ x = -1 ∧ Even n
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 : ℕ
hy : y ∈ ↑n.divisors
h : n / x = n / y
⊢ x = y

Tactic:
mem_coe,

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
h : n / x = n / y
⊢ x = y
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ n.choose k ≤ 2 ^ (n - 1)

Tactic:
← Nat.sub_add_cancel p

Goal state after:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: r n : ℕ
⊢ (2 * n).choose (2 * n / 2) = (2 * n).choose n

Tactic:
by rw [Nat.mul_div_cancel_left n zero_lt_two]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Tactic:
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k

Tactic:
let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))

Goal state after:
n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = p ^ padicValNat p n * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
hk,

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ padicValNat p n * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : ↑k ≤ emultiplicity a b
⊢ a ^ k ∣ b

Tactic:
classical
  cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ False

Tactic:
hk,

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ multiplicity a b * (a * k)
hk : c = a * k
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p n : ℕ
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
by
  rcases eq_or_ne p 1 with rfl | hp
  · simp
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [← padicValNat_eq_emultiplicity_of_ne_one, *]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0

Tactic:
exact
    ⟨fun h =>
      or_iff_not_imp_right.2 fun hb =>
        have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
        Classical.by_contradiction fun ha1 : a ≠ 1 =>
          have ha_gt_one : 1 < a :=
            lt_of_not_ge fun _ =>
              match a with
              | 0 => ha rfl
              | 1 => ha1 rfl
              | b+2 => by lia
          not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
      fun h => by cases h <;> simp [*]⟩

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b

Tactic:
by
  simp [fixedLengthDigits]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, L ∈ Finset.image (fun L ↦ a :: L) (fixedLengthDigits hb l)

Tactic:
Finset.mem_image

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Tactic:
rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
rw [_root_.pow_succ']

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [← add_tsub_cancel_of_le hf, Finsupp.prod_add_index' (by simp) Nat.pow_add,
    prod_factorization_pow_eq_self hn]

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by_cases h0 : orderOf x = 0
  · rw [h0, coprime_zero_right] at h
    exact ⟨1, by rw [h, pow_one, pow_one]⟩
  by_cases h1 : orderOf x = 1
  · exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
  obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by lia)
  exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1)!.factorization p = (n + 1).factorization p + n !.factorization p

Tactic:
by
        rw [factorial_succ, factorization_mul (zero_ne_add_one n).symm n.factorial_ne_zero,
          coe_add, Pi.add_apply]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℤ
⊢ FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Tactic:
simp only [FiniteMultiplicity.def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 = orderOf x * orderOf y

Tactic:
exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

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

Goal state before:
pp: a b c : ℕ
h : b ∣ c
hb : b ≠ 0
hc : c ≠ 0
⊢ b.factorization a ≤ c.factorization a

Tactic:
obtain ⟨k, rfl⟩ := h

Goal state after:
a b : ℕ
hb : b ≠ 0
k : ℕ
hc : b * k ≠ 0
⊢ b.factorization a ≤ (b * k).factorization a
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = n - k.factorization p

Tactic:
nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]
  rw [Nat.add_sub_cancel_right]

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

Goal state before:
pp: a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
suffices (a.factorization ⊓ b.factorization).prod (· ^ ·) = gcd a b by
    rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]

Goal state after:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) = a.gcd b
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ ringChar R ≠ 0

Tactic:
exact CharP.ringChar_ne_zero_of_finite R

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

Goal state before:
pp: case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

pp: case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
· simp [choose_eq_zero_of_lt hkp]

Goal state after:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑(g ^ H.index) = 1

Tactic:
QuotientGroup.mk_pow H,

Goal state after:
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑g ^ H.index = 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩ <;> simp [coeff_C]

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

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ a = c ^ n ∧ b = c ^ m

Tactic:
by
    refine ⟨ha, ?_⟩
    apply Nat.pow_left_injective hn0
    simp [← h, ha, Nat.pow_right_comm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
⊢ ↑p = 0

Tactic:
rw [← hn, Nat.cast_card_eq_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ p ∣ n

Tactic:
Nat.dvd_iff_mod_eq_zero

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ n % p = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M (p.divX * X)

Tactic:
rw [hpX0, zero_mul]

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M 0