mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ Injective2 cons

Tactic:
refine fun x₀ y₀ x y h ↦ ?_

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
⊢ x₀ = y₀ ∧ x = y
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0

Tactic:
by
  rw [← cons_zero_single_eq_single_succ, cons_injective2.eq_iff, and_comm]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Tactic:
simp only [eraseLead, coeff_erase]

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

Goal state before:
pp: case neg.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

pp: case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
· simp [hy, hy0]

Goal state after:
case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p + -q).coeff n = -q.coeff n

Tactic:
coeff_add_eq_right_of_lt,

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (-q).coeff n = -q.coeff n

R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ p.natDegree < n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree * (-X).natDegree = p.natDegree

Tactic:
natDegree_neg,

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree * X.natDegree = p.natDegree
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
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f

Tactic:
refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf
  · simp
  · intro n r _ hnN
    simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
    conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
    rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
  · intros
    simp [*, add_mul]

Goal state after:
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' _]

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

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff ≠ 0
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' _]

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

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ ¬n✝ + 1 + 1 = 0

Tactic:
exact Nat.succ_ne_zero _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (X * p).reverse = p.reverse

Tactic:
rw [commute_X p, reverse_mul_X]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (-C 1 * f) = -reflect N f

Tactic:
← C_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (C (-1) * f) = -reflect N f
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
intro h
    use tail m
    rw [← h.2, cons_tail]
    simp [h.1]

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
rintro h f g - hg rfl hdg

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hg : g.Monic
hp : (f * g).Monic
hp1 : f * g ≠ 1
h : ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 ((f * g).natDegree / 2) → ¬q ∣ f * g
hdg : g.natDegree ∈ Ioc 0 ((f * g).natDegree / 2)
⊢ False
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:
rw [Finset.card_range, nsmul_eq_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
by
  apply eq_tsub_of_add_eq
  simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff (-q).natDegree = 1

Tactic:
natDegree_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff q.natDegree = 1
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:
rw [smul_eq_mul, coeff_mul]

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 : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * g.coeff x.2 ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
x : R
hx : x ∈ I.leadingCoeff
⊢ x ∈ J.leadingCoeff

Tactic:
rcases (I.mem_leadingCoeff x).1 hx with ⟨p, hpI, rfl⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
p : R[X]
hpI : p ∈ I
hx : p.leadingCoeff ∈ I.leadingCoeff
⊢ p.leadingCoeff ∈ J.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
⊢ I.leadingCoeff * J.leadingCoeff ≤ (I * J).leadingCoeff

Tactic:
refine (mul_le).2 ?_

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
⊢ ∀ r ∈ I.leadingCoeff, ∀ s ∈ J.leadingCoeff, r * s ∈ (I * J).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
⊢ False

Tactic:
obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ (algebraMap R (MvPolynomial (↥s) R)) r ∣ a' * b'

Tactic:
convert! _root_.map_dvd (killCompl Subtype.val_injective) hd

Goal state after:
case e'_3
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ (algebraMap R (MvPolynomial (↥s) R)) r = (killCompl ⋯) ((algebraMap R (MvPolynomial σ R)) r)

case e'_4
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ a' * b' = (killCompl ⋯) ((rename Subtype.val) a' * (rename Subtype.val) b')
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
⊢ (RingHom.id A).FiniteType

Tactic:
by simp [FiniteType]; infer_instance

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j j' : Fin k
x✝ : j' ∈ Finset.univ
⊢ c j j' ∈ Set.range b ∪ Set.range (Function.uncurry c)

Tactic:
by simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩]

Goal state after:
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
n : σ →₀ ℕ
⊢ coeff n (f • g) ∈ I

Tactic:
rw [smul_eq_mul, coeff_mul]

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 : σ →₀ ℕ
⊢ ∑ x ∈ antidiagonal n, coeff x.1 f * coeff x.2 g ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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

Goal state before:
pp: case hn
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, ¬Even a

Tactic:
use 1

Goal state after:
case h
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ¬Even 1
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case hn
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ∃ a, ¬Even a

Tactic:
use 1

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ¬Even 1
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) ↔ I = ⊥

Tactic:
constructor
  · intro h
    rw [← map_eq_bot_iff_of_injective h.1]
    exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm
  · exact fun h => ⟨(injective_iff_ker_eq_bot _).mpr <| by rw [mk_ker, h], mk_surjective⟩

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

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
⊢ x = p ∧ y = p

Tactic:
obtain rfl | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›

Goal state after:
case inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p * 1
this : 1 ∣ p
⊢ x = p ∧ y = p

case inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p
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 ↑(centralizer R s)) = (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
⊢ (↑(centralizer R s) ∪ star ↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer
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
⊢ p a ha

Tactic:
refine Algebra.adjoin_induction (fun x hx ↦ ?_) algebraMap add mul ha

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : 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
⊢ p x ⋯
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| (m ^ (n % period m a) * m ^ (period m a * (n / period m a))) • a

Tactic:
mul_smul,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a) • m ^ (period m a * (n / period m a)) • a
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| (g ^ (j % ↑(period g a)) * g ^ (↑(period g a) * (j / ↑(period g a)))) • a

Tactic:
mul_smul,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| g ^ (j % ↑(period g a)) • g ^ (↑(period g a) * (j / ↑(period g a))) • a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s t : List α
p : s ~ t
⊢ s.permutations' ~ t.permutations'

Tactic:
induction p with
  | nil => simp
  | cons _ _ IH => exact IH.flatMap_right _
  | swap =>
    dsimp
    rw [flatMap_assoc, flatMap_assoc]
    apply Perm.flatMap_left
    intro l' _
    apply perm_permutations'Aux_comm
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

Tactic:
refine Quot.inductionOn a (fun x ↦ ?_)

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
x : α
⊢ Quot.mk (⇑(orbitRel G α)) x = b
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
induction s using Quot.inductionOn with | _ l

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ (g⁻¹ * h * g) • a = (g⁻¹ * g) • a ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
inv_mul_cancel,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ (g⁻¹ * h * g) • a = 1 • a ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length

Tactic:
induction s using Quot.inductionOn with | _ l

Goal state after:
case h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup

Tactic:
induction s using Quot.inductionOn with | _ l

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (a ∈ S ↔ b ∈ S) → ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S

Tactic:
intros; split_ifs <;> simp [*]

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

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
· have := isRotated_nil_iff.1 hab
        contradiction

Goal state after:
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
rcases pp.dvd_or_dvd h with hd | hd

Goal state after:
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x

Tactic:
mul_smul,

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ • g₂ • x = 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
⊢ (g⁻¹ * ⋯.choose) • g⁻¹ • x = g⁻¹ • x

Tactic:
mul_smul,

Goal state after:
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
⊢ g⁻¹ • ⋯.choose • g⁻¹ • x = g⁻¹ • x
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.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
List.mem_union_iff

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 ∨ p ∈ b.primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Tactic:
exact one_mem _

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
· rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

Goal state after: