Theorem: ex_1_2_10_ii_aux_1 (AlgebraI/Subgroups.lean)

State before:
x : Equiv.Perm (Fin 4)
⊢ orderOf x = 2 ↔ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
rw [orderOf_eq_iff two_pos]
State after:
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) ↔ x ≠ 1 ∧ x ^ 2 = 1

State before:
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) ↔ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
constructor
State after:
case mp
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) → x ≠ 1 ∧ x ^ 2 = 1

case mpr
x : Equiv.Perm (Fin 4)
⊢ x ≠ 1 ∧ x ^ 2 = 1 → x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1

State before:
case mp
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) → x ≠ 1 ∧ x ^ 2 = 1
Tactic:
rintro ⟨h1, h2⟩
State after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1 ∧ x ^ 2 = 1

State before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
refine ⟨?_, h1⟩
State after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1

State before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1
Tactic:
have := h2 1 one_lt_two one_pos
State after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
this : x ^ 1 ≠ 1
⊢ x ≠ 1

State before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
this : x ^ 1 ≠ 1
⊢ x ≠ 1
Tactic:
rwa [pow_one] at this
State after:
no goals

State before:
case mpr
x : Equiv.Perm (Fin 4)
⊢ x ≠ 1 ∧ x ^ 2 = 1 → x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
rintro ⟨h1, h2⟩
State after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1

State before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
refine ⟨h2, ?_⟩
State after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ ∀ m < 2, 0 < m → x ^ m ≠ 1

State before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
intros m hm1 hm2
State after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ x ^ m ≠ 1

State before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ x ^ m ≠ 1
Tactic:
obtain rfl : m = 1 := by linarith
State after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
hm1 : 1 < 2
hm2 : 0 < 1
⊢ x ^ 1 ≠ 1

State before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
hm1 : 1 < 2
hm2 : 0 < 1
⊢ x ^ 1 ≠ 1
Tactic:
rwa [pow_one]
State after:
no goals

State before:
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ m = 1
Tactic:
linarith
State after:
no goals