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

Goal state before:
pp: case pos
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

Tactic:
· simp [he₂]

Goal state after:
case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
⊢ ((X - C x) * P).eraseLead.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
rcases n.lt_or_ge P.natDegree with hn | hn

Goal state after:
case neg.inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

case neg.inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (C r))) = coeff m✝ (coeff m✝¹ (C (C r)))

Tactic:
simp [sumAlgEquiv, C, monomial, coeff]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
rw [← natDegree_neg] at qn
  rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (C r))) = coeff m✝ (C r)

Tactic:
simp [sumAlgEquiv, C, monomial, coeff]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ N

Tactic:
← Nat.sub_add_cancel hnN

Goal state after:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ (N - n + n)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0) → ∃ a, ¬coeff a f = 0 ∧ a 0 = i

pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ¬coeff a f = 0 ∧ a 0 = i) → ∃ x, ¬coeff (cons i x) f = 0

Tactic:
· rintro ⟨m, hm⟩
    exact ⟨cons i m, hm, cons_zero _ _⟩

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ¬coeff a f = 0 ∧ a 0 = i) → ∃ x, ¬coeff (cons i x) f = 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ #(range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)

Tactic:
Finset.card_range,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
⊢ n • x ^ (n - 1) = ↑n * x ^ (n - 1)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
· rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim

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

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

Tactic:
simpa using geom_sum_mul (op x) n

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

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

Tactic:
(h.symm.pow_right _).eq,

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ r = 0

Tactic:
← C_inj,

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ C r = C 0

R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ Type ?u.41
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
⊢ p ∈ Ideal.span ↑s

Tactic:
generalize hn : p.natDegree = k

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
k : ℕ
hn : p.natDegree = k
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ s),
          algebraMap_mem' := ⋯ }.unop.toSubsemiring =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)

Tactic:
unop_toSubsemiring,

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ s)).unop =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_2
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ (algebraMap R A) r ∈ toSubmodule S * toSubmodule T

Tactic:
rw [← one_mul (algebraMap _ _ _)]

Goal state after:
case refine_2
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ 1 * (algebraMap R A) r ∈ toSubmodule S * toSubmodule T
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * toSubmodule S * toSubmodule T
⊢ x * y ∈ toSubmodule S * toSubmodule T

Tactic:
isIdempotentElem_toSubmodule

Goal state after:
case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * toSubmodule T
⊢ x * y ∈ toSubmodule S * toSubmodule T
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
⊢ ∑ i ∈ d.support, ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ m * n

Tactic:
have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
    rw [← Finset.sum_mul]
    apply mul_le_mul' (.trans _ hF) le_rfl
    rw [MvPolynomial.totalDegree]
    exact Finset.le_sup_of_le hd le_rfl

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
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∑ i ∈ d.support, ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ m * n
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Tactic:
convert! ← modEq_and_modEq_iff_modEq_lcm using 1
  rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf).symm (f a) = (Quotient.mk (ker f)) a

Tactic:
by
  apply (Ideal.quotientKerAlgEquivOfSurjective hf).injective
  simp

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

Goal state before:
pp: R : Type u
S✝ : Type v
F : Type w
inst✝⁹ : Ring R
inst✝⁸ : Semiring S✝
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
S : Type v
inst✝² : Ring S
I : Ideal R
J : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ LeftInverse (⇑(quotientMap I ↑f.symm ⋯)) (↑↑(quotientMap J ↑f ⋯)).toFun

Tactic:
rintro ⟨r⟩
    simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe,
      quotientMap_mk, RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Fintype α
⊢ Finset (List α)

Tactic:
let univSubsets := ((Finset.univ : Finset α).powerset.1 : (Multiset (Finset α)))

Goal state after:
case refine_1
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
⊢ Finset (List α)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x ↦ a :: x).snd ++ [a :: (ts ++ [t])]

Tactic:
simp [map_permutationsAux2]

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
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : x ∈ s ∨ Star.star x ∈ s
⊢ p x ⋯

Tactic:
obtain (hx | hx) := hx

Goal state after:
case inl
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
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

case inr
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
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ p x ⋯
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x

Tactic:
rwa [tsub_add_cancel_of_le h]

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ tl = []

Tactic:
simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h

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

Goal state before:
pp: case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ 1
⊢ ∃ a, a ∈ [] ∧ p ∣ a

Tactic:
exact absurd h pp.not_dvd_one

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H

Tactic:
smul_def,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (↑b • c)⁻¹ * b • x✝¹ ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (↑b • c)⁻¹ * b • x✝¹ ∈ H

Tactic:
smul_def,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (↑b • c)⁻¹ * ↑b • x✝¹ ∈ H
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ n.primeFactorsList

Tactic:
refine perm_of_prod_eq_prod ?_ ?_ ?_

Goal state after:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l.prod = n.primeFactorsList.prod

case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

pp: case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

pp: case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Tactic:
· exact (ha rfl).elim

Goal state after:
case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
mem_primeFactorsList_mul ha.ne' hb.ne',

Goal state after:
case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
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
K : Subgroup G'
⊢ (comap (f.comp K.subtype) H).index = H.relIndex (map f K)

Tactic:
index_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ H.relIndex (f.comp K.subtype).range = H.relIndex (map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ (comap f ⊥).index = Nat.card ↥f.range

Tactic:
index_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ ⊥.relIndex f.range = Nat.card ↥f.range
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'
⊢ (map f H).index = (comap f (map f H)).index * f.range.index

Tactic:
index_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (map f H).relIndex f.range * f.range.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
rw [← relIndex_top_right] at hH hK ⊢
  exact relIndex_inf_ne_zero hH hK

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: case zero
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
inst✝ : Module (ZMod 0) R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

pp: case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
· obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _
      simp [ZMod, Int.cast_comm]

Goal state after:
case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
· apply Fin.val_add

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

Goal state before:
pp: m n : ℕ
⊢ (m % n).gcd n = m.gcd n

Tactic:
exact Nat.ModEq.gcd_eq (by simp [Nat.ModEq])

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

Goal state before:
pp: m n : ℕ
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
by
  suffices (m % n).gcd n = m.gcd n by grind
  exact Nat.ModEq.gcd_eq (by simp [Nat.ModEq])

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∈ {∑ x ∈ (n + 1 + 1).properDivisors, x}

Tactic:
eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _),

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∈ (n + 1 + 1).properDivisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ ∑ i ∈ range n.succ, a / b ^ i * 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 - ∑ 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)
Module: Mathlib.Data.Nat.Choose.Bounds

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

Tactic:
choose_succ_succ',

Goal state after:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ 2 ^ (n + 1)
Module: Mathlib.Data.Nat.Choose.Central

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

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

Goal state after:
n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 2 ^ (2 * n)
Module: Mathlib.Data.Nat.Choose.Central

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

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

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

Goal state before:
pp: case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p tl = ofDigits p (hd :: tl).tail

Tactic:
List.tail_cons

Goal state after:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p tl = ofDigits p tl
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)

Tactic:
cases digits with
    | nil => simp
    | cons hd tl =>
      rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
      apply add_lt_of_lt_sub
      apply lt_of_lt_of_le (b := p)
      · exact w₁ hd List.mem_cons_self
      · rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

Goal state after: