mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ n.primeFactorsList = [] → n = 0 ∨ n = 1

case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactorsList = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p

Tactic:
exact fun p => prime_of_mem_primeFactorsList

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

Goal state before:
pp: ⊢ primeFactors 0 = ∅

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ a✝ ∈ primeFactors 0 ↔ a✝ ∈ ∅
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: ⊢ primeFactors 1 = ∅

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Tactic:
ext

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b

Tactic:
constructor

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf 1 / (addOrderOf 1).gcd a.succ = n / n.gcd (a + 1)

Tactic:
ZMod.addOrderOf_one

Goal state after:
case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ n / n.gcd a.succ = n / n.gcd (a + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a n : ℕ
a0 : a ≠ 0
⊢ addOrderOf 1 / (addOrderOf 1).gcd a = n / n.gcd a

Tactic:
ZMod.addOrderOf_one

Goal state after:
a n : ℕ
a0 : a ≠ 0
⊢ n / n.gcd a = n / n.gcd a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a

Tactic:
by
  cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.cast_val_eq_self

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast

Tactic:
ext

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (n✝ + 1)
⊢ (Int.cast ∘ cast) x✝ = x✝.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective ⇑(castHom ⋯ R)

Tactic:
Fintype.bijective_iff_injective_and_card,

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R) ∧ Fintype.card (ZMod n) = Fintype.card R
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a * b) = Fin.cast h a * Fin.cast h b

Tactic:
ext

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑(Fin.cast h (a * b)) = ↑(Fin.cast h a * Fin.cast h b)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a + b) = Fin.cast h a + Fin.cast h b

Tactic:
ext

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑(Fin.cast h (a + b)) = ↑(Fin.cast h a + Fin.cast h b)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index = Nat.card ↥f.ker

Tactic:
by
  rw [← mul_left_inj' hf.index_ne_zero, card_mul_index, index_ker, index_mul_card]

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

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

Tactic:
constructor

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

case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
constructor

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

case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

Tactic:
ext

Goal state after:
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ x✝ ∈ AddSubgroup.zmultiples ↑n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n.succ | d ∣ n} = n.divisors

Tactic:
ext

Goal state after:
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ {d ∈ range n.succ | d ∣ n} ↔ a✝ ∈ n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n | d ∣ n} = n.properDivisors

Tactic:
ext

Goal state after:
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ {d ∈ range n | d ∣ n} ↔ a✝ ∈ n.properDivisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ a = b

Tactic:
ext

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ ↑a = ↑b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ NeZero n

Tactic:
constructor

Goal state after:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0

case mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val → a.val * b.val < n

case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ a.val * b.val < n → (a * b).val = a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 0 = ∅

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 0 = ∅

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ a✝ ∈ properDivisors 0 ↔ a✝ ∈ ∅
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 1 = {1}

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ a✝ ∈ divisors 1 ↔ a✝ ∈ {1}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 0 = ∅

Tactic:
ext

Goal state after:
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 0 ↔ a✝ ∈ ∅
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 1 = {(1, 1)}

Tactic:
ext

Goal state after:
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Tactic:
ext

Goal state after:
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal ↔ x✝ ∈ ↑n.divisorsAntidiagonal
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors

Tactic:
ext

Goal state after:
n a✝ : ℕ
⊢ a✝ ∈ image Prod.fst n.divisorsAntidiagonal ↔ a✝ ∈ n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
ext

Goal state after:
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) ↔
    a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n

case mpr
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}

Tactic:
ext

Goal state after:
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ p.divisors ↔ a✝ ∈ {1, p}
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
constructor

Goal state after:
case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun

case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
constructor

Goal state after:
case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun

case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
fin_cases x

Goal state after:
case inr.right.«0»
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
y : ZMod 0
⊢ to_fun (inv_fun ((fun i ↦ i) ⟨0, ⋯⟩, y)) = ((fun i ↦ i) ⟨0, ⋯⟩, y)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
constructor

