mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (⇑(of R M) '' ↑G) = ⊤

Tactic:
use Finset.biUnion S fun f => f.coeff.support

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := ⋯
⊢ adjoin R (⇑(of R M) '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval fun s ↦ (of R M) ↑s)

Tactic:
intro f

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ⇑((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s)

Tactic:
intro f

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = f
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (m : σ →₀ ℕ), coeff m x ∈ I

Tactic:
intro f

Goal state after:
case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
⊢ f ∈ ⇑C '' ↑I → ∀ (m : σ →₀ ℕ), coeff m f ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
intro f

Goal state after:
case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
⊢ ∀ x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (f • x) ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a : ℤ
⊢ a % n = 0 ↔ n ∣ a

Tactic:
dvd_iff_emod_eq_zero

Goal state after:
n a : ℤ
⊢ a % n = 0 ↔ a % n = 0
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

Tactic:
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
  let p := ringChar R
  cases CharP.char_is_prime_or_zero R p with
  | inl hp => simpa using h p hp
  | inr h => have : CharP R 0 := h ▸ inferInstance; exact CharP.charP_to_charZero R

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
⊢ Function.Injective ⇑f

Tactic:
by
  refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf
  rw [Algebra.algebraMap_eq_smul_one] at hr'
  exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

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

Goal state before:
pp: n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
by
    let a := n + 2
    have ha : a ≠ 1 := Nat.succ_succ_ne_one n
    simp only [a, true_iff, Ne, not_false_iff, ha]
    exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩

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

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
have hpd : p ^ (k + l) * p ∣ m * n := by
      let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
      rwa [pow_succ'] at hpmn'

Goal state after:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
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
⊢ span R ↑(Submonoid.closure (↑s ∪ star ↑s)) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
Submonoid.closure_eq_one_union,

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
⊢ span R ({1} ∪ ↑(Subsemigroup.closure (↑s ∪ star ↑s))) = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
revert hm hn
  refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_
  · rwa [Nat.gcd_zero_left]
  · rw [Nat.gcd_rec]
    exact ih (hn.mod hm) hm

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

Goal state before:
pp: α : Type u_1
is is' ts : List α
⊢ (is ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')

Tactic:
induction is generalizing is' with

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

Goal state before:
pp: case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

pp: case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
· rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x

Goal state after:
case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
⊢ g ^ j • a = a ↔ ↑(period g a) ∣ j

Tactic:
match j with
  | (n : ℕ) => rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
  | -(n + 1 : ℕ) =>
    rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod (fun x ↦ a • x) b) ∣ n

Tactic:
by
  rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
intro f

Goal state after:
α : Type u_1
f✝ : α → α
x : α
g : α → α
h : Function.Commute f✝ g
hco : (minimalPeriod f✝ x).Coprime (minimalPeriod g x)
f : α → α
⊢ ∀ {g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : (permutations'Aux x s).length = s.length + 1
⊢ (permutations'Aux x (y :: s)).length = (y :: s).length + 1

Tactic:
simpa using IH

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

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ⋯⟩ ∈ H.subgroupOf K

Tactic:
simp only [Subgroup.mem_subgroupOf]

Goal state after:
case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ H
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
    simp [this]

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

Goal state before:
pp: α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
⊢ ↑l₁.cyclicPermutations = ↑l₂.cyclicPermutations

Tactic:
simpa using h.cyclicPermutations.perm

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k

Tactic:
lhs

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a

Tactic:
rw [chain_coe_cons, nil_append, List.isChain_pair]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = g • x

Tactic:
by
  rw [← smul_one_smul (G ⧸ H) g x, ← QuotientGroup.mk_one, Quotient.smul_coe,
    smul_eq_mul, mul_one]

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

Goal state before:
pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Tactic:
← mem_primeFactorsList_iff_dvd hn.ne' (prime_of_mem_primeFactorsList h)

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∈ n.primeFactorsList
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n.primeFactors.Nonempty ↔ 1 < n

Tactic:
by
  contrapose!
  rw [primeFactors_eq_empty, Nat.le_one_iff_eq_zero_or_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
⊢ (comap f H).index = H.index

Tactic:
by
  have key : ∀ x y : G',
      QuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) := by
    simp only [QuotientGroup.leftRel_apply]
    exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
  refine Nat.card_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)
  · simp_rw [← Quotient.eq''] at key
    refine Quotient.ind' fun x => ?_
    refine Quotient.ind' fun y => ?_
    exact (key x y).mpr
  · refine Quotient.ind' fun x => ?_
    obtain ⟨y, hy⟩ := hf x
    exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

Tactic:
rw [index_eq_two_iff, (Equiv.inv G).exists_congr]
  refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_
  simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (b : ℕ × ℕ),
        (have y := n / a;
            if a * y = n then some (a, y) else none) =
            some b →
          ∀ (b' : ℕ × ℕ),
            (have y := n / a';
                if a' * y = n then some (a', y) else none) =
                some b' →
              b.2 > b'.2

Tactic:
simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt,
    and_imp, Prod.forall, Prod.mk.injEq]

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (a_2 b : ℕ),
        a * (n / a) = n → a = a_2 → n / a = b → ∀ (a b_1 : ℕ), a' * (n / a') = n → a' = a → n / a' = b_1 → b_1 < b
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

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

pp: case succ.succ
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
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
· cases hn rfl

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

case succ.succ
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
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

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

Tactic:
· cases hn rfl

Goal state after:
case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ ∑ k ∈ range n, a / b ^ (k + 1) * b + a / b ^ 0 * b - ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
sum_range_succ,

Goal state after:
a b n : ℕ
⊢ ∑ k ∈ range n, a / b ^ (k + 1) * b + a / b ^ 0 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1

Tactic:
· right
      rwa [show 0 + 1 = 1 from rfl, mul_one] at he

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 4 ^ n

Tactic:
by
  rw [show 4 = 2 ^ 2 by rfl, ← pow_mul]
  apply choose_lt_two_pow
  lia

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

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ 2 ∣ n.centralBinom

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]
  exact two_dvd_centralBinom_succ n.pred

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

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
⊢ ∀ (x : ℤ →+ A), x ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ x.ker

Tactic:
intro f

Goal state after:
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ f.ker
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
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1

Tactic:
rw [Nat.mod_add_div]

Goal state after:
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:
by
  fun_induction go with
  | case1 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]
  | case2 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]
  | case3 =>
    simp_all [Nat.dvd_iff_mod_eq_zero]

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

Goal state before:
pp: p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)

Tactic:
apply maxPowDvdDiv_of_pow_mul_eq

Goal state after:
case hn
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0

case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)

Tactic:
ac_rfl

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

Goal state before:
pp: case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ↑hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
sum_range_succ,

Goal state after:
case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) *
      (∑ x ∈ range tl.length, ofDigits p (List.drop x.succ (hd :: tl)) +
        ofDigits p (List.drop tl.length.succ (hd :: tl))) =
    ↑hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b < ↑n
⊢ multiplicity a b < n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

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 → l1.length = l2.length

Tactic:
hlen

Goal state after:
case zero
b n : ℕ
l1 l2 : List Char
hlen : 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 →
    (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

Tactic:
hlen

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
hlen : 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: case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
norm_cast at hk

Goal state after:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : n✝ + 1 ≤ Nat.find h✝
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: 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
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (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

Tactic:
simp only [hx, if_false]

Goal state after:
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
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

Tactic:
simp only [cast_lt, find_lt_iff] at hm

Goal state after:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (ψ x) ∣ orderOf x

Tactic:
by
  apply orderOf_dvd_of_pow_eq_one
  rw [← map_pow, pow_orderOf_eq_one]
  apply map_one

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
contrapose! hab

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), b.factorization p ≤ a.factorization p
⊢ b ≤ a
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})) =
    ↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))

Tactic:
by
        rw [sum_add_distrib, sum_boole]
        simp

Goal state after: