mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℕ
hab : a = b
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
⊢ ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : a = b
x : ZMod a
⊢ ((ringEquivCongr h) x).val = x.val

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
⊢ a ^ n ∈ H

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(↑a).val = a % ↑n

Tactic:
by

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

Goal state before:
pp: a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index

Tactic:
by

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑a = 0 ↔ ↑b ∣ a

Tactic:
by

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

Goal state before:
pp: a b : ℤ
c : ℕ
⊢ ↑a = ↑b ↔ ↑c ∣ b - a

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ ↑a = 0 ↔ b ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ (pi Set.univ H).index = ∏ i, (H i).index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (toAddSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ℤ
⊢ (↑a).cast = a % ↑n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
⊢ (AddSubgroup.toSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x.cast + y.cast) % ↑n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
H K L : Subgroup G
f : G →* G'
inst✝¹ : H.FiniteIndex
inst✝ : K.FiniteIndex
⊢ (H.prod K).FiniteIndex

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x * y).cast = x.cast * y.cast % ↑n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x.cast - y.cast) % ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : ZMod n
⊢ (-x).cast = -x.cast % ↑n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ i ∈ s, f i).FiniteIndex

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (-1).val = n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : H.IsFiniteRelIndex L
h : H ≤ K
⊢ K.IsFiniteRelIndex L

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
h : K ≤ L
inst✝ : H.IsFiniteRelIndex L
⊢ H.IsFiniteRelIndex K

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.FiniteIndex
⊢ H.IsFiniteRelIndex K

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑n - 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
⊢ K.index < H.index

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G✝ : Type u_1
G' : Type u_2
inst✝² : Group G✝
inst✝¹ : Group G'
H✝ K L : Subgroup G✝
f : G✝ →* G'
G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
h : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ Function.Injective ⇑((MulDistribMulAction.toMonoidEnd H G) h)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
⊢ (k - 1).cast = (if k = 0 then ↑n else k.cast) - 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ Function.Injective ⇑((DistribMulAction.toAddMonoidEnd H G) h)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (stabilizer G x).index = Nat.card X

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Function.Surjective ⇑f

Tactic:
by

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

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:
by
  constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_intCast, Int.emod_add_mul_ediv]
  · rintro ⟨k, rfl⟩
    rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ
nzm : NeZero m
h : m ≤ n
⊢ Injective cast

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : M
hx : x ∈ Set.range ⇑f
hy : y ∈ Set.range ⇑f
⊢ #{g | f g = x} = #{g | f g = y}

Tactic:
by

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n x₁ x₂ : ℕ
x✝ : ℕ × ℕ
x y : ℕ
hx₁ :
  (x, y) ∈
    let y := n / x₁;
    if x₁ * y = n then some (x₁, y) else none
hx₂ :
  (x, y) ∈
    let y := n / x₂;
    if x₂ * y = n then some (x₂, y) else none
⊢ x₁ = x₂

Tactic:
by

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

Goal state before:
pp: p n : ℕ
_h : 0 ≤ ↑n
⊢ ↑(↑n).toNat = ↑↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

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

Goal state before:
pp: p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ ↑(Int.negSucc n).toNat = ↑(Int.negSucc n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n ∉ n.properDivisors

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Injective val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ val 1 = 1 % n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ val 2 = 2 % n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝² : Ring R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Module (ZMod n) R
r : ZMod n
x : R
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1

Tactic:
by

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

Goal state before:
pp: hn : 1 ≠ 1
⊢ val 1 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 1
⊢ 1 < n + 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ cons n n.properDivisors ⋯ = n.divisors

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.divisors ↔ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
m₁ : Module (ZMod n) M
inst✝ : Module R M
⊢ IsScalarTower (ZMod n) R M

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝¹ : Semiring R
inst✝ : Fintype M'
⊢ #R[M'] = lift.{v, u} #R ^ card M'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝¹ : Semiring R
inst✝ : Fintype M
⊢ #R[M] = #R ^ card M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Infinite M'
inst✝ : Nontrivial R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Infinite M
inst✝ : Nontrivial R
⊢ #R[M] = max #R #M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Nonempty M'
inst✝ : Infinite R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Nonempty M
inst✝ : Infinite R
⊢ #R[M] = max #R #M

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #R[X] = max #R ℵ₀

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
n : ℕ
⊢ if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∀ (a a' : ℕ) (b : ℕ × ℕ),
    (have y := n / a;
        if a * y = n then some (a, y) else none) =
        some b →
      (have y := n / a';
          if a' * y = n then some (a', y) else none) =
          some b →
        a = a'

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a * b).val = a.val * b.val % n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a * b).val ≤ a.val * b.val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ List.Pairwise (fun x1 x2 ↦ x1.1 < x2.1) n.divisorsAntidiagonalList

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∀ (a : ℕ × ℕ), ¬a.1 < a.1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.divisors → n ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #(Ico 1 (n + 1)) = n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1

Tactic:
by

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

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ m.divisors ⊆ n.properDivisors

Tactic:
by

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : Fact (1 < n)
h : 0 = 1
⊢ 0 = val 0

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ Nontrivial (ZMod 0)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 1 = 0 ↔ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
hm : m ∣ n
⊢ {d ∈ n.divisors | d ∣ m} = m.divisors

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisors 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors = ∅ ↔ n = 0

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ a * a.sign = ↑a.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑(a.natAbs.gcd 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 1 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
h : m ∈ n.divisors
⊢ 0 < m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.properDivisors ↔ 1 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors.sup id = n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
h : m ∈ n.properDivisors
⊢ 1 < n / m

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ) = ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
⊢ if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = ∅ ↔ n ≤ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ) = ↑(a.val.gcd n.succ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ divisorsAntidiagonal 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(a.val.gcd n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 1⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ n + 1 + 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ↑n = 1 ↔ Odd n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n ≠ 0 ↔ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n x y : ℕ
hn : n ≠ 0
⊢ (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 ∈ n.divisors

Tactic:
by

Goal state after: