[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
⊢ index (comap f H) = index H
[PROOFSTEP]
letI := QuotientGroup.leftRel H
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this : Setoid G := QuotientGroup.leftRel H
⊢ index (comap f H) = index H
[PROOFSTEP]
letI := QuotientGroup.leftRel (H.comap f)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ index (comap f H) = index H
[PROOFSTEP]
have key : ∀ x y : G', Setoid.r x y ↔ Setoid.r (f x) (f y) :=
  by
  simp only [QuotientGroup.leftRel_apply]
  exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
[PROOFSTEP]
simp only [QuotientGroup.leftRel_apply]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
⊢ ∀ (x y : G'), x⁻¹ * y ∈ comap f H ↔ (↑f x)⁻¹ * ↑f y ∈ H
[PROOFSTEP]
exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
x y : G'
⊢ ↑f (x⁻¹ * y) = (↑f x)⁻¹ * ↑f y
[PROOFSTEP]
rw [f.map_mul, f.map_inv]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ index (comap f H) = index H
[PROOFSTEP]
refine' Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨_, _⟩)
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
simp_rw [← Quotient.eq''] at key
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
⊢ Function.Injective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
refine' Quotient.ind' fun x => _
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄,
    Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
        Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a₂ →
      Quotient.mk'' x = a₂
[PROOFSTEP]
refine' Quotient.ind' fun y => _
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key✝ : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (↑f x) = Quotient.mk'' (↑f y)
x y : G'
⊢ Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' x) =
      Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) (Quotient.mk'' y) →
    Quotient.mk'' x = Quotient.mk'' y
[PROOFSTEP]
exact (key x y).mpr
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
⊢ Function.Surjective (Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)))
[PROOFSTEP]
refine' Quotient.ind' fun x => _
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
[PROOFSTEP]
obtain ⟨y, hy⟩ := hf x
[GOAL]
case refine'_2.intro
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
hf : Function.Surjective ↑f
this✝ : Setoid G := QuotientGroup.leftRel H
this : Setoid G' := QuotientGroup.leftRel (comap f H)
key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (↑f x) (↑f y)
x : G
y : G'
hy : ↑f y = x
⊢ ∃ a, Quotient.map' ↑f (_ : ∀ (x y : G'), Setoid.r x y → Setoid.r (↑f x) (↑f y)) a = Quotient.mk'' x
[PROOFSTEP]
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
⊢ comap f H = comap (MonoidHom.rangeRestrict f) (subgroupOf H (MonoidHom.range f))
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K✝ L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G' →* G
K : Subgroup G'
⊢ relindex (comap f H) K = relindex H (map f K)
[PROOFSTEP]
rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.subtype_range]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex H K * relindex K L = relindex H L
[PROOFSTEP]
rw [← relindex_subgroupOf hKL]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hHK : H ≤ K
hKL : K ≤ L
⊢ relindex (subgroupOf H L) (subgroupOf K L) * relindex K L = relindex H L
[PROOFSTEP]
exact relindex_mul_index fun x hx => hHK hx
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) K = relindex H K
[PROOFSTEP]
rw [relindex, relindex, inf_subgroupOf_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) H = relindex K H
[PROOFSTEP]
rw [inf_comm, inf_relindex_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H (K ⊓ L) * relindex K L = relindex (H ⊓ K) L
[PROOFSTEP]
rw [← inf_relindex_right H (K ⊓ L), ← inf_relindex_right K L, ← inf_relindex_right (H ⊓ K) L, inf_assoc,
  relindex_mul_relindex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Normal K
⊢ relindex K (K ⊔ H) = relindex K H
[PROOFSTEP]
rw [sup_comm, relindex_sup_right]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ index H = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)
[PROOFSTEP]
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff, QuotientGroup.exists_mk,
  QuotientGroup.forall_mk, Ne.def, QuotientGroup.eq, mul_one, xor_iff_iff_not]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (∃ x, ¬x ∈ H ∧ ∀ (x_1 : G), ¬x_1 ∈ H → x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
[PROOFSTEP]
refine' exists_congr fun a => ⟨fun ha b => ⟨fun hba hb => _, fun hb => _⟩, fun ha => ⟨_, fun b hb => _⟩⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False
[PROOFSTEP]
exact ha.1 ((mul_mem_cancel_left hb).1 hba)
[GOAL]
case refine'_2
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ¬a ∈ H ∧ ∀ (x : G), ¬x ∈ H → x⁻¹ * a ∈ H
b : G
hb : ¬b ∈ H
⊢ b * a ∈ H
[PROOFSTEP]
exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
[GOAL]
case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ ¬a ∈ H
[PROOFSTEP]
rw [← inv_mem_iff (x := a), ← ha, inv_mul_self]
[GOAL]
case refine'_3
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
⊢ 1 ∈ H
[PROOFSTEP]
exact one_mem _
[GOAL]
case refine'_4
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ ¬b ∈ H
b : G
hb : ¬b ∈ H
⊢ b⁻¹ * a ∈ H
[PROOFSTEP]
rwa [ha, inv_mem_iff (x := b)]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
[PROOFSTEP]
by_cases ha : a ∈ H
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
[PROOFSTEP]
simp only [ha, true_iff_iff, mul_mem_cancel_left ha]
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
[PROOFSTEP]
by_cases hb : b ∈ H
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
[PROOFSTEP]
simp only [hb, iff_true_iff, mul_mem_cancel_right hb]
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
[PROOFSTEP]
simp only [ha, hb, iff_self_iff, iff_true_iff]
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
⊢ a * b ∈ H
[PROOFSTEP]
rcases index_eq_two_iff.1 h with ⟨c, hc⟩
[GOAL]
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H
[PROOFSTEP]
refine' (hc _).or.resolve_left _
[GOAL]
case neg.intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a b : G
ha : ¬a ∈ H
hb : ¬b ∈ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ ¬a * b * c ∈ H
[PROOFSTEP]
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : index H = 2
a : G
⊢ a * a ∈ H
[PROOFSTEP]
rw [mul_mem_iff_of_index_two h]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H ⊤ = index H
[PROOFSTEP]
rw [← relindex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H = Nat.card { x // x ∈ H }
[PROOFSTEP]
rw [relindex, bot_subgroupOf, index_bot]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H ⊥ = 1
[PROOFSTEP]
rw [relindex, subgroupOf_bot_eq_top, index_top]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex H H = 1
[PROOFSTEP]
rw [relindex, subgroupOf_self, index_top]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ index (MonoidHom.ker f) = Nat.card ↑(Set.range ↑f)
[PROOFSTEP]
rw [← MonoidHom.comap_bot, index_comap, relindex_bot_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ Nat.card { x // x ∈ MonoidHom.range f } = Nat.card ↑(Set.range ↑f)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ relindex (MonoidHom.ker f) K = Nat.card ↑(↑f '' ↑K)
[PROOFSTEP]
rw [← MonoidHom.comap_bot, relindex_comap, relindex_bot_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ K✝ L : Subgroup G
H : Type u_2
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ Nat.card { x // x ∈ map f K } = Nat.card ↑(↑f '' ↑K)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ Nat.card { x // x ∈ H } * index H = Nat.card G
[PROOFSTEP]
rw [← relindex_bot_left, ← index_bot]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex ⊥ H * index H = index ⊥
[PROOFSTEP]
exact relindex_mul_index bot_le
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card G ∣ Nat.card H
[PROOFSTEP]
rw [Nat.card_congr (MonoidHom.ofInjective hf).toEquiv]
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Injective ↑f
⊢ Nat.card { x // x ∈ MonoidHom.range f } ∣ Nat.card H
[PROOFSTEP]
exact Dvd.intro f.range.index f.range.card_mul_index
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
⊢ Nat.card H ∣ Nat.card G
[PROOFSTEP]
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
⊢ Nat.card (G ⧸ MonoidHom.ker f) ∣ Nat.card G
[PROOFSTEP]
exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index
[GOAL]
G✝ : Type u_1
inst✝⁴ : Group G✝
H✝ K L : Subgroup G✝
G : Type u_2
H : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Fintype G
inst✝ : Fintype H
f : G →* H
hf : Function.Surjective ↑f
⊢ Fintype.card H ∣ Fintype.card G
[PROOFSTEP]
simp only [← Nat.card_eq_fintype_card, nat_card_dvd_of_surjective f hf]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
⊢ index (map f H) = index (H ⊔ MonoidHom.ker f) * index (MonoidHom.range f)
[PROOFSTEP]
rw [← comap_map_eq, index_comap, relindex_mul_index (H.map_le_range f)]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (map f H) ∣ index H
[PROOFSTEP]
rw [index_map, f.range_top_of_surjective hf, index_top, mul_one]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ index (H ⊔ MonoidHom.ker f) ∣ index H
[PROOFSTEP]
exact index_dvd_of_le le_sup_left
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index (map f H)
[PROOFSTEP]
rw [index_map, sup_of_le_left hf]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : MonoidHom.ker f ≤ H
⊢ index H ∣ index H * index (MonoidHom.range f)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ index H * Fintype.card { x // x ∈ H } = Fintype.card G
[PROOFSTEP]
rw [← relindex_bot_left_eq_card, ← index_bot_eq_card, mul_comm]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
hH : Fintype { x // x ∈ H }
⊢ relindex ⊥ H * index H = index ⊥
[PROOFSTEP]
exact relindex_mul_index bot_le
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
[PROOFSTEP]
classical exact ⟨Fintype.card H, H.index_mul_card.symm⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
[PROOFSTEP]
exact ⟨Fintype.card H, H.index_mul_card.symm⟩
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : relindex H L ≠ 0
hK : relindex K L ≠ 0
⊢ relindex (H ⊓ K) L ≠ 0
[PROOFSTEP]
replace hH : H.relindex (K ⊓ L) ≠ 0 := mt (relindex_eq_zero_of_le_right inf_le_right) hH
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex K L ≠ 0
hH : relindex H (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ K) L ≠ 0
[PROOFSTEP]
rw [← inf_relindex_right] at hH hK ⊢
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex (K ⊓ L) L ≠ 0
hH : relindex (H ⊓ (K ⊓ L)) (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ K ⊓ L) L ≠ 0
[PROOFSTEP]
rw [inf_assoc]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : relindex (K ⊓ L) L ≠ 0
hH : relindex (H ⊓ (K ⊓ L)) (K ⊓ L) ≠ 0
⊢ relindex (H ⊓ (K ⊓ L)) L ≠ 0
[PROOFSTEP]
exact relindex_ne_zero_trans hH hK
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : index H ≠ 0
hK : index K ≠ 0
⊢ index (H ⊓ K) ≠ 0
[PROOFSTEP]
rw [← relindex_top_right] at hH hK ⊢
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : relindex H ⊤ ≠ 0
hK : relindex K ⊤ ≠ 0
⊢ relindex (H ⊓ K) ⊤ ≠ 0
[PROOFSTEP]
exact relindex_inf_ne_zero hH hK
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
by_cases h : H.relindex L = 0
[GOAL]
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
exact (le_of_eq (relindex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
[PROOFSTEP]
rw [← inf_relindex_right, inf_assoc, ← relindex_mul_relindex _ _ L inf_le_right inf_le_right, inf_relindex_right,
  inf_relindex_right]
[GOAL]
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex H (K ⊓ L) * relindex K L ≤ relindex H L * relindex K L
[PROOFSTEP]
exact mul_le_mul_right' (relindex_le_of_le_right inf_le_right h) (K.relindex L)
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ index (H ⊓ K) ≤ index H * index K
[PROOFSTEP]
simp_rw [← relindex_top_right, relindex_inf_le]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), index (f i) ≠ 0
⊢ index (⨅ (i : ι), f i) ≠ 0
[PROOFSTEP]
simp_rw [← relindex_top_right] at hf ⊢
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), relindex (f i) ⊤ ≠ 0
⊢ relindex (⨅ (i : ι), f i) ⊤ ≠ 0
[PROOFSTEP]
exact relindex_iInf_ne_zero hf
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
ι : Type u_2
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ index (⨅ (i : ι), f i) ≤ ∏ i : ι, index (f i)
[PROOFSTEP]
simp_rw [← relindex_top_right, relindex_iInf_le]
[GOAL]
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
⊢ index H ≠ 0
[PROOFSTEP]
cases nonempty_fintype (G ⧸ H)
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ index H ≠ 0
[PROOFSTEP]
rw [index_eq_card]
[GOAL]
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Fintype.card (G ⧸ H) ≠ 0
[PROOFSTEP]
exact Fintype.card_ne_zero
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : FiniteIndex H
⊢ FiniteIndex (normalCore H)
[PROOFSTEP]
rw [normalCore_eq_ker]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : FiniteIndex H
⊢ FiniteIndex (MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)))
[PROOFSTEP]
infer_instance
[GOAL]
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ FiniteIndex (center G)
[PROOFSTEP]
obtain ⟨S, -, hS⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS : closure ↑S = ⊤
⊢ FiniteIndex (center G)
[PROOFSTEP]
exact ⟨mt (Finite.card_eq_zero_of_embedding (quotientCenterEmbedding hS)) Finite.card_pos.ne'⟩
[GOAL]
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
[PROOFSTEP]
rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
[GOAL]
case intro.intro
G : Type u_1
inst✝² : Group G
H K L : Subgroup G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ index (center G) ≤ Nat.card (↑↑S → ↑(commutatorSet G))
[PROOFSTEP]
exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)


[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
⊢ ∀ {x : PresentedGroup rels}, ↑g x = ↑(toGroup h) x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ↑g x = ↑(toGroup h) x
[PROOFSTEP]
refine' QuotientGroup.induction_on x _
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α), ↑g ↑z = ↑(toGroup h) ↑z
[PROOFSTEP]
exact fun _ ↦ FreeGroup.lift.unique (g.comp (QuotientGroup.mk' _)) hg


[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
⊢ ¬IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
rw [IsTorsion, not_forall]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsTorsion G
src✝ : Monoid G := inst✝
g : G
⊢ g⁻¹ * g = 1
[PROOFSTEP]
erw [← pow_succ', tsub_add_cancel_of_le, pow_orderOf_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsTorsion G
src✝ : Monoid G := inst✝
g : G
⊢ 1 ≤ orderOf g
[PROOFSTEP]
exact orderOf_pos' (tG g)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
⊢ IsOfFinOrder h
[PROOFSTEP]
obtain ⟨g, hg⟩ := hf h
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder h
[PROOFSTEP]
rw [← hg]
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder (↑f g)
[PROOFSTEP]
exact f.isOfFinOrder (tG g)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
⊢ ∃ n, 0 < n ∧ g ^ n = 1
[PROOFSTEP]
obtain ⟨ngn, ngnpos, hngn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tH <| f g)
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
[PROOFSTEP]
have hmem := f.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
hmem : g ^ ngn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
[PROOFSTEP]
lift g ^ ngn to N using hN.symm ▸ hmem with gn h
[GOAL]
case intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
⊢ ∃ n, 0 < n ∧ g ^ n = 1
[PROOFSTEP]
obtain ⟨nn, nnpos, hnn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp (tN gn)
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ ∃ n, 0 < n ∧ g ^ n = 1
[PROOFSTEP]
exact ⟨ngn * nn, mul_pos ngnpos nnpos, by rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hN : N = MonoidHom.ker f
tH : IsTorsion H
tN : IsTorsion { x // x ∈ N }
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : ↑f g ^ ngn = 1
gn : { x // x ∈ N }
h : ↑gn = g ^ ngn
hmem✝ hmem : ↑gn ∈ MonoidHom.ker f
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ g ^ (ngn * nn) = 1
[PROOFSTEP]
rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
h : ExponentExists G
g : G
⊢ IsOfFinOrder g
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := h
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g
[PROOFSTEP]
exact (isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, npos, hn g⟩
[GOAL]
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := (isOfFinAddOrder_iff_nsmul_eq_zero _).mp (tR 1)
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0
[PROOFSTEP]
exact ⟨n, npos, by simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]⟩
[GOAL]
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0
[PROOFSTEP]
simp only [nsmul_eq_smul_cast R _ f, ← nsmul_one, hn, zero_smul]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑(((fun x x_1 => x * x_1)
            { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1) })^[n]
        1) =
    ↑1
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } * x_1)^[n]
        1) =
    1
[PROOFSTEP]
rw [mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑((fun x_1 => { val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_2 => x * x_2) n 1) } ^ n * x_1)
        1) =
    1
[PROOFSTEP]
change _ * 1 = 1
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
x✝ : { x // x ∈ torsion G }
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1
⊢ ↑({ val := x, property := (_ : ∃ n, n > 0 ∧ Function.IsPeriodicPt (fun x_1 => x * x_1) n 1) } ^ n) * 1 = 1
[PROOFSTEP]
rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk, (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₁
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₂
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
n : ℕ
hn : b✝ ^ p ^ n = 1
⊢ ∃ m, (a✝ * b✝) ^ p ^ m = 1
[PROOFSTEP]
exact ⟨m + n, by rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn, one_pow]⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
a✝ b✝ : G
hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}
hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}
m : ℕ
hm : a✝ ^ p ^ m = 1
n : ℕ
hn : b✝ ^ p ^ n = 1
⊢ (a✝ * b✝) ^ p ^ (m + n) = 1
[PROOFSTEP]
rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn, one_pow]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf 1 = p ^ 0
[PROOFSTEP]
rw [pow_zero, orderOf_one]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : { x // x ∈ primaryComponent G p }
⊢ ∃ n, orderOf g = p ^ n
[PROOFSTEP]
simpa [primaryComponent] using g.property
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
⊢ ∀ {x : G}, x ∈ primaryComponent G p → x ∈ primaryComponent G p' → x = 1
[PROOFSTEP]
rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
[GOAL]
case intro.zero.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ Nat.zero
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
[PROOFSTEP]
rwa [pow_zero, orderOf_eq_one_iff] at hn
[GOAL]
case intro.succ.intro
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ Nat.succ n
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1
[PROOFSTEP]
exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
tG : IsTorsion G
⊢ torsion G = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
H : Type u_2
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤
[PROOFSTEP]
tauto
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Monoid G
⊢ ¬IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
simp_rw [IsTorsionFree, Ne.def, not_forall, Classical.not_not, exists_prop]
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
x : G
hx : x ≠ 1
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
[PROOFSTEP]
exact ⟨x, hx, tG x⟩
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
⊢ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
[GOAL]
case intro
G : Type u_1
H : Type u_2
inst✝ : Group G
hN : Nontrivial G
tfG : IsTorsionFree G
x : G
hx : x ≠ 1
⊢ ∃ g, ¬IsOfFinOrder g
[PROOFSTEP]
exact ⟨x, (tfG x) hx⟩
[GOAL]
G : Type u_1
H✝ : Type u_2
inst✝ : Group G
tG : IsTorsionFree G
H : Subgroup G
h : { x // x ∈ H }
hne : h ≠ 1
⊢ ↑h ≠ 1
[PROOFSTEP]
norm_cast
[GOAL]
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g : G ⧸ torsion G
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1
[PROOFSTEP]
induction' g using QuotientGroup.induction_on' with g
[GOAL]
case H
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1
[PROOFSTEP]
obtain ⟨m, mpos, hm⟩ := (isOfFinOrder_iff_pow_eq_one _).mp hfin
[GOAL]
case H.intro.intro
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
⊢ ↑g = 1
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ := (isOfFinOrder_iff_pow_eq_one _).mp ((QuotientGroup.eq_one_iff _).mp hm)
[GOAL]
case H.intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝ : CommGroup G
g✝ : G ⧸ torsion G
hne✝ : g✝ ≠ 1
hfin✝ : IsOfFinOrder g✝
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x => x ^ m) g ^ n = 1
⊢ ↑g = 1
[PROOFSTEP]
exact
  (QuotientGroup.eq_one_iff g).mpr
    ((isOfFinOrder_iff_pow_eq_one _).mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)


[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, List.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ insert a s = a ::ₘ s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ Multiset.count a✝ (insert a s) = Multiset.count a✝ (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, Multiset.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ insert a s = Finset.cons a s h
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
a✝ : α
⊢ a✝ ∈ insert a s ↔ a✝ ∈ Finset.cons a s h
[PROOFSTEP]
simp
[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, Finset.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ Finset.range n = Finset.cons n' (Finset.range n') (_ : ¬n' ∈ Finset.range n')
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', Finset.range_succ, Finset.insert_eq_cons]
[GOAL]
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
⊢ Finset.univ = elems
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems
[PROOFSTEP]
simpa using complete x
[GOAL]
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ Finset.sum ∅ f = ↑0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ Finset.prod ∅ f = ↑1
[PROOFSTEP]
simp


[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
x✝ : A
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) x✝ 0 = 1
[PROOFSTEP]
classical exact dif_pos rfl
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
x✝ : A
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) x✝ 0 = 1
[PROOFSTEP]
exact dif_pos rfl
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) a n✝ ^ n✝ = a
[PROOFSTEP]
dsimp only
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n✝) a_1 = a)) ^ n✝ = a
[PROOFSTEP]
rw [dif_neg hn]
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ Exists.choose (_ : ∃ a_1, (fun a => a ^ n✝) a_1 = a) ^ n✝ = a
[PROOFSTEP]
exact (H hn a).choose_spec
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ n • ⊤
[PROOFSTEP]
rw [H hn]
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ n✝ • (fun a n => if hn : n = 0 then 0 else Exists.choose (_ : a ∈ n • ⊤)) a n✝ = a
[PROOFSTEP]
simp_rw [dif_neg hn]
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ n✝ • Exists.choose (_ : a ∈ n✝ • ⊤) = a
[PROOFSTEP]
generalize_proofs h1
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
h1 : a ∈ n✝ • ⊤
⊢ n✝ • Exists.choose h1 = a
[PROOFSTEP]
exact h1.choose_spec.2
[GOAL]
𝕜 : Type ?u.71834
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
q : 𝕜
⊢ (fun q n => q / ↑n) q 0 = 0
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type ?u.71834
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (fun q n => q / ↑n) q n = q
[PROOFSTEP]
rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel q (Int.cast_ne_zero.mpr hn)]
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a n ^
      n =
    a
[PROOFSTEP]
induction n
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a (ofNat a✝) ^
      ofNat a✝ =
    a
[PROOFSTEP]
change RootableBy.root a _ ^ _ = a
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ RootableBy.root a a✝ ^ ofNat a✝ = a
[PROOFSTEP]
norm_num
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ RootableBy.root a a✝ ^ a✝ = a
[PROOFSTEP]
rw [RootableBy.root_cancel]
[GOAL]
case ofNat.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ a✝ ≠ 0
[PROOFSTEP]
rw [Int.ofNat_eq_coe] at hn
[GOAL]
case ofNat.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ↑a✝ ≠ 0
⊢ a✝ ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a -[a✝+1] ^
      -[a✝+1] =
    a
[PROOFSTEP]
change (RootableBy.root a _)⁻¹ ^ _ = a
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (RootableBy.root a (a✝ + 1))⁻¹ ^ -[a✝+1] = a
[PROOFSTEP]
norm_num
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ RootableBy.root a (a✝ + 1) ^ (a✝ + 1) = a
[PROOFSTEP]
rw [RootableBy.root_cancel]
[GOAL]
case negSucc.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ a✝ + 1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ (fun a n => RootableBy.root a ↑n) a n ^ n = a
[PROOFSTEP]
simpa only [zpow_coe_nat] using RootableBy.root_cancel a (show (n : ℤ) ≠ 0 by exact_mod_cast hn)
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n) ^ n = x
[PROOFSTEP]
rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy]


[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
x✝ : ∃ S, closure S = P ∧ Set.Finite S
S : Set M
hS : closure S = P
hf : Set.Finite S
⊢ closure ↑(Set.Finite.toFinset hf) = P
[PROOFSTEP]
simp [hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : FG P
S : Set M
hS : closure S = P
hf : Set.Finite S
⊢ AddSubmonoid.closure (↑Additive.toMul ⁻¹' S) = ↑toAddSubmonoid P
[PROOFSTEP]
simp [← Submonoid.toAddSubmonoid_closure, hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : Submonoid M
h : AddSubmonoid.FG (↑toAddSubmonoid P)
T : Set (Additive M)
hT : AddSubmonoid.closure T = ↑toAddSubmonoid P
hf : Set.Finite T
⊢ closure (↑Multiplicative.ofAdd ⁻¹' T) = P
[PROOFSTEP]
simp [← AddSubmonoid.toSubmonoid'_closure, hT]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
P : AddSubmonoid N
⊢ FG P ↔ Submonoid.FG (↑toSubmonoid P)
[PROOFSTEP]
convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
⊢ FG M
[PROOFSTEP]
cases nonempty_fintype M
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ FG M
[PROOFSTEP]
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤
[PROOFSTEP]
rw [Finset.coe_univ]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure Set.univ = ⊤
[PROOFSTEP]
exact Submonoid.closure_univ
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
[PROOFSTEP]
classical
obtain ⟨s, rfl⟩ := h
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : FG P
e : M →* M'
⊢ FG (Submonoid.map e P)
[PROOFSTEP]
obtain ⟨s, rfl⟩ := h
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ FG (Submonoid.map e (closure ↑s))
[PROOFSTEP]
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (↑e) s) = Submonoid.map e (closure ↑s)
[PROOFSTEP]
rw [Finset.coe_image, MonoidHom.map_mclosure]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
h : FG (Submonoid.map e P)
⊢ FG P
[PROOFSTEP]
obtain ⟨s, hs⟩ := h
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ FG P
[PROOFSTEP]
use s.preimage e (he.injOn _)
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s))) = P
[PROOFSTEP]
apply Submonoid.map_injective_of_injective he
[GOAL]
case h.a
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e (closure ↑(Finset.preimage s ↑e (_ : Set.InjOn (↑e) (↑e ⁻¹' ↑s)))) = Submonoid.map e P
[PROOFSTEP]
rw [← hs, MonoidHom.map_mclosure e, Finset.coe_preimage]
[GOAL]
case h.a
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (↑e '' (↑e ⁻¹' ↑s)) = closure ↑s
[PROOFSTEP]
congr
[GOAL]
case h.a.e_s
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ ↑e '' (↑e ⁻¹' ↑s) = ↑s
[PROOFSTEP]
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs, MonoidHom.mrange_eq_map e]
[GOAL]
case h.a.e_s
M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid N
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ↑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤
[PROOFSTEP]
exact Submonoid.monotone_map le_top
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG N
[PROOFSTEP]
conv_rhs => rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
| Submonoid.FG N
[PROOFSTEP]
rw [← N.range_subtype, MonoidHom.mrange_eq_map]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N✝
N : Submonoid M
⊢ FG { x // x ∈ N } ↔ Submonoid.FG (Submonoid.map (Submonoid.subtype N) ⊤)
[PROOFSTEP]
exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
[PROOFSTEP]
classical
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
use s.image f
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map, MonoidHom.mrange_top_iff_surjective]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
⊢ FG M'
[PROOFSTEP]
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'
[PROOFSTEP]
use s.image f
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ↑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (↑f) s) = ⊤
[PROOFSTEP]
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map, MonoidHom.mrange_top_iff_surjective]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
s : Finset M
⊢ FG { x // x ∈ Submonoid.closure ↑s }
[PROOFSTEP]
refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : AddMonoid N
s : Finset M
⊢ Submonoid.closure ↑(Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))) = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
x✝ : ∃ S, closure S = P ∧ Set.Finite S
S : Set G
hS : closure S = P
hf : Set.Finite S
⊢ closure ↑(Set.Finite.toFinset hf) = P
[PROOFSTEP]
simp [hS]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ Submonoid.FG P.toSubmonoid
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P → Submonoid.FG P.toSubmonoid
[PROOFSTEP]
rintro ⟨S, rfl⟩
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.FG (closure ↑S).toSubmonoid
[PROOFSTEP]
rw [Submonoid.fg_iff]
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ ∃ S_1, Submonoid.closure S_1 = (closure ↑S).toSubmonoid ∧ Set.Finite S_1
[PROOFSTEP]
refine' ⟨S ∪ S⁻¹, _, S.finite_toSet.union S.finite_toSet.inv⟩
[GOAL]
case mp.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
S : Finset G
⊢ Submonoid.closure (↑S ∪ (↑S)⁻¹) = (closure ↑S).toSubmonoid
[PROOFSTEP]
exact (Subgroup.closure_toSubmonoid _).symm
[GOAL]
case mpr
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid → FG P
[PROOFSTEP]
rintro ⟨S, hS⟩
[GOAL]
case mpr.intro
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ FG P
[PROOFSTEP]
refine' ⟨S, le_antisymm _ _⟩
[GOAL]
case mpr.intro.refine'_1
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ closure ↑S ≤ P
[PROOFSTEP]
rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
[GOAL]
case mpr.intro.refine'_1
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
[PROOFSTEP]
exact Submonoid.subset_closure
[GOAL]
case mpr.intro.refine'_2
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P ≤ closure ↑S
[PROOFSTEP]
rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
[GOAL]
case mpr.intro.refine'_2
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(closure ↑S).toSubmonoid
[PROOFSTEP]
exact Subgroup.subset_closure
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ FG P ↔ AddSubgroup.FG (↑toAddSubgroup P)
[PROOFSTEP]
rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : Subgroup G
⊢ Submonoid.FG P.toSubmonoid ↔ AddSubmonoid.FG (↑toAddSubgroup P).toAddSubmonoid
[PROOFSTEP]
exact (Subgroup.toSubmonoid P).fg_iff_add_fg
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : AddSubgroup H
⊢ FG P ↔ Subgroup.FG (↑toSubgroup P)
[PROOFSTEP]
rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
P : AddSubgroup H
⊢ AddSubmonoid.FG P.toAddSubmonoid ↔ Submonoid.FG (↑toSubgroup P).toSubmonoid
[PROOFSTEP]
exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
⊢ FG G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ FG G
[PROOFSTEP]
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Subgroup.closure_univ⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure ↑Finset.univ = ⊤
[PROOFSTEP]
rw [Finset.coe_univ]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤
[PROOFSTEP]
exact Subgroup.closure_univ
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ FG { x // x ∈ Subgroup.closure ↑s }
[PROOFSTEP]
refine' ⟨⟨s.preimage Subtype.val (Subtype.coe_injective.injOn _), _⟩⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure ↑(Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))) = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage, ← Subgroup.coeSubtype, Subgroup.closure_preimage_eq_top]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ rank G' ≤ rank G
[PROOFSTEP]
classical
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
trans (S.image f).card
· apply Group.rank_le
  rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
· exact Finset.card_image_le.trans_eq hS1
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ rank G' ≤ rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ rank G
[PROOFSTEP]
trans (S.image f).card
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ Finset.card (Finset.image (↑f) S)
[PROOFSTEP]
apply Group.rank_le
[GOAL]
case hS
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (↑f) S) = ⊤
[PROOFSTEP]
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
inst✝⁵ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ↑f
S : Finset G
hS1 : Finset.card S = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Finset.card (Finset.image (↑f) S) ≤ rank G
[PROOFSTEP]
exact Finset.card_image_le.trans_eq hS1
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup H✝
H K : Subgroup G
inst✝¹ : Group.FG { x // x ∈ H }
inst✝ : Group.FG { x // x ∈ K }
h : H = K
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ K }
[PROOFSTEP]
subst h
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁵ : Monoid M
inst✝⁴ : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup H✝
H : Subgroup G
inst✝¹ inst✝ : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } = Group.rank { x // x ∈ H }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
classical
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
  by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)
apply (Group.rank_le (closure (s : Set G)) ht).trans
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
· apply Finset.card_filter_le
· apply Subtype.coe_injective.injOn
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val (Subtype.coe_injective.injOn _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
have ht : closure (t : Set (closure (s : Set G))) = ⊤ :=
  by
  rw [Finset.coe_preimage]
  exact closure_preimage_eq_top (s : Set G)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ closure ↑t = ⊤
[PROOFSTEP]
rw [Finset.coe_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤
[PROOFSTEP]
exact closure_preimage_eq_top (s : Set G)
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Group.rank { x // x ∈ closure ↑s } ≤ Finset.card s
[PROOFSTEP]
apply (Group.rank_le (closure (s : Set G)) ht).trans
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Finset.card t ≤ Finset.card s
[PROOFSTEP]
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G)))
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H✝
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ Finset.card t ≤ Finset.card s
case H
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t
[PROOFSTEP]
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
[GOAL]
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H✝
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
H : Set.InjOn Subtype.val ↑t
⊢ Finset.card (Finset.filter (fun x => x ∈ Set.range Subtype.val) s) ≤ Finset.card s
[PROOFSTEP]
apply Finset.card_filter_le
[GOAL]
case H
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : AddMonoid N
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
t : Finset { x // x ∈ closure ↑s } := Finset.preimage s Subtype.val (_ : Set.InjOn (fun a => ↑a) (Subtype.val ⁻¹' ↑s))
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t
[PROOFSTEP]
apply Subtype.coe_injective.injOn
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
[PROOFSTEP]
haveI := Fintype.ofFinite s
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure s } ≤ Nat.card ↑s
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : AddMonoid N
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank { x // x ∈ closure ↑(Set.toFinset s) } ≤ Finset.card (Set.toFinset s)
[PROOFSTEP]
exact rank_closure_finset_le_card s.toFinset


[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h : p
⊢ 0 < if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h : ¬p
⊢ 0 < if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : p
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : ¬p
⊢ 0 ≤ if p then a else b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : p
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : ¬p
⊢ (if p then a else b) ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ min a b ≠ c
[PROOFSTEP]
rw [min_def]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then a else b) ≠ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : a ≤ b
⊢ a ≠ c
[PROOFSTEP]
assumption
[GOAL]
case neg
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : ¬a ≤ b
⊢ b ≠ c
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ max a b ≠ c
[PROOFSTEP]
rw [max_def]
[GOAL]
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then b else a) ≠ c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : a ≤ b
⊢ b ≠ c
[PROOFSTEP]
assumption
[GOAL]
case neg
R : Type u_1
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
h✝ : ¬a ≤ b
⊢ a ≠ c
[PROOFSTEP]
assumption
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < a / a
[PROOFSTEP]
{rw [Int.ediv_self ha.ne']; exact zero_lt_one
}
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < a / a
[PROOFSTEP]
rw [Int.ediv_self ha.ne']
[GOAL]
a : ℤ
ha : 0 < a
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
n : ℕ
x✝ : PUnit
m : Q(ℕ)
this✝ : «$b» =Q bit0 «$m»
_a : Q(LinearOrderedRing «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q StrictOrderedRing.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .nonnegative q(pow_bit0_nonneg $a $m)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
pa : Q(0 ≤ «$a»)
_oα : Q(OrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q OrderedSemiring.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .nonnegative (q(pow_nonneg $pa $b))
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
ofNonneg : Q(0 ≤ «$a») → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    pure (Strictness.nonnegative q((_ : 0 ≤ «$a» ^ «$b»)))
pa : Q(«$a» ≠ 0)
_oα : Q(OrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q OrderedSemiring.toPartialOrder
_a : Q(NoZeroDivisors «$α»)
⊢ Q(«$e» ≠ 0)
[PROOFSTEP]
exact q(pow_ne_zero $b $pa)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
e : Q(«$α»)
fn✝ : Expr
a : Q(«$α»)
b : Q(ℕ)
result : Strictness zα pα e
ra : Strictness zα pα a
ofNonneg : Q(0 ≤ «$a») → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    pure (Strictness.nonnegative q((_ : 0 ≤ «$a» ^ «$b»)))
ofNonzero : Q(«$a» ≠ 0) → Q(OrderedSemiring «$α») → MetaM (Strictness zα pα e) :=
  fun pa _oα =>
    let_fun zα_eq := (_ : «$zα» =Q MonoidWithZero.toZero);
    let_fun pα_eq := (_ : «$pα» =Q OrderedSemiring.toPartialOrder);
    do
    let _a ← synthInstanceQ q(NoZeroDivisors «$α»)
    pure (Strictness.nonzero q((_ : «$a» ^ «$b» ≠ 0)))
pa : Q(0 < «$a»)
_a : Q(StrictOrderedSemiring «$α»)
this : «$e» =Q «$a» ^ «$b»
zα_eq✝ : «$zα» =Q MonoidWithZero.toZero
pα_eq✝ : «$pα» =Q StrictOrderedSemiring.toPartialOrder
⊢ Strictness zα pα e
[PROOFSTEP]
exact .positive (q(pow_pos $pa $b))


[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂
[PROOFSTEP]
simpa only [h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] using distrib e₂ e₁ e₁ e₂
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂
[PROOFSTEP]
funext a b
[GOAL]
case h.h
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b
[PROOFSTEP]
calc
  m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by {simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
  }
  _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
[PROOFSTEP]
{simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
}
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
[PROOFSTEP]
simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b
[PROOFSTEP]
simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a
[PROOFSTEP]
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂
[GOAL]
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)
[PROOFSTEP]
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c


[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
[PROOFSTEP]
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
[PROOFSTEP]
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ↑f ⁅g₁, g₂⁆ = ⁅↑f g₁, ↑f g₂⁆
[PROOFSTEP]
simp_rw [commutatorElement_def, map_mul f, map_inv f]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂
[PROOFSTEP]
rw [eq_bot_iff, commutator_le]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
[PROOFSTEP]
refine' forall_congr' fun p => forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => _
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q
[PROOFSTEP]
rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
[PROOFSTEP]
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le, mem_centralizer_iff_commutator_eq_one, ←
  commutatorElement_def] at h1 h2 ⊢
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ∀ (h : G), h ∈ ↑H₃ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
[PROOFSTEP]
intro x hx y hy z hz
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = 1
[PROOFSTEP]
trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
[PROOFSTEP]
group
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
[PROOFSTEP]
rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
[PROOFSTEP]
group
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
⊢ Normal ⁅H₁, H₂⁆
[PROOFSTEP]
let base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ Normal ⁅H₁, H₂⁆
[PROOFSTEP]
change (closure base).Normal
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ Normal (closure base)
[PROOFSTEP]
suffices h_base : base = Group.conjugatesOfSet base
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure base)
[PROOFSTEP]
rw [h_base]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure (Group.conjugatesOfSet base))
[PROOFSTEP]
exact Subgroup.normalClosure_normal
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ base = Group.conjugatesOfSet base
[PROOFSTEP]
refine' Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => _
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base
[PROOFSTEP]
simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1, a_1 ∈ {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x} ∧ ∃ c, c * a_1 * c⁻¹ = a
⊢ a ∈ base
[PROOFSTEP]
rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
[GOAL]
case h_base.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
c : G
hc : c ∈ H₁
e : G
he : e ∈ H₂
d : G
⊢ d * ⁅c, e⁆ * d⁻¹ ∈ base
[PROOFSTEP]
exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
constructor
[GOAL]
case left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
intro p hp q hq
[GOAL]
case left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
[GOAL]
case right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
rw [← map_commutatorElement]
[GOAL]
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ↑f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ = prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ ≤ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
rw [commutator_le]
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ∀ (g₁ : G × G'), g₁ ∈ prod H₁ K₁ → ∀ (g₂ : G × G'), g₂ ∈ prod H₂ K₂ → ⁅g₁, g₂⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
[GOAL]
case a.mk.intro.mk.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).fst ∈ ↑H₁.toSubmonoid
hp₂ : (p₁, p₂).snd ∈ ↑K₁.toSubmonoid
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).fst ∈ ↑H₂.toSubmonoid
hq₂ : (q₁, q₂).snd ∈ ↑K₂.toSubmonoid
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [prod_le_iff]
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
constructor
[GOAL]
case a.left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
case a.left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case a.left.h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ prod H₁ K₁
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.left.h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ prod H₂ K₂
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
case a.right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case a.right.h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ prod H₁ K₁
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.right.h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ prod H₂ K₂
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun i => ⁅H i, K i⁆
[PROOFSTEP]
classical
apply le_antisymm (commutator_pi_pi_le H K)
· rw [pi_le_iff]
  intro i hi
  rw [map_commutator]
  apply commutator_mono <;>
    · rw [le_pi_iff]
      intro j _hj
      rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
      by_cases h : j = i
      · subst h
        simpa using hx
      · simp [h, one_mem]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun i => ⁅H i, K i⁆
[PROOFSTEP]
apply le_antisymm (commutator_pi_pi_le H K)
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ (pi Set.univ fun i => ⁅H i, K i⁆) ≤ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
rw [pi_le_iff]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ∀ (i : η), map (MonoidHom.single (fun i => Gs i) i) ⁅H i, K i⁆ ≤ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
intro i hi
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ map (MonoidHom.single (fun i => Gs i) i) ⁅H i, K i⁆ → hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ ⁅map (MonoidHom.single (fun i => Gs i) i) (H i), map (MonoidHom.single (fun i => Gs i) i) (K i)⁆ →
    hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.single (fun i => Gs i) i) (H i) ≤ pi Set.univ H
[PROOFSTEP]
rw [le_pi_iff]
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ (i_1 : η),
    i_1 ∈ Set.univ → map (Pi.evalMonoidHom (fun i => Gs i) i_1) (map (MonoidHom.single (fun i => Gs i) i) (H i)) ≤ H i_1
[PROOFSTEP]
intro j _hj
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
⊢ map (Pi.evalMonoidHom (fun i => Gs i) j) (map (MonoidHom.single (fun i => Gs i) i) (H i)) ≤ H j
[PROOFSTEP]
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
subst h
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(H j)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) j) x) ∈ H j
[PROOFSTEP]
simpa using hx
[GOAL]
case neg
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
simp [h, one_mem]
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.single (fun i => Gs i) i) (K i) ≤ pi Set.univ K
[PROOFSTEP]
rw [le_pi_iff]
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ (i_1 : η),
    i_1 ∈ Set.univ → map (Pi.evalMonoidHom (fun i => Gs i) i_1) (map (MonoidHom.single (fun i => Gs i) i) (K i)) ≤ K i_1
[PROOFSTEP]
intro j _hj
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
⊢ map (Pi.evalMonoidHom (fun i => Gs i) j) (map (MonoidHom.single (fun i => Gs i) i) (K i)) ≤ K j
[PROOFSTEP]
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
[GOAL]
case h₂.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
subst h
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(K j)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) j) x) ∈ K j
[PROOFSTEP]
simpa using hx
[GOAL]
case neg
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
simp [h, one_mem]