mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
| F f

Tactic:
rw [lift_unique' F]
    simp [lift_apply]

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
| f.coeff.sum fun a b ↦ b • F (single a 1)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ((monomial n) a).support.max = ↑n

Tactic:
support_monomial n ha,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ {n}.max = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < ↑n

Tactic:
subst hp

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (p.sum fun a b ↦ ((C.comp f) b * X ^ a).coeff n) = f (p.coeff n)

Tactic:
sum

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 ∈ p.support, ((C.comp f) (p.coeff n_1) * X ^ n_1).coeff n = f (p.coeff n)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
⊢ (X + C a).degree = 1

Tactic:
by
  have : degree (C a) < degree (X : R[X]) :=
    calc
      degree (C a) ≤ 0 := degree_C_le
      _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
      _ = degree X := degree_X.symm
  rw [degree_add_eq_left_of_degree_lt this, degree_X]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
· simp only [hq, mul_zero, leadingCoeff_zero]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ g (eval₂ f x p) = eval₂ g (g x) (map f p)

Tactic:
eval₂_at_apply,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ g (eval₂ f x p) = g (eval x (map f p))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hf : IsUnit (leadingCoeff 0)
H : IsUnit (map φ 0)
dz : degree 0 = 0
⊢ False

Tactic:
simp at H

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval₂ ψ (ψ a) (map (algebraMap R S) p)

Tactic:
eval₂_at_apply,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = ψ (eval a (map (algebraMap R S) p))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ ∀ x_1 ∈ t, x_1 ∉ (Finsupp.indicator t fun i x_2 ↦ x i).support → X x_1 ^ (Finsupp.indicator t fun i x_2 ↦ x i) x_1 = 1

Tactic:
· intro i hi hi'
    rw [Finsupp.mem_support_iff, ne_eq, not_not] at hi'
    rw [hi', pow_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support ∆ q.support ⊆ (p + q).support

Tactic:
rw [symmDiff_def, Finset.sup_eq_union]
  apply Finset.union_subset
  · exact support_sdiff_support_subset_support_add p q
  · rw [add_comm]
    exact support_sdiff_support_subset_support_add q p

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0

Tactic:
by
  classical
  split_ifs with h
  · conv_rhs => rw [← coeff_mul_monomial _ s]
    rw [tsub_add_cancel_of_le h]
  · contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl

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

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))

pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))

Tactic:
· intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ degreeOf i f

Tactic:
degreeOf_eq_sup i

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ f.support.sup fun m ↦ m i
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
k : Fin n
⊢ (cons y s).tail k = s k

Tactic:
by simp only [tail_apply, cons_succ]

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

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ((monomial n) a).support.min = ↑n

Tactic:
support_monomial n ha,

Goal state after:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ {n}.min = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = ↑(p.natTrailingDegree + q.natTrailingDegree)

Tactic:
trailingDegree_mul' h,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree = ↑(p.natTrailingDegree + q.natTrailingDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₁
⊢ (commAlgEquiv R S₁ S₂) (X i) = C (X i)

Tactic:
ext x y; simp [X, C, monomial, commAlgEquiv]

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

Goal state before:
pp: case refine_3
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
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f →
          eval₂ i (⅟x) (reflect N g) * x ^ N = eval₂ i x g →
            eval₂ i (⅟x) (reflect N (f + g)) * x ^ N = eval₂ i x (f + g)

Tactic:
· intros
    simp [*, add_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈ cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Tactic:
by
  simpa using congr(x ∈ $image_support_finSuccEquiv)

Goal state after:
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:
by
  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.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG

Tactic:
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (∑ i ∈ range n, X ^ i).comp (X + 1) = ∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i

Tactic:
ext i
  trans (n.choose (i + 1) : R); swap
  · simp only [finsetSum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]
    rw [Finset.sum_eq_single i, if_pos rfl]
    · simp +contextual only [@eq_comm _ i, if_false,
        imp_true_iff]
    · simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt,
        Nat.cast_zero, Finset.mem_range, not_lt, if_true, imp_true_iff]
  induction n generalizing i with
  | zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  | succ n ih =>
    simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f (Algebra.adjoin R ↑(s.preimage ⇑f ⋯)) = map f S

Tactic:
by
      rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
      rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
      exact map_mono le_top

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
⊢ f ∈ map C (comap C I)

Tactic:
| _ _ ih
   => 

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
⊢ f ∈ map C (comap C I)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case e'_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ C r = (finSuccEquiv R d).symm (Polynomial.C (C r))

Tactic:
simp [← finSuccEquiv_comp_C_eq_C]

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

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ c + n * b [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
modEq_add_modulus_mul_iff

Goal state after:
n a b c : ℤ
⊢ a ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Nat.card α - 1 = card α - 1

Tactic:
Nat.card_eq_fintype_card

Goal state after:
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α - 1 = card α - 1
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup

Tactic:
by
  have h_nodup : l.val.Nodup := l.nodup
  rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup
  rw [← Finset.coe_toList l]
  exact nodup_permutations l.val.toList (h_nodup)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations' = (map f ts).permutations'

Tactic:
by
  induction ts with
  | nil => rfl
  | cons t ts ih => simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ (t :: ts).permutationsAux is
⊢ l ~ t :: ts ++ is

Tactic:
permutationsAux_cons,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations
⊢ l ~ t :: ts ++ is
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
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
permutationsAux_cons,

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
⊢ (foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations).length +
      is.length ! =
    ((t :: ts).length + is.length)!
Module: Mathlib.Data.List.Permutation

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

Tactic:
permutationsAux_cons,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations
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 : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b : A
hb : b ∈ adjoin R s
⊢ p ⟨b, hb⟩

Tactic:
by
    induction hb using adjoin_induction with
    | mem _ h => exact mem _ h
    | algebraMap _ => exact algebraMap _
    | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂
    | star _ _ h => exact star _ h

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

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

Tactic:
Int.add_emod_right,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (i % ↑(period g a)) • a = g ^ i • a
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
h : {n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
⊢ minimalPeriod (f i) (x i) ∣ sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

pp: case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
h : ¬{n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
⊢ minimalPeriod (f i) (x i) ∣ sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}

Tactic:
· exact (Nat.sInf_mem h).2 i

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
x : (i : ι) → α i
i : ι
h : ¬{n | 0 < n ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}.Nonempty
⊢ minimalPeriod (f i) (x i) ∣ sInf {n | n > 0 ∧ ∀ (i : ι), minimalPeriod (f i) (x i) ∣ n}
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case refine_5
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
a x : ↥(adjoin R s)
hx : f x = g x
⊢ f (star x) = g (star x)

Tactic:
· simp only [map_star, hx]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ ∑ g, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X) × G)

Tactic:
← Fintype.card_sigma,

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ Fintype.card ((g : G) × ↑(fixedBy X g)) = Fintype.card (Quotient (orbitRel G X) × G)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

Tactic:
simp [zero_mul]

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

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

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

Goal state after:
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.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1

Tactic:
· rw [or_iff_not_imp_right]
      intro ne_n
      have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
      symm
      rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]
      exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

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

Goal state before:
pp: case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = ↑x.val

Tactic:
ZMod.natCast_val

Goal state after:
case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = x.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = ↑x.val

Tactic:
ZMod.natCast_val

Goal state after:
case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = x.cast
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k

Tactic:
exact Nat.div_lt_self (by simpa) (by simpa)

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val % n

Tactic:
by rw [Nat.mod_eq_of_lt (-a).val_lt]

Goal state after: