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

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ ↑(insert 1 y) * ↑(insert 1 y) ⊆ ↑(span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y))

Tactic:
coe_insert

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ insert 1 ↑y * insert 1 ↑y ⊆ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
n

Goal state after:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
⊢ f.coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hx✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
⊢ ∀ (n : ℕ), (f • g).coeff n ∈ I

Tactic:
n

Goal state after:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hx✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f • g).coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).degree ≤ ↑n

Tactic:
apply le_trans (degree_mul_le _ _) _

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ p.degree + (X ^ (n - p.natDegree)).degree ≤ ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
⊢ I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Tactic:
by
  intro r hr
  simp only [mem_leadingCoeffNth] at hr ⊢
  rcases hr with ⟨p, hpI, hpdeg, rfl⟩
  refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩
  refine le_trans (degree_mul_le _ _) ?_
  grw [hpdeg, degree_X_pow_le]
  rw [← Nat.cast_add, add_tsub_cancel_of_le H]

Goal state after:
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
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
n

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
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
⊢ coeff n 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
f g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
⊢ ∀ (m : σ →₀ ℕ), coeff m (f • g) ∈ I

Tactic:
n

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 g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f • g) ∈ I
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
⊢ ↑a = ↑b

Tactic:
by
  wlog hle : a ≤ b
  · exact (this R p h.symm (le_of_not_ge hle)).symm
  rw [Nat.modEq_iff_dvd' hle] at h
  rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
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
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
x✝ : ↥s
⊢ ((Algebra.adjoin R ↑s).val.comp algHom) ↑x✝ = ↑x✝

Tactic:
simp [algHom]

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✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer

Tactic:
coe_centralizer

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (s ∪ star s).centralizer.centralizer = (s ∪ star s).centralizer.centralizer
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.permutationsAux (t :: is)).length + is.length ! * is.length.succ

Tactic:
Nat.add_comm (_ * _),

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
⊢ (ts.permutationsAux (t :: is)).length + is.length * is.length ! + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
⊢ ∀ y ∈ List.range (minimalPeriod f x), f^[m] x = f^[y] x → m = y

Tactic:
n

Goal state after:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
⊢ n ∈ List.range (minimalPeriod f x) → f^[m] x = f^[n] x → m = n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
x : α × β
⊢ IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2

Tactic:
simp [IsPeriodicPt]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
n : ℕ
⊢ IsPeriodicPt (Pi.map f) n x ↔ ∀ (i : ι), IsPeriodicPt (f i) n (x i)

Tactic:
simp [IsPeriodicPt]

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

Goal state before:
pp: case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (∀ (m : M), m • a = a) → (orbit M a).Subsingleton

Tactic:
rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩

Goal state after:
case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
h : ∀ (m : M), m • a = a
m p : M
⊢ (fun m ↦ m • a) m = (fun m ↦ m • a) p
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
this : ∀ (g : Ω), Finite ↑g.orbit
⊢ Finite ((ω : Ω) × ↑ω.orbit)

Tactic:
exact Finite.instSigma

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

Goal state before:
pp: case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

Tactic:
simp [hx, hy] at hxy

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
⊢ ∀ (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x

Tactic:
n

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
⊢ 0 < n → x ^ n = 0 → ¬Prime x
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G ⧸ H
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) g) = g

Tactic:
cases g using Quotient.inductionOn' with

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
⊢ ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K
Module: Mathlib.Data.ZMod.Basic

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

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

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).divisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
ext a

Goal state after:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ 1 ∈ n.properDivisors

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).properDivisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range k)

Tactic:
ext a

Goal state after:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range k)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ range k, f (p ^ x)

Tactic:
by
  simp [h, properDivisors_prime_pow]

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

Goal state before:
pp: a b n : ℕ
⊢ ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n) ≤
    ∑ i ∈ range n, a / b ^ i + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
