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

Goal state before:
pp: case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i ↦ (f i).totalDegree

Tactic:
| cons a s has hind =>

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

Tactic:
by
  simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]

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

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n

Tactic:
refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_
    rwa [trailingCoeff, ← coeff_mul_X_pow]

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ natDegree 0 = degreeOf none 0

Tactic:
Polynomial.natDegree_zero,

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ 0 = degreeOf none 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b * p).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ (p * C b).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
apply List.sum_le_foldr_max natDegree

Goal state after:
case h0
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ natDegree 0 ≤ 0

case hadd
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ ∀ (x y : S[X]), (x + y).natDegree ≤ max x.natDegree y.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : MonicDegreeEq R n
f : R →+* S
⊢ (Polynomial.map f ↑p).coeff n = 1 ∧ ∀ i > n, (Polynomial.map f ↑p).coeff i = 0

Tactic:
simp +contextual [coeff_map, p.2]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree 0 = degreeOf 0 0

Tactic:
Polynomial.natDegree_zero,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ 0 = degreeOf 0 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
⊢ r ^ 0 ^ a - r ∣ r ^ 0 ^ b - r

Tactic:
zero_pow ha₀,

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
⊢ r ^ 0 - r ∣ r ^ 0 ^ b - r
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
have := congr_arg Neg.neg (geom_sum_mul x n)
  rw [neg_sub, ← mul_neg, neg_sub] at this
  exact this

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), True

Tactic:
forall_const

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

Goal state before:
pp: case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
· have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
    exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Submonoid

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • (a✝ + b✝) = a✝ + b✝

Tactic:
rw [smul_add, ha, hb]

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

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x ∈ antidiagonal (m + n), f.coeff x.1 * g.coeff x.2 ∉ P

Tactic:
← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x ∈ insert (m, n) ((antidiagonal ((m, n).1 + (m, n).2)).erase (m, n)), f.coeff x.1 * g.coeff x.2 ∉ P
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

Tactic:
← Set.image_singleton,

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span (⇑C '' {r})).IsPrime
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
⊢ FiniteType S A

Tactic:
obtain ⟨s, hS⟩ := hA.out
  refine ⟨⟨s, eq_top_iff.2 fun b => ?_⟩⟩
  have le : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S s) := by
    apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))
    simp only [Subalgebra.coe_restrictScalars]
    exact Algebra.subset_adjoin
  exact le (eq_top_iff.1 hS b)

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Goal state after:
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
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff * (X ^ (k - q.natDegree)).leadingCoeff ≠ 0

Tactic:
rw [Polynomial.leadingCoeff_X_pow, mul_one]

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
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥A * finrank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
simpa only [map_mul] using! congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))

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

Goal state before:
pp: R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) x✝) = coeff m 0) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f

Tactic:
simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

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

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

Tactic:
have := AddSubmonoidClass.nsmulMemClass (S := S)
  rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]

Goal state after:
Module: Mathlib.Algebra.CharP.Two

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

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Goal state after:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑↑n = if Even ↑n then 0 else 1

case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑(-↑n) = if Even (-↑n) then 0 else 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : 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
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ (Unitization.starLift (NonUnitalStarSubalgebraClass.subtype s)).range = StarAlgebra.adjoin R ↑s

Tactic:
Unitization.starLift_range

Goal state after:
R : Type u_1
S : 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
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + y ^ 2

Tactic:
add_sq

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
x y : R
⊢ x ^ 2 + y ^ 2 = x ^ 2 + y ^ 2
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p

Tactic:
by rw [h.1, h.2, pow_one]

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
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A →ₐ[R₁] B
hIJ : I ≤ comap f J
r : R₁
⊢ (↑↑(quotientMap J (↑f) hIJ)).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ (B ⧸ J)) r

Tactic:
simp only [RingHom.toFun_eq_coe,
    quotientMap_algebraMap, AlgHom.coe_toRingHom, AlgHom.commutes, Quotient.mk_algebraMap]

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

