Theorem: ex_1_2_9 (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ ↑A ∩ ↑B = {1}
Tactic:
refine' Set.eq_singleton_iff_unique_mem.mpr ⟨_, fun x hx => _⟩
State after:
case refine'_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑A ∩ ↑B

case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ ↑A ∩ ↑B
⊢ x = 1

State before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ ↑A ∩ ↑B
⊢ x = 1
Tactic:
rw [Set.mem_inter_iff, SetLike.mem_coe, SetLike.mem_coe] at hx
State after:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x = 1

State before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x = 1
Tactic:
rw [← pow_one x, ← h]
State after:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1

State before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
Tactic:
apply pow_gcd_eq_one
State after:
case refine'_2.hm
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥A = 1

case refine'_2.hn
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥B = 1

State before:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑B
Tactic:
simp only [SetLike.mem_coe]
State after:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ B

State before:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ B
Tactic:
exact Subgroup.one_mem _
State after:
no goals

State before:
case refine'_2.hm
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥A = 1
Tactic:
rw [← Subgroup.coe_mk A x hx.1, ← Subgroup.coe_pow, Monoid.pow_exponent_eq_one,
  Subgroup.coe_one]
State after:
no goals

State before:
case refine'_2.hn
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥B = 1
Tactic:
rw [← Subgroup.coe_mk B x hx.2, ← Subgroup.coe_pow, Monoid.pow_exponent_eq_one,
  Subgroup.coe_one]
State after:
no goals