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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)

Tactic:
exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ t.prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) t).prod

Tactic:
refine Multiset.induction_on t ?_ fun a t ht => ?_; · simp
  rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x ↦ X - C x) t).prod.coeff ((Multiset.map (fun x ↦ X - C x) t).prod.natDegree - 1)

Tactic:
congr

Goal state after:
case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map (fun x ↦ X - C x) t).prod.natDegree
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
x : R
n : ℕ
f : R →+* S
⊢ f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i

Tactic:
simp [map_sum f]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
x y : R
n : ℕ
f : R →+* S
⊢ f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)

Tactic:
simp [map_sum f]

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

Goal state before:
pp: case a
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 : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ y ^ (n - 1 - (n - 1 - x✝)) * x ^ (n - 1 - x✝) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
congr

Goal state after:
case a.e_a.e_a
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 : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ n - 1 - (n - 1 - x✝) = x✝
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 - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
  rw [sub_add_cancel] at this
  rw [← this, add_sub_cancel_right]

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
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))

Tactic:
congr

Goal state after:
case e_a.e_a
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
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)
x : A
hx : x ∈ p
⊢ ∀ y ∈ q, x * y ∈ ↑(Subalgebra.toSubmodule (adjoin R (s ∪ t)))

Tactic:
y

Goal state after:
case refine_1
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)
x : A
hx : x ∈ p
y : A
⊢ y ∈ q → x * y ∈ ↑(Subalgebra.toSubmodule (adjoin R (s ∪ t)))
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)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ span (↥(adjoin R s)) q

Tactic:
exact subset_span hy

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
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m

Tactic:
by
  apply op_injective
  simp only [op_sub, op_mul, op_pow, op_sum]
  have : (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
      ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
    refine sum_congr rfl fun k _ => ?_
    have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
    simpa [Commute, SemiconjBy] using hp
  simp only [this]
  convert! (Commute.op h).mul_geom_sum₂_Ico hmn

Goal state after:
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
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
intro f g _ hg n

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

Goal state before:
pp: σ : 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
⊢ (natDegree ∘ fun i ↦ (algebraMap R R[X]) (F.coeff i) * i.prod fun n e ↦ f n ^ e) d ≤ m * n

Tactic:
Function.comp_apply,

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
⊢ ((algebraMap R R[X]) (F.coeff d) * d.prod fun n e ↦ f n ^ e).natDegree ≤ m * n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1
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
hx : x ∈ N'
⊢ (↑↥A i) x ∈ M'

Tactic:
induction hx using span_induction with

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

Goal state before:
pp: case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x ∈ p.support, ϕ ((monomial x) (coeff x p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i, ϕ (X i) ^ d i

Tactic:
congr

Goal state after:
case intro.e_f
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ (fun x ↦ ϕ ((monomial x) (coeff x p))) = fun d ↦ (ϕ.comp C) (coeff d p) * ∏ i, ϕ (X i) ^ d i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I

Tactic:
intro f g _ hg n

Goal state after:
case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ coeff n (f • g) ∈ I
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2
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
hx : x ∈ N'
⊢ (↑↥A f) x ∈ M'

Tactic:
induction hx using span_induction with

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3
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✝ : ↥M'
x : M
hx : x ∈ M'
⊢ x ∈ ((↑↥A f).domRestrict N').range

Tactic:
induction hx using span_induction with

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.two_dvd, iff_true]

Goal state after:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : List R
⊢ l.sum ^ 2 = (List.map (fun x ↦ x ^ 2) l).sum

Tactic:
list_sum_sq

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x : R
⊢ ∀ ⦃a₂ : R⦄, (fun x ↦ x ^ 2) x = (fun x ↦ x ^ 2) a₂ → x = a₂

Tactic:
y

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x y : R
⊢ (fun x ↦ x ^ 2) x = (fun x ↦ x ^ 2) y → x = y
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)

Tactic:
congr

Goal state after:
case e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n

Tactic:
let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn

Goal state after:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p ^ (k + l).succ ∣ m * n := hpmn
⊢ p ^ (k + l) * p ∣ m * n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd

Tactic:
by
  induction ys generalizing f f' with
  | nil => simp
  | cons ys_hd _ ys_ih =>
    simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
    rw [ys_ih]
    · refine ⟨?_, rfl⟩
      simp only [← map_cons, ← map_append]; apply H
    · intro a; apply H

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

Goal state before:
pp: case mk
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
carrier✝ : Set A
mul_mem'✝ : ∀ {a b : A}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : A},
    a ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
algebraMap_mem'✝ :
  ∀ (r : R),
    (algebraMap R A) r ∈
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
          zero_mem' := zero_mem'✝ }.carrier
star_mem'✝¹ :
  ∀ {a : A},
    a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier →
      star a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝ }.carrier
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
h :
  (fun S ↦ S.carrier)
      { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
        zero_mem' := zero_mem'✝, algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝¹ } =
    (fun S ↦ S.carrier) { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
      algebraMap_mem' := algebraMap_mem'✝, star_mem' := star_mem'✝¹ } =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x

Tactic:
by
  conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x

Tactic:
congr

Goal state after:
case e_a
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[minimalPeriod f x] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ (List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x))).Nodup

Tactic:
List.nodup_map_iff_inj_on List.nodup_range

Goal state after:
α : Type u_1
f : α → α
x : α
⊢ ∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)

Tactic:
exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).next x h = z

Tactic:
by rw [next, nextOr, if_pos hx]

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

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun x ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' =
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
congr

Goal state after:
case succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ (fun x ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) = permutations'Aux t
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: 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
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F R A B
inst✝ : StarHomClass F A B
f g : F
a : A
ha : f a = g a
⊢ star a ∈ ((↑↑f).equalizer ↑↑g).carrier

Tactic:
simpa only [← map_star] using! congrArg star ha

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ (head :: tail)[idxOf a (head :: tail) - 1] =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]

Tactic:
congr

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

Tactic:
rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ Subsingleton (orbitRel.Quotient G α) → Nonempty (orbitRel.Quotient G α)
Module: Mathlib.Data.List.Prime

Goal state before:
pp: 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

pp: 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

Tactic:
· exact ⟨L_hd, mem_cons_self, hd⟩

Goal state after:
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.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : IsChain r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Tactic:
List.isChain_iff_pairwise

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), a * b ∈ H ∨ b ∈ H
b : G
h' : a * b ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
by simpa using mul_mem h'.1 (inv_mem h'.2)

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

Goal state before:
pp: case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) - ↑(n + 1) = cast a + cast b - ↑(n + 1)

Tactic:
congr

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 1 = ∅

Tactic:
rw [properDivisors, Ico_self, filter_empty]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑n.divisors → n / x = n / x₂ → x = x₂

Tactic:
y

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
⊢ y ∈ ↑n.divisors → n / x = n / y → x = y
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
by
  ext; simp [mem_divisorsAntidiag, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n.choose r) ≤ ↑n ^ r / ↑r !

Tactic:
rw [le_div_iff₀']

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

Tactic:
congr

Goal state after:
case succ.e_head
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) = x

case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
obtain rfl | hm := eq_or_ne m 0

Goal state after:
case inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k n : ℕ
| fun y ↦ m * y + k = n

Tactic:
y

Goal state after:
m k n y : ℕ
| m * y + k = n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i ↦ b * (a * b ^ i)) l (List.range l.length)

Tactic:
congr

Goal state after:
case e_f
b : ℕ
l : List ℕ
⊢ (fun a i ↦ a * b ^ (i + 1)) = fun a i ↦ b * (a * b ^ i)