gcongr with i hi
      rw [pow_succ, ← Nat.div_div_eq_div_mul]
      exact Nat.div_mul_le_self _ _

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
⊢ f = g

Tactic:
ext a

Goal state after:
n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
a : ZMod n
⊢ f a = g a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : G)

Goal state after:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
simpa [sub_eq_add] using sub_add_sub_cancel x y z

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
· simp [hf.emultiplicity_eq_multiplicity]

Goal state after:
case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a : ℕ
ha : a ∈ {x | x ≠ 0}
b : ℕ
hb : b ∈ {x | x ≠ 0}
h : a.factorization = b.factorization
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ Nat.find h1 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
· rw [emultiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n

Tactic:
apply Nat.not_succ_le_self

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m + m) = a ^ n

Tactic:
simp [tsub_add_cancel_of_le hmn.le]

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

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hm₀ := eq_or_ne m 0
  · simp
  obtain rfl | hn₀ := eq_or_ne n 0
  · simp
  · rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]

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

Goal state before:
pp: n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)

Tactic:
ext
  simp [one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]

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

Goal state before:
pp: case refine_2
h2 : _root_.Prime 2
b : Bool
⊢ ∀ (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
n

Goal state after:
case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
⊢ (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX ≠ 0

Tactic:
simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
by
    rw [map_mul, expand_C, map_pow, expand_X, pow_one]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [hf, map_zero, natDegree_zero, zero_mul]

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

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h✝ : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
rename_i _ _ _ h'

Goal state after:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t

pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t

Tactic:
· rw [ha, count_cons_self, add_comm]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
by simp [h]

Goal state after:
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 - (X - C a) * (p /ₘ (X - C a))) = eval a p

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - eval a ((X - C a) * (p /ₘ (X - C a))) = eval a p
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 - eval a (X - C a) * eval a (p /ₘ (X - C a)) = eval a p

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a p - (eval a X - eval a (C a)) * eval a (p /ₘ (X - C a)) = eval a p
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
I : Set ι
hI : I.Finite
V : ι → Set α
u : (i : ι) → ι' i
hu : ∀ (i : ι), p i (u i) ∧ s i (u i) ⊆ V i
⊢ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ ⋂ i ∈ I, V i

Tactic:
exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩

Goal state after:
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
⊢ eval a (X - C a) * eval a (p /ₘ (X - C a)) = 0

Tactic:
eval_sub,

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

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

Tactic:
eval_sub,

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0

Tactic:
by
  classical
  simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff, multiplicity_eq_zero,
    dvd_iff_isRoot, not_imp_not]

Goal state after:
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: α : Type u_2
β : Type u_3
m : α → β
f : Filter β
⊢ (comap m f).ker = m ⁻¹' f.ker

Tactic:
ext a

Goal state after:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) • X ^ (n - k)

Tactic:
by
  rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : Type u_3
κ : Type u_4
f : Filter α
p : κ → Prop
s : κ → Set α
h : f.HasBasis p s
⊢ (pi fun x ↦ f).HasBasis (fun Ik ↦ Ik.1.Finite ∧ p Ik.2) fun Ik ↦ Ik.1.pi fun x ↦ s Ik.2

Tactic:
by
  refine hasBasis_pi_same_index (fun _ ↦ h) (fun I k hI hk ↦ ?_)
  rcases h.mem_iff.mp (biInter_mem hI |>.mpr fun i hi ↦ h.mem_of_mem (hk i hi))
    with ⟨k₀, hk₀, hk₀'⟩
  exact ⟨k₀, hk₀, fun i hi ↦ hk₀'.trans (biInter_subset_of_mem hi)⟩

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
f : (i : ι) → α i
⊢ (pi fun x ↦ pure (f x)) = pure f

Tactic:
simp only [← principal_singleton, pi_principal, univ_pi_singleton]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inl.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inl.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
try exact Or.inl ha

Goal state after:
case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a