Goal state before:
pp: α : Type u_1
is l : List α
H : l ~ [] ++ is → (∃ ts' x, l = ts' ++ is) ∨ l ∈ is.permutationsAux []
⊢ l ~ is → l ∈ is.permutations

Tactic:
simpa [permutations, perm_nil] using H

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

Goal state before:
pp: case pos.refine_1.inr
α : 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
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
exact H _ hM'

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

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x ↦ flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (fun x ↦ flatMap (permutations'Aux x✝) (permutations'Aux y✝ x)) l✝.permutations'

Tactic:
apply Perm.flatMap_left

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ ∀ (a : List α),
    a ∈ l✝.permutations' →
      flatMap (permutations'Aux y✝) (permutations'Aux x✝ a) ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ a)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
cons_append,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: (zs ++ [x])).nextOr x d = d
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
refine ⟨?_, nodup_permutations s⟩
  contrapose
  rw [← exists_duplicate_iff_not_nodup]
  intro ⟨x, hs⟩
  rw [duplicate_iff_sublist] at hs
  obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs
  rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]
  use x :: x :: l
  rw [List.duplicate_iff_sublist, ← permutations_take_two]
  exact take_sublist 2 _

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

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Tactic:
have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
    exact Quotient.eq''.mp h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (hl : l ≠ []), Chain r ↑l ↔ IsChain r (l.getLast hl :: l)) →
      ∀ (hl : l ++ [a] ≠ []), Chain r ↑(l ++ [a]) ↔ IsChain r ((l ++ [a]).getLast hl :: (l ++ [a]))

Tactic:
intro m a _H _
    rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))

Tactic:
rw [pairwise_cons]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])
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
inst✝ : QuotientAction X H
b : X
q : G ⧸ H
⊢ ↑(b • Quotient.out q) = b • q

Tactic:
← Quotient.smul_mk,

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : Monoid X
inst✝¹ : MulAction X G
H : Subgroup G
inst✝ : QuotientAction X H
b : X
q : G ⧸ H
⊢ b • ↑(Quotient.out q) = b • q
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
by
  rw [chain_iff_pairwise] at hs
  exact antisymm (hs a ha b hb) (hs b hb a ha)

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

Goal state before:
pp: n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: n.primeFactorsList)

Tactic:
by
  match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro a h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      rw [primeFactorsList]
      refine List.IsChain.cons_cons
        ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)
      exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast

Tactic:
· apply Int.cast_add

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
· simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]
    exact Nat.le_of_dvd (Nat.succ_pos m)

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

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : 1 < ∑ i ∈ range k.succ.succ, x ^ i
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
exact zero_lt_one.trans this

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

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1) ^ k

Tactic:
exact choose_add_le_add_one_pow m k

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

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

Tactic:
ZMod.val_pos

Goal state after:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a ≠ 0
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, 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)

Tactic:
simp only [List.drop, List.drop_length]

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 tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

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

pp: case inl.cons.inr
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
h' : ¬tl = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
· simp [ofDigits]

Goal state after:
case inl.cons.inr
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
h' : ¬tl = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inr.cons
p : ℕ
h : p < 1
head✝ : ℕ
tail✝ : List ℕ
h_nonempty : head✝ :: tail✝ ≠ []
h_ne_zero : (head✝ :: tail✝).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ head✝ :: tail✝, l < p
⊢ 0 = ofDigits 0 (head✝ :: tail✝) - (head✝ :: tail✝).sum

Tactic:
· simp [ofDigits]

Goal state after:
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:
else

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
⊢ (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.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
else

Goal state after:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ count p n.primeFactorsList = n.factorization p
Module: Mathlib.RingTheory.Multiplicity

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

pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

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 [add_comm, emultiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab

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

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)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p ∣ n

Tactic:
else

Goal state after:
n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p ∣ n