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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ Finset.image (Finsupp.mapDomain f) (p.support.preimage (Finsupp.mapDomain f) ⋯) ⊆ p.support

Tactic:
Finset.image_preimage

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ {x ∈ p.support | x ∈ range (Finsupp.mapDomain f)} ⊆ p.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun m ↦ m n

Tactic:
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g

Tactic:
simp only [degreeOf]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ Multiset.count i (f * g).degrees ≤ Multiset.count i f.degrees + Multiset.count i g.degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
simp only [degreeOf]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ #f.support ≤ 1

Tactic:
by_cases hpz : f = 0
  case pos => simp [hpz]
  case neg => exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
i : ℕ
⊢ (reflect N f).coeff i = f.coeff ((revAt N) i)

Tactic:
rcases f with ⟨f⟩

Goal state after:
R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := f }).coeff i = { toFinsupp := f }.coeff ((revAt N) i)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
Monic,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ (n + 1)).Monic

Tactic:
pow_succ

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
Monic,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).Monic

Tactic:
Monic,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).Monic

Tactic:
Monic,

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).Monic

Tactic:
Monic,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).Monic

Tactic:
Monic,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).leadingCoeff = 1
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 : R[X]), (∃ a ∈ t, X - C a = f) → f.Monic

Tactic:
rintro _ ⟨_, _, rfl⟩

Goal state after:
case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
w✝ : R
left✝ : w✝ ∈ t
⊢ (X - C w✝).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
hm : Monic 1
hnd : natDegree 1 = 2
⊢ False

Tactic:
simp [natDegree_one] at hnd

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

Goal state before:
pp: case refine_2
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)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ↑(l z) ∈ span R p
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
← Set.image_id p,

Goal state after:
case refine_2
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)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ↑(l z) ∈ span R (_root_.id '' p)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False

Tactic:
← X_mul,

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (X * p).degree
⊢ False
Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder

Goal state before:
pp: F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
⊢ K = ⊥ ∨ K = ⊤

Tactic:
have : FiniteDimensional _ _ := .of_finrank_pos hp.pos

Goal state after:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this : FiniteDimensional F A
⊢ K = ⊥ ∨ K = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r

Tactic:
convert_to Prime (C r) ↔ _

Goal state after:
case e'_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime (C r)

case convert_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Type ?u.42

case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Tactic:
refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑((FreeAlgebra.lift R) Subtype.val)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ n f, Surjective ⇑f

Tactic:
rw [iff_quotient_mvPolynomial']

Goal state after:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → ∃ n f, Surjective ⇑f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support))

Tactic:
intro f hf

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.coeff.support))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support))

Tactic:
intro f hf

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support))
Module: Mathlib.RingTheory.Polynomial.Basic

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

pp: case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

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

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 hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]

Goal state after:
case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

case mp.refine_3
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (x y : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      y ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
        (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I

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
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ d * a ≡ b ^ (d + 1) [ZMOD n]

Tactic:
pow_succ

Goal state after:
case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ d * a ≡ b ^ d * b [ZMOD n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD ↑n.natAbs] ↔ a ≡ b [ZMOD n]

Tactic:
by simp [natCast_natAbs]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

Tactic:
by
  apply Ideal.ext
  intro x
  constructor
  · intro hx
    obtain ⟨y, hy⟩ := Quotient.mk_surjective x
    rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
    rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
    exact ⟨y, hx, rfl⟩
  · intro hx
    rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
    obtain ⟨y, hy⟩ := hx
    rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
    exact hy.left

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0

Tactic:
refine ⟨e, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ (Quotient.mk (I i)) e = 1

case refine_2
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Odd p ↔ 3 ≤ p

Tactic:
rw [← not_iff_not, not_odd_iff_even, hp.even_iff, not_le]

Goal state after:
p : ℕ
hp : Prime p
⊢ p = 2 ↔ p < 3
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
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3

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
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
⊢ ∀ (r : R ⧸ p) (x : A ⧸ P), r • x = (quotientMap P (algebraMap R A) h) r * x

Tactic:
rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.smul_def _ _)

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x
  · exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

Goal state after:
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
ι : Sort u_5
S : ι → StarSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Tactic:
apply h.minimalPeriod_of_comp_dvd_mul.antisymm

Goal state after:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ fixedPoints G α = Set.univ

Tactic:
apply Set.eq_univ_of_forall

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α), x ∈ fixedPoints G α
Module: Mathlib.Data.List.Cycle

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

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
    length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h

Goal state after:
case h
α : Type u_1
l : List α
h : l = [] ∨ ∃ a, l = [a]
⊢ ∀ ⦃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 b : α
hg : b = g • a
x : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer hg) x) = (MulAut.conj g) ↑x

Tactic:
by
  simp [stabilizerEquivStabilizer]

Goal state after:
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 b : α
hg : b = g • a
x : ↥(stabilizer G b)
⊢ ↑((stabilizerEquivStabilizer hg).symm x) = (MulAut.conj g⁻¹) ↑x

Tactic:
by
  simp [stabilizerEquivStabilizer]

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

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

Tactic:
rcases b with - | ⟨b, m⟩

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

case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
⊢ (match [] 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.Cycle

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

Tactic:
rcases b with - | ⟨b, m⟩

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

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.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s

Tactic:
induction s with
  | nil => exact fun _ ↦ Cycle.Chain.nil r
  | cons a l => ?_

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
⊢ (∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b) → Chain r ↑(a :: l)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
simp only [index_eq_two_iff', xor_iff_or_and_not_and]
  exact exists_congr fun a ↦ ⟨fun h ↦ ⟨fun ha ↦ ((h a)).2 ⟨mul_mem ha ha, ha⟩, fun b ↦ (h b).1⟩,
    fun h b ↦ ⟨h.2 b, fun h' ↦ h.1 (by simpa using mul_mem h'.1 (inv_mem h'.2))⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ¬H.FiniteIndex ↔ H.index = 0

Tactic:
by
  simp [finiteIndex_iff]

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

Goal state before:
pp: case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = z.val + p * k

Tactic:
rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_natCast, Nat.mod_add_div]

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

Goal state before:
pp: case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
⊢ Injective cast

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ f

Goal state after:
case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : cast ⟨x, hx⟩ = cast ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
by
  ext ⟨d, nd⟩
  simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
    Prod.ext_iff, and_left_comm, exists_eq_left]
  constructor
  · rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
    rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
    exact ⟨rfl, hn⟩
  · rintro ⟨rfl, hn⟩
    exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

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

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1

Tactic:
by
  rw [mul_comm, mul_inv_of_unit a h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
rw [@eq_comm (Finset ℕ) _ _]

Goal state after:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ {1} = (n✝ + 1 + 1).properDivisors