Goal state after:
case mp
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k → ∃ j, ∃ (_ : j < k), x = p ^ j

case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k
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
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
have : NeZero (m * n) := ⟨hmn0⟩

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)
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i

Tactic:
rw [pow_succ, ← Nat.div_div_eq_div_mul]

Goal state after:
case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n

Tactic:
constructor

Goal state after:
case mp
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n

case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 0 = ∅

Tactic:
ext

Goal state after:
a✝ : ℤ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisors = z.divisors

Tactic:
ext

Goal state after:
z a✝ : ℤ
⊢ a✝ ∈ (-z).divisors ↔ a✝ ∈ z.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.fst z.divisorsAntidiag = z.divisors

Tactic:
ext

Goal state after:
z a✝ : ℤ
⊢ a✝ ∈ image Prod.fst z.divisorsAntidiag ↔ a✝ ∈ z.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.snd z.divisorsAntidiag = z.divisors

Tactic:
ext

Goal state after:
z a✝ : ℤ
⊢ a✝ ∈ image Prod.snd z.divisorsAntidiag ↔ a✝ ∈ z.divisors
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
ext

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
ext

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
ext

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ (-z).divisorsAntidiag ↔
    a✝ ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
constructor

Goal state after:
case succ.mp
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n✝ + 1

case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ AddSubgroup.zmultiples ↑n ≤ f.ker

Tactic:
constructor

Goal state after:
case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ f.ker

case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b n : ℕ
⊢ b.digits n = [] ↔ n = 0

Tactic:
constructor

Goal state after:
case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
ext

Goal state after:
case e_f
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ ofDigits p (head✝ :: tail✝) ≤ ofDigits q (head✝ :: tail✝)

Tactic:
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 i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)

Tactic:
by
  induction i with
  | zero => simp
  | succ i hi =>
    rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n → multiplicity a b = n

case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ emultiplicity ↑a ↑b = emultiplicity a b

Tactic:
unfold emultiplicity FiniteMultiplicity

Goal state after:
a b : ℕ
⊢ (if h : ∃ n, ¬↑a ^ (n + 1) ∣ ↑b then ↑(Nat.find h) else ⊤) = if h : ∃ n, ¬a ^ (n + 1) ∣ b then ↑(Nat.find h) else ⊤
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor

Goal state after:
case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b

case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

Tactic:
le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne'

Goal state after:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ¬count p n.primeFactorsList + 1 ≤ padicValNat p n

Tactic:
le_padicValNat_iff_replicate_subperm_primeFactorsList pp hn0.ne'

Goal state after:
case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ ¬replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: ⊢ factorization 0 = 0

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ (factorization 0) a✝ = 0 a✝
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: ⊢ factorization 1 = 0

Tactic:
ext

Goal state after:
a✝ : ℕ
⊢ (factorization 1) a✝ = 0 a✝
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ↑(Finset.range (b ^ l)) = {n | n < b ^ l}

Tactic:
ext

Goal state after:
b : ℕ
hb : 1 < b
l x✝ : ℕ
⊢ x✝ ∈ ↑(Finset.range (b ^ l)) ↔ x✝ ∈ {n | n < b ^ l}
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 0 = {[]}

Tactic:
ext

Goal state after:
b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ ∈ fixedLengthDigits hb 0 ↔ a✝ ∈ {[]}
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 1 = Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
ext

Goal state after:
b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ ∈ fixedLengthDigits hb 1 ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ ∈ fixedLengthDigits hb 1 ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
rw [mem_fixedLengthDigits_iff, List.length_eq_one_iff]

Goal state after:
b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ ((∃ a, a✝ = [a]) ∧ ∀ x ∈ a✝, x < b) ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ Nat.find h1 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
· classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization ↔ (f.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization → (f.prod fun x1 x2 ↦ x1 ^ x2) = n

case mpr
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) = n → f = n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n ↔ n = 0 ∨ ¬p ∣ n

Tactic:
constructor

Goal state after:
case mp
n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n → n = 0 ∨ ¬p ∣ n

case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n