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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
x : MvPolynomial σ S₁
⊢ x ∈ range ⇑(map f) ↔ ↑x.coeffs ⊆ range ⇑f

Tactic:
refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)
  · induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
⊢ cons y 0 = single 0 y

Tactic:
ext j
  cases j using Fin.cases <;> simp

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

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

pp: case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
on_goal 1 =>
    rw [h0, f.map_zero, Finset.sum_eq_zero]
    intro d hd

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)
Module: Mathlib.Data.Finsupp.Fin

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

Tactic:
and_comm

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ s = 0 ∧ x = y ↔ s = 0 ∧ 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
⊢ x = 0 ∧ s = single i y ↔ s = single i y ∧ x = 0

Tactic:
and_comm

Goal state after:
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ s = single i y ∧ x = 0 ↔ s = single i y ∧ x = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ ∑ s, d s ≤ d.sum fun x e ↦ e

Tactic:
rw [Finsupp.sum_fintype]

Goal state after:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ ∀ (i : σ), 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ p.totalDegree < ∑ i ∈ m.support, m i

Tactic:
rw [h]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ 0 < ∑ i ∈ m.support, m i
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.trailingDegree.toNat = q.trailingDegree.toNat

Tactic:
rw [h]

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).trailingDegree = ↑n

Tactic:
trailingDegree,

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.trailingDegree.toNat = p.support.min' ⋯

Tactic:
trailingDegree,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ENat.toNat p.support.min = p.support.min' ⋯
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)

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

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

Tactic:
rw [← ENat.natCast_le_natCast, ENat.natCast_add, ← trailingDegree_eq_natTrailingDegree hp,
    ← trailingDegree_eq_natTrailingDegree hq, ← trailingDegree_eq_natTrailingDegree h]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
⊢ p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · nontriviality R
    rw [h, natTrailingDegree_X_pow, ← h]
  · ext n
    rw [coeff_X_pow]
    obtain hn | rfl | hn := lt_trichotomy n p.natDegree
    · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
    · simpa only [if_pos rfl] using! h₁.leadingCoeff
    · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption

Goal state after:
case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(C g.leadingCoeff * X ^ g.natDegree).support ≤ cg.succ

case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (C g.leadingCoeff * X ^ g.natDegree).natDegree ≤ O

case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ eval₂ φ a ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f

Tactic:
(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) ((uniqueAlgEquiv R σ).symm f)) = Polynomial.eval₂ φ (a default) f
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
    exact DFunLike.congr_fun this p
  ext; simp [commAlgEquiv, mapAlgHom, X, C, monomial, coeff, AddMonoidAlgebra.one_def]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (((optionEquivLeft R σ) p).coeff m) = coeff (optionElim m d) p

Tactic:
by
  rw [← optionEquivLeft_coeff_some_coeff_none]
  congr <;> simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (C 1).nextCoeff = 0

Tactic:
nextCoeff_C_eq_zero

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (φ f).natDegree = fu f.natDegree →
          (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
intro f g fg _ fk gk

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ (f + g)).natDegree = fu (f + g).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0

Tactic:
nextCoeff_C_eq_zero

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
mem_Ioc,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree ≤ p.natDegree / 2)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
p q : R[X]
h : p = q
⊢ (toMvPolynomial i) p = (toMvPolynomial i) q

Tactic:
rw [h]

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

Goal state before:
pp: case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

Tactic:
simp only [Multiset.mem_map]
      rintro _ ⟨_, _, rfl⟩
      apply monic_X_sub_C

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p - q).Monic

Tactic:
by
  rw [sub_eq_add_neg]
  apply hp.add_of_left
  rwa [degree_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ False

Tactic:
zero_dvd_iff

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : b = 0
⊢ False
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 + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Tactic:
by
  simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
    (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']
  refine sum_congr rfl fun i hi => ?_
  suffices n - 1 - i + 1 = n - i by rw [this]
  rw [Finset.mem_range] at hi
  lia

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

Tactic:
rw [h]

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.succ
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
n : ℕ
⊢ (C x).coeff (n + 1) ∈ P

Tactic:
· simp only [coeff_C_of_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R A

Tactic:
· rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S

Tactic:
· rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

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

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) p) (((aeval f) p') v) = ((aeval f) (p * p')) v

Tactic:
by simp only [Module.End.mul_apply, aeval_mul]

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

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) q) (((aeval f) q') v) = ((aeval f) (q * q')) v

Tactic:
by simp only [Module.End.mul_apply, aeval_mul]

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

Goal state before:
pp: n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]

Tactic:
induction m with
  | zero => simp
  | succ d hd => rw [pow_succ, pow_succ]; exact hd.mul h

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

Goal state before:
pp: case refine_2.inl_add_inr
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
r : R
a : A
⊢ (lift f).toRingHom (inl r + ↑a) ∈ S

Tactic:
simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
x : ℤˣ
⊢ x ∈ {1, -1}

Tactic:
by cases Int.units_eq_one_or x <;> simp [*]

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

Goal state before:
pp: case refine_2.inl_add_inr
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
r : R
a : A
⊢ (↑(starLift f)).toRingHom (inl r + ↑a) ∈ S

Tactic:
simpa using! add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Goal state after:
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
⊢ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s

Tactic:
simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coe_subtype,
    Subtype.range_coe_subtype]

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 {x | x ∈ s} = StarAlgebra.adjoin R ↑s
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
⊢ p ∣ x * y

Tactic:
rw [h]

Goal state after:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ p ^ 2
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 : NonUnitalStarSubalgebra R A
⊢ span R ({1} ∪ ↑(Subsemigroup.closure (↑s ∪ star ↑s))) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
span_union,

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 : NonUnitalStarSubalgebra R A
⊢ R ∙ 1 ⊔ span R ↑(Subsemigroup.closure (↑s ∪ star ↑s)) = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(period a b) ∣ n

Tactic:
zpow_smul_eq_iff_period_dvd

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ ↑(period a b) ∣ n ↔ ↑(period a b) ∣ n
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 : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

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 : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.prev l ⋯).length) (h₂ : i < (l.rotate (l.length - 1)).length),
    (pmap l.prev l ⋯)[i] = (l.rotate (l.length - 1))[i]

Tactic:
· intro n hn hn'
    rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

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

Goal state before:
pp: case cons.right.inr.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n = m
hn' : as.insertIdx m x = a
⊢ False

Tactic:
← hm'

Goal state after:
case cons.right.inr.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n = m
hn' : as.insertIdx m x = bs.insertIdx m x
⊢ False
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:
unique_iff_subsingleton_and_nonempty,

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'

Tactic:
heq_iff_eq

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'

Tactic:
heq_iff_eq

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr.refine_1
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ 0 < n

Tactic:
grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]

Goal state after: