Theorem: l1_2_20_iii (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
Tactic:
have := (IsOfFinOrder.orderOf_pos h).ne'
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
Tactic:
rw [l1_2_20_i' _ _ h]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = ↑(orderOf g)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = ↑(orderOf g)
Tactic:
trans #((Set.Ico 0 (orderOf g)).image fun i => g ^ i)
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g))

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g)) = ↑(orderOf g)

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g)) = ↑(orderOf g)
Tactic:
simp only [Cardinal.mk_fintype, Nat.cast_inj, Fintype.card_ofFinset]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Finset.image (fun i => g ^ i) (Set.toFinset (Set.Ico 0 (orderOf g)))).card = orderOf g

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Finset.image (fun i => g ^ i) (Set.toFinset (Set.Ico 0 (orderOf g)))).card = orderOf g
Tactic:
rw [Finset.card_image_of_injOn]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Set.toFinset (Set.Ico 0 (orderOf g))).card = orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Set.toFinset (Set.Ico 0 (orderOf g))).card = orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
Tactic:
simp only [tsub_zero, eq_self_iff_true, Set.toFinset_card, Nat.card_fintypeIco]
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
Tactic:
intro x hx y hy hxy
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y
Tactic:
rwa [pow_eq_pow_iff_modEq, Nat.ModEq, Nat.mod_eq_of_lt, Nat.mod_eq_of_lt] at hxy
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x = y % orderOf g
⊢ y < orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x = y % orderOf g
⊢ y < orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g
Tactic:
simpa using hy
State after:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
x : ℕ
hx : x ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
y : ℕ
hy : y ∈ ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
hxy : x % orderOf g = y % orderOf g
⊢ x < orderOf g
Tactic:
simpa using hx
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g))
Tactic:
congr
State after:
no goals