mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
rw [mem_range] at j_in

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 < m
⊢ n - 1 - j = n - m + (m - 1 - j)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
⊢ x = 0

Tactic:
by
  refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)
  obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0
  convert! I.mul_mem_left (C y) hx
  rw [← C.map_mul, hR.mul_comm y x, hy, map_one]

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

Goal state before:
pp: case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ MulOpposite.unop x ∈ Set.range ⇑(algebraMap R A) ↔ x ∈ Set.range ⇑(algebraMap R Aᵐᵒᵖ)

Tactic:
Set.mem_range,

Goal state after:
case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, (algebraMap R Aᵐᵒᵖ) y = x
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ ⊤.FG

Tactic:
rw [← Subalgebra.prod_top]; exact hA.1.prod hB.1

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
by
  algebraize_only [f, g, g.comp f]
  exact Algebra.FiniteType.trans hf hg

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := ⋯
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤

Tactic:
have : S.biUnion (fun f => f.coeff.support) = ⋃ f ∈ S, (f.coeff.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (of' R M '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this : DecidableEq M := ⋯
⊢ adjoin R (⇑(of R M) '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤

Tactic:
have : S.biUnion (fun f => f.coeff.support) = ⋃ f ∈ S, (f.coeff.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
S : Finset R[M]
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(S.biUnion fun f ↦ f.coeff.support) = ⋃ f ∈ S, ↑f.coeff.support
⊢ adjoin R (⇑(of R M) '' ↑(S.biUnion fun f ↦ f.coeff.support)) = ⊤
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Tactic:
rw [modEq_iff_dvd]

Goal state after:
a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
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 : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ (Ideal.Quotient.mk I) v = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ v ∈ I
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 : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f H)

Tactic:
by
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
  intro u hu
  obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
  rw [Ideal.Quotient.lift_mk] at hu
  rw [Ideal.Quotient.eq_zero_iff_mem]
  exact hI (RingHom.mem_ker.mpr hu)

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✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ (unitization s).range = Algebra.adjoin R ↑s

Tactic:
unitization,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ (Unitization.lift (NonUnitalSubalgebraClass.subtype s)).range = Algebra.adjoin R ↑s
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

Tactic:
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩

Goal state after:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
unitization,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (NonUnitalSubalgebra.unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
unitization,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
⊢ (NonUnitalSubalgebra.unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
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
⊢ (unitization s).range = StarAlgebra.adjoin R ↑s

Tactic:
unitization,

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
⊢ (Unitization.starLift (NonUnitalStarSubalgebraClass.subtype s)).range = StarAlgebra.adjoin R ↑s
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
⊢ Function.Injective ⇑starAlgHom

Tactic:
have := AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom)
        fun _ ↦ by simp [starAlgHom]
      rw [StarAlgHom.coe_comp] at this
      exact this.of_comp

Goal state after:
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
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd

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

Goal state before:
pp: R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLEₐ R h)).comp (Quotient.mkₐ R (map (Quotient.mkₐ R I) J)) = Quotient.factorₐ R h

Tactic:
by
  ext x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  rfl

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

Goal state before:
pp: α : Type u_1
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys id).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
rw [show @id (List α) = ([] ++ ·) by funext _; rfl]

Goal state after:
α : Type u_1
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x ↦ [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ x ∈ ⋃ n, ⋃ (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f

Tactic:
simp [mem_periodicPts]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
minimalPeriod,

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ (if h : x ∈ periodicPts f then Nat.find h else 0) ≤ 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
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

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

Goal state before:
pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h

Goal state after:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

Tactic:
intro hyp g hg
    apply Eq.subset
    rw [← mem_stabilizer_iff]
    exact hyp hg

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.primeFactorsList = [p]

Tactic:
by
  have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl
  rw [this, primeFactorsList]
  simp only [Eq.symm this]
  have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
  simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0

Tactic:
exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
rcases hp with hp' | hp'

Goal state after:
case refine_2.inl
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ a.primeFactorsList
⊢ Prime p

case refine_2.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ b.primeFactorsList
⊢ Prime p
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (n✝ + 1)
⊢ (Int.cast ∘ cast) x✝ = x✝.cast

Tactic:
simp [ZMod, ZMod.cast]

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

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).cast = if ↑0 ≤ a.cast + b.cast then a.cast + b.cast - ↑0 else a.cast + b.cast

Tactic:
simp; rfl

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Tactic:
apply Int.cast_add

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
Fin.coe_neg_one

Goal state after:
case succ
n✝ : ℕ
⊢ n✝ + 1 = n✝ + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]

Goal state after:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x✝ : n.divisors.Nonempty
hn : n = 0
m : ℕ
hm : m ∈ n.divisors
⊢ False

Tactic:
simp [hn] at hm

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}

Tactic:
simp [mul_eq_one, Prod.ext_iff]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x ≠ ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
apply ne_of_lt

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
dsimp only [to_fun, inv_fun, ZMod.castHom_apply]

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

Goal state before:
pp: z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, mul_comm]

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

Goal state before:
pp: m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
enter [

Goal state after:
m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p ^ k ∣ n

Tactic:
pow_dvd_iff_le_of_spec hp hn h hl

Goal state after:
case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
have : 0 < b ^ k := by positivity

Goal state after:
case pos
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
this : 0 < b ^ k
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p

Goal state after:
case inl
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

case inr.inl
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < 1
⊢ (1 - 1) * ∑ i ∈ range L.length, ofDigits 1 L / 1 ^ i.succ = ofDigits 1 L - L.sum

case inr.inr
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + b * (ofDigits b tl₁ + ofDigits b tl₂)

Tactic:
mul_add

Goal state after:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L

Tactic:
induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p n : ℕ
⊢ (p.digits n).sum ≤ n

Tactic:
induction n with
  | zero => exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  | succ n =>
    induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: p n : ℕ
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p

Goal state after:
case inl
p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

case inr.inl
n : ℕ
⊢ (1 - 1) * ∑ i ∈ range (log 1 n).succ, n / 1 ^ i.succ = n - (digits 1 n).sum

case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x * x_1) 1 = 0

Tactic:
minimalPeriod,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ (if h : 1 ∈ periodicPts fun x_1 ↦ x * x_1 then Nat.find h else 0) = 0
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

Tactic:
subst h
    rw [factorization_mul hd <| right_ne_zero_of_mul hn]
    apply self_le_add_right

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p

Tactic:
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
← add_tsub_cancel_of_le hf,

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ (n.factorization + (f - n.factorization)).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]

Goal state after:
case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
simp_rw [erase_ne hqp]

Goal state after:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ a.factorization q ≤ b.factorization q
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
· let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
    simp [hr]

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

Goal state before:
pp: case inr
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hn : n ≠ 0
⊢ m'.Coprime n'

Tactic:
exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)

Goal state after: