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

Goal state before:
pp: case pos
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]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree

pp: case neg
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]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : f.natDegree < k
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
· rw [natDegree_add_eq_right_of_natDegree_lt, gk]
      rw [fk, gk]
      exact fc FG fg

Goal state after:
case neg
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]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : f.natDegree < k
⊢ (φ f + φ g).natDegree = fu g.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n

Tactic:
refine List.sum_le_card_nsmul _ _ ?_

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ x ∈ List.map natDegree tl, x ≤ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRegular p

Tactic:
by
  constructor
  · intro q r h
    dsimp only at h
    rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
  · intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
apply natDegree_prod'

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∏ i ∈ s, (f i).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree

Tactic:
simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
    simp only [Nat.cast_lt, hP.natDegree_pow]
    intro k
    exact nsmul_lt_nsmul_left hdeg

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ (algebraMap (↥(Subring.closure ↑p.coeffs)) R) (p.restriction.coeff n) = p.coeff n

Tactic:
Algebra.algebraMap_ofSubsemiring_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S ↔ ∃ ι x f, Surjective ⇑f

Tactic:
constructor
  · rw [iff_quotient_mvPolynomial]
    rintro ⟨s, f, hsur⟩
    use { x : S // x ∈ s }, inferInstance, f
  · rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

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

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ((algebraMap R R[X]) (F.coeff d) * d.prod fun n e ↦ f n ^ e).natDegree ≤ m * n

Tactic:
← Polynomial.C_eq_algebraMap

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ (Polynomial.C (F.coeff d) * d.prod fun n e ↦ f n ^ e).natDegree ≤ m * n
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
have := AddSubmonoidClass.nsmulMemClass (S := S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n : ℕ
⊢ ↑n = if Even n then 0 else 1

Tactic:
by
  induction n <;> aesop (add simp [one_add_one_eq_two])

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

Goal state before:
pp: n : ℕ
⊢ ¬2 ∣ n ↔ ¬Even n

Tactic:
even_iff_two_dvd

Goal state after:
n : ℕ
⊢ ¬2 ∣ n ↔ ¬2 ∣ n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: ⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0

Tactic:
by simpa using Exists.intro 2 Nat.prime_two

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
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S✝ : StarSubalgebra R A
f : A →⋆ₐ[R] B
S : StarSubalgebra R A
⊢ ∀ {a : B}, a ∈ (Subalgebra.map (↑f) S.toSubalgebra).carrier → star a ∈ (Subalgebra.map (↑f) S.toSubalgebra).carrier

Tactic:
rintro _ ⟨a, ha, rfl⟩
      exact map_star f a ▸ Set.mem_image_of_mem _ (S.star_mem' ha)

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

Goal state before:
pp: 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 : NonUnitalStarSubalgebra R A
⊢ R ∙ 1 ⊔ span R ↑(Subsemigroup.closure (↑s ∪ star ↑s)) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
← NonUnitalStarAlgebra.adjoin_eq_span,

Goal state after:
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 : NonUnitalStarSubalgebra R A
⊢ R ∙ 1 ⊔ (NonUnitalStarAlgebra.adjoin R ↑s).toSubmodule = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)

Tactic:
by
  rw [← isPeriodicPt_iff_minimalPeriod_dvd]
  exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)

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

Goal state before:
pp: 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
⊢ (adjoin R s).toSubalgebra ≤ (centralizer R ↑(centralizer R s)).toSubalgebra

Tactic:
centralizer_toSubalgebra,

Goal state after:
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
⊢ (adjoin R s).toSubalgebra ≤ Subalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n : ℕ
hn : n < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n] = (y :: s).insertIdx n x

Tactic:
cases n
    · simp
    · simpa [get] using IH _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k.succ < (hd :: tl).length

Tactic:
by simpa using hk

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < (pmap l.next l ⋯).length

Tactic:
by simpa using hk

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ ∑ g, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X)) * Fintype.card G

Tactic:
by
  rw [← Fintype.card_prod, ← Fintype.card_sigma,
    Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup G X)]

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

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

Tactic:
by
  rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Goal state after:
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
⊢ 0 < ∑ i ∈ range n, x ^ i ∨ ∑ i ∈ range n, x ^ i = 0 ↔ ¬(Even n ∧ x + 1 < 0)

Tactic:
or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn),

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (Odd n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
Nat.odd_iff,

Goal state after:
n : ℕ
hn : n % 2 = 1
a : ZMod n
⊢ a + a = 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

Tactic:
rw [mul_zero, zero_add]

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

Goal state before:
pp: b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d

Tactic:
simp only [List.reverse_cons]

Goal state after:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d
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₂
    simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
    obtain ⟨b, rfl⟩ := H₁
    exact ⟨b, ha⟩

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

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun x ↦ n * x) (hd :: tl))

Tactic:
rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

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

Goal state before:
pp: case inr
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
| inr hle =>

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ 0 ≤ b + 2

Tactic:
simp only [zero_le]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
k : ℕ
⊢ a ^ k ∣ b ↔ k ≤ multiplicity a b

Tactic:
exact_mod_cast hf.emultiplicity_eq_multiplicity ▸ pow_dvd_iff_le_emultiplicity

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

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization = f

Tactic:
rw [Finsupp.prod, factorization_prod (pow_ne_zero _ <| hf · · |>.ne_zero),
    sum_congr rfl (hf · · |>.factorization_pow)]

Goal state after:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x1 ∈ f.support, single x1 (f x1) = f
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ orderOf x = n

Tactic:
suffices a = 1 by simp [this, ha]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ a = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ ¬0 < multiplicity p a

Tactic:
intro nh

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k p : ℕ
hp : Prime p
⊢ p ^ k * n / p ^ (p ^ k * n).factorization p = n / p ^ n.factorization p

Tactic:
rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]

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

Goal state before:
pp: case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : p ∉ (n.choose k).factorization.support
⊢ (fun x1 x2 ↦ x1 ^ x2) p ((n.choose k).factorization p) = 1

Tactic:
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n ↦ x ^ n

Tactic:
contrapose this

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : Injective fun n ↦ x ^ n
⊢ Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ∑ x ∈ Ico 1 b, if p ^ x ∣ n + 1 then 1 else 0)

Tactic:
sum_boole

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ x ∈ Ico 1 b, n / p ^ x + ↑(#({x ∈ Ico 1 b | p ^ x ∣ n + 1})))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n ↦ x ^ n

Tactic:
contrapose this

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
s : Set G := (fun n ↦ x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : s.Finite
this : Injective fun n ↦ x ^ n
⊢ Set.InjOn (fun n ↦ x ^ n) (Set.Ioi 0)
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ (x + y) ^ p - y ^ p

Tactic:
rw [add_pow_prime_eq hpri, add_right_comm, add_assoc, add_sub_assoc, add_sub_cancel_right]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card ↥s

Tactic:
by
  simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f
⊢ (expand R (p ^ n.succ)) f = (⇑(expand R p))^[n.succ] f

Tactic:
by
    rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]

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

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0

Tactic:
split_ifs with hpn

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : p ∣ n
⊢ f.coeff (n / p) = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
by
  nontriviality S
  have : Nontrivial R := f.domain_nontrivial
  have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
    div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
        calc
          _ ≤ degree (p %ₘ q) := degree_map_le
          _ < degree q := degree_modByMonic_lt _ hq
          _ = _ :=
            Eq.symm <|
              degree_map_eq_of_leadingCoeff_ne_zero _
                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
  exact ⟨this.1.symm, this.2.symm⟩

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

case inr.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff p.natDegree = ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - (a - a) * eval a (p /ₘ (X - C a)) = eval a p

Tactic:
sub_self,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - 0 * eval a (p /ₘ (X - C a)) = eval a p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ (a - a) * eval a (p /ₘ (X - C a)) = 0

Tactic:
sub_self,

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ 0 * eval a (p /ₘ (X - C a)) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ derivative (p ^ 2) = C 2 * p * derivative p

Tactic:
rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) * derivative (X + C c) = C ↑m * (X + C c) ^ (m - 1)

Tactic:
derivative_X_add_C,

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) * 1 = C ↑m * (X + C c) ^ (m - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) * derivative (X + C c) = C 2 * (X + C c)

Tactic:
derivative_X_add_C,

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) * 1 = C 2 * (X + C c)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)

Tactic:
le_rootMultiplicity_iff hpq,

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ (rootMultiplicity x p + rootMultiplicity x q) ∣ p * q
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets

Tactic:
iInf_eq_iInf_finset,

Goal state after:
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ (⨅ t, ⨅ i ∈ t, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case add
R : Type u
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q
a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q
⊢ derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q

pp: case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q

Tactic:
· simp [*, mul_add]

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
⊢ (⇑derivative)^[k + 1] P = 0

Tactic:
by_cases P = 0

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
h✝ : P = 0
⊢ (⇑derivative)^[k + 1] P = 0

case neg
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
h✝ : ¬P = 0
⊢ (⇑derivative)^[k + 1] P = 0