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

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑↑k - 1 = ↑↑k - 1

pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k

Tactic:
]

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ 1 ≤ ↑k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : 1 ≤ ↑k
⊢ 1 ≤ ↑k

Tactic:
]

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : 1 ≤ ↑k
⊢ 1 ≤ ↑k
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
⊢ J.relIndex K = J.relIndex K

Tactic:
]

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

Goal state before:
pp: case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = n

Tactic:
]

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
⊢ J.relIndex K = J.relIndex K

Tactic:
]

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
⊢ Nat.card X = Nat.card X

Tactic:
]

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

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ z = z

Tactic:
]

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

Goal state before:
pp: case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = n

Tactic:
]

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
⊢ Nat.card M ≤ Nat.card (G ⧸ f.ker)

Tactic:
]

Goal state after:
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
⊢ Nat.card M ≤ Nat.card (G ⧸ f.ker)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z = z

Tactic:
]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]

Tactic:
]

Goal state after:
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ ↑n ∣ x✝ ↔ ↑n ∣ x✝

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
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 g : G
f' : G →* M := ↑f
⊢ f' g = f' x * f' y ↔ f' g = f' x * f' y

Tactic:
]

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 = cast 0 ↔ a = 0

Tactic:
]

Goal state after:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = cast 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = insert n ({d ∈ Ico 1 n | d ∣ n})

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
r : R
k : ℤ
⊢ r * ↑k = r * ↑k

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z

Tactic:
]

Goal state after:
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
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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.val + b.val

pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val + b.val
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 + b).val + n - n

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
]

Goal state after:
case mpr
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val

pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
· simpa [ZMod.val] using! Int.natAbs_add_le _ _

Goal state after:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val

Tactic:
]

Goal state after:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
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 < x + 1 ∧ x + 1 < 1

Tactic:
]

Goal state after:
case refine_1
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 < x + 1 ∧ x + 1 < 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ filterMap
      (fun x ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯ =
    filterMap
      (fun x ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
a b : ZMod n
⊢ a.val * b.val % n ≤ a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ (a, n / a) = d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ (b, n / b) = ha
⊢ d.1 < ha.1

Tactic:
]

Goal state after:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ (a, n / a) = d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ (b, n / b) = ha
⊢ d.1 < ha.1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ a < b

Tactic:
]

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ a < b
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n = n

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0

Tactic:
]

Goal state after:
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = a * a⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 < n ↔ 1 < n

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < x * ∑ i ∈ range n, x ^ i

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < x * ∑ i ∈ range n, x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ m < n

Tactic:
]

Goal state after:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ m < n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = a * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
]

Goal state after:
case refine_2
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ (x.2, x.1).2 * (x.2, x.1).1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℤ
⊢ n % ↑2 = 1 % ↑2 ↔ n % 2 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
]

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

Goal state after:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

Goal state after:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n x : ℕ
h : (x % n).gcd n = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

Goal state after:
n : ℕ
⊢ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
]

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors

Tactic:
]

Goal state after:
n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: m n✝ n x : ℕ
h : x.Coprime n
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0

Tactic:
]

Goal state after:
case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
]

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
]

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ x ∈ n.properDivisors, x + n = ∑ i ∈ n.properDivisors, i + n

Tactic:
]

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

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

Tactic:
]

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val
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:
]

Goal state after:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n

Tactic:
]

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Tactic:
]

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

Goal state before:
pp: n p : ℕ
hp : Nat.Prime p
⊢ ¬p ∣ n ↔ ¬p ∣ n

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ = 1 ∨ a✝ = p

Tactic:
]

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

Goal state before:
pp: p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ ¬p ∣ a ↔ ¬p ∣ a

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
]

Goal state after:
p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
]

Goal state after:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
]

Goal state after:
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
]

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a = b
⊢ a = b

Tactic:
]

Goal state after:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a = b
⊢ a = b
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors \ s = ∅
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
]

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

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
]

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → ∑ x ∈ (n + 1 + 1).properDivisors, x = 1