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

Goal state before:
pp: case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.val < n✝ + 1

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℕ
⊢ (↑a).val = a % 0

pp: case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

Tactic:
·

Goal state after:
case zero
a : ℕ
⊢ (↑a).val = a % 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

Tactic:
·

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

Goal state before:
pp: case zero
k : ℕ
⊢ ↑k = 0 ↔ 0 ∣ k

pp: case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k

Tactic:
·

Goal state after:
case zero
k : ℕ
⊢ ↑k = 0 ↔ 0 ∣ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k

Tactic:
·

Goal state after:
case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0

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

Tactic:
·

Goal state after:
case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : H.relIndex L = 0
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

pp: case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : H.relIndex L = 0
⊢ (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

pp: case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val

pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.cast = ↑a.val

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

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

Goal state before:
pp: case zero
a : ZMod 0
⊢ ↑a.cast = a

pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Tactic:
·

Goal state after:
case zero
a : ZMod 0
⊢ ↑a.cast = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast

pp: case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Nat.cast ∘ val = cast

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast
Module: Mathlib.Data.ZMod.Basic

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

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

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
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

pp: case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ a.cast + b.cast then a.cast + b.cast - ↑(n + 1) else a.cast + b.cast

Tactic:
·

Goal state after:
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
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

pp: case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
·

Goal state after:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)
Module: Mathlib.GroupTheory.Index

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

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 1
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

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

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
·

Goal state after:
case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b
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
⊢ cast 1 = 1

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ H.index ∣ 2

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
⊢ H.index ∣ 2

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ H.index ∣ 2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1

Tactic:
·

Goal state after:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
⊢ H.index ∣ 2

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
⊢ H.index ∣ 2
Module: Mathlib.GroupTheory.Index

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

Tactic:
rintro ⟨a, ha⟩
    by_cases ha' : a ∈ H
    · suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]
      exact fun b ↦ (ha b).elim (fun h ↦ by simpa using mul_mem h (inv_mem ha')) id
    · refine dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)
      simpa using mul_mem (inv_mem h.2) h.1

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1

Tactic:
·

Goal state after:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1
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

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast

Tactic:
·

Goal state after:
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
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
by
  have := fintypeOfIndexNeZero hi
  exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

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

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast

Tactic:
·

Goal state after:
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
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₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ 0 < n₂ - n₁

Tactic:
by lia

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₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ n₂ - n₁ ≤ H.index

Tactic:
by lia

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₁ < n₂
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₁ < n₂
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
h : 0 = 0
⊢ ZMod 0 ≃+* ZMod 0

pp: case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)

pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
·

Goal state after:
case zero.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
h : 0 = 0
⊢ ZMod 0 ≃+* ZMod 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)

pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
·

Goal state after:
case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
·

Goal state after:
case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
·

Goal state after:
case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
·

Goal state after:
case zero
a : ℤ
⊢ (↑a).cast = a % ↑0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
·

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

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

Tactic:
·

Goal state after:
case zero
⊢ ↑(-1) = 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

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

pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

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

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

pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

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

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

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

Tactic:
·

Goal state after:
case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1
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).cast = k.cast - 1

Tactic:
·

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1
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.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
·

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

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
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: case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑z.val + ↑p * k

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
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: case zero
inst✝ : NeZero 0
⊢ Injective val

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Injective val

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
⊢ Injective val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

pp: case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
Module: Mathlib.Algebra.Algebra.ZMod

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

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

Tactic:
·

Goal state after:
case zero
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
inst✝ : Module (ZMod 0) R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x
Module: Mathlib.Algebra.Algebra.ZMod

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

Tactic:
·

Goal state after:
case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

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

Tactic:
·

Goal state after:
case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ (a + b).val = (a.val + b.val) % (n✝ + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

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

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0
Module: Mathlib.NumberTheory.Divisors

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

pp: case mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b

Tactic:
·

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

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

Tactic:
·

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

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val
Module: Mathlib.Algebra.Polynomial.Cardinal

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

pp: case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀
Module: Mathlib.Algebra.Polynomial.Cardinal

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

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