mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree = p.totalDegree

Tactic:
classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (by simpa) fun m : σ →₀ ℕ => Multiset.card (toMultiset m)
    have hb : b ∉ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ (monomial p.natDegree) p.leadingCoeff = p

Tactic:
classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Goal state after:
case insert.inr.inl.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
IH : (∅.sum f).degree = ∅.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (∅.sum f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (∅.sup fun i ↦ (f i).degree)

case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).trailingDegree = ↑n

Tactic:
rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#f.eraseLead.support = 0

Tactic:
eraseLead_support

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support

Tactic:
eraseLead_support

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c

Tactic:
rw [card_support_eraseLead, fc, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Tactic:
· refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ φ r * a default ^ d default = φ r * d.prod fun n e ↦ a n ^ e

Tactic:
rw [Finsupp.unique_single d, Finsupp.prod_single_index]

Goal state after:
case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ φ r * a default ^ (Finsupp.single default (d default)) default = φ r * a default ^ d default

case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ a default ^ 0 = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ eval₂ φ a ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f

Tactic:
by
  rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm]
  rw [AlgEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
· simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ p.leadingCoeff * p.leadingCoeff⁻¹ = 1

Tactic:
mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
⊢ (∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (natDegree ∘ f) s

Tactic:
by
  simpa using! natDegree_multiset_sum_le (s.val.map f)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : (∑ i, C (x i) * X ^ k i).support = image k univ
⊢ #univ = n

Tactic:
card_fin

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : (∑ i, C (x i) * X ^ k i).support = image k univ
⊢ n = n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.Monic ↔ p.Monic

Tactic:
by
  simp only [Monic, leadingCoeff, natDegree_restriction]
  rw [← @coeff_restriction _ _ p]
  exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
⊢ (g.comp f).FiniteType

Tactic:
exact Algebra.FiniteType.trans hf hg

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Tactic:
let d := gcd m c
  rw [modEq_iff_dvd] at h ⊢
  refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (gcd_dvd_right ..), Int.sub_mul]
    exact Int.ediv_dvd_ediv (gcd_dvd_left ..) h
  · rw [gcd_div (gcd_dvd_left ..) (gcd_dvd_right ..), natAbs_natCast,
      Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : f y = 0
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)

Tactic:
← mem_ker

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case inl_add_inr
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : f (Unitization.inl r) + ↑a = 0
⊢ Unitization.inl r + ↑a = 0

Tactic:
← Unitization.algebraMap_eq_inl,

Goal state after:
case inl_add_inr
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : f ((algebraMap R (Unitization R ↥s)) r) + ↑a = 0
⊢ Unitization.inl r + ↑a = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) (∑ i, f i * e i)) i = g i

Tactic:
rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]

Goal state after:
case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ (Quotient.mk (I i)) (f i * e i) = g i

case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (Quotient.mk (I i)) (f x * e x) = 0
Module: Mathlib.Data.Nat.Prime.Basic

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

Tactic:
simpa using Exists.intro 2 Nat.prime_two

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
⊢ IsPeriodicPt f m x

Tactic:
by
  rcases hx with ⟨r, hr, hr'⟩
  suffices n ≤ (n / r + 1) * r by
    unfold IsPeriodicPt IsFixedPt
    convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
      rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
  rw [Nat.add_mul, one_mul]
  exact (Nat.lt_div_mul_add hr).le

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (if h : x ∈ periodicPts f then Nat.find h else 0) x

Tactic:
split_ifs with hx

Goal state after:
case pos
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).Nodup

Tactic:
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on List.nodup_range]
  intro m hm n hn hmn
  rw [List.mem_range] at hm hn
  rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r ↑(List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x))) ↔
    ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
← Cycle.map_coe,

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (Cycle.map (fun n ↦ f^[n] x) ↑(List.range (minimalPeriod f x))) ↔
    ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : 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
⊢ (x :: l).permutations'.Nodup

Tactic:
rw [permutations']

Goal state after:
case cons
α : 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
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
⊢ some (if a = x then y else (y :: tail).nextOr a d) = (y :: tail)[idxOf a (x :: y :: tail)]?

Tactic:
split_ifs with hx

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : a = x
⊢ some y = (y :: tail)[idxOf a (x :: y :: tail)]?

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) = (y :: tail)[idxOf a (x :: y :: tail)]?
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

Tactic:
simp only [Set.smul_mem_smul_set_iff, hx]

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

Goal state before:
pp: m n : ℕ
⊢ IsUnit ↑m ↔ m.Coprime n

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
  have H' := val_coe_unit_coprime H.unit
  rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'
  rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']
  exact Nat.gcd_rec n m

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

Goal state before:
pp: n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
constructor
  · obtain (_ | _ | n) := n
    · simpa [ZMod] using not_subsingleton _
    · simp [ZMod]
    · simpa [ZMod] using not_subsingleton _
  · rintro rfl
    infer_instance

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

Goal state before:
pp: case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

Tactic:
choose_zero_right

Goal state after:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n

case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y : G
⊢ x - y = x + y

Tactic:
by simp [neg_eq_self, sub_eq_add_neg]

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

Goal state before:
pp: b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: n p : ℕ
hnp : 1 < p ∧ n ≠ 0
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

Tactic:
fun_induction go with

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

Goal state before:
pp: case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
length_digits b n hb h,

Goal state after:
case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ n < b ^ k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
rw [length_digits b n hb h, ← log_lt_iff_lt_pow hb h]

Goal state after:
case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ log b n < k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
· simpa only [digits_of_lt (b + 2) n hn hnb]

Goal state after:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n : ℕ
⊢ digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits

Tactic:
induction n using Nat.binaryRecFromOne with
  | zero => simp
  | one => simp
  | bit b n h ih =>
    rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

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

Goal state before:
pp: case zero
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length

Tactic:
simp only [Nat.toDigitsCore]

Goal state after:
case zero
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → l1.length = l2.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length

Tactic:
simp only [Nat.toDigitsCore]

Goal state after:
case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length →
      (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
        (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
by rw [ha] at h; exact h 1

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

Goal state before:
pp: n p : ℕ
⊢ n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
← notMem_support_iff,

Goal state after:
n p : ℕ
⊢ p ∉ n.factorization.support ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
⊢ p ∉ n.factorization.support ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
support_factorization,

Goal state after:
n p : ℕ
⊢ p ∉ n.primeFactors ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
· exact ((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
by_cases hl : l = 0
      · simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]
      rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
      simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]
      rw [Finset.sum_comm]
      simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]
      rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
      ring

Goal state after:
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
⊢ orderOf x = n

Tactic:
obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)
  suffices a = 1 by simp [this, ha]
  -- Assume `a` is not one...
  by_contra h
  have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm
  -- Use the minimum prime factor of `a` as `p`.
  refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_
  rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
  · exact Nat.minFac_dvd a
  · rw [isOfFinOrder_iff_pow_eq_one]
    exact Exists.intro n (id ⟨hn, hx⟩)

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

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q

Tactic:
simp [pp.factorization, hqp.symm]

Goal state after: