mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * H.relIndex K = H.index

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * H.relIndex K = H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ (H.subgroupOf L).relIndex (K.subgroupOf L) * K.relIndex L = H.relIndex L
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).index = (H.subgroupOf K).index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K.relIndex H = K.relIndex H

Tactic:
]

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)).relIndex L = (H ⊓ (K ⊓ L)).relIndex L

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : K.Normal
⊢ K.relIndex H = K.relIndex H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H

Tactic:
]

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ 1 ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b ∉ H

Tactic:
]

Goal state after:
case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b ∉ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ b, ?m.40 b) ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ?m.40 ((Equiv.inv G) a)

pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ G → Prop

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ∀ (b : G), Xor ((Equiv.inv G) a * b ∈ H) (b ∈ H)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a ∉ H

Tactic:
]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a ∉ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a ∈ H ↔ a ∈ H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H = Nat.card ↥H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 = 1

Tactic:
]

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'
⊢ Nat.card ↥f.range = Nat.card ↥f.range

Tactic:
]

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'
K : Subgroup G
f : G →* G'
⊢ Nat.card ↥(map f K) = Nat.card ↥(map f K)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = ⊥.index

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = ⊥.index
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'
hf : Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G
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
f : G →* G'
⊢ (map f H).index = (map f H).index

Tactic:
]

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
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index
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
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index
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'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H
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
f : G →* G'
hf : Injective ⇑f
⊢ H.index * f.range.index = H.index * f.range.index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ K.index * H.index = K.index * H.index

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card G = Nat.card G

Tactic:
]

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'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
case zero
a : ℕ
⊢ (↑a).val = a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n a : ℕ
h : a < n
⊢ a = a

pp: n a : ℕ
h : a < n
⊢ a < n

Tactic:
]

Goal state after:
n a : ℕ
h : a < n
⊢ a < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ZMod 0
⊢ n = 1 ∨ n = -1 ↔ n = 1 ∨ n = -1

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ CharP (ZMod n) n

Tactic:
]

Goal state after:
n : ℕ
⊢ CharP (ZMod n) n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (comap L.subtype J).relIndex (comap L.subtype K) ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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

Goal state before:
pp: p n q : ℕ
h : n ≤ n + q
⊢ ↑(p ^ n) * ↑p ^ q = 0

Tactic:
]

Goal state after:
p n q : ℕ
h : n ≤ n + q
⊢ ↑(p ^ n) * ↑p ^ q = 0
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index = 0 ∨ H.index = 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2
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)

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.Data.ZMod.Basic

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

Tactic:
]

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ b, ?m.43 b) ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H

pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ?m.43 ((Equiv.inv G) a)

pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ G → Prop

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∀ (b : G), (Equiv.inv G) a * b ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0

Tactic:
]

Goal state after:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
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)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
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)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)
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₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
]

Goal state after:
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₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
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₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H

Tactic:
]

Goal state after:
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₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0

Tactic:
]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k

Tactic:
]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k
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 = 0
hn : n = 0
⊢ False

Tactic:
]

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False
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
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
]

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)
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)
⊢ ↑a * ↑b % (m + 1) = ↑a * ↑b % (m + 1)

Tactic:
]

Goal state after:
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)
⊢ (↑a + ↑b) % (m + 1) = (↑a + ↑b) % (m + 1)

Tactic:
]

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

Goal state before:
pp: a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x

Tactic:
]

Goal state after:
a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x
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 hab).trans (ringEquivCongr hbc)) x

Tactic:
]

Goal state after:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ ↑a = ↑0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑a = ↑a

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: a b : ℕ
⊢ b ∣ a ↔ b ∣ a

Tactic:
]

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
x y : ι → G
⊢ piSetoid x y ↔ piSetoid x y

Tactic:
]

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

Goal state before:
pp: case zero
a : ℤ
⊢ cast a = a

Tactic:
]

Goal state after:
case zero
a : ℤ
⊢ cast a = a
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index ≠ 0 ↔ H.index ≠ 0

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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 ↥f.ker ∧ Finite (G ⧸ f.ker) ↔ Finite ↥f.ker ∧ Finite (G ⧸ f.ker)

Tactic:
]

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

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

Tactic:
]

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
⊢ (⨅ x, f ↑x).FiniteIndex

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ x, f ↑x).FiniteIndex
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ n✝ + 1 = n✝ + 1

Tactic:
]

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.subgroupOf L).FiniteIndex
h : H ≤ K
⊢ (K.subgroupOf L).FiniteIndex

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : (H.subgroupOf L).FiniteIndex
h : H ≤ K
⊢ (K.subgroupOf L).FiniteIndex
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.relIndex K ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
h : K ≤ L
inst✝ : H.IsFiniteRelIndex L
⊢ H.relIndex K ≠ 0
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑n = ↑n

Tactic:
]

Goal state after:
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
⊢ ↑n - 1 = ↑n - 1

Tactic:
]

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
h0 : K.index ≠ 0
⊢ ¬K ≤ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H
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
⊢ (MulAction.toPermHom G (G ⧸ H)).ker.FiniteIndex

Tactic:
]

Goal state after:
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
⊢ (MulAction.toPermHom G (G ⧸ H)).ker.FiniteIndex
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 = ↑k - 1

Tactic:
]

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 : (AddSubgroup.toSubgroup H).FiniteIndex
⊢ (AddSubgroup.toSubgroup H.normalCore).FiniteIndex

Tactic:
]

Goal state after:
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 : (AddSubgroup.toSubgroup H).FiniteIndex
⊢ (AddSubgroup.toSubgroup H.normalCore).FiniteIndex
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:
← mul_left_inj' hf.index_ne_zero,

Goal state after:
G : Type u_1
inst✝ : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index * f.ker.index = Nat.card ↥f.ker * f.ker.index
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

case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0
Module: Mathlib.GroupTheory.Index

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

Tactic:
]

Goal state after: