awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
obtain :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ rank G
⊢ rank H ≤ rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := rank_spec G

Premises used: Group.rank_spec
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
trans : rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
trans₁ : Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G
⊢ rank H ≤ rank G

Tactic:
trans (S.image f).card

Premises used: Finset.card, DFunLike.coe, Finset.image
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
hS : Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤
⊢ rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)

Tactic:
apply rank_le

Premises used: Group.rank_le
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
hS : Eq.{u_2 + 1} (α := Subgroup H) (Subgroup.closure ((⇑f : (a : G) → H) '' (↑S : Set G))) ⊤
hS₁ : Subgroup.map f (Subgroup.closure (↑S : Set G)) = ⊤
hS₂ : Subgroup.map f ⊤ = ⊤
hS₃ hS₄ : Eq.{u_2 + 1} (α := Subgroup H) ⊤ ⊤
⊢ Eq (α := Subgroup H) (Subgroup.closure (↑(Finset.image (⇑f : (a : G) → H) S) : Set H)) ⊤

Tactic:
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]

Premises used: Subgroup.map_top_of_surjective, Finset.coe_image, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G

Tactic:
Finset.card_image_le.trans_eq hS1

Premises used: LE.le.trans_eq, Finset.card_image_le
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
S : Finset G
hS1 : S.card = rank G
hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G

Tactic:
exact Finset.card_image_le.trans_eq hS1

Premises used: LE.le.trans_eq, Finset.card_image_le
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
obtain :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ rank G
obtain₁ :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    rank H ≤ Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S)
obtain₂ obtain₃ :
  ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤),
    Finset.card.{u_2} (α := H) (Finset.image (⇑f : (a : G) → H) S) ≤ rank G
⊢ rank H ≤ rank G

Tactic:
classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply 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

Premises used: Subgroup.map_top_of_surjective, Group.rank_le, Finset.coe_image, Group.rank_spec, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
f : G →* H
⊢ rank.{u_2} ↥f.range ≤ rank G

Tactic:
rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective

Premises used: MonoidHom.rangeRestrict, Group.rank_le_of_surjective, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
e : G ≃* H
⊢ rank G = rank H

Tactic:
le_antisymm (rank_le_of_surjective e.symm e.symm.surjective)
    (rank_le_of_surjective e e.surjective)

Premises used: Group.rank_le_of_surjective, MonoidHomClass.toMonoidHom, MulEquiv.surjective, le_antisymm, MulEquiv.symm
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Group.FG.{u_1} ↥H
inst_2 : Group.FG.{u_1} ↥K
h : H = K
subst : ∀ [inst_3 : Group.FG.{u_1} ↥H], rank.{u_1} ↥H = rank.{u_1} ↥H
⊢ rank.{u_1} ↥H = rank.{u_1} ↥K

Tactic:
subst h
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 inst_2 : Group.FG.{u_1} ↥H
⊢ rank.{u_1} ↥H = rank.{u_1} ↥H

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
rw :
  Eq (α := Subgroup ↥(closure (↑s : Set G)))
    (closure
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x) ⁻¹' (↑s : Set G)))
    ⊤
⊢ Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤

Tactic:
rw [Finset.coe_preimage]

Premises used: Finset.coe_preimage
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
⊢ Eq (α := Subgroup ↥(closure (↑s : Set G)))
    (closure
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x) ⁻¹' (↑s : Set G)))
    ⊤

Tactic:
closure_preimage_eq_top (s : Set G)

Premises used: SetLike.coe, Subgroup.closure_preimage_eq_top
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
⊢ Eq (α := Subgroup ↥(closure (↑s : Set G)))
    (closure
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x) ⁻¹' (↑s : Set G)))
    ⊤

Tactic:
exact closure_preimage_eq_top (s : Set G)

Premises used: SetLike.coe, Subgroup.closure_preimage_eq_top
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
⊢ Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤

Tactic:
have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
apply : t.card ≤ s.card
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card

Tactic:
apply (rank_le ht).trans

Premises used: Group.rank_le, LE.le.trans
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
H :
  Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))
rw :
  {x ∈ s |
        Membership.mem (γ := Set G)
          (Set.range (ι := ↥(closure (↑s : Set G)))
            (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)))
          x}.card ≤
    s.card
⊢ t.card ≤ s.card

Tactic:
rw [← Finset.card_image_of_injOn H, Finset.image_preimage]

Premises used: Finset.image_preimage, Finset.card_image_of_injOn
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
H :
  Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))
⊢ {x ∈ s |
        Membership.mem (γ := Set G)
          (Set.range (ι := ↥(closure (↑s : Set G)))
            (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)))
          x}.card ≤
    s.card

Tactic:
apply Finset.card_filter_le

Premises used: Finset.card_filter_le
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
suffices :
  Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))
⊢ t.card ≤ s.card

Tactic:
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
t : Finset ↥(closure (↑s : Set G)) :=
  s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯
ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤
⊢ Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
    (↑t : Set ↥(closure (↑s : Set G)))

Tactic:
apply Subtype.coe_injective.injOn

Premises used: Function.Injective.injOn, Subtype.coe_injective
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Finset G
let let₁ let₂ : rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
let₃ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
    rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card
let₄ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤), t.card ≤ s.card
let₅ :
  let t : Finset ↥(closure (↑s : Set G)) :=
    s.preimage (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x)) ⋯;
  ∀ (ht : Eq (α := Subgroup ↥(closure (↑s : Set G))) (closure (↑t : Set ↥(closure (↑s : Set G)))) ⊤),
    Set.InjOn (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure (↑s : Set G)) x))
      (↑t : Set ↥(closure (↑s : Set G)))
⊢ rank.{u_1} ↥(closure (↑s : Set G)) ≤ s.card

Tactic:
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 (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn

Premises used: Function.Injective.injOn, Subtype.coe_injective
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
haveI : ∀ (this : Fintype (↑s : Type u_1)), rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)
⊢ rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)

Tactic:
haveI := Fintype.ofFinite s
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Fintype (↑s : Type u_1)
rw : rank.{u_1} ↥(closure (↑s.toFinset : Set G)) ≤ s.toFinset.card
⊢ rank.{u_1} ↥(closure s) ≤ Nat.card.{u_1} (↑s : Type u_1)

Tactic:
rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]

Premises used: Subgroup.rank_congr, Set.toFinset_card, congr_arg, Nat.card_eq_fintype_card, Set.coe_toFinset
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ rank.{u_1} ↥(closure (↑s.toFinset : Set G)) ≤ s.toFinset.card

Tactic:
rank_closure_finset_le_card s.toFinset

Premises used: Subgroup.rank_closure_finset_le_card, Set.toFinset
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
s : Set G
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ rank.{u_1} ↥(closure (↑s.toFinset : Set G)) ≤ s.toFinset.card

Tactic:
exact rank_closure_finset_le_card s.toFinset

Premises used: Subgroup.rank_closure_finset_le_card, Set.toFinset
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
g : G
rw :
  Nat.card.{u_1} ↥(comap (MulEquiv.toMonoidHom ConjAct.toConjAct) (MulAction.stabilizer (ConjAct G) g)) =
    Nat.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Nat.card.{u_1} ↥(centralizer {g}) = Nat.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [centralizer_eq_comap_stabilizer]

Premises used: Subgroup.centralizer_eq_comap_stabilizer
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Nat.card.{u_1} ↥(comap (MulEquiv.toMonoidHom ConjAct.toConjAct) (MulAction.stabilizer (ConjAct G) g)) =
    Nat.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b : D ≀ᵣ Q
⊢ a * b = { left := a.left * fun (x : Q) ↦ b.left (a.right⁻¹ * x), right := a.right * b.right }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b : D ≀ᵣ Q
⊢ (a * b).left = a.left * fun (x : Q) ↦ b.left (a.right⁻¹ * x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b : D ≀ᵣ Q
⊢ (a * b).right = a.right * b.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
⊢ Eq (α := Q → D) (left 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
⊢ Eq.{u_2 + 1} (α := Q) (right.{u_1, u_2} (D := D) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
⊢ a⁻¹.left = fun (x : Q) ↦ a.left⁻¹ (a.right * x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
⊢ a⁻¹.right = a.right⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b c : D ≀ᵣ Q
left : ∀ (x : Q), (a * b * c).left x = (a * (b * c)).left x
right : (a * b * c).right = (a * (b * c)).right
⊢ a * b * c = a * (b * c)

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b c : D ≀ᵣ Q
x : Q
⊢ (a * b * c).left x = (a * (b * c)).left x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a b c : D ≀ᵣ Q
⊢ (a * b * c).right = (a * (b * c)).right

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
left : ∀ (x : Q), (1 * a).left x = a.left x
right : (1 * a).right = a.right
⊢ 1 * a = a

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
x : Q
⊢ (1 * a).left x = a.left x

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
⊢ (1 * a).right = a.right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
left : ∀ (x : Q), (a * 1).left x = a.left x
right : (a * 1).right = a.right
⊢ a * 1 = a

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
x : Q
⊢ (a * 1).left x = a.left x

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
⊢ (a * 1).right = a.right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
left : ∀ (x : Q), (a⁻¹ * a).left x = RegularWreathProduct.left 1 x
right : (a⁻¹ * a).right = RegularWreathProduct.right.{u_1, u_2} (D := D) 1
⊢ a⁻¹ * a = 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
x : Q
⊢ (a⁻¹ * a).left x = left 1 x

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
a : D ≀ᵣ Q
⊢ (a⁻¹ * a).right = right.{u_1, u_2} (D := D) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
x x_1 : Q
left :
  ∀ (x_2 : Q),
    RegularWreathProduct.left { left := 1, right := x * x_1 } x_2 =
      (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).left x_2
right :
  RegularWreathProduct.right.{u_1, u_2} (D := D) { left := 1, right := x * x_1 : D ≀ᵣ Q } =
    (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).right
⊢ { left := 1, right := x * x_1 } =
    HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
x x_1 x_2 : Q
⊢ left { left := 1, right := x * x_1 } x_2 =
    (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).left x_2

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
x x_1 : Q
⊢ right.{u_1, u_2} (D := D) { left := 1, right := x * x_1 : D ≀ᵣ Q } =
    (HMul.hMul (α := D ≀ᵣ Q) { left := 1, right := x : D ≀ᵣ Q } { left := 1, right := x_1 : D ≀ᵣ Q }).right

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
q : Q
⊢ Eq (α := Q → D) (left ((inl : (a : Q) → D ≀ᵣ Q) q)) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
q : Q
⊢ right.{u_1, u_2} (D := D) ((inl : (a : Q) → D ≀ᵣ Q) q) = q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
⊢ Eq (α := (a : D ≀ᵣ Q) → Q) (⇑rightHom : (a : D ≀ᵣ Q) → Q) right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
h :
  ∀ (x : Q),
    Eq (α := Q) ((MonoidHom.comp (N := D ≀ᵣ Q) rightHom inl : (a : Q) → Q) x : Q) ((MonoidHom.id Q : (a : Q) → Q) x : Q)
⊢ Eq (α := Q →* Q) (MonoidHom.comp (N := D ≀ᵣ Q) rightHom inl) (MonoidHom.id Q)

Tactic:
ext
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
x : Q
⊢ Eq (α := Q) ((MonoidHom.comp (N := D ≀ᵣ Q) rightHom inl : (a : Q) → Q) x : Q) ((MonoidHom.id Q : (a : Q) → Q) x : Q)

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
q : Q
⊢ (rightHom : (a : D ≀ᵣ Q) → Q) ((inl : (a : Q) → D ≀ᵣ Q) q : D ≀ᵣ Q) = q

Tactic:
simp
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
inst_2 : Finite D
inst_3 : Finite Q
⊢ Finite (D ≀ᵣ Q)

Tactic:
Finite.of_equiv _ (equivProd D Q).symm

Premises used: Finite.of_equiv, RegularWreathProduct.equivProd, Equiv.symm
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Finite Q
rw : Nat.card ((Q → D) × Q) = Nat.card D ^ Nat.card Q * Nat.card Q
rw₁ : Nat.card (Q → D) * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
rw₂ rw₃ : Nat.card D ^ Nat.card Q * Nat.card Q = Nat.card D ^ Nat.card Q * Nat.card Q
⊢ Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q

Tactic:
rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]

Premises used: RegularWreathProduct.equivProd, Nat.card_fun, Nat.card_congr, Nat.card_prod
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst_2 : Group D₁
inst_3 : Group Q₁
inst_4 : Group D₂
inst_5 : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
left :
  ∀ (x_1 : Q₁),
    RegularWreathProduct.left
        ((fun (x : D₂ ≀ᵣ Q₂) ↦
            ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
                right := (g.symm : (a : Q₂) → Q₁) x.right } :
              D₁ ≀ᵣ Q₁))
          ((fun (x : D₁ ≀ᵣ Q₁) ↦
              ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                  right := (g : (a : Q₁) → Q₂) x.right } :
                D₂ ≀ᵣ Q₂))
            x))
        x_1 =
      x.left x_1
right :
  RegularWreathProduct.right.{u_3, u_4} (D := D₁)
      ((fun (x : D₂ ≀ᵣ Q₂) ↦
          ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
              right := (g.symm : (a : Q₂) → Q₁) x.right } :
            D₁ ≀ᵣ Q₁))
        ((fun (x : D₁ ≀ᵣ Q₁) ↦
            ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁),
                right := (g : (a : Q₁) → Q₂) x.right } :
              D₂ ≀ᵣ Q₂))
          x)) =
    x.right
⊢ (fun (x : D₂ ≀ᵣ Q₂) ↦
        ({ left := ((⇑f.symm : (a : D₂) → D₁) ∘ x.left) ∘ (⇑g : (a : Q₁) → Q₂),
            right := (g.symm : (a : Q₂) → Q₁) x.right } :
          D₁ ≀ᵣ Q₁))
      ((fun (x : D₁ ≀ᵣ Q₁) ↦
          ({ left := (⇑f : (a : D₁) → D₂) ∘ x.left ∘ (⇑g.symm : (a : Q₂) → Q₁), right := (g : (a : Q₁) → Q₂) x.right } :
            D₂ ≀ᵣ Q₂))
        x) =
    x

Tactic:
